use crate::{
    ghost::Plain,
    logic::ops::{AddLogic, MulLogic, NegLogic, NthBitLogic, SubLogic},
    prelude::*,
};
// Resolve links like [`i8::add`] in the generated documentation
#[cfg(doc)]
use core::ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Rem, RemAssign, Sub, SubAssign};

macro_rules! mach_int {
    ($t:ty, $ty_nm:expr, $zero:expr, $to_int:literal) => {
        impl View for $t {
            type ViewTy = Int;
            #[logic]
            #[builtin(concat!($ty_nm, $to_int))]
            fn view(self) -> Self::ViewTy {
                dead
            }
        }

        impl DeepModel for $t {
            type DeepModelTy = Int;
            #[logic(open, inline)]
            fn deep_model(self) -> Self::DeepModelTy {
                pearlite! { self@ }
            }
        }

        impl Plain for $t {
            #[trusted]
            #[ensures(*result == *snap)]
            #[check(ghost)]
            #[allow(unused_variables)]
            fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self> {
                Ghost::conjure()
            }
        }

        extern_spec! {
            impl Default for $t {
                #[check(ghost)]
                #[ensures(result == $zero)]
                fn default() -> $t { 0 }
            }

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

        impl AddLogic for $t {
            type Output = Self;
            #[logic]
            #[builtin(concat!($ty_nm, ".add"))]
            #[allow(unused_variables)]
            fn add_logic(self, other: Self) -> Self {
                dead
            }
        }

        impl SubLogic for $t {
            type Output = Self;
            #[logic]
            #[builtin(concat!($ty_nm, ".sub"))]
            #[allow(unused_variables)]
            fn sub_logic(self, other: Self) -> Self {
                dead
            }
        }

        impl MulLogic for $t {
            type Output = Self;
            #[logic]
            #[builtin(concat!($ty_nm, ".mul"))]
            #[allow(unused_variables)]
            fn mul_logic(self, other: Self) -> Self {
                dead
            }
        }

        impl NegLogic for $t {
            type Output = Self;
            #[logic]
            #[builtin(concat!($ty_nm, ".neg"))]
            fn neg_logic(self) -> Self {
                dead
            }
        }

        impl NthBitLogic for $t {
            #[logic]
            #[builtin(concat!($ty_nm, ".nth"))]
            #[allow(unused_variables)]
            fn nth_bit(self, n: Int) -> bool {
                dead
            }
        }
    };
}

mach_int!(u8, "creusot.int.UInt8$BW$", 0u8, ".t'int");
mach_int!(u16, "creusot.int.UInt16$BW$", 0u16, ".t'int");
mach_int!(u32, "creusot.int.UInt32$BW$", 0u32, ".t'int");
mach_int!(u64, "creusot.int.UInt64$BW$", 0u64, ".t'int");
mach_int!(u128, "creusot.int.UInt128$BW$", 0u128, ".t'int");
#[cfg(target_pointer_width = "64")]
mach_int!(usize, "creusot.int.UInt64$BW$", 0usize, ".t'int");
#[cfg(target_pointer_width = "32")]
mach_int!(usize, "creusot.int.UInt32$BW$", 0usize, ".t'int");
#[cfg(target_pointer_width = "16")]
mach_int!(usize, "creusot.int.UInt16$BW$", 0usize, ".t'int");

mach_int!(i8, "creusot.int.Int8$BW$", 0i8, ".to_int");
mach_int!(i16, "creusot.int.Int16$BW$", 0i16, ".to_int");
mach_int!(i32, "creusot.int.Int32$BW$", 0i32, ".to_int");
mach_int!(i64, "creusot.int.Int64$BW$", 0i64, ".to_int");
mach_int!(i128, "creusot.int.Int128$BW$", 0i128, ".to_int");
#[cfg(target_pointer_width = "64")]
mach_int!(isize, "creusot.int.Int64$BW$", 0isize, ".to_int");
#[cfg(target_pointer_width = "32")]
mach_int!(isize, "creusot.int.Int32$BW$", 0isize, ".to_int");
#[cfg(target_pointer_width = "16")]
mach_int!(isize, "creusot.int.Int16$BW$", 0isize, ".to_int");

/// Adds specifications for checked, wrapping, saturating, and overflowing operations on the given
/// integer type
macro_rules! spec_type {
    ($type:ty) => {
        // Specify addition, subtraction and multiplication
        spec_op_common!{$type, +, checked_add, wrapping_add, saturating_add, overflowing_add, unchecked_add}
        spec_op_common!{$type, -, checked_sub, wrapping_sub, saturating_sub, overflowing_sub, unchecked_sub}
        spec_op_common!{$type, *, checked_mul, wrapping_mul, saturating_mul, overflowing_mul, unchecked_mul}
        spec_impl_common!{$type}
        spec_div_rem!{$type}

        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result == -self)]
                fn wrapping_neg(self) -> $type;
            }
        }

        // Specify division separately, because it has the additional precondition that the divisor
        // is non-zero. Overflow on division can only occur on signed types and only when computing
        // `$type::MIN / -1`.
        extern_spec! {
            impl $type {
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns `None` iff the divisor is zero or the division overflows
                #[ensures((result == None) == (rhs@ == 0 || (self@ == $type::MIN@ && rhs@ == -1)))]
                // Else, returns the result of the division
                #[ensures(forall<r: $type> result == Some(r) ==> r@ == self@ / rhs@)]
                fn checked_div(self, rhs: $type) -> Option<$type>;

                #[allow(dead_code)]
                #[check(ghost)]
                // Panics if the divisor is zero
                #[requires(rhs@ != 0)]
                // Returns `self` if the division overflows
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == self@)]
                // Else, returns the result of the division
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
                fn wrapping_div(self, rhs: $type) -> $type;

                #[allow(dead_code)]
                #[check(ghost)]
                // Panics if the divisor is zero
                #[requires(rhs@ != 0)]
                // Returns `$type::MIN` if the division overflows
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result@ == $type::MIN@)]
                // Else, returns the result of the division
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result@ == self@ / rhs@)]
                fn saturating_div(self, rhs: $type) -> $type;

                #[allow(dead_code)]
                #[check(ghost)]
                // Panics if the divisor is zero
                #[requires(rhs@ != 0)]
                // Returns `self` if the division overflows
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) ==> result.0@ == self@)]
                // Else, returns the result of the division
                #[ensures((self@ == $type::MIN@ && rhs@ == -1) || result.0@ == self@ / rhs@)]
                // Overflow only occurs when computing `$type::MIN / -1`
                #[ensures(result.1 == (self@ == $type::MIN@ && rhs@ == -1))]
                fn overflowing_div(self, rhs: $type) -> ($type, bool);
            }
        }
    };
}

