Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Utilities for constructing and destructing Source Tetra expressions.
- takeAnnotOfExp :: GExp l -> Maybe (GXAnnot l)
- bindOfBindMT :: GXBindVarMT l -> GXBindVar l
- takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l)
- makeTApps :: GType l -> [GType l] -> GType l
- takeTApps :: GType l -> [GType l]
- makeTBot :: GType l -> GType l
- makeTFun :: GType l -> GType l -> GType l
- makeTFuns :: [GType l] -> GType l -> GType l
- makeTFuns' :: [GType l] -> Maybe (GType l)
- (~>) :: GType l -> GType l -> GType l
- takeTFun :: GType l -> Maybe (GType l, GType l)
- takeTFuns :: GType l -> ([GType l], GType l)
- takeTFuns' :: GType l -> [GType l]
- makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l
- makeTForalls :: Anon l => l -> [GType l] -> ([GType l] -> GType l) -> GType l
- takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l)
- makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l
- takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l)
- takeTUnion :: GType l -> Maybe (GType l, GType l, GType l)
- makeTUnions :: GType l -> [GType l] -> GType l
- takeTUnions :: Eq (GType l) => GType l -> Maybe (GType l, [GType l])
- splitTUnionsOfKind :: Eq (GType l) => GType l -> GType l -> Maybe [GType l]
- makeXLAMs :: [GXBindVarMT l] -> GExp l -> GExp l
- makeXLams :: [GXBindVarMT l] -> GExp l -> GExp l
- makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l
- takeXLAMs :: GExp l -> Maybe ([GXBindVarMT l], GExp l)
- takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l)
- takeXLamFlags :: GExp l -> Maybe ([(Bool, GXBindVarMT l)], GExp l)
- makeXApps :: GExp l -> [GExp l] -> GExp l
- makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l
- takeXApps :: GExp l -> Maybe (GExp l, [GExp l])
- takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l])
- takeXAppsAsList :: GExp l -> [GExp l]
- takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))])
- takeXConApps :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l])
- takeXPrimApps :: GExp l -> Maybe (GXPrim l, [GExp l])
- bindOfClause :: GClause l -> GXBindVar l
- pattern XRun :: forall t. GExp t -> GExp t
- pattern XBox :: forall t. GExp t -> GExp t
- dcUnit :: DaCon n t
- takeNameOfDaCon :: DaCon n t -> Maybe n
- takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n)
- bindsOfPat :: Pat n -> [Bind n]
- wApp :: a -> Witness a n -> Witness a n -> Witness a n
- wApps :: a -> Witness a n -> [Witness a n] -> Witness a n
- takeXWitness :: Exp a n -> Maybe (Witness a n)
- takeWAppsAsList :: Witness a n -> [Witness a n]
- takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])
Documentation
Binds
bindOfBindMT :: GXBindVarMT l -> GXBindVar l Source #
Take the GBind
of a GBindMT
takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l) Source #
Take the type of a GBindMT
.
Types
Type Applications
takeTApps :: GType l -> [GType l] #
Flatten a sequence of type applications into the function part and arguments, if any.
Sum Types
Function Types
makeTFun :: GType l -> GType l -> GType l infixr 9 #
Construct a function type with the given parameter and result type.
makeTFuns' :: [GType l] -> Maybe (GType l) #
Like makeTFuns
but taking the parameter and return types as a list.
takeTFun :: GType l -> Maybe (GType l, GType l) #
Destruct a function type into its parameter and result types,
returning Nothing
if this isn't a function type.
takeTFuns :: GType l -> ([GType l], GType l) #
Destruct a function type into into all its parameters and result type, returning an empty parameter list if this isn't a function type.
takeTFuns' :: GType l -> [GType l] #
Like takeFuns
, but yield the parameter and return types in the same list.
Forall Types
makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #
Construct a forall quantified type using an anonymous binder.
makeTForalls :: Anon l => l -> [GType l] -> ([GType l] -> GType l) -> GType l #
Construct a forall quantified type using some anonymous binders.
takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l) #
Destruct a forall quantified type, if this is one.
The kind we return comes from the abstraction rather than the Forall constructor.
Exists Types
makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #
Construct an exists quantified type using an anonymous binder.
takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l) #
Destruct an exists quantified type, if this is one.
The kind we return comes from the abstraction rather than the Exists constructor.
Union types
takeTUnion :: GType l -> Maybe (GType l, GType l, GType l) #
Take the kind, left and right types from a union type.
makeTUnions :: GType l -> [GType l] -> GType l #
Make a union type from a kind and list of component types.
takeTUnions :: Eq (GType l) => GType l -> Maybe (GType l, [GType l]) #
Split a union type into its components. If this is not a union, or is an ill kinded union then Nothing.
splitTUnionsOfKind :: Eq (GType l) => GType l -> GType l -> Maybe [GType l] #
Split a union of the given kind into its components. When we split a sum we need to check that the kind attached to the sum type constructor is the one that we were expecting, otherwise we risk splitting ill-kinded sums without noticing it.
Terms
Lambdas
makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l Source #
Make some nested lambda abstractions, using a flag to indicate whether the lambda is a level-1 (True), or level-0 (False) binder.
takeXLAMs :: GExp l -> Maybe ([GXBindVarMT l], GExp l) Source #
Split type lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l) Source #
Split nested value or witness lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLamFlags :: GExp l -> Maybe ([(Bool, GXBindVarMT l)], GExp l) Source #
Split nested lambdas from the front of an expression, with a flag indicating whether the lambda was a level-1 (True), or level-0 (False) binder.
Applications
makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l Source #
Build sequence of applications.
Similar to xApps
but also takes list of annotations for
the XApp
constructors.
takeXApps :: GExp l -> Maybe (GExp l, [GExp l]) Source #
Flatten an application into the function part and its arguments.
Returns Nothing
if there is no outer application.
takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l]) Source #
Flatten an application into the function part and its arguments.
This is like takeXApps
above, except we know there is at least one argument.
takeXAppsAsList :: GExp l -> [GExp l] Source #
Flatten an application into the function parts and arguments, if any.
takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))]) Source #
Destruct sequence of applications.
Similar to takeXAppsAsList
but also keeps annotations for later.
takeXConApps :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l]) Source #
Flatten an application of a data constructor into the constructor and its arguments.
Returns Nothing
if the expression isn't a constructor application.
takeXPrimApps :: GExp l -> Maybe (GXPrim l, [GExp l]) Source #
Flatten an application of a primop into the variable and its arguments.
Returns Nothing
if the expression isn't a primop application.
Clauses
bindOfClause :: GClause l -> GXBindVar l Source #
Take the binding variable of a clause.
Casts
Data Constructors
takeNameOfDaCon :: DaCon n t -> Maybe n #
Take the name of data constructor, if there is one.
takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n) #
Take the type annotation of a data constructor, if we know it locally.
Patterns
bindsOfPat :: Pat n -> [Bind n] #
Take the binds of a Pat
.
Witnesses
wApps :: a -> Witness a n -> [Witness a n] -> Witness a n #
Construct a sequence of witness applications
takeWAppsAsList :: Witness a n -> [Witness a n] #
Flatten an application into the function parts and arguments, if any.
takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n]) #
Flatten an application of a witness into the witness constructor name and its arguments.
Returns nothing if there is no witness constructor in head position.