//! This module provides runtime utilities for the compiled
//! executable code of [`verus_builtin_macros::exec_spec_verified`]
//! and [`verus_builtin_macros::exec_spec_unverified`].
#![cfg(all(feature = "alloc", feature = "std"))]

use crate::multiset::*;
use crate::prelude::*;
use std::collections::HashMap;
use std::collections::HashSet;
pub use verus_builtin_macros::exec_spec_unverified;
pub use verus_builtin_macros::exec_spec_verified;

mod map;
pub use map::*;
mod multiset;
pub use multiset::*;
mod option;
pub use option::*;
mod seq;
pub use seq::*;
mod set;
pub use set::*;
mod string;
pub use string::*;

verus! {

/// [`ToRef`] and [`ToOwned`] are almost the same trait
/// but separated to avoid type inference ambiguities.
pub trait ToRef<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
    fn get_ref(self) -> (res: T)
        ensures
            res.deep_view() == self.deep_view(),
    ;
}

pub trait ToOwned<T: Sized + DeepView>: Sized + DeepView<V = T::V> {
    fn get_owned(self) -> (res: T)
        ensures
            res.deep_view() == self.deep_view(),
    ;
}

/// Cloned objects have the same deep view
pub trait DeepViewClone: Sized + DeepView {
    fn deep_clone(&self) -> (res: Self)
        ensures
            res.deep_view() == self.deep_view(),
    ;
}

/// Any spec types used in [`exec_spec_verified`] or [`exec_spec_unverified`] macros
/// must implement this trait to indicate
/// the corresponding exec type (owned and borrowed versions).
pub trait ExecSpecType where
    for <'a>&'a Self::ExecOwnedType: ToRef<Self::ExecRefType<'a>>,
    for <'a>Self::ExecRefType<'a>: ToOwned<Self::ExecOwnedType>,
 {
    /// Owned version of the exec type.
    type ExecOwnedType: DeepView<V = Self>;

    /// Reference version of the exec type.
    type ExecRefType<'a>: DeepView<V = Self>;
}

/// Types whose Rust equality (`==`) decides deep-view equality.
pub trait ObeysDeepEq: Sized + PartialEq + DeepView {
    proof fn lemma_obeys_deep_eq()
        ensures
            crate::laws_eq::obeys_deep_eq::<Self>(),
    ;
}

/// Executable deep-view equality, i.e., `==` on a type that [`ObeysDeepEq`].
#[inline(always)]
pub fn deep_eq<T: ObeysDeepEq>(x: T, y: T) -> (res: bool)
    ensures
        res == (x.deep_view() =~~= y.deep_view()),
{
    proof {
        T::lemma_obeys_deep_eq();
        reveal(crate::laws_eq::obeys_deep_eq);
    }
    x.eq(&y)
}

impl<'a, T: ObeysDeepEq> ObeysDeepEq for &'a T {
    proof fn lemma_obeys_deep_eq() {
        broadcast use crate::laws_eq::lemma_ref_obeys_deep_eq;

        T::lemma_obeys_deep_eq();
    }
}

/// Spec for executable version of [`Seq`] and [`str`] indexing.
pub trait ExecSpecIndex<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
    type Elem: DeepView;

    fn exec_index(self, index: usize) -> Self::Elem
        requires
            0 <= index < self.deep_view().len(),
    ;
}

/// Spec for executable version of `len`.
pub trait ExecSpecLen {
    fn exec_len(self) -> usize;
}

/// A macro to implement various traits for primitive arithmetic types.
macro_rules! impl_primitives {
    ($(,)?) => {};
    ($t:ty $(,$rest:ty)* $(,)?) => {
        verus! {
            impl ExecSpecType for $t {
                type ExecOwnedType = $t;
                type ExecRefType<'a> = $t;
            }

            impl<'a> ToRef<$t> for &'a $t {
                #[inline(always)]
                fn get_ref(self) -> $t {
                    *self
                }
            }

            impl ToOwned<$t> for $t {
                #[inline(always)]
                fn get_owned(self) -> $t {
                    self
                }
            }

            impl DeepViewClone for $t {
                #[inline(always)]
                fn deep_clone(&self) -> Self {
                    *self
                }
            }

            impl ObeysDeepEq for $t {
                proof fn lemma_obeys_deep_eq() {
                    reveal(crate::laws_eq::obeys_deep_eq);
                }
            }
        }

        impl_primitives!($($rest),*);
    };
}

impl_primitives! {
    u8, u16, u32, u64, u128, usize,
    i8, i16, i32, i64, i128, isize,
    bool, char,
}
// impl on tuples up to size 4, to match the impls of View in vstd


macro_rules! impl_exec_spec_tuple {
    ([$(
        ($T:ident, $n:tt)
    ),*])=> {
        verus! {

            impl<'a, $($T: Sized + DeepView),*> ToRef<&'a ($($T,)*)> for &'a ($($T,)*) {
                #[inline(always)]
                fn get_ref(self) -> &'a ($($T,)*) {
                    self
                }
            }

            impl<'a, $($T: DeepView + DeepViewClone),*> ToOwned<($($T,)*)> for &'a ($($T,)*) {
                #[inline(always)]
                fn get_owned(self) -> ($($T,)*) {
                    self.deep_clone()
                }
            }

            impl<$($T: DeepViewClone),*> DeepViewClone for ($($T,)*) {
                #[inline(always)]
                #[allow(non_snake_case)]
                fn deep_clone(&self) -> Self {
                    ($(self.$n.deep_clone(),)*)
                }
            }

            impl<$($T: ObeysDeepEq),*> ObeysDeepEq for ($($T,)*) {
                proof fn lemma_obeys_deep_eq() {
                    broadcast use crate::laws_eq::group_laws_eq;
                    $( $T::lemma_obeys_deep_eq(); )*
                }
            }

        }
    };
}

impl_exec_spec_tuple!([(T0, 0)]);

impl_exec_spec_tuple!([(T0, 0), (T1, 1)]);

impl_exec_spec_tuple!([(T0, 0), (T1, 1), (T2, 2)]);

impl_exec_spec_tuple!([(T0, 0), (T1, 1), (T2, 2), (T3, 3)]);

} // verus!