pub trait NumExt {
    #[logic]
    fn leading_zeros_logic(self) -> u32;

    #[logic]
    fn trailing_zeros_logic(self) -> u32;

    #[logic]
    fn leading_ones_logic(self) -> u32;

    #[logic]
    fn trailing_ones_logic(self) -> u32;
}

macro_rules! spec_unsized {
    ($type:ty, $zero:expr, $one:expr) => {
        spec_type!($type);

        impl NumExt for $type {
            #[logic(opaque)]
            #[trusted]
            #[ensures(result <= $type::BITS)]
            #[ensures((result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one))]
            #[ensures((result == $type::BITS) == (self == $zero))]
            fn leading_zeros_logic(self) -> u32 {
                dead
            }

            #[logic(opaque)]
            #[trusted]
            #[ensures(result <= $type::BITS)]
            #[ensures((result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
            #[ensures((result == $type::BITS) == (self == $zero))]
            fn trailing_zeros_logic(self) -> u32 {
                dead
            }

            #[logic(opaque)]
            #[trusted]
            #[ensures(result <= $type::BITS)]
            #[ensures((result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero))]
            #[ensures((result == $type::BITS) == (self == $type::MAX))]
            fn leading_ones_logic(self) -> u32 {
                dead
            }

            #[logic(opaque)]
            #[trusted]
            #[ensures(result <= $type::BITS)]
            #[ensures((result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32)))]
            #[ensures((result == $type::BITS) == (self == $type::MAX))]
            fn trailing_ones_logic(self) -> u32 {
                dead
            }
        }

        extern_spec! {
            impl $type {
                    #[check(ghost)]
                    #[ensures(if self == $zero { result == (self == $zero) } else { result == (self@ % rhs@ == 0) })]
                    fn is_multiple_of(self, rhs: Self) -> bool;

                    #[check(ghost)]
                    #[ensures(result == (self != $zero && self & (self - $one) == $zero))]
                    fn is_power_of_two(self) -> bool;

                    #[check(ghost)]
                    #[ensures(result == self.leading_zeros_logic())]
                    fn leading_zeros(self) -> u32;

                    #[check(ghost)]
                    #[ensures(result == self.trailing_zeros_logic())]
                    fn trailing_zeros(self) -> u32;

                    #[check(ghost)]
                    #[ensures(result == self.leading_ones_logic())]
                    fn leading_ones(self) -> u32;

                    #[check(ghost)]
                    #[ensures(result == self.trailing_ones_logic())]
                    fn trailing_ones(self) -> u32;
            }
        }
    };
}

