{-# options -fno-warn-incomplete-patterns #-}
module Stdlib where

import Z3.Monad as Z3

import AST
import Data.Set (Set)
import qualified Data.Set as Set

opEq [VInt x, VInt y] = VBool (x == y)
opEq [VBool x, VBool y] = VBool (x == y)
opEq [VDom x, VDom y] = VBool (x == y)
opNot [VBool x] = VBool (not x)
opAnd [VBool x, VBool y] = VBool (x && y)
opOr [VBool x, VBool y] = VBool (x || y)
opIns [VInt x, VDom y] = VDom (Set.insert x y)
opDel [VInt x, VDom y] = VDom (Set.delete x y)
opUnion [VDom x, VDom y] = VDom (Set.union x y)
opIntersection [VDom x, VDom y] = VDom (Set.intersection x y)
opDiff [VDom x, VDom y] = VDom (Set.difference x y)
opIn [VInt x, VDom y] = VBool (Set.member x y)
opSubset [VDom x, VDom y] = VBool (Set.isSubsetOf x y)
opAdd [VInt x, VInt y] = VInt (x + y)
opMul [VInt x, VInt y] = VInt (x * y)
opSub [VInt x, VInt y] = VInt (x - y)
opNeg [VInt x] = VInt (-x)
opDiv [VInt x, VInt y] = VInt (x `div` y)
opMod [VInt x, VInt y] = VInt (x `mod` y)
opRem [VInt x, VInt y] = VInt (x `rem` y)
opLt [VInt x, VInt y] = VBool (x < y)
opLe [VInt x, VInt y] = VBool (x <= y)
opGt [VInt x, VInt y] = VBool (x > y)
opGe [VInt x, VInt y] = VBool (x >= y)

mkEq [x, y] = Z3.mkEq x y
mkNot [x] = Z3.mkNot x
mkAnd [x, y] = Z3.mkAnd [x, y]
mkOr [x, y] = Z3.mkOr [x, y]
mkIns [x, y] = Z3.mkSetAdd y x
mkDel [x, y] = Z3.mkSetDel y x
mkUnion [x, y] = Z3.mkSetUnion [x, y]
mkIntersection [x, y] = Z3.mkSetIntersect [x, y]
mkDiff [x, y] = Z3.mkSetDifference x y
mkIn [x, y] = Z3.mkSetMember x y
mkSubset [x, y] = Z3.mkSetSubset x y
mkAdd [x, y] = Z3.mkAdd [x, y]
mkMul [x, y] = Z3.mkMul [x, y]
mkSub [x, y] = Z3.mkSub [x, y]
mkNeg [x] = Z3.mkUnaryMinus x
mkDiv [x, y] = Z3.mkDiv x y
mkMod [x, y] = Z3.mkMod x y
mkRem [x, y] = Z3.mkRem x y
mkLt [x, y] = Z3.mkLt x y
mkLe [x, y] = Z3.mkLe x y
mkGt [x, y] = Z3.mkGt x y
mkGe [x, y] = Z3.mkGe x y
