Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- type family GAnnot l
- type family GBind l
- type family GBound l
- type family GPrim l
- data GExp l
- data GAbs l
- data GArg l
- data GLets l
- data GAlt l = AAlt !(GPat l) !(GExp l)
- data GPat l
- data GCast l
- = CastWeakenEffect !(Type l)
- | CastPurify !(GWitness l)
- | CastBox
- | CastRun
- data GWitness l
- data GWiCon l = WiConBound !(GBound l) !(Type l)
- pattern XLAM :: forall t. GBind t -> GExp t -> GExp t
- pattern XLam :: forall t. GBind t -> GExp t -> GExp t
- module DDC.Type.Exp.Simple.Predicates
- isXVar :: GExp l -> Bool
- isXCon :: GExp l -> Bool
- isAtomX :: GExp l -> Bool
- isAtomR :: GArg l -> Bool
- isAtomW :: GWitness l -> Bool
- isXAbs :: GExp l -> Bool
- isXLAM :: GExp l -> Bool
- isXLam :: GExp l -> Bool
- isXApp :: GExp l -> Bool
- isXLet :: GExp l -> Bool
- isPDefault :: GPat l -> Bool
- module DDC.Type.Exp.Simple.Compounds
- makeXAbs :: [GAbs l] -> GExp l -> GExp l
- takeXAbs :: GExp l -> Maybe ([GAbs l], GExp l)
- makeXLAMs :: [GBind l] -> GExp l -> GExp l
- takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l)
- makeXLams :: [GBind l] -> GExp l -> GExp l
- takeXLams :: GExp l -> Maybe ([GBind l], GExp l)
- makeXApps :: GExp l -> [GArg l] -> GExp l
- takeXApps :: GExp l -> Maybe (GExp l, [GArg l])
- splitXApps :: GExp l -> (GExp l, [GArg l])
- takeXConApps :: GExp l -> Maybe (DaCon l (Type l), [GArg l])
- takeXPrimApps :: GExp l -> Maybe (GPrim l, [GArg l])
- dcUnit :: DaCon n t
- takeNameOfDaCon :: DaCon n t -> Maybe n
- takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n)
- type ShowLanguage l = (Show l, Show (GAnnot l), Show (GBind l), Show (GBound l), Show (GPrim l))
Abstract Syntax
Expressions
Type functions associated with a language definition.
These produce the types used for annotations, bindings, bound occurrences and primitives for that language.
Generic term expression representation.
XAnnot !(GAnnot l) !(GExp l) | An annotated expression. |
XPrim !(GPrim l) | Primitive operator or literal. |
XCon !(DaCon l (Type l)) | Data constructor. |
XVar !(GBound l) | Value or Witness variable (level-0). |
XAbs !(GAbs l) !(GExp l) | Function abstraction. |
XApp !(GExp l) !(GArg l) | Function application. |
XLet !(GLets l) !(GExp l) | Possibly recursive bindings. |
XCase !(GExp l) ![GAlt l] | Case branching. |
XCast !(GCast l) !(GExp l) | Type casting. |
ShowLanguage l => Show (GExp l) Source # | |
data PrettyMode (GExp l) Source # | |
Abstractions.
This indicates what sort of object is being abstracted over in an XAbs.
ShowLanguage l => Show (GAbs l) Source # | |
Arguments.
Carries an argument that can be supplied to a function.
ShowLanguage l => Show (GArg l) Source # | |
data PrettyMode (GArg l) Source # | |
Possibly recursive bindings.
LLet !(GBind l) !(GExp l) | Non-recursive binding. |
LRec ![(GBind l, GExp l)] | Recursive binding. |
LPrivate ![GBind l] !(Maybe (Type l)) ![GBind l] | Introduce a private region variable and witnesses to its properties. |
ShowLanguage l => Show (GLets l) Source # | |
data PrettyMode (GLets l) Source # | |
Case alternatives.
ShowLanguage l => Show (GAlt l) Source # | |
data PrettyMode (GAlt l) Source # | |
Patterns.
PDefault | The default pattern always succeeds. |
PData !(DaCon l (Type l)) ![GBind l] | Match a data constructor and bind its arguments. |
ShowLanguage l => Show (GPat l) Source # | |
Type casts.
CastWeakenEffect !(Type l) | Weaken the effect of an expression. |
CastPurify !(GWitness l) | Purify the effect of an expression. |
CastBox | Box up a computation, suspending its evaluation and capturing its effects in the S computaiton type. |
CastRun | Run a computation, releasing its effects into the context. |
ShowLanguage l => Show (GCast l) Source # | |
Witnesses.
WVar !(GBound l) | Witness variable. |
WCon !(GWiCon l) | Witness constructor. |
WApp !(GWitness l) !(GWitness l) | Witness application. |
WType !(Type l) | Type can appear as an argument of a witness application. |
ShowLanguage l => Show (GWitness l) Source # | |
Witness constructors.
WiConBound !(GBound l) !(Type l) | Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed. |
ShowLanguage l => Show (GWiCon l) Source # | |
Predicates
Atoms
Abstractions
isXLam :: GExp l -> Bool Source #
Check whether an expression is a value or witness abstraction (level-0).
Applications
Let bindings
Patterns
Compounds
Abstractions
takeXAbs :: GExp l -> Maybe ([GAbs l], GExp l) Source #
Split type and value/witness abstractions from the front of an expression,
or Nothing
if there aren't any.
takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l) Source #
Split type lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLams :: GExp l -> Maybe ([GBind l], GExp l) Source #
Split nested value or witness lambdas from the front of an expression,
or Nothing
if there aren't any.
Applications
takeXApps :: GExp l -> Maybe (GExp l, [GArg l]) Source #
Flatten an application into the functional expression and its arguments, or `Nothing if this is not an application.
splitXApps :: GExp l -> (GExp l, [GArg l]) Source #
Flatten an application into a functional expression and its arguments, or just return the expression with no arguments if this is not an application.
takeXConApps :: GExp l -> Maybe (DaCon l (Type l), [GArg l]) Source #
Flatten an application of a data constructor into the constructor itself
and its arguments, or Nothing
if this is not an application of a
data constructor.
takeXPrimApps :: GExp l -> Maybe (GPrim l, [GArg l]) Source #
Flatten an application of a primitive operators into the operator itself
and its arguments, or Nothing
if this is not an application of a
primitive.
Data Constructors
takeNameOfDaCon :: DaCon n t -> Maybe n Source #
Take the name of data constructor, if there is one.
takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n) Source #
Take the type annotation of a data constructor, if we know it locally.