ddc-core-0.2.1.2: Disciple Core language and type checker.

Safe HaskellSafe-Inferred

DDC.Core.Exp

Contents

Description

Abstract syntax for the Disciple core language.

Synopsis

Documentation

module DDC.Type.Exp

Computation expressions

data Exp a n Source

Well-typed expressions live in the Data universe, and their types always have kind *.

Expressions do something useful at runtime, and might diverge or cause side effects.

Constructors

XVar a (Bound n)

Value variable or primitive operation.

XCon a (Bound 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 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

SubstituteXX Exp 
BindStruct (Exp a) 
LiftW (Exp a) 
LiftX (Exp a) 
SubstituteTX (Exp a) 
SubstituteWX (Exp a) 
SpreadX (Exp a) 
(Eq a, Eq n) => Eq (Exp a n) 
(Show a, Show n) => Show (Exp a n) 
(Pretty n, Eq n) => Pretty (Exp a n) 

data Cast n Source

Type casts.

Constructors

CastWeakenEffect (Effect n)

Weaken the effect of an expression.

CastWeakenClosure (Closure n)

Weaken the closure of an expression.

CastPurify (Witness n)

Purify the effect of an expression.

CastForget (Witness n)

Hide sharing of the closure of an expression.

Instances

BindStruct Cast 
Rewrite Cast 
SubstituteTX Cast 
SubstituteWX Cast 
SpreadX Cast 
Eq n => Eq (Cast n) 
Show n => Show (Cast n) 
(Pretty n, Eq n) => Pretty (Cast n) 

data Lets a n Source

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.

LLetRegion (Bind n) [Bind n]

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

LWithRegion (Bound n)

Holds a region handle during evaluation.

Instances

SpreadX (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) 

data LetMode n Source

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

data Alt a n Source

Case alternatives.

Constructors

AAlt (Pat n) (Exp a n) 

Instances

SubstituteXX Alt 
BindStruct (Alt a) 
LiftW (Alt a) 
LiftX (Alt a) 
SubstituteTX (Alt a) 
SubstituteWX (Alt a) 
SpreadX (Alt a) 
(Eq a, Eq n) => Eq (Alt a n) 
(Show a, Show n) => Show (Alt a n) 
(Pretty n, Eq n) => Pretty (Alt a n) 

data Pat n Source

Pattern matching.

Constructors

PDefault

The default pattern always succeeds.

PData (Bound 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) 

Witnesses expressions

data Witness n Source

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

data WiCon n Source

Witness constructors.

Constructors

WiConBuiltin WbCon

Witness constructors baked into the language.

WiConBound (Bound n)

Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities.

Instances

SpreadX WiCon 
Eq n => Eq (WiCon n) 
Show n => Show (WiCon n) 
(Pretty n, Eq n) => Pretty (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