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