DDC.Source.Tetra.Exp.Generic

Abstract syntax for Tetra Source expressions.

Classes

class HasAnonBind l where

Methods

isAnon :: l -> GBind l -> Bool

Instances

HasAnonBind (Annot a)

Expressions

type family GName l

Type functions associated with the language AST.

Instances

type GName (Annot a) = Name

type family GAnnot l

Instances

type GAnnot (Annot a) = a

type family GBind l

Instances

type GBind (Annot a) = Bind Name

type family GBound l

Instances

type GBound (Annot a) = Bound Name

type family GPrim l

Instances

type GPrim (Annot a) = PrimVal

data GExp l

Well-typed expressions have types of kind Data.

Constructors

XVar !(GAnnot l) !(GBound l)

Value variable or primitive operation.

XPrim !(GAnnot l) !(GPrim l)

Primitive values.

XCon !(GAnnot l) !(DaCon (GName l))

Data constructor or literal.

XLAM !(GAnnot l) !(GBind l) !(GExp l)

Type abstraction (level-1).

XLam !(GAnnot l) !(GBind l) !(GExp l)

Value and Witness abstraction (level-0).

XApp !(GAnnot l) !(GExp l) !(GExp l)

Application.

XLet !(GAnnot l) !(GLets l) !(GExp l)

A non-recursive let-binding.

XCase !(GAnnot l) !(GExp l) ![GAlt l]

Case branching.

XCast !(GAnnot l) !(GCast l) !(GExp l)

Type cast.

XType !(GAnnot l) !(Type (GName l))

Type can appear as the argument of an application.

XWitness !(GAnnot l) !(GWitness l)

Witness can appear as the argument of an application.

XDefix !(GAnnot l) [GExp l]

Some expressions and infix operators that need to be resolved into proper function applications.

XInfixOp !(GAnnot l) String

Use of a naked infix operator, like in 1 + 2. INVARIANT: only appears in the list of an XDefix node.

XInfixVar !(GAnnot l) String

Use of an infix operator as a plain variable, like in (+) 1 2. INVARIANT: only appears in the list of an XDefix node.

Instances

HasAnonBind l => MapBoundX GExp l

ExpandLanguage l => Expand GExp l

Defix GExp l

ShowLanguage l => Show (GExp l)

NFDataLanguage l => NFData (GExp l)

data GLets l

Possibly recursive bindings. Whether these are taken as recursive depends on whether they appear in an XLet or XLetrec group.

Constructors

LLet !(GBind l) !(GExp l)

Non-recursive expression binding.

LRec ![(GBind l, GExp l)]

Recursive binding of lambda abstractions.

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

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

LGroup ![GClause l]

A possibly recursive group of binding clauses.

Multiple clauses in the group may be part of the same function.

Instances

Defix GLets l

ShowLanguage l => Show (GLets l)

NFDataLanguage l => NFData (GLets l)

data GAlt l

Case alternatives.

Constructors

AAlt !(GPat l) ![GGuardedExp l]

Instances

HasAnonBind l => MapBoundX GAlt l

ExpandLanguage l => Expand GAlt l

Defix GAlt l

ShowLanguage l => Show (GAlt l)

NFDataLanguage l => NFData (GAlt l)

data GPat l

Patterns.

Constructors

PDefault

The default pattern always succeeds.

PData !(DaCon (GName l)) ![GBind l]

Match a data constructor and bind its arguments.

Instances

ShowLanguage l => Show (GPat l)

NFDataLanguage l => NFData (GPat l)

data GClause l

Binding clause

Constructors

SSig !(GAnnot l) !(GBind l) !(Type (GName l))

A separate type signature.

SLet !(GAnnot l) !(GBind l) ![GPat l] ![GGuardedExp l]

A function binding using pattern matching and guards.

Instances

HasAnonBind l => MapBoundX GClause l

Defix GClause l

ShowLanguage l => Show (GClause l)

NFDataLanguage l => NFData (GClause l)

data GGuardedExp l

An expression with some guards.

Constructors

GGuard !(GGuard l) !(GGuardedExp l)

GExp !(GExp l)

Instances

HasAnonBind l => MapBoundX GGuardedExp l

ExpandLanguage l => Expand GGuardedExp l

Defix GGuardedExp l

ShowLanguage l => Show (GGuardedExp l)

NFDataLanguage l => NFData (GGuardedExp l)

data GGuard l

Expression guards.

Constructors

GPat !(GPat l) !(GExp l)

GPred !(GExp l)

GDefault

Instances

HasAnonBind l => MapBoundX GGuard l

ExpandLanguage l => Expand GGuard l

Defix GGuard l

ShowLanguage l => Show (GGuard l)

NFDataLanguage l => NFData (GGuard l)

data GCast l

Type casts.

Constructors

CastWeakenEffect !(Effect (GName l))

Weaken the effect of an expression. The given effect is added to the effect of the body.

CastPurify !(GWitness l)

Purify the effect (action) of an expression.

CastBox

Box a computation, capturing its effects in the S computation type.

CastRun

Run a computation, releasing its effects into the environment.

Instances

HasAnonBind l => MapBoundX GCast l

ShowLanguage l => Show (GCast l)

NFDataLanguage l => NFData (GCast l)

data DaCon n :: * -> *

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

Eq n => Eq (DaCon n)

Show n => Show (DaCon n)

NFData n => NFData (DaCon n)

Witnesses

data GWitness l

Witnesses.

Constructors

WVar !(GAnnot l) !(GBound l)

Witness variable.

WCon !(GAnnot l) !(GWiCon l)

Witness constructor.

WApp !(GAnnot l) !(GWitness l) !(GWitness l)

Witness application.

WType !(GAnnot l) !(Type (GName l))

Type can appear as an argument of a witness application.

Instances

HasAnonBind l => MapBoundX GWitness l

ShowLanguage l => Show (GWitness l)

NFDataLanguage l => NFData (GWitness l)

data GWiCon l

Witness constructors.

Constructors

WiConBound !(GBound l) !(Type (GName 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)

NFDataLanguage l => NFData (GWiCon l)

Dictionaries

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

type NFDataLanguage l = (NFData l, NFData (GAnnot l), NFData (GName l), NFData (GBind l), NFData (GBound l), NFData (GPrim l))