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 t
- data WiCon n = WiConBound !(Bound n) !(Type n)
- module DDC.Type.Exp.Simple.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.Exp.Simple.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 (Type 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 t
- takeNameOfDaCon :: DaCon n t -> Maybe n
- takeTypeOfDaCon :: DaCon n (Type 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 (Type 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 # | |
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) Source # | |
Possibly recursive bindings.
Case alternatives.
Reannotate Alt Source # | |
Complies Alt Source # | |
SubstituteWX Alt Source # | |
SubstituteXX 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) Source # | |
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 # | |
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 # | |
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
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
Types and Witnesses
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
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 (Type 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
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 t -> Maybe n Source #
Take the name of data constructor, if there is one.