Safe Haskell | None |
---|---|
Language | Haskell2010 |
The abstract syntax
- data Head a
- data Local a = Local {}
- data Global a = Global {}
- data Expr a
- data Quant
- data QuantInfo = NoInfo
- data Case a = Case {}
- data Builtin
- intBuiltin :: Builtin -> Bool
- litBuiltin :: Builtin -> Bool
- eqRelatedBuiltin :: Builtin -> Bool
- logicalBuiltin :: Builtin -> Bool
- data Lit
- data Pattern a
- data PolyType a = PolyType {
- polytype_tvs :: [a]
- polytype_args :: [Type a]
- polytype_res :: Type a
- data Type a
- = TyVar a
- | TyCon a [Type a]
- | [Type a] :=>: (Type a)
- | BuiltinType BuiltinType
- data BuiltinType
- data Function a = Function {}
- data Signature a = Signature {}
- data Sort a = Sort {
- sort_name :: a
- sort_arity :: Int
- data Datatype a = Datatype {
- data_name :: a
- data_tvs :: [a]
- data_cons :: [Constructor a]
- data Constructor a = Constructor {
- con_name :: a
- con_discrim :: a
- con_args :: [(a, Type a)]
- data Theory a = Theory {
- thy_datatypes :: [Datatype a]
- thy_sorts :: [Sort a]
- thy_sigs :: [Signature a]
- thy_funcs :: [Function a]
- thy_asserts :: [Formula a]
- emptyTheory :: Theory a
- joinTheories :: Theory a -> Theory a -> Theory a
- data Formula a = Formula {}
- data Role
- transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a
- transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a)
- transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a
- transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a)
- transformType :: (Type a -> Type a) -> Type a -> Type a
- transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a
Documentation
(Head a) :@: [Expr a] infix 5 | |
Lcl (Local a) | |
Lam [Local a] (Expr a) | |
Match (Expr a) [Case a] | The default case comes first if there is one |
Let (Local a) (Expr a) (Expr a) | |
Quant QuantInfo Quant [Local a] (Expr a) |
Functor Expr | |
Foldable Expr | |
Traversable Expr | |
TransformBi a (Expr a) | |
Monad m => TransformBiM m (Expr a) (Formula a) | |
Monad m => TransformBiM m (Expr a) (Theory a) | |
Monad m => TransformBiM m (Local a) (Expr a) | |
Monad m => TransformBiM m (Pattern a) (Expr a) | |
Monad m => TransformBiM m (Expr a) (Function a) | |
Monad m => TransformBiM m (Expr a) (Expr a) | |
Eq a => Eq (Expr a) | |
Ord a => Ord (Expr a) | |
Show a => Show (Expr a) | |
(Ord a, PrettyVar a) => Pretty (Expr a) | |
UniverseBi (Theory a) (Expr a) | |
UniverseBi (Function a) (Expr a) | |
UniverseBi (Expr a) (Expr a) | |
UniverseBi (Expr a) (Pattern a) | |
UniverseBi (Expr a) (Local a) | |
UniverseBi (Expr a) (Global a) | |
TransformBi (Type a) (Expr a) | |
TransformBi (Pattern a) (Expr a) | |
TransformBi (Expr a) (Expr a) | |
TransformBi (Expr a) (Function a) | |
TransformBi (Expr a) (Theory a) | |
TransformBi (Local a) (Expr a) | |
TransformBi (Head a) (Expr a) |
intBuiltin :: Builtin -> Bool Source
litBuiltin :: Builtin -> Bool Source
eqRelatedBuiltin :: Builtin -> Bool Source
logicalBuiltin :: Builtin -> Bool Source
Patterns in branches
Functor Pattern | |
Foldable Pattern | |
Traversable Pattern | |
Monad m => TransformBiM m (Pattern a) (Expr a) | |
Eq a => Eq (Pattern a) | |
Ord a => Ord (Pattern a) | |
Show a => Show (Pattern a) | |
PrettyVar a => Pretty (Pattern a) | |
UniverseBi (Expr a) (Pattern a) | |
TransformBi (Pattern a) (Expr a) | |
TransformBi (Pattern a) (Theory a) |
Polymorphic types
PolyType | |
|
Types
TyVar a | |
TyCon a [Type a] | |
[Type a] :=>: (Type a) | |
BuiltinType BuiltinType |
Functor Type | |
Foldable Type | |
Traversable Type | |
Monad m => TransformBiM m (Type a) (Type a) | |
Eq a => Eq (Type a) | |
Ord a => Ord (Type a) | |
Show a => Show (Type a) | |
PrettyVar a => Pretty (Type a) | |
UniverseBi (Theory a) (Type a) | |
UniverseBi (Datatype a) (Type a) | |
UniverseBi (Function a) (Type a) | |
UniverseBi (Type a) (Type a) | |
TransformBi (Type a) (Theory a) | |
TransformBi (Type a) (Expr a) | |
TransformBi (Type a) (Type a) |
Functor Function | |
Foldable Function | |
Traversable Function | |
Definition Function | |
Monad m => TransformBiM m (Function a) (Theory a) | |
Monad m => TransformBiM m (Expr a) (Function a) | |
Eq a => Eq (Function a) | |
Ord a => Ord (Function a) | |
Show a => Show (Function a) | |
(Ord a, PrettyVar a) => Pretty (Function a) | |
UniverseBi (Function a) (Expr a) | |
UniverseBi (Function a) (Global a) | |
UniverseBi (Function a) (Type a) | |
TransformBi (Expr a) (Function a) |
Uninterpreted function
Uninterpreted sort
Sort | |
|
Data definition
Datatype | |
|
data Constructor a Source
Constructor | |
|
Functor Constructor | |
Foldable Constructor | |
Traversable Constructor | |
Eq a => Eq (Constructor a) | |
Ord a => Ord (Constructor a) | |
Show a => Show (Constructor a) | |
UniverseBi (Theory a) (Constructor a) |
Theory | |
|
Functor Theory | |
Foldable Theory | |
Traversable Theory | |
Monad m => TransformBiM m (Function a) (Theory a) | |
Monad m => TransformBiM m (Expr a) (Theory a) | |
Eq a => Eq (Theory a) | |
Ord a => Ord (Theory a) | |
Show a => Show (Theory a) | |
Monoid (Theory a) | |
(Ord a, PrettyVar a) => Pretty (Theory a) | |
UniverseBi (Theory a) Builtin | |
UniverseBi (Theory a) (Expr a) | |
UniverseBi (Theory a) (Type a) | |
UniverseBi (Theory a) (Constructor a) | |
UniverseBi (Theory a) (Global a) | |
TransformBi (Type a) (Theory a) | |
TransformBi (Pattern a) (Theory a) | |
TransformBi (Expr a) (Theory a) | |
TransformBi (Head a) (Theory a) |
emptyTheory :: Theory a Source
joinTheories :: Theory a -> Theory a -> Theory a Source
transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a Source
transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a) Source