module Test.Target.Expr where
import Language.Fixpoint.Types
eq :: Expr -> Expr -> Pred
eq = PAtom Eq
infix 4 `eq`
ge :: Expr -> Expr -> Pred
ge = PAtom Ge
infix 5 `ge`
le :: Expr -> Expr -> Pred
le = PAtom Le
infix 5 `le`
gt :: Expr -> Expr -> Pred
gt = PAtom Gt
infix 5 `gt`
lt :: Expr -> Expr -> Pred
lt = PAtom Lt
infix 5 `lt`
iff :: Pred -> Pred -> Pred
iff = PIff
infix 3 `iff`
imp :: Pred -> Pred -> Pred
imp = PImp
infix 3 `imp`
app :: Symbolic a => a -> [Expr] -> Expr
app f es = EApp (dummyLoc $ symbol f) es
var :: Symbolic a => a -> Expr
var = EVar . symbol
prop :: Expr -> Pred
prop = PBexp
instance Num Expr where
fromInteger = ECon . I . fromInteger
(+) = EBin Plus
() = EBin Minus
(*) = EBin Times
abs = error "abs of Liquid.Fixpoint.Types.Expr"
signum = error "signum of Liquid.Fixpoint.Types.Expr"
instance Real Expr where
toRational (ECon (I i)) = fromIntegral i
toRational x = error $ "toRational: " ++ show x
instance Enum Expr where
toEnum = ECon . I . fromIntegral
fromEnum (ECon (I i)) = fromInteger i
fromEnum x = error $ "fromEnum: " ++ show x
instance Integral Expr where
div = EBin Div
mod = EBin Mod
quotRem x y = (x `div` y, x `mod` y)
toInteger (ECon (I i)) = i
toInteger x = error $ "toInteger: " ++ show x