use crate::{
    ghost::Plain,
    invariant::{InhabitedInvariant, Subset},
    logic::ops::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic},
    ord_laws_impl,
    prelude::*,
};
use core::{
    cmp,
    ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Neg, Rem, RemAssign, Sub, SubAssign},
};

/// An unbounded, mathematical integer.
///
/// This type cannot be only be constructed in logical or ghost code.
///
/// # Integers in pearlite
///
/// Note that in pearlite, all integer literals are of type `Int`:
/// ```
/// # use creusot_std::prelude::*;
/// let x = 1i32;
/// //             ↓ need to use the view operator to convert `i32` to `Int`
/// proof_assert!(x@ == 1);
/// ```
///
/// You can use the usual operators on integers: `+`, `-`, `*`, `/` and `%`.
///
/// Note that those operators are _not_ available in ghost code.
#[intrinsic("int")]
#[builtin("int")]
pub struct Int;

impl Clone for Int {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}
impl Copy for Int {}
impl Plain for Int {
    #[trusted]
    #[ensures(*result == *snap)]
    #[check(ghost)]
    #[allow(unused_variables)]
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
        Ghost::conjure()
    }
}

// Logical functions
impl Int {
    /// Compute `self^p`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(3.pow(4) == 729);
    /// ```
    #[logic]
    #[builtin("int.Power.power")]
    #[allow(unused_variables)]
    pub fn pow(self, p: Int) -> Int {
        dead
    }

    /// Compute `2^p`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(pow2(4) == 16);
    /// ```
    #[logic]
    #[builtin("bv.Pow2int.pow2")]
    #[allow(unused_variables)]
    pub fn pow2(self) -> Int {
        dead
    }

    /// Compute the maximum of `self` and `x`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(10.max(2) == 10);
    /// ```
    #[logic]
    #[builtin("int.MinMax.max")]
    #[allow(unused_variables)]
    pub fn max(self, x: Int) -> Int {
        dead
    }

    /// Compute the minimum of `self` and `x`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(10.max(2) == 2);
    /// ```
    #[logic]
    #[builtin("int.MinMax.min")]
    #[allow(unused_variables)]
    pub fn min(self, x: Int) -> Int {
        dead
    }

    /// Compute the euclidean division of `self` by `d`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(10.div_euclid(3) == 3);
    /// ```
    #[logic]
    #[builtin("int.EuclideanDivision.div")]
    #[allow(unused_variables)]
    pub fn div_euclid(self, d: Int) -> Int {
        dead
    }

    /// Compute the remainder of the euclidean division of `self` by `d`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    ///  proof_assert!(10.rem_euclid(3) == 1);
    /// ```
    #[logic]
    #[builtin("int.EuclideanDivision.mod")]
    #[allow(unused_variables)]
    pub fn rem_euclid(self, d: Int) -> Int {
        dead
    }

    /// Compute the absolute difference of `self` and `x`.
    ///
    /// # Example
    ///
    /// ```
    /// # use creusot_std::prelude::*;
    /// proof_assert!(10.abs_diff(3) == 7);
    /// proof_assert!(3.abs_diff(10) == 7);
    /// proof_assert!((-5).abs_diff(5) == 10);
    /// ```
    #[logic(open)]
    pub fn abs_diff(self, other: Int) -> Int {
        if self < other { other - self } else { self - other }
    }
}

impl AddLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.Int.(+)")]
    #[allow(unused_variables)]
    fn add_logic(self, other: Self) -> Self {
        dead
    }
}

impl SubLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.Int.(-)")]
    #[allow(unused_variables)]
    fn sub_logic(self, other: Self) -> Self {
        dead
    }
}

impl MulLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.Int.(*)")]
    #[allow(unused_variables)]
    fn mul_logic(self, other: Self) -> Self {
        dead
    }
}

impl DivLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.ComputerDivision.div")]
    #[allow(unused_variables)]
    fn div_logic(self, other: Self) -> Self {
        dead
    }
}

impl RemLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.ComputerDivision.mod")]
    #[allow(unused_variables)]
    fn rem_logic(self, other: Self) -> Self {
        dead
    }
}

impl NegLogic for Int {
    type Output = Self;
    #[logic]
    #[builtin("int.Int.(-_)")]
    fn neg_logic(self) -> Self {
        dead
    }
}

// ========== Ghost operations =============

