{-# LANGUAGE OverloadedStrings, Safe #-} module SMTLib2.Int where import SMTLib2.AST tInt :: Type tInt :: Type tInt = Ident -> [Type] -> Type TApp (Name -> [Integer] -> Ident I Name "Int" []) [] num :: Integral a => a -> Expr num :: forall a. Integral a => a -> Expr num a a = Literal -> Expr Lit (Integer -> Literal LitNum (a -> Integer forall a. Integral a => a -> Integer toInteger a a)) nNeg :: Expr -> Expr nNeg :: Expr -> Expr nNeg Expr x = Ident -> [Expr] -> Expr app Ident "-" [Expr x] nSub :: Expr -> Expr -> Expr nSub :: Expr -> Expr -> Expr nSub Expr x Expr y = Ident -> [Expr] -> Expr app Ident "-" [Expr x,Expr y] nAdd :: Expr -> Expr -> Expr nAdd :: Expr -> Expr -> Expr nAdd Expr x Expr y = Ident -> [Expr] -> Expr app Ident "+" [Expr x,Expr y] nMul :: Expr -> Expr -> Expr nMul :: Expr -> Expr -> Expr nMul Expr x Expr y = Ident -> [Expr] -> Expr app Ident "*" [Expr x,Expr y] nDiv :: Expr -> Expr -> Expr nDiv :: Expr -> Expr -> Expr nDiv Expr x Expr y = Ident -> [Expr] -> Expr app Ident "div" [Expr x,Expr y] nMod :: Expr -> Expr -> Expr nMod :: Expr -> Expr -> Expr nMod Expr x Expr y = Ident -> [Expr] -> Expr app Ident "mod" [Expr x,Expr y] nAbs :: Expr -> Expr nAbs :: Expr -> Expr nAbs Expr x = Ident -> [Expr] -> Expr app Ident "abs" [Expr x] nLeq :: Expr -> Expr -> Expr nLeq :: Expr -> Expr -> Expr nLeq Expr x Expr y = Ident -> [Expr] -> Expr app Ident "<=" [Expr x,Expr y] nLt :: Expr -> Expr -> Expr nLt :: Expr -> Expr -> Expr nLt Expr x Expr y = Ident -> [Expr] -> Expr app Ident "<" [Expr x,Expr y] nGeq :: Expr -> Expr -> Expr nGeq :: Expr -> Expr -> Expr nGeq Expr x Expr y = Ident -> [Expr] -> Expr app Ident ">=" [Expr x,Expr y] nGt :: Expr -> Expr -> Expr nGt :: Expr -> Expr -> Expr nGt Expr x Expr y = Ident -> [Expr] -> Expr app Ident ">" [Expr x,Expr y]