Safe Haskell	Safe-Inferred

DDC.Core.Exp.Simple

Contents

Expressions
Witnesses
Data Constructors
Witness Constructors

Description

Core language AST with a separate node to hold annotations.

This version of the AST is used when generating code where most or all of the annotations would be empty. General purpose transformations should deal with the fully annotated version of the AST instead.

Synopsis

Documentation

module DDC.Type.Exp

Expressions

data Exp a n Source

Well-typed expressions have types of kind Data.

Constructors

XAnnot a (Exp a n)	Annotation.
XVar !(Bound n)	Value variable or primitive operation.
XCon !(DaCon n)	Data constructor or literal.
XLAM !(Bind n) !(Exp a n)	Type abstraction (level-1).
XLam !(Bind n) !(Exp a n)	Value and Witness abstraction (level-0).
XApp !(Exp a n) !(Exp a n)	Application.
XLet !(Lets a n) !(Exp a n)	Possibly recursive bindings.
XCase !(Exp a n) ![Alt a n]	Case branching.
XCast !(Cast a n) !(Exp a n)	Type cast.
XType !(Type n)	Type can appear as the argument of an application.
XWitness !(Witness a n)	Witness can appear as the argument of an application.

Instances

Annotate Exp Exp
Deannotate Exp Exp
BindStruct (Exp a)
(Eq a, Eq n) => Eq (Exp a n)
(Show a, Show n) => Show (Exp a n)
(NFData a, NFData n) => NFData (Exp a n)

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.
CastWeakenClosure ![Exp a n]	Weaken the closure of an expression. The closures of these expressions are added to the closure of the body.
CastPurify !(Witness a n)	Purify the effect (action) of an expression.
CastForget !(Witness a n)	Forget about the closure (sharing) 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

Annotate Cast Cast
Deannotate Cast Cast
BindStruct (Cast a)
(Eq a, Eq n) => Eq (Cast a n)
(Show a, Show n) => Show (Cast a n)
(NFData a, NFData n) => NFData (Cast a n)

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 local region variable, and witnesses to its properties.
LWithRegion !(Bound n)	Holds a region handle during evaluation.

Instances

Annotate Lets Lets
Deannotate Lets Lets
(Eq a, Eq n) => Eq (Lets a n)
(Show a, Show n) => Show (Lets a n)
(NFData a, NFData n) => NFData (Lets a n)

data Alt a n Source

Case alternatives.

Constructors

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

Instances

Annotate Alt Alt
Deannotate Alt Alt
BindStruct (Alt a)
(Eq a, Eq n) => Eq (Alt a n)
(Show a, Show n) => Show (Alt a n)
(NFData a, NFData n) => NFData (Alt 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
Eq n => Eq (Pat n)
Show n => Show (Pat n)
(Pretty n, Eq n) => Pretty (Pat n)
NFData n => NFData (Pat n)

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

WAnnot a (Witness a n)
WVar !(Bound n)	Witness variable.
WCon !(WiCon n)	Witness constructor.
WApp !(Witness a n) !(Witness a n)	Witness application.
WJoin !(Witness a n) !(Witness a n)	Joining of witnesses.
WType !(Type n)	Type can appear as the argument of an application.

Instances

Annotate Witness Witness
Deannotate Witness Witness
BindStruct (Witness a)
(Eq a, Eq n) => Eq (Witness a n)
(Show a, Show n) => Show (Witness a n)
(NFData a, NFData n) => NFData (Witness a n)

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. 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. Name of the data constructor.

Instances

SpreadX DaCon
Eq n => Eq (DaCon n)
Show n => Show (DaCon n)
(Pretty n, Eq n) => Pretty (DaCon n)
NFData n => NFData (DaCon n)

Witness Constructors

data WiCon n Source

Witness constructors.

Constructors

WiConBuiltin !WbCon	Witness constructors baked into the language.
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
Eq n => Eq (WiCon n)
Show n => Show (WiCon n)
(Pretty n, Eq n) => Pretty (WiCon n)
NFData n => NFData (WiCon n)

data WbCon Source

Built-in witness constructors.

These are used to convert a runtime capability into a witness that the corresponding property is true.

Constructors

WbConPure	(axiom) The pure effect is pure. pure :: Pure !0
WbConEmpty	(axiom) The empty closure is empty. empty :: Empty $0
WbConUse	Convert a capability guaranteeing that a region is in the global heap, into a witness that a closure using this region is empty. This lets us rely on the garbage collector to reclaim objects in the region. It is needed when we suspend the evaluation of expressions that have a region in their closure, because the type of the returned thunk may not reveal that it references objects in that region. use :: [r : %]. Global r => Empty (Use r)
WbConRead	Convert a capability guaranteeing the constancy of a region, into a witness that a read from that region is pure. This lets us suspend applications that read constant objects, because it doesn't matter if the read is delayed, we'll always get the same result. read :: [r : %]. Const r => Pure (Read r)
WbConAlloc	Convert a capability guaranteeing the constancy of a region, into a witness that allocation into that region is pure. This lets us increase the sharing of constant objects, because we can't tell constant objects of the same value apart. alloc :: [r : %]. Const r => Pure (Alloc r)

Instances

Eq WbCon
Show WbCon
Pretty WbCon
NFData WbCon