// Ghost functions
impl Int {
    /// Create a new `Int` value
    ///
    /// The result is wrapped in a [`Ghost`], so that it can only be access inside a
    /// [`ghost!`] block.
    ///
    /// You should not have to use this method directly: instead, use the `int` suffix
    /// inside of a `ghost` block:
    /// ```
    /// # use creusot_std::prelude::*;
    /// let x: Ghost<Int> = ghost!(1int);
    /// ghost! {
    ///     let y: Int = 2int;
    /// };
    /// ```
    #[trusted]
    #[check(ghost)]
    #[ensures(*result == value@)]
    #[allow(unreachable_code)]
    #[allow(unused_variables)]
    pub fn new(value: i128) -> Ghost<Self> {
        Ghost::conjure()
    }

    #[trusted]
    #[check(ghost)]
    #[ensures(^self == *self + 1)]
    pub fn incr_ghost(&mut self) {}

    #[trusted]
    #[check(ghost)]
    #[ensures(^self == *self - 1)]
    pub fn decr_ghost(&mut self) {}
}

impl PartialEq for Int {
    #[trusted]
    #[check(ghost)]
    #[ensures(result == (*self == *other))]
    #[allow(unused_variables)]
    fn eq(&self, other: &Self) -> bool {
        panic!()
    }

    #[check(ghost)]
    #[ensures(result == (*self != *other))]
    fn ne(&self, other: &Self) -> bool {
        !self.eq(other)
    }
}

impl PartialOrd for Int {
    #[trusted]
    #[check(ghost)]
    #[ensures(result == Some((*self).cmp_log(*other)))]
    #[allow(unused_variables)]
    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
        panic!()
    }

    #[trusted]
    #[check(ghost)]
    #[ensures(result == (*self).lt_log(*other))]
    #[allow(unused_variables)]
    fn lt(&self, other: &Self) -> bool {
        panic!()
    }

    #[trusted]
    #[check(ghost)]
    #[ensures(result == (*self).le_log(*other))]
    #[allow(unused_variables)]
    fn le(&self, other: &Self) -> bool {
        panic!()
    }

    #[trusted]
    #[check(ghost)]
    #[ensures(result == (*self).gt_log(*other))]
    #[allow(unused_variables)]
    fn gt(&self, other: &Self) -> bool {
        panic!()
    }

    #[trusted]
    #[check(ghost)]
    #[ensures(result == (*self).ge_log(*other))]
    #[allow(unused_variables)]
    fn ge(&self, other: &Self) -> bool {
        panic!()
    }
}

impl Add for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[ensures(result == self + other)]
    #[allow(unused_variables)]
    fn add(self, other: Int) -> Self {
        panic!()
    }
}

impl Sub for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[ensures(result == self - other)]
    #[allow(unused_variables)]
    fn sub(self, other: Int) -> Self {
        panic!()
    }
}

impl Mul for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[ensures(result == self * other)]
    #[allow(unused_variables)]
    fn mul(self, other: Int) -> Self {
        panic!()
    }
}

impl Div for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[requires(other != 0)]
    #[ensures(result == self / other)]
    #[allow(unused_variables)]
    fn div(self, other: Int) -> Self {
        panic!()
    }
}

impl Rem for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[requires(other != 0)]
    #[ensures(result == self % other)]
    #[allow(unused_variables)]
    fn rem(self, other: Int) -> Self {
        panic!()
    }
}

impl Neg for Int {
    type Output = Int;
    #[trusted]
    #[check(ghost)]
    #[ensures(result == -self)]
    fn neg(self) -> Self {
        panic!()
    }
}

impl AddAssign for Int {
    #[check(ghost)]
    #[ensures(^self == *self + rhs)]
    fn add_assign(&mut self, rhs: Int) {
        *self = *self + rhs;
    }
}

impl SubAssign for Int {
    #[check(ghost)]
    #[ensures(^self == *self - rhs)]
    fn sub_assign(&mut self, rhs: Int) {
        *self = *self - rhs;
    }
}

impl MulAssign for Int {
    #[check(ghost)]
    #[ensures(^self == *self * rhs)]
    fn mul_assign(&mut self, rhs: Int) {
        *self = *self * rhs;
    }
}

impl DivAssign for Int {
    #[check(ghost)]
    #[requires(rhs != 0)]
    #[ensures(^self == *self / rhs)]
    fn div_assign(&mut self, rhs: Int) {
        *self = *self / rhs;
    }
}

impl RemAssign for Int {
    #[check(ghost)]
    #[requires(rhs != 0)]
    #[ensures(^self == *self % rhs)]
    fn rem_assign(&mut self, rhs: Int) {
        *self = *self % rhs;
    }
}

#[derive(Copy)]
struct NatInner(Int);

impl Invariant for NatInner {
    #[logic]
    fn invariant(self) -> bool {
        self.0 >= 0
    }
}

impl InhabitedInvariant for NatInner {
    #[logic]
    #[ensures(result.invariant())]
    fn inhabits() -> Self {
        Self(0)
    }
}

impl Clone for NatInner {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}

