use super::super::prelude::*;
use core::marker::PointeeSized;

use verus as verus_skip_verusfmt;
verus_skip_verusfmt! {

#[verifier::external_trait_specification]
pub trait ExTuple {
    type ExternalTraitSpecificationFor: core::marker::Tuple;
}

#[verifier::external_trait_specification]
pub trait ExFnOnce<Args: core::marker::Tuple> {
    type ExternalTraitSpecificationFor: core::ops::FnOnce<Args>;

    type Output;
}

#[verifier::external_trait_specification]
pub trait ExFnMut<Args: core::marker::Tuple>: FnOnce<Args> {
    type ExternalTraitSpecificationFor: core::ops::FnMut<Args>;
}

#[verifier::external_trait_specification]
pub trait ExFn<Args: core::marker::Tuple>: FnMut<Args> {
    type ExternalTraitSpecificationFor: core::ops::Fn<Args>;
}

#[verifier::external_trait_specification]
pub trait ExDeref: PointeeSized {
    type ExternalTraitSpecificationFor: core::ops::Deref;

    type Target: ?Sized;

    fn deref(&self) -> &Self::Target;
}

#[verifier::external_trait_specification]
pub trait ExDerefMut: core::ops::Deref + PointeeSized {
    type ExternalTraitSpecificationFor: core::ops::DerefMut;

    fn deref_mut(&mut self) -> &mut Self::Target;
}

#[verifier::external_trait_specification]
#[verifier::external_trait_extension(IndexSpec via IndexSpecImpl)]
pub trait ExIndex<Idx> where Idx: ?Sized {
    type ExternalTraitSpecificationFor: core::ops::Index<Idx>;

    type Output: ?Sized;

    // NOTE: this used as a precondition for both `Index` and `IndexMut`,
    // since both share the same `s[i]` syntax.
    spec fn index_req(&self, index: &Idx) -> bool;

    fn index(&self, index: Idx) -> (output: &Self::Output) where Idx: Sized
        requires
            self.index_req(&index),
    ;
}

#[verifier::external_trait_specification]
pub trait ExIndexMut<Idx>: core::ops::Index<Idx> where Idx: ?Sized {
    type ExternalTraitSpecificationFor: core::ops::IndexMut<Idx>;

    fn index_mut(&mut self, index: Idx) -> (output: &mut Self::Output) where Idx: Sized
        requires
            self.index_req(&index),
    ;
}

#[verifier::external_trait_specification]
pub trait ExInteger: Copy {
    type ExternalTraitSpecificationFor: Integer;
}

#[verifier::external_trait_specification]
pub trait ExSpecOrd<Rhs> {
    type ExternalTraitSpecificationFor: SpecOrd<Rhs>;
}

#[cfg(not(verus_verify_core))]
#[verifier::external_trait_specification]
pub trait ExAllocator {
    type ExternalTraitSpecificationFor: core::alloc::Allocator;
}

#[verifier::external_trait_specification]
pub trait ExFreeze: PointeeSized {
    type ExternalTraitSpecificationFor: core::marker::Freeze;
}

#[verifier::external_trait_specification]
pub trait ExHash: PointeeSized {
    type ExternalTraitSpecificationFor: core::hash::Hash;
}

#[verifier::external_trait_specification]
pub trait ExPtrPointee: PointeeSized {
    type ExternalTraitSpecificationFor: core::ptr::Pointee;

    type Metadata:
        Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze;
}

#[verifier::external_trait_specification]
pub trait ExBorrow<Borrowed> where Borrowed: ?Sized {
    type ExternalTraitSpecificationFor: core::borrow::Borrow<Borrowed>;
}

#[verifier::external_trait_specification]
pub trait ExStructural {
    type ExternalTraitSpecificationFor: Structural;
}

// Since this trait involves the unstable library feature `const_destruct`,
// we only enable it when verifying core
#[cfg(verus_verify_core)]
#[verifier::external_trait_specification]
trait ExDestruct: PointeeSized {
    type ExternalTraitSpecificationFor: core::marker::Destruct;
}

#[verifier::external_trait_specification]
pub trait ExMetaSized {
    type ExternalTraitSpecificationFor: core::marker::MetaSized;
}

pub assume_specification<T>[ core::mem::swap::<T> ](a: &mut T, b: &mut T)
    ensures
        *final(a) == *old(b),
        *final(b) == *old(a),
    opens_invariants none
    no_unwind
;

#[verifier::external_type_specification]
pub struct ExOrdering(core::cmp::Ordering);

#[verifier::external_type_specification]
#[verifier::accept_recursive_types(V)]
#[verifier::ext_equal]
pub struct ExOption<V>(core::option::Option<V>);

#[verifier::external_type_specification]
#[verifier::accept_recursive_types(T)]
#[verifier::reject_recursive_types_in_ground_variants(E)]
pub struct ExResult<T, E>(core::result::Result<T, E>);

// I don't really expect this to be particularly useful;
// this is mostly here because I wanted an easy way to test
// the combination of external_type_specification & external_body
// in a cross-crate context.
#[verifier::external_type_specification]
#[verifier::external_body]
pub struct ExDuration(core::time::Duration);

#[verifier::external_type_specification]
#[verifier::accept_recursive_types(V)]
pub struct ExPhantomData<V: PointeeSized>(core::marker::PhantomData<V>);

pub assume_specification[ core::intrinsics::likely ](b: bool) -> (c: bool)
    ensures
        c == b,
;

pub assume_specification[ core::intrinsics::unlikely ](b: bool) -> (c: bool)
    ensures
        c == b,
;

pub assume_specification<T, F: FnOnce() -> T>[ bool::then ](b: bool, f: F) -> (ret: Option<T>)
    requires
        b ==> f.requires(()),
    ensures
        if b {
            ret.is_some() && f.ensures((), ret.unwrap())
        } else {
            ret.is_none()
        },
;

pub assume_specification<T> [core::hint::must_use] (value: T) -> (ret: T)
    ensures
        ret == value,
;

pub assume_specification [core::panicking::panic] (s: &'static str) -> !
    requires
        false,
;

pub assume_specification [core::panicking::panic_fmt] (s: core::fmt::Arguments<'_>) -> !
    requires
        false,
;

// Called by `assert_eq!` and `assert_ne!`; not external_body, since the macros construct an `AssertKind`
#[verifier::external_type_specification]
pub struct ExAssertKind(core::panicking::AssertKind);

pub assume_specification<T, U>[ core::panicking::assert_failed::<T, U> ](
    kind: core::panicking::AssertKind,
    left: &T,
    right: &U,
    args: Option<core::fmt::Arguments<'_>>,
) -> !
    where
        T: core::fmt::Debug + ?Sized,
        U: core::fmt::Debug + ?Sized,
    requires
        false,
;

} // verus!

#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::accept_recursive_types(T)]
pub struct ExAssertParamIsClone<T: Clone + PointeeSized>(core::clone::AssertParamIsClone<T>);