THFun
Fields deriveFunctionType :: (Maybe [Maybe THType], Maybe THType) -> (Maybe [Maybe THType], Maybe THType) getSymbol :: (Maybe [Maybe THType], Maybe THType) -> ExpQ allEqSymbol :: ExpQ match :: PatQ matchAllEq :: PatQ -> PatQ

data THExpression Source

Constructors

THExpr
Fields deriveType :: THType getExpr' :: ExpQ

type THBind = Map String THExpression Source

deriveAllEqType :: [THExpression] -> THType Source

toFunction :: BasicExpr -> THFunction Source

toOrd :: Name -> THFunction Source

toArith :: Name -> THFunction Source

toArithBin :: Name -> THFunction Source

toLogic :: Name -> THFunction Source

toExpression :: THBind -> BasicExpr -> THExpression Source

toQuantifier :: Quantifier -> THBind -> [BasicExpr] -> BasicExpr -> THExpression Source

parseList :: String -> Maybe ([BasicExpr], String) Source

parseExpr :: String -> Maybe (BasicExpr, String) Source

parseName :: String -> Maybe (String, String) Source

parseHs :: String -> Maybe (String, String) Source

parseArgs :: String -> Maybe [BasicExpr] Source

parseSingleExpr :: String -> Maybe BasicExpr Source

expr :: QuasiQuoter Source

This quasiquoter can be used to generate SMTLib2 expressions or pattern matches. For example, to assert the fact that variable x is equal to variable y we can use

[expr| (= x y) |] >>= assert

To perform pattern matching against an expression e, we can use:

analyze e >>= \re -> case re of
  [expr| (+ x y) |] -> ...

Types can also be generated using for example:

myExpr :: Backend b => SMT b (Expr b [expr| (Array Int Bool) |])
myExpr = [expr| ((as const (Array Int Bool)) False) |]

declare :: QuasiQuoter Source

define :: QuasiQuoter Source

toFunDef :: [(String, THType)] -> BasicExpr -> THBind -> [ExpQ] -> ExpQ Source

entypeExpr :: Proxy (t :: Type) -> e t -> e t Source

toExpr :: THBind -> BasicExpr -> ExpQ Source

enforceTypes :: Proxy tps -> (List e tps -> a) -> List e tps -> a Source

toVarSig :: [BasicExpr] -> [(String, THType)] Source

toQuant :: [(String, Type)] -> Map String Exp -> Q (Exp, Map String Exp) Source

quantSig :: [(String, Type)] -> TypeQ Source

asSig :: Proxy sig -> (List e sig -> a) -> List e sig -> a Source

toPat :: BasicExpr -> PatQ Source

distinct' :: Embed m e => [e t] -> m (e BoolType) Source

arith' :: (Embed m e, SMTArith t) => ArithOp -> [e t] -> m (e t) Source

logic' :: Embed m e => LogicOp -> [e BoolType] -> m (e BoolType) Source

and' :: Embed m e => [e BoolType] -> m (e BoolType) Source

or' :: Embed m e => [e BoolType] -> m (e BoolType) Source

xor' :: Embed m e => [e BoolType] -> m (e BoolType) Source

implies' :: Embed m e => [e BoolType] -> m (e BoolType) Source

plus' :: (Embed m e, SMTArith t) => [e t] -> m (e t) Source

minus' :: (Embed m e, SMTArith t) => [e t] -> m (e t) Source

mult' :: (Embed m e, SMTArith t) => [e t] -> m (e t) Source

toType :: BasicExpr -> THType Source

thElementType :: THType -> THType Source

thIndexType :: THType -> Either [Type] ExpQ Source

thMakeArray :: Either [Type] ExpQ -> THType -> THType Source

mkArgsPat :: [BasicExpr] -> PatQ Source

mkAllEqPat :: [BasicExpr] -> PatQ Source

mkNum :: Integer -> TypeQ Source