#[cfg(creusot)]
use crate::ghost::Objective;

use crate::{
    ghost::{
        Container, FnGhost,
        perm::{Perm, SendPerm, SyncPerm},
    },
    logic::FMap,
    prelude::*,
    std::sync::{
        committer::Committer,
        view::{HasTimestamp, SyncView, Timestamp},
    },
};

/// Creusot wrapper around [`std::sync::atomic::Ordering`].
#[allow(non_snake_case)]
pub mod Ordering {
    use std::sync::atomic;

    pub trait Ordering {
        const ORDERING: atomic::Ordering;
    }

    pub struct None;

    macro_rules! impl_orders {
        ($( $order:ident ),+) => { $(

            pub struct $order;

            impl Ordering for $order {
                const ORDERING: atomic::Ordering = atomic::Ordering::$order;
            }

        )* };
    }

    impl_orders!(Relaxed, Release, Acquire, SeqCst);
}

use Ordering::Ordering as _;

macro_rules! impl_atomic {
    ($( ($type:ty, $atomic_type:ident $(< $T:ident >)?) ),+) => { $(

        #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
        pub struct $atomic_type $(< $T >)?(::std::sync::atomic::$atomic_type $(< $T >)?);

        impl $(< $T >)? SendPerm for $atomic_type $(< $T >)? {}
        impl $(< $T >)? SyncPerm for $atomic_type $(< $T >)? {}

        #[cfg(creusot)]
        #[trusted]
        impl $(< $T >)? Objective for Perm<$atomic_type $(< $T >)?> {}

        impl $(< $T >)? Container for $atomic_type $(< $T >)? {
            type Value = FMap<Timestamp, ($type, SyncView)>;
        }

        impl $(< $T >)? HasTimestamp for $atomic_type $(< $T >)? {
            #[logic(opaque)]
            fn get_timestamp(self, _: SyncView) -> Timestamp {
                dead
            }

            #[logic(law)]
            #[requires(x <= y)]
            #[ensures(self.get_timestamp(x) <= self.get_timestamp(y))]
            #[trusted]
            fn get_timestamp_monotonic(self, x: SyncView, y: SyncView) {}
        }

        impl $(< $T >)? $atomic_type $(< $T >)? {
            #[ensures(*result.1.val() == FMap::singleton(result.0.get_timestamp(^sync_view), (val, **sync_view)))]
            #[ensures(*result.1.ward() == result.0)]
            #[trusted]
            #[check(terminates)]
            #[allow(unused_variables)]
            pub fn new(val: $type, sync_view: Ghost<&mut SyncView>) -> (Self, Ghost<Box<Perm<$atomic_type $(< $T >)?>>>) {
                (Self(std::sync::atomic::$atomic_type::new(val)), Ghost::conjure())
            }

            // TODO: [VL] into_inner

            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::load`].")]
            #[requires(Load::ORDERING == Ordering::Acquire::ORDERING || Load::ORDERING == Ordering::Relaxed::ORDERING)]
            #[requires(forall<c: &Committer<Self, $type, Load, Ordering::None>>
                !c.shot_store() ==> c.ward() == *self ==> f.precondition((c,))
            )]
            #[ensures(exists<c: &Committer<Self, $type, Load, Ordering::None>>
                !c.shot_store() && c.ward() == *self && c.val_load() == result && f.postcondition_once((c,), ())
            )]
            #[trusted]
            #[allow(unused_variables)]
            pub fn load<F, Load: Ordering::Ordering>(&self, f: Ghost<F>) -> $type
            where
                F: FnGhost + FnOnce(&Committer<Self, $type, Load, Ordering::None>),
            {
                self.0.load(if cfg!(feature = "sc-drf") {
                    Ordering::SeqCst::ORDERING
                } else {
                    Load::ORDERING
                })
            }

            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::store`].")]
            #[requires(Store::ORDERING == Ordering::Release::ORDERING || Store::ORDERING == Ordering::Relaxed::ORDERING)]
            #[requires(forall<c: &mut Committer<Self, $type, Ordering::None, Store>>
                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val ==>
                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
            )]
            #[ensures(exists<c: &mut Committer<Self, $type, Ordering::None, Store>>
                !c.shot_store() && c.ward() == *self && c.val_store() == val &&
                f.postcondition_once((c,), ())
            )]
            #[trusted]
            #[allow(unused_variables)]
            pub fn store<F, Store: Ordering::Ordering>(&self, val: $type, f: Ghost<F>)
            where
                F: FnGhost + FnOnce(&mut Committer<Self, $type, Ordering::None, Store>),
            {
                self.0.store(
                    val,
                    if cfg!(feature = "sc-drf") {
                        Ordering::SeqCst::ORDERING
                    } else {
                        Store::ORDERING
                    },
                )
            }
        }

    )* };
}

macro_rules! impl_atomic_int {
    ($( ($int_type:ty, $atomic_type:ident) ),+) => { $(

        impl_atomic!(($int_type, $atomic_type));

        // Nothing yet.

    )* };
}

impl_atomic! {
    (bool, AtomicBool),
    (*mut T, AtomicPtr<T>)
}

impl_atomic_int! {
    (i8, AtomicI8),
    (u8, AtomicU8),
    (i16, AtomicI16),
    (u16, AtomicU16),
    (i32, AtomicI32),
    (u32, AtomicU32),
    (i64, AtomicI64),
    (u64, AtomicU64),
    (isize, AtomicIsize),
    (usize, AtomicUsize)
}
