DDC.Core.Exp

Abstract syntax for the Disciple core language.

Documentation

module DDC.Type.Exp

Computation expressions

data Exp a n

Well-typed expressions produce Data values when evaluated, and their types aways have 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 !(Type n)

Type can appear as the argument of an application.

XWitness !(Witness n)

Witness can appear as the argument of an application.

Instances

Reannotate Exp

SubstituteXX Exp

Complies Exp

BindStruct (Exp a)

SpreadX (Exp a)

SupportX (Exp a)

SubstituteTX (Exp a)

SubstituteWX (Exp a)

Ord n => MapBoundT (Exp a) n

MapBoundX (Exp a) n

(Eq a, Eq n) => Eq (Exp a n)

(Show a, Show n) => Show (Exp a n)

(Pretty n, Eq n) => Pretty (Exp a n)

(NFData a, NFData n) => NFData (Exp a n)

data DaCon n

Data constructors.

Constructors

DaCon

Fields

daConName :: !(DaConName n)

Name of the data constructor.

daConType :: !(Type n)

Type of the data constructor. The type must be closed.

daConIsAlgebraic :: !Bool

Algebraic constructors can be deconstructed with case-expressions, and must have a data type declaration.

Non-algebraic types like Float can't be inspected with case-expressions.

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)

data DaConName n

Data constructor names.

Constructors

DaConUnit

The unit data constructor is builtin.

DaConNamed n

Data constructor name defined by the client.

Instances

Eq n => Eq (DaConName n)

Show n => Show (DaConName n)

NFData n => NFData (DaConName n)

data Cast a n

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 n)

Purify the effect (action) of an expression.

CastForget !(Witness n)

Forget about the closure (sharing) of an expression.

Instances

Reannotate Cast

SubstituteXX Cast

BindStruct (Cast a)

SpreadX (Cast a)

SupportX (Cast a)

SubstituteTX (Cast a)

SubstituteWX (Cast a)

Ord n => MapBoundT (Cast a) n

MapBoundX (Cast a) n

(Eq a, Eq n) => Eq (Cast a n)

(Show a, Show n) => Show (Cast a n)

(Pretty n, Eq n) => Pretty (Cast a n)

(NFData a, NFData n) => NFData (Cast a n)

data Lets a n

Possibly recursive bindings.

Constructors

LLet !(LetMode n) !(Bind n) !(Exp a n)

Non-recursive expression binding.

LRec ![(Bind n, Exp a n)]

Recursive binding of lambda abstractions.

LLetRegions ![Bind n] ![Bind n]

Bind a local region variable, and witnesses to its properties.

LWithRegion !(Bound n)

Holds a region handle during evaluation.

Instances

Reannotate Lets

SpreadX (Lets a)

SupportX (Lets a)

(Eq a, Eq n) => Eq (Lets a n)

(Show a, Show n) => Show (Lets a n)

(Pretty n, Eq n) => Pretty (Lets a n)

(NFData a, NFData n) => NFData (Lets a n)

data LetMode n

Describes how a let binding should be evaluated.

Constructors

LetStrict

Evaluate binding before substituting the result.

LetLazy !(Maybe (Witness n))

Use lazy evaluation. The witness shows that the head region of the bound expression can contain thunks (is lazy), or Nothing if there is no head region.

Instances

Rename LetMode

BindStruct LetMode

SpreadX LetMode

SupportX LetMode

SubstituteTX LetMode

SubstituteWX LetMode

Ord n => MapBoundT LetMode n

MapBoundX LetMode n

Eq n => Eq (LetMode n)

Show n => Show (LetMode n)

(Pretty n, Eq n) => Pretty (LetMode n)

NFData n => NFData (LetMode n)

data Alt a n

Case alternatives.

Constructors

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

Instances

Reannotate Alt

SubstituteXX Alt

Complies Alt

BindStruct (Alt a)

SpreadX (Alt a)

SupportX (Alt a)

SubstituteTX (Alt a)

SubstituteWX (Alt a)

Ord n => MapBoundT (Alt a) n

MapBoundX (Alt a) n

(Eq a, Eq n) => Eq (Alt a n)

(Show a, Show n) => Show (Alt a n)

(Pretty n, Eq n) => Pretty (Alt a n)

(NFData a, NFData n) => NFData (Alt a n)

data Pat n

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 expressions

data Witness n

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

Constructors

WVar !(Bound n)

Witness variable.

WCon !(WiCon n)

Witness constructor.

WApp !(Witness n) !(Witness n)

Witness application.

WJoin !(Witness n) !(Witness n)

Joining of witnesses.

WType !(Type n)

Type can appear as the argument of an application.

Instances

Rename Witness

BindStruct Witness

SpreadX Witness

SupportX Witness

SubstituteTX Witness

SubstituteWX Witness

Ord n => MapBoundT Witness n

MapBoundX Witness n

Eq n => Eq (Witness n)

Show n => Show (Witness n)

(Pretty n, Eq n) => Pretty (Witness n)

NFData n => NFData (Witness n)

data WiCon n

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

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