{-# 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]