content: {-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
  {-# 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 x y = x + y
  
  {-# NOINLINE minus #-}
  minus :: Int -> Int -> Int
  minus x y = x - y
  
  {-# NOINLINE times #-}
  times :: Int -> Int -> Int
  times x y = x * y
  
  -------------------------------------------------------------------
  --------------------------- Comparisons ---------------------------
  -------------------------------------------------------------------
  
  {-# NOINLINE eq #-}
  eq :: Int -> Int -> Bool
  eq x y = x == y
  
  {-# NOINLINE neq #-}
  neq :: Int -> Int -> Bool
  neq x y = not (x == y)
  
  {-# NOINLINE leq #-}
  leq :: Int -> Int -> Bool
  leq x y = x <= y
  
  {-# NOINLINE geq #-}
  geq :: Int -> Int -> Bool
  geq x y = x >= y
  
  {-# NOINLINE lt #-}
  lt :: Int -> Int -> Bool
  lt x y = x < y
  
  {-# NOINLINE gt #-}
  gt :: Int -> Int -> Bool
  gt x y = x > y
  
  -------------------------------------------------------------------
  ------------------------ Specifications ---------------------------
  -------------------------------------------------------------------
  
  
  {-@ ignore liquidAssertB @-}
  {-@ assume liquidAssertB :: x:{v:Bool | v} -> {v: Bool | v} @-}
  {-# NOINLINE liquidAssertB #-}
  liquidAssertB :: Bool -> Bool
  liquidAssertB b = b
  
  {-@ assume liquidAssert :: {v:Bool | v} -> a -> a  @-}
  {-# NOINLINE liquidAssert #-}
  liquidAssert :: Bool -> a -> a
  liquidAssert _ x = x
  
  {-@ ignore liquidAssume @-}
  {-@ assume liquidAssume :: b:Bool -> a -> {v: a | b}  @-}
  {-# NOINLINE liquidAssume #-}
  liquidAssume :: Bool -> a -> a
  liquidAssume b x = if b then x else error "liquidAssume fails"
  
  {-@ ignore liquidAssumeB @-}
  {-@ assume liquidAssumeB :: forall <p :: a -> Bool>. (a<p> -> {v:Bool| v}) -> a -> a<p> @-}
  liquidAssumeB :: (a -> Bool) -> a -> a
  liquidAssumeB p x | p x = x
                    | otherwise = error "liquidAssumeB fails"
  
  
  {-@ ignore unsafeError @-}
  {-# NOINLINE unsafeError #-}
  unsafeError :: String -> a
  unsafeError = error
  
  
  {-@ liquidError :: {v:String | 0 = 1} -> a  @-}
  {-# NOINLINE liquidError #-}
  liquidError :: String -> a
  liquidError = error
  
  {-@ assume crash  :: forall a . x:{v:Bool | v} -> a @-}
  {-# NOINLINE crash #-}
  crash :: Bool -> a
  crash = undefined
  
  {-# NOINLINE force #-}
  force :: Bool
  force = True
  
  {-# NOINLINE choose #-}
  choose :: Int -> Int
  choose = 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 x = x `mod` 2 == 0
  
  {-@ assume isOdd :: x:Int -> {v:Bool | ((v) <=> ((x mod 2) = 1))} @-}
  {-# NOINLINE isOdd #-}
  isOdd   :: Int -> Bool
  isOdd x = x `mod` 2 == 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 f (a:as) (b:bs) = f a b : safeZipWith f as bs
  safeZipWith _ []     []     = []
  safeZipWith _ _ _ = error "safeZipWith: cannot happen!"
  
  {-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p => q)} @-}
  infixr 8 ==>
  (==>) :: Bool -> Bool -> Bool
  False ==> False = True
  False ==> True  = True
  True  ==> True  = True
  True  ==> False = False
  
  {-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p <=> q)} @-}
  infixr 8 <=>
  (<=>) :: Bool -> Bool -> Bool
  False <=> False = True
  False <=> True  = False
  True  <=> True  = True
  True  <=> False = False
  