/// Natural numbers, i.e., integers that are greater or equal to 0.
#[derive(Copy)]
pub struct Nat(Subset<NatInner>);

impl View for Nat {
    type ViewTy = Int;
    #[logic(open)]
    fn view(self) -> Int {
        self.to_int()
    }
}

impl Clone for Nat {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}
impl Plain for Nat {
    #[check(ghost)]
    #[ensures(*result == *s)]
    #[allow(unused_variables)]
    fn into_ghost(s: Snapshot<Self>) -> Ghost<Self> {
        ghost! {
            let n: Snapshot<Int> = snapshot!(s.to_int());
            let _ = snapshot!(Self::ext_eq);
            Self(Subset::new(NatInner(n.into_ghost().into_inner())))
        }
    }
}

impl Nat {
    #[logic]
    #[ensures(result >= 0)]
    pub fn to_int(self) -> Int {
        self.0.inner().0
    }

    #[logic]
    #[requires(n >= 0)]
    #[ensures(result.to_int() == n)]
    pub fn new(n: Int) -> Nat {
        Nat(Subset::new_logic(NatInner(n)))
    }

    #[logic(open)]
    #[ensures(result == (self == other))]
    pub fn ext_eq(self, other: Self) -> bool {
        let _ = Subset::<NatInner>::inner_inj;
        self.to_int() == other.to_int()
    }
}

impl AddLogic for Nat {
    type Output = Self;
    #[logic]
    #[ensures(result@ == self@ + other@)]
    fn add_logic(self, other: Self) -> Self {
        Self::new(self.to_int() + other.to_int())
    }
}

impl MulLogic for Nat {
    type Output = Self;
    #[logic]
    #[ensures(result@ == self@ * other@)]
    fn mul_logic(self, other: Self) -> Self {
        Self::new(self.to_int() * other.to_int())
    }
}

impl OrdLogic for Nat {
    #[logic(open)]
    fn cmp_log(self, other: Self) -> cmp::Ordering {
        self.to_int().cmp_log(other.to_int())
    }

    ord_laws_impl! { let _ = Nat::ext_eq; }
}

/// Positive numbers, i.e. numbers that are strictly greater than 0.
#[derive(Copy)]
pub struct Positive(Subset<PositiveInner>);

#[derive(Copy)]
struct PositiveInner(Int);

impl Invariant for PositiveInner {
    #[logic]
    fn invariant(self) -> bool {
        self.0 > 0int
    }
}
impl InhabitedInvariant for PositiveInner {
    #[logic]
    #[ensures(result.invariant())]
    fn inhabits() -> Self {
        Self(1int)
    }
}

impl Clone for PositiveInner {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}

impl View for Positive {
    type ViewTy = Int;
    #[logic(open)]
    fn view(self) -> Int {
        self.to_int()
    }
}

impl Clone for Positive {
    #[check(ghost)]
    #[ensures(result == *self)]
    fn clone(&self) -> Self {
        *self
    }
}

impl Plain for Positive {
    #[check(ghost)]
    #[ensures(*result == *s)]
    #[allow(unused_variables)]
    fn into_ghost(s: Snapshot<Self>) -> Ghost<Self> {
        ghost! {
            let n: Snapshot<Int> = snapshot!(s.to_int());
            let _ = snapshot!(Self::ext_eq);
            Self(Subset::new(PositiveInner(n.into_ghost().into_inner())))
        }
    }
}

impl Positive {
    #[logic]
    #[ensures(result > 0)]
    pub fn to_int(self) -> Int {
        self.0.inner().0
    }

    #[logic]
    #[requires(n > 0)]
    #[ensures(result.to_int() == n)]
    pub fn new(n: Int) -> Self {
        Self(Subset::new_logic(PositiveInner(n)))
    }

    #[logic(open)]
    #[ensures(result == (self == other))]
    pub fn ext_eq(self, other: Self) -> bool {
        let _ = Subset::<PositiveInner>::inner_inj;
        self.to_int() == other.to_int()
    }
}

impl AddLogic for Positive {
    type Output = Self;

    #[logic]
    #[ensures(result@ == self@ + other@)]
    fn add_logic(self, other: Self) -> Self {
        Self::new(self.to_int() + other.to_int())
    }
}

impl MulLogic for Positive {
    type Output = Self;

    #[logic]
    #[ensures(result@ == self@ * other@)]
    fn mul_logic(self, other: Self) -> Self {
        Self::new(self.to_int() * other.to_int())
    }
}

impl OrdLogic for Positive {
    #[logic(open)]
    fn cmp_log(self, other: Self) -> cmp::Ordering {
        self.to_int().cmp_log(other.to_int())
    }

    ord_laws_impl! { let _ = Positive::ext_eq; }
}
