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