Documentation

type family AllEq tp n :: [Type] Source

allEqToList :: Natural n -> List a (AllEq tp n) -> [a tp] Source

allEqFromList :: [a tp] -> (forall n. Natural n -> List a (AllEq tp n) -> r) -> r Source

allEqOf :: Repr tp -> Natural n -> List Repr (AllEq tp n) Source

mapAllEq :: Monad m => (e1 tp -> m (e2 tp)) -> Natural n -> List e1 (AllEq tp n) -> m (List e2 (AllEq tp n)) Source

data Function fun con field sig where Source

data AnyFunction fun con field where Source

data OrdOp Source

data ArithOp Source

data ArithOpInt Source

data LogicOp Source

data BVCompOp Source

data BVBinOp Source

data BVUnOp Source

data LetBinding v e t Source

data Quantifier Source

data Expression v qv fun con field fv lv e res where Source

class SMTOrd t where Source

class SMTArith t where Source

functionType :: Monad m => (forall arg t. fun `(arg, t)` -> m (List Repr arg, Repr t)) -> (forall arg dt. IsDatatype dt => con `(arg, dt)` -> m (List Repr arg, Datatype `(DatatypeSig dt, dt)`)) -> (forall dt t. IsDatatype dt => field `(dt, t)` -> m (Datatype `(DatatypeSig dt, dt)`, Repr t)) -> Function fun con field `(arg, res)` -> m (List Repr arg, Repr res) Source

expressionType :: (Monad m, Functor m) => (forall t. v t -> m (Repr t)) -> (forall t. qv t -> m (Repr t)) -> (forall arg t. fun `(arg, t)` -> m (List Repr arg, Repr t)) -> (forall arg dt. IsDatatype dt => con `(arg, dt)` -> m (List Repr arg, Datatype `(DatatypeSig dt, dt)`)) -> (forall dt t. IsDatatype dt => field `(dt, t)` -> m (Datatype `(DatatypeSig dt, dt)`, Repr t)) -> (forall t. fv t -> m (Repr t)) -> (forall t. lv t -> m (Repr t)) -> (forall t. e t -> m (Repr t)) -> Expression v qv fun con field fv lv e res -> m (Repr res) Source

mapExpr Source

mapFunction :: (Functor m, Monad m) => (forall arg t. fun1 `(arg, t)` -> m (fun2 `(arg, t)`)) -> (forall arg t. con1 `(arg, t)` -> m (con2 `(arg, t)`)) -> (forall t res. field1 `(t, res)` -> m (field2 `(t, res)`)) -> Function fun1 con1 field1 `(arg, res)` -> m (Function fun2 con2 field2 `(arg, res)`) Source

data RenderMode Source

renderExprDefault :: (GetType qv, GShow v, GShow qv, GShow fun, GShow con, GShow field, GShow fv, GShow lv, GShow e) => RenderMode -> Expression v qv fun con field fv lv e tp -> ShowS Source

renderExpr :: GetType qv => RenderMode -> (forall tp. v tp -> ShowS) -> (forall tp. qv tp -> ShowS) -> (forall arg res. fun `(arg, res)` -> ShowS) -> (forall arg dt. con `(arg, dt)` -> ShowS) -> (forall dt res. field `(dt, res)` -> ShowS) -> (forall tp. fv tp -> ShowS) -> (forall tp. lv tp -> ShowS) -> (forall tp. e tp -> ShowS) -> Expression v qv fun con field fv lv e tp -> ShowS Source

renderValue :: RenderMode -> (forall arg dt. con `(arg, dt)` -> ShowS) -> Value con tp -> ShowS Source

renderFunction :: RenderMode -> (forall arg res. fun `(arg, res)` -> ShowS) -> (forall arg dt. con `(arg, dt)` -> ShowS) -> (forall dt res. field `(dt, res)` -> ShowS) -> Function fun con field `(arg, res)` -> ShowS Source

renderType :: RenderMode -> Repr tp -> ShowS Source

data NoVar t Source

data NoFun sig Source

data NoCon sig Source

data NoField sig Source