Safe Haskell	Safe
Language	Haskell98

DDC.Core.Exp.Annot.Exp

Contents

Expressions
Witnesses
Data Constructors
Witness Constructors

Description

Core language AST that includes an annotation on every node of an expression.

This is the default representation for Disciple Core, and should be preferred over the Simple version of the AST in most cases.

Local transformations on this AST should propagate the annotations in a way that would make sense if they were source position identifiers that tracked the provenance of each code snippet. If the specific annotations attached to the AST would not make sense after such a transformation, then the client should erase them to () beforehand using the reannotate transform.
Global transformations that drastically change the provenance of code snippets should accept an AST with an arbitrary annotation type, but produce one with the annotations set to ().

Synopsis

Documentation

module DDC.Type.Exp

Expressions

data Exp a n Source

Well-typed expressions have types of kind Data.

Constructors

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.

Instances

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 { modeExpLets :: PrettyMode (Lets a n) modeExpAlt :: PrettyMode (Alt a n) modeExpVarTypes :: Bool modeExpConTypes :: Bool modeExpUseLetCase :: Bool }

data Lets a n Source

Possibly recursive bindings.

Constructors

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.

Instances

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 { modeLetsExp :: PrettyMode (Exp a n) modeLetsSuppressTypes :: Bool }

data Alt a n Source

Case alternatives.

Constructors

AAlt !(Pat n) !(Exp a n)

Instances

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 { modeAltExp :: PrettyMode (Exp a n) }

data Pat n Source

Pattern matching.

Constructors

PDefault	The default pattern always succeeds.
PData !(DaCon n) ![Bind n]	Match a data constructor and bind its arguments.

Instances

SpreadX Pat Source
Eq n => Eq (Pat n) Source
Show n => Show (Pat n) Source
NFData n => NFData (Pat n) Source

data Cast a n Source

Type casts.

Constructors

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.

Instances

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

data Witness a n Source

When a witness exists in the program it guarantees that a certain property of the program is true.

Constructors

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.

Instances

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 DaCon n Source

Data constructors.

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.
Fields daConName :: !n Name of the data constructor. daConType :: !(Type n) Type of the data constructor.
DaConBound	Data constructor that has a data type declaration.
Fields daConName :: !n Name of the data constructor.

Instances

SpreadX DaCon Source
Eq n => Eq (DaCon n) Source
Show n => Show (DaCon n) Source
NFData n => NFData (DaCon n) Source

Witness Constructors

data WiCon n Source

Witness constructors.

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.

Instances

SpreadX WiCon Source
Eq n => Eq (WiCon n) Source
Show n => Show (WiCon n) Source
NFData n => NFData (WiCon n) Source