Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- module DDC.Type.Exp
- data Exp a n
- data Lets a n
- data Alt a n = AAlt !(Pat n) !(Exp a n)
- data Pat n
- data Cast a n
- = CastWeakenEffect !(Effect n)
- | CastPurify !(Witness a n)
- | CastBox
- | CastRun
- data Witness a n
- data DaCon n
- data WiCon n = WiConBound !(Bound n) !(Type n)
- module DDC.Type.Predicates
- isXVar :: Exp a n -> Bool
- isXCon :: Exp a n -> Bool
- isAtomX :: Exp a n -> Bool
- isAtomW :: Witness a n -> Bool
- isXLAM :: Exp a n -> Bool
- isXLam :: Exp a n -> Bool
- isLambdaX :: Exp a n -> Bool
- isXApp :: Exp a n -> Bool
- isXCast :: Exp a n -> Bool
- isXCastBox :: Exp a n -> Bool
- isXCastRun :: Exp a n -> Bool
- isXLet :: Exp a n -> Bool
- isPDefault :: Pat n -> Bool
- isXType :: Exp a n -> Bool
- isXWitness :: Exp a n -> Bool
- module DDC.Type.Compounds
- annotOfExp :: Exp a n -> a
- mapAnnotOfExp :: (a -> a) -> Exp a n -> Exp a n
- xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n
- xLams :: a -> [Bind n] -> Exp a n -> Exp a n
- makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n
- takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)
- takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)
- takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)
- data Param n
- = ParamType (Bind n)
- | ParamValue (Bind n)
- | ParamBox
- takeXLamParam :: Exp a n -> Maybe ([Param n], Exp a n)
- xApps :: a -> Exp a n -> [Exp a n] -> Exp a n
- makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n
- takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])
- takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])
- takeXAppsAsList :: Exp a n -> [Exp a n]
- takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])
- takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])
- takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])
- xLets :: a -> [Lets a n] -> Exp a n -> Exp a n
- xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a n
- splitXLets :: Exp a n -> ([Lets a n], Exp a n)
- splitXLetsAnnot :: Exp a n -> ([(Lets a n, a)], Exp a n)
- bindsOfLets :: Lets a n -> ([Bind n], [Bind n])
- specBindsOfLets :: Lets a n -> [Bind n]
- valwitBindsOfLets :: Lets a n -> [Bind n]
- patOfAlt :: Alt a n -> Pat n
- takeCtorNameOfAlt :: Alt a n -> Maybe n
- bindsOfPat :: Pat n -> [Bind n]
- makeRuns :: a -> Int -> Exp a n -> Exp a n
- wApp :: a -> Witness a n -> Witness a n -> Witness a n
- wApps :: a -> Witness a n -> [Witness a n] -> Witness a n
- annotOfWitness :: Witness a n -> a
- takeXWitness :: Exp a n -> Maybe (Witness a n)
- takeWAppsAsList :: Witness a n -> [Witness a n]
- takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])
- takeXType :: Exp a n -> Maybe (Type n)
- xUnit :: a -> Exp a n
- dcUnit :: DaCon n
- takeNameOfDaCon :: DaCon n -> Maybe n
- takeTypeOfDaCon :: DaCon n -> Maybe (Type n)
Abstract Syntax
module DDC.Type.Exp
Expressions
Well-typed expressions have types of kind Data
.
XVar !a !(Bound n) | Value variable or primitive operation. |
XCon !a !(DaCon n) | Data constructor or literal. |
XLAM !a !(Bind n) !(Exp a n) | Type abstraction (level-1). |
XLam !a !(Bind n) !(Exp a n) | Value and Witness abstraction (level-0). |
XApp !a !(Exp a n) !(Exp a n) | Application. |
XLet !a !(Lets a n) !(Exp a n) | Possibly recursive bindings. |
XCase !a !(Exp a n) ![Alt a n] | Case branching. |
XCast !a !(Cast a n) !(Exp a n) | Type cast. |
XType !a !(Type n) | Type can appear as the argument of an application. |
XWitness !a !(Witness a n) | Witness can appear as the argument of an application. |
Reannotate Exp Source | |
Complies Exp Source | |
SubstituteWX Exp Source | |
SubstituteXX Exp Source | |
Annotate Exp Exp Source | |
Deannotate Exp Exp Source | |
SpreadX (Exp a) Source | |
SupportX (Exp a) Source | |
SubstituteTX (Exp a) Source | |
MapBoundX (Exp a) n Source | |
(Eq a, Eq n) => Eq (Exp a n) Source | |
(Show a, Show n) => Show (Exp a n) Source | |
(NFData a, NFData n) => NFData (Exp a n) Source | |
data PrettyMode (Exp a n) = PrettyModeExp {
|
Possibly recursive bindings.
LLet !(Bind n) !(Exp a n) | Non-recursive expression binding. |
LRec ![(Bind n, Exp a n)] | Recursive binding of lambda abstractions. |
LPrivate ![Bind n] !(Maybe (Type n)) ![Bind n] | Bind a private region variable, and witnesses to its properties. |
Reannotate Lets Source | |
Annotate Lets Lets Source | |
Deannotate Lets Lets Source | |
SpreadX (Lets a) Source | |
SupportX (Lets a) Source | |
(Eq a, Eq n) => Eq (Lets a n) Source | |
(Show a, Show n) => Show (Lets a n) Source | |
(NFData a, NFData n) => NFData (Lets a n) Source | |
data PrettyMode (Lets a n) = PrettyModeLets {
|
Case alternatives.
Reannotate Alt Source | |
Complies Alt Source | |
SubstituteWX Alt Source | |
SubstituteXX Alt Source | |
Annotate Alt Alt Source | |
Deannotate Alt Alt Source | |
SpreadX (Alt a) Source | |
SupportX (Alt a) Source | |
SubstituteTX (Alt a) Source | |
MapBoundX (Alt a) n Source | |
(Eq a, Eq n) => Eq (Alt a n) Source | |
(Show a, Show n) => Show (Alt a n) Source | |
(NFData a, NFData n) => NFData (Alt a n) Source | |
data PrettyMode (Alt a n) = PrettyModeAlt {
|
Pattern matching.
Type casts.
CastWeakenEffect !(Effect n) | Weaken the effect of an expression. The given effect is added to the effect of the body. |
CastPurify !(Witness a n) | Purify the effect (action) of an expression. |
CastBox | Box up a computation, capturing its effects in the S computation type. |
CastRun | Run a computation, releasing its effects into the environment. |
Reannotate Cast Source | |
SubstituteWX Cast Source | |
SubstituteXX Cast Source | |
Annotate Cast Cast Source | |
Deannotate Cast Cast Source | |
SpreadX (Cast a) Source | |
SupportX (Cast a) Source | |
SubstituteTX (Cast a) Source | |
MapBoundX (Cast a) n Source | |
(Eq a, Eq n) => Eq (Cast a n) Source | |
(Show a, Show n) => Show (Cast a n) Source | |
(NFData a, NFData n) => NFData (Cast a n) Source |
Witnesses
When a witness exists in the program it guarantees that a certain property of the program is true.
WVar a !(Bound n) | Witness variable. |
WCon a !(WiCon n) | Witness constructor. |
WApp a !(Witness a n) !(Witness a n) | Witness application. |
WType a !(Type n) | Type can appear as the argument of an application. |
Reannotate Witness Source | |
SubstituteWX Witness Source | |
Annotate Witness Witness Source | |
Deannotate Witness Witness Source | |
SpreadX (Witness a) Source | |
SupportX (Witness a) Source | |
SubstituteTX (Witness a) Source | |
MapBoundX (Witness a) n Source | |
(Eq a, Eq n) => Eq (Witness a n) Source | |
(Show a, Show n) => Show (Witness a n) Source | |
(NFData a, NFData n) => NFData (Witness a n) Source |
Data Constructors
Data constructors.
DaConUnit | Baked in unit data constructor. |
DaConPrim | Primitive data constructor used for literals and baked-in constructors. The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor. |
DaConBound | Data constructor that has a data type declaration. |
|
Witness Constructors
Witness constructors.
WiConBound !(Bound n) !(Type n) | Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed. |
Predicates
module DDC.Type.Predicates
Atoms
Lambdas
isXLam :: Exp a n -> Bool Source
Check whether an expression is a value or witness abstraction (level-0).
isLambdaX :: Exp a n -> Bool Source
Check whether an expression is a spec, value, or witness abstraction.
Applications
Cast
isXCastBox :: Exp a n -> Bool Source
Check whether this is a box cast.
isXCastRun :: Exp a n -> Bool Source
Check whether this is a run cast.
Let bindings
Patterns
isPDefault :: Pat n -> Bool Source
Check whether an alternative is a PDefault
.
Types and Witnesses
isXWitness :: Exp a n -> Bool Source
Check whether an expression is an XWitness
.
Compounds
module DDC.Type.Compounds
Annotations
annotOfExp :: Exp a n -> a Source
Take the outermost annotation from an expression.
mapAnnotOfExp :: (a -> a) -> Exp a n -> Exp a n Source
Apply a function to the annotation of an expression.
Lambdas
makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n 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 :: Exp a n -> Maybe ([Bind n], Exp a n) Source
Split type lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n) Source
Split nested value or witness lambdas from the front of an expression,
or Nothing
if there aren't any.
takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n) 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.
Parameters of a function.
ParamType (Bind n) | |
ParamValue (Bind n) | |
ParamBox |
Applications
makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n Source
takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n]) Source
Flatten an application into the function part and its arguments.
Returns Nothing
if there is no outer application.
takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n]) 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 :: Exp a n -> [Exp a n] Source
Flatten an application into the function parts and arguments, if any.
takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)]) Source
Destruct sequence of applications.
Similar to takeXAppsAsList
but also keeps annotations for later.
takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n]) 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 :: Exp a n -> Maybe (n, [Exp a n]) Source
Flatten an application of a primop into the variable and its arguments.
Returns Nothing
if the expression isn't a primop application.
Lets
xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a n Source
Wrap some let-bindings around an expression, with individual annotations.
splitXLets :: Exp a n -> ([Lets a n], Exp a n) Source
Split let-bindings from the front of an expression, if any.
splitXLetsAnnot :: Exp a n -> ([(Lets a n, a)], Exp a n) Source
Split let-bindings from the front of an expression, with annotations.
bindsOfLets :: Lets a n -> ([Bind n], [Bind n]) Source
Take the binds of a Lets
.
The level-1 and level-0 binders are returned separately.
specBindsOfLets :: Lets a n -> [Bind n] Source
Like bindsOfLets
but only take the spec (level-1) binders.
valwitBindsOfLets :: Lets a n -> [Bind n] Source
Like bindsOfLets
but only take the value and witness (level-0) binders.
Alternatives
takeCtorNameOfAlt :: Alt a n -> Maybe n Source
Take the constructor name of an alternative, if there is one.
Patterns
bindsOfPat :: Pat n -> [Bind n] Source
Take the binds of a Pat
.
Casts
makeRuns :: a -> Int -> Exp a n -> Exp a n Source
Wrap an expression in the given number of run
casts.
Witnesses
wApps :: a -> Witness a n -> [Witness a n] -> Witness a n Source
Construct a sequence of witness applications
annotOfWitness :: Witness a n -> a Source
Take the annotation from a witness.
takeXWitness :: Exp a n -> Maybe (Witness a n) Source
Take the witness from an XWitness
argument, if any.
takeWAppsAsList :: Witness a n -> [Witness a n] Source
Flatten an application into the function parts and arguments, if any.
takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n]) Source
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.
Types
Data Constructors
takeNameOfDaCon :: DaCon n -> Maybe n Source
Take the name of data constructor, if there is one.
takeTypeOfDaCon :: DaCon n -> Maybe (Type n) Source
Take the type annotation of a data constructor, if we know it locally.