//! Marker trait for [`#[check(ghost)]`][check#checkghost] functions
use crate::prelude::*;

mod private {
    /// Sealer for [`FnGhost`].
    pub trait _Sealed {}
}

/// Marker trait for functions that are [`#[check(ghost)]`][check#checkghost].
///
/// Right now, this is automatically implemented for `#[check(ghost)]` closures,
/// but not functions or methods.
#[intrinsic("fn_ghost")]
pub trait FnGhost: private::_Sealed {}

// In non-creusot mode, FnGhost does nothing
#[cfg(not(creusot))]
impl<F> private::_Sealed for F {}
#[cfg(not(creusot))]
impl<F> FnGhost for F {}

/// Structure that implements [`FnGhost`].
///
/// This cannot be built by itself: instead, it automatically wraps
/// `#[check(ghost)]` closures.
#[doc(hidden)]
#[intrinsic("fn_ghost_wrapper")]
pub struct FnGhostWrapper<F>(pub F);

impl<F: Clone> Clone for FnGhostWrapper<F> {
    #[ensures(F::clone.postcondition((&self.0,), result.0))]
    fn clone(&self) -> Self {
        Self(self.0.clone())
    }
}
impl<F: Copy> Copy for FnGhostWrapper<F> {}

#[cfg(creusot)]
impl<I: core::marker::Tuple, F: FnOnce<I>> FnOnce<I> for FnGhostWrapper<F> {
    type Output = F::Output;

    #[trusted]
    #[requires(self.precondition(args))]
    #[ensures(self.postcondition_once(args, result))]
    #[check(ghost_trusted)]
    extern "rust-call" fn call_once(self, args: I) -> Self::Output {
        self.0.call_once(args)
    }
}
#[cfg(creusot)]
impl<I: core::marker::Tuple, F: FnMut<I>> FnMut<I> for FnGhostWrapper<F> {
    #[trusted]
    #[requires((*self).precondition(args))]
    #[ensures((*self).postcondition_mut(args, ^self, result))]
    #[check(ghost_trusted)]
    extern "rust-call" fn call_mut(&mut self, args: I) -> Self::Output {
        self.0.call_mut(args)
    }
}
#[cfg(creusot)]
impl<I: core::marker::Tuple, F: Fn<I>> Fn<I> for FnGhostWrapper<F> {
    #[trusted]
    #[requires((*self).precondition(args))]
    #[ensures((*self).postcondition(args, result))]
    #[check(ghost_trusted)]
    extern "rust-call" fn call(&self, args: I) -> Self::Output {
        self.0.call(args)
    }
}

impl<F> FnGhostWrapper<F> {
    /// DO NOT CALL THIS FUNCTION! This is an implementation detail, used by the `#[check(ghost)]`
    /// attribute.
    #[doc(hidden)]
    #[check(ghost)]
    #[ensures(result.0 == f)]
    pub fn __new(f: F) -> Self {
        Self(f)
    }
}
#[cfg(creusot)]
impl<F> private::_Sealed for FnGhostWrapper<F> {}
#[cfg(creusot)]
impl<F> FnGhost for FnGhostWrapper<F> {}