/// Adds specifications for checked, wrapping, saturating, and overflowing versions of the given
/// operation on the given type. This only works for operations that have no additional pre- or
/// postconditions.
macro_rules! spec_op_common {
    (
        $type:ty,
        $op:tt,
        $checked:ident,
        $wrapping:ident,
        $saturating:ident,
        $overflowing:ident,
        $unchecked:ident
    ) => {
        extern_spec! {
            impl $type {
                // Checked: performs the operation on `Int`, returns `Some` if the result is between
                // `$type::MIN` and `$type::MAX`, or `None` if the result cannot be represented by
                // `$type`
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns `None` iff the result is out of range
                #[ensures(
                    (result == None)
                    == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
                )]
                // Returns `Some(result)` if the result is in range
                #[ensures(forall<r: $type> result == Some(r) ==> r@ == (self@ $op rhs@))]
                fn $checked(self, rhs: $type) -> Option<$type>;

                // Wrapping: performs the operation on `Int` and converts back to `$type`
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result == self $op rhs)]
                fn $wrapping(self, rhs: $type) -> $type;

                // Saturating: performs the operation on `Int` and clamps the result between
                // `$type::MIN` and `$type::MAX`
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns the result if it is in range
                #[ensures(
                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
                    ==> result@ == (self@ $op rhs@)
                )]
                // Returns the nearest bound if the result is out of range
                #[ensures((self@ $op rhs@) < $type::MIN@ ==> result@ == $type::MIN@)]
                #[ensures((self@ $op rhs@) > $type::MAX@ ==> result@ == $type::MAX@)]
                fn $saturating(self, rhs: $type) -> $type;

                // Overflowing: performs the operation on `Int` and converts back to `$type`, and
                // indicates whether an overflow occurred
                #[allow(dead_code)]
                #[check(ghost)]
                // Returns the result if it is in range
                #[ensures(
                    (self@ $op rhs@) >= $type::MIN@ && (self@ $op rhs@) <= $type::MAX@
                    ==> result.0@ == (self@ $op rhs@)
                )]
                // Returns the result shifted by a multiple of the type's range if it is out of
                // range. For addition and subtraction, `k` (qualified over below) will always be 1
                // or -1, but the verifier is able to deduce that.
                #[ensures(
                    exists<k: Int> result.0@ == (self@ $op rhs@) + k * ($type::MAX@ - $type::MIN@ + 1)
                )]
                // Overflow occurred iff the result is out of range
                #[ensures(
                    result.1 == ((self@ $op rhs@) < $type::MIN@ || (self@ $op rhs@) > $type::MAX@)
                )]
                fn $overflowing(self, rhs: $type) -> ($type, bool);

                #[check(ghost)]
                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
                #[ensures(result@ == self@ $op rhs@)]
                unsafe fn $unchecked(self, rhs: $type) -> $type;
            }
        }
    };
}

