module Z3.Lang.Exprs (
Compilable(..)
, IsTy(..)
, IsFun(..)
, Castable(..)
, IsNum
, IsInt
, IsReal
, Uniq
, Layout
, Expr (..)
, Pattern (..)
, Quantifier(..)
, QExpr(..)
, FunApp (..)
, BoolBinOp (..)
, BoolMultiOp (..)
, CRingOp (..)
, IntOp (..)
, RealOp (..)
, CmpOpE (..)
, CmpOpI (..)
, typecheck
, TCM
, TCC
, ok
, withHypo
, newTCC
, evalTCM
) where
import Z3.Lang.Monad ( Z3 )
import Z3.Lang.TY
import qualified Z3.Base as Base
import Control.Monad.RWS
import Data.Typeable ( Typeable )
class Compilable t where
compile :: t -> Z3 Base.AST
class (Eq a, Show a, Typeable a, Compilable (Expr a)) => IsTy a where
typeInv :: Expr a -> Expr Bool
tc :: Expr a -> TCM ()
mkSort :: TY a -> Z3 Base.Sort
mkLiteral :: a -> Z3 Base.AST
getValue :: Base.AST -> Z3 a
class IsFun a where
domain :: TY a -> Z3 [Base.Sort]
range :: TY a -> Z3 Base.Sort
class (IsTy a, Num a) => IsNum a where
class (IsNum a, Integral a) => IsInt a where
class (IsNum a, Fractional a, Real a) => IsReal a where
type Uniq = Int
type Layout = Int
data Expr :: * -> * where
Lit :: IsTy a => a -> Expr a
Const :: !Uniq -> Base.AST -> Expr a
Tag :: !Layout -> Expr a
Not :: Expr Bool -> Expr Bool
BoolBin :: BoolBinOp -> Expr Bool -> Expr Bool -> Expr Bool
BoolMulti :: BoolMultiOp -> [Expr Bool] -> Expr Bool
Quant :: QExpr t => Quantifier -> t -> Expr Bool
Neg :: IsNum a => Expr a -> Expr a
CRingArith :: IsNum a => CRingOp -> [Expr a] -> Expr a
IntArith :: IsInt a => IntOp -> Expr a -> Expr a -> Expr a
RealArith :: IsReal a => RealOp -> Expr a -> Expr a -> Expr a
CmpE :: IsTy a => CmpOpE -> [Expr a] -> Expr Bool
CmpI :: IsNum a => CmpOpI -> Expr a -> Expr a -> Expr Bool
Ite :: IsTy a => Expr Bool -> Expr a -> Expr a -> Expr a
App :: IsTy a => FunApp a -> Expr a
Cast :: (IsTy a, IsTy b, Castable a b) => Expr a -> Expr b
class QExpr t where
compileQuant :: Quantifier -> [Base.Symbol] -> [Base.Sort] -> t -> Z3 Base.AST
class (IsTy a, IsTy b) => Castable a b where
compileCast :: TY (a,b) -> Base.AST -> Z3 Base.AST
data Pattern where
Pat :: IsTy a => Expr a -> Pattern
data Quantifier = ForAll | Exists
deriving (Eq, Show)
data FunApp :: * -> * where
FuncDecl :: IsFun a => Base.FuncDecl -> FunApp a
PApp :: IsTy a => FunApp (a -> b) -> Expr a -> FunApp b
data BoolBinOp = Xor | Implies | Iff
deriving (Eq,Show)
data BoolMultiOp = And | Or
deriving (Eq,Show)
data CRingOp = Add | Mul | Sub
deriving (Eq,Show)
data IntOp = Quot | Mod | Rem
deriving (Eq,Show)
data RealOp = Div
deriving (Eq,Show)
data CmpOpE = Eq | Distinct
deriving (Eq, Show, Typeable)
data CmpOpI = Le | Lt | Ge | Gt
deriving (Eq, Show, Typeable)
newtype TCM a = TCM { unTCM :: RWS Context [TCC] () a }
deriving Monad
type TCC = Expr Bool
type Context = [Expr Bool]
ok :: TCM ()
ok = return ()
withHypo :: Expr Bool -> TCM a -> TCM a
withHypo h = TCM . local (h:) . unTCM
newTCC :: [Expr Bool] -> TCM ()
newTCC tccs = TCM $ do
hs <- ask
tell $ map (mkTCC hs) tccs
where mkTCC [] = id
mkTCC hs = BoolBin Implies (BoolMulti And hs)
evalTCM :: TCM a -> (a,[TCC])
evalTCM m = evalRWS (unTCM m) [] ()
typecheck :: IsTy a => Expr a -> [Expr Bool]
typecheck e = snd $ evalTCM (tc e)