{-# LANGUAGE MagicHash      #-}

module Language.Haskell.Liquid.Prelude where

-------------------------------------------------------------------
--------------------------- Arithmetic ----------------------------
-------------------------------------------------------------------

{-@ assume plus   :: x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}  @-}
{-@ assume minus  :: x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x - y} @-}
{-@ assume times  :: x:Int -> y:Int -> Int                           @-}
{-@ assume eq     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x = y)}  @-}
{-@ assume neq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x != y)} @-}
{-@ assume leq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x <= y)} @-}
{-@ assume geq    :: x:Int -> y:Int -> {v:Bool | ((v) <=> x >= y)} @-}
{-@ assume lt     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x < y)}  @-}
{-@ assume gt     :: x:Int -> y:Int -> {v:Bool | ((v) <=> x > y)}  @-}

{-# NOINLINE plus #-}
plus :: Int -> Int -> Int
plus :: Int -> Int -> Int
plus Int
x Int
y = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
y

{-# NOINLINE minus #-}
minus :: Int -> Int -> Int
minus :: Int -> Int -> Int
minus Int
x Int
y = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
y

{-# NOINLINE times #-}
times :: Int -> Int -> Int
times :: Int -> Int -> Int
times Int
x Int
y = Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
y

-------------------------------------------------------------------
--------------------------- Comparisons ---------------------------
-------------------------------------------------------------------

{-# NOINLINE eq #-}
eq :: Int -> Int -> Bool
eq :: Int -> Int -> Bool
eq Int
x Int
y = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y

{-# NOINLINE neq #-}
neq :: Int -> Int -> Bool
neq :: Int -> Int -> Bool
neq Int
x Int
y = Bool -> Bool
not (Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y)

{-# NOINLINE leq #-}
leq :: Int -> Int -> Bool
leq :: Int -> Int -> Bool
leq Int
x Int
y = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
y

{-# NOINLINE geq #-}
geq :: Int -> Int -> Bool
geq :: Int -> Int -> Bool
geq Int
x Int
y = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
y

{-# NOINLINE lt #-}
lt :: Int -> Int -> Bool
lt :: Int -> Int -> Bool
lt Int
x Int
y = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y

{-# NOINLINE gt #-}
gt :: Int -> Int -> Bool
gt :: Int -> Int -> Bool
gt Int
x Int
y = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
y

-------------------------------------------------------------------
------------------------ Specifications ---------------------------
-------------------------------------------------------------------


{-@ ignore liquidAssertB @-}
{-@ assume liquidAssertB :: x:{v:Bool | v} -> {v: Bool | v} @-}
{-# NOINLINE liquidAssertB #-}
liquidAssertB :: Bool -> Bool
liquidAssertB :: Bool -> Bool
liquidAssertB Bool
b = Bool
b

{-@ assume liquidAssert :: {v:Bool | v} -> a -> a  @-}
{-# NOINLINE liquidAssert #-}
liquidAssert :: Bool -> a -> a
liquidAssert :: Bool -> a -> a
liquidAssert Bool
_ a
x = a
x

{-@ ignore liquidAssume @-}
{-@ assume liquidAssume :: b:Bool -> a -> {v: a | b}  @-}
{-# NOINLINE liquidAssume #-}
liquidAssume :: Bool -> a -> a
liquidAssume :: Bool -> a -> a
liquidAssume Bool
b a
x = if Bool
b then a
x else [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"liquidAssume fails"

{-@ ignore liquidAssumeB @-}
{-@ assume liquidAssumeB :: forall <p :: a -> Bool>. (a<p> -> {v:Bool| v}) -> a -> a<p> @-}
liquidAssumeB :: (a -> Bool) -> a -> a
liquidAssumeB :: (a -> Bool) -> a -> a
liquidAssumeB a -> Bool
p a
x | a -> Bool
p a
x = a
x
                  | Bool
otherwise = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"liquidAssumeB fails"


{-@ ignore unsafeError @-}
{-# NOINLINE unsafeError #-}
unsafeError :: String -> a
unsafeError :: [Char] -> a
unsafeError = [Char] -> a
forall a. HasCallStack => [Char] -> a
error


{-@ liquidError :: {v:String | 0 = 1} -> a  @-}
{-# NOINLINE liquidError #-}
liquidError :: String -> a
liquidError :: [Char] -> a
liquidError = [Char] -> a
forall a. HasCallStack => [Char] -> a
error

{-@ assume crash  :: forall a . x:{v:Bool | v} -> a @-}
{-# NOINLINE crash #-}
crash :: Bool -> a
crash :: Bool -> a
crash = Bool -> a
forall a. HasCallStack => a
undefined

{-# NOINLINE force #-}
force :: Bool
force :: Bool
force = Bool
True

{-# NOINLINE choose #-}
choose :: Int -> Int
choose :: Int -> Int
choose = Int -> Int
forall a. HasCallStack => a
undefined

-------------------------------------------------------------------
----------- Modular Arithmetic Wrappers ---------------------------
-------------------------------------------------------------------

-- tedium because fixpoint doesn't want to deal with (x mod y) only (x mod c)
{-@ assume isEven :: x:Int -> {v:Bool | ((v) <=> ((x mod 2) = 0))} @-}
{-# NOINLINE isEven #-}
isEven   :: Int -> Bool
isEven :: Int -> Bool
isEven Int
x = Int
x Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0

{-@ assume isOdd :: x:Int -> {v:Bool | ((v) <=> ((x mod 2) = 1))} @-}
{-# NOINLINE isOdd #-}
isOdd   :: Int -> Bool
isOdd :: Int -> Bool
isOdd Int
x = Int
x Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1

-----------------------------------------------------------------------------------------------

{-@ safeZipWith :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len v = len xs} 
                -> {v : [c] | len v = len xs } @-}
safeZipWith :: (a->b->c) -> [a]->[b]->[c]
safeZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith a -> b -> c
f (a
a:[a]
as) (b
b:[b]
bs) = a -> b -> c
f a
a b
b c -> [c] -> [c]
forall a. a -> [a] -> [a]
: (a -> b -> c) -> [a] -> [b] -> [c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith a -> b -> c
f [a]
as [b]
bs
safeZipWith a -> b -> c
_ []     []     = []
safeZipWith a -> b -> c
_ [a]
_ [b]
_ = [Char] -> [c]
forall a. HasCallStack => [Char] -> a
error [Char]
"safeZipWith: cannot happen!"

{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p =>  q)} @-}
infixr 8 ==>
(==>) :: Bool -> Bool -> Bool
Bool
False ==> :: Bool -> Bool -> Bool
==> Bool
False = Bool
True
Bool
False ==> Bool
True  = Bool
True
Bool
True  ==> Bool
True  = Bool
True
Bool
True  ==> Bool
False = Bool
False