macro_rules! spec_impl_common {
    ($type:ty) => {
        spec_impl_common!{Add, add, +, AddAssign, add_assign, +=, $type}
        spec_impl_common!{Sub, sub, -, SubAssign, sub_assign, -=, $type}
        spec_impl_common!{Mul, mul, *, MulAssign, mul_assign, *=, $type}
    };
    ($op_trait:ident, $op_method:ident, $op:tt, $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $type:ty) => {
        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, $type}
        spec_impl_common!{@ $op_trait, $op_method, $op, $type, $type, &$type}
        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, $type}
        spec_impl_common!{@ $op_trait, $op_method, $op, $type, &$type, &$type}
        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, $type}
        spec_impl_common!{@assign $op_assign_trait, $op_assign_method, $op_assign, $op, $type, &$type}
    };
    (@ $op_trait:ident, $op_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
        extern_spec! {
            impl core::ops::$op_trait<$rhs> for $lhs {
                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
                #[ensures(result@ == self@ $op rhs@)]
                fn $op_method(self, rhs: $rhs) -> $type {
                    self $op rhs
                }
            }
        }
    };
    (@assign $op_assign_trait:ident, $op_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
        extern_spec! {
            impl core::ops::$op_assign_trait<$rhs> for $type {
                #[requires($type::MIN@ <= self@ $op rhs@ && self@ $op rhs@ <= $type::MAX@)]
                #[ensures((^self)@ == self@ $op rhs@)]
                fn $op_assign_method(&mut self, rhs: $rhs) {
                    *self $op_assign rhs
                }
            }
        }
    }
}

macro_rules! spec_div_rem {
    ($type:ty) => {
        spec_div_rem!{@ Div, div, /, $type}
        spec_div_rem!{@ Rem, rem, %, $type}
        spec_div_rem!{@assign DivAssign, div_assign, /=, /, $type}
        spec_div_rem!{@assign RemAssign, rem_assign, %=, %, $type}
    };
    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty) => {
        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, $type}
        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, $type, &$type}
        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, $type}
        spec_div_rem!{@ $divrem_trait, $divrem_method, $op, $type, &$type, &$type}
    };
    (@ $divrem_trait:ident, $divrem_method:ident, $op:tt, $type:ty, $lhs:ty, $rhs:ty) => {
        extern_spec! {
            impl core::ops::$divrem_trait<$rhs> for $lhs {
                #[requires(rhs@ != 0)]
                #[requires(!(self@ == $type::MIN@ && rhs@ == -1))]
                #[ensures(result@ == self@ $op rhs@)]
                fn $divrem_method(self, rhs: $rhs) -> $type {
                    self $op rhs
                }
            }
        }
    };
    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty) => {
        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, $type}
        spec_div_rem!{@assign $divrem_assign_trait, $divrem_assign_method, $op_assign, $op, $type, &$type}
    };
    (@assign $divrem_assign_trait:ident, $divrem_assign_method:ident, $op_assign:tt, $op:tt, $type:ty, $rhs:ty) => {
        extern_spec! {
            impl core::ops::$divrem_assign_trait<$rhs> for $type {
                #[requires(rhs@ != 0)]
                #[requires(!(*self == $type::MIN && rhs@ == -1))]
                #[ensures((^self)@ == self@ $op rhs@)]
                fn $divrem_assign_method(&mut self, rhs: $rhs) {
                    *self $op_assign rhs
                }
            }
        }
    };
}

/// Adds specifications for the abs_diff operation on the given pair of signed
/// and unsigned integer types
macro_rules! spec_abs_diff {
    ($unsigned:ty, $signed:ty) => {
        extern_spec! {
            impl $unsigned {
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result@ == self@.abs_diff(other@))]
                fn abs_diff(self, other: $unsigned) -> $unsigned;
            }

            impl $signed {
                #[allow(dead_code)]
                #[check(ghost)]
                #[ensures(result@ == self@.abs_diff(other@))]
                fn abs_diff(self, other: $signed) -> $unsigned;
            }
        }
    };
}

spec_unsized!(u8, 0u8, 1u8);
spec_unsized!(u16, 0u16, 1u16);
spec_unsized!(u32, 0u32, 1u32);
spec_unsized!(u64, 0u64, 1u64);
spec_unsized!(u128, 0u128, 1u128);
spec_unsized!(usize, 0usize, 1usize);

spec_type!(i8);
spec_type!(i16);
spec_type!(i32);
spec_type!(i64);
spec_type!(i128);
spec_type!(isize);

spec_abs_diff!(u8, i8);
spec_abs_diff!(u16, i16);
spec_abs_diff!(u32, i32);
spec_abs_diff!(u64, i64);
spec_abs_diff!(u128, i128);
spec_abs_diff!(usize, isize);
