DDC.Core.Exp.Generic.Exp

Generic expression representation.

Documentation

type family GAnnot l

Type functions associated with a language definition.

These produce the types used for annotations, bindings, bound occurrences and primitives for that language.

type family GBind l

type family GBound l

type family GPrim l

data GExp l

Generic expression representation.

Constructors

XAnnot !(GAnnot l) !(GExp l)

An annotated expression.

XPrim !(GPrim l)

Primitive operator or literal.

XCon !(DaCon l)

Data constructor.

XVar !(GBound l)

Value or Witness variable (level-0).

XAbs !(GAbs l) !(GExp l)

Function abstraction.

XApp !(GExp l) !(GArg l)

Function application.

XLet !(GLets l) !(GExp l)

Possibly recursive bindings.

XCase !(GExp l) ![GAlt l]

Case branching.

XCast !(GCast l) !(GExp l)

Type casting.

Instances

ShowLanguage l => Show (GExp l)

data PrettyMode (GExp l) = PrettyModeExp {

• modeExpArg :: PrettyMode (GArg l)
• modeExpLets :: PrettyMode (GLets l)
• modeExpAlt :: PrettyMode (GAlt l)
• modeExpUseLetCase :: Bool

}

data GAbs l

Abstractions.

This indicates what sort of object is being abstracted over in an XAbs.

Constructors

ALAM !(GBind l)

Level-1 abstraction (spec)

ALam !(GBind l)

Level-0 abstraction (value and witness)

Instances

ShowLanguage l => Show (GAbs l)

pattern XLAM :: GBind t -> GExp t -> GExp t

pattern XLam :: GBind t -> GExp t -> GExp t

data GArg l

Arguments.

Carries an argument that can be supplied to a function.

Constructors

RType !(Type l)

Type argument.

RExp !(GExp l)

Value argument.

RWitness !(GWitness l)

Witness argument.

Instances

ShowLanguage l => Show (GArg l)

data PrettyMode (GArg l) = PrettyModeArg {

• modeArgExp :: PrettyMode (GExp l)

}

data GLets l

Possibly recursive bindings.

Constructors

LLet !(GBind l) !(GExp l)

Non-recursive binding.

LRec ![(GBind l, GExp l)]

Recursive binding.

LPrivate ![GBind l] !(Maybe (Type l)) ![GBind l]

Introduce a private region variable and witnesses to its properties.

Instances

ShowLanguage l => Show (GLets l)

data PrettyMode (GLets l) = PrettyModeLets {

• modeLetsExp :: PrettyMode (GExp l)

}

data GAlt l

Case alternatives.

Constructors

AAlt !(GPat l) !(GExp l)

Instances

ShowLanguage l => Show (GAlt l)

data PrettyMode (GAlt l) = PrettyModeAlt {

• modeAltExp :: PrettyMode (GExp l)

}

data GPat l

Patterns.

Constructors

PDefault

The default pattern always succeeds.

PData !(DaCon l) ![GBind l]

Match a data constructor and bind its arguments.

Instances

ShowLanguage l => Show (GPat l)

data GCast l

Type casts.

Constructors

CastWeakenEffect !(Type l)

Weaken the effect of an expression.

CastPurify !(GWitness l)

Purify the effect of an expression.

CastBox

Box up a computation, suspending its evaluation and capturing its effects in the S computaiton type.

CastRun

Run a computation, releasing its effects into the context.

Instances

ShowLanguage l => Show (GCast l)

data GWitness l

Witnesses.

Constructors

WVar !(GBound l)

Witness variable.

WCon !(GWiCon l)

Witness constructor.

WApp !(GWitness l) !(GWitness l)

Witness application.

WType !(Type l)

Type can appear as an argument of a witness application.

Instances

ShowLanguage l => Show (GWitness l)

data GWiCon l

Witness constructors.

Constructors

WiConBound !(GBound l) !(Type l)

Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed.

Instances

ShowLanguage l => Show (GWiCon l)

type ShowLanguage l = (Show l, Show (GAnnot l), Show (GBind l), Show (GBound l), Show (GPrim l))

Synonym for Show constraints of all language types.