DDC.Core.Exp.Generic

Abstract Syntax

Expressions

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 term expression representation.

Constructors

XAnnot !(GAnnot l) !(GExp l)

An annotated expression.

XPrim !(GPrim l)

Primitive operator or literal.

XCon !(DaCon l (Type 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)

Methods

showsPrec :: Int -> GExp l -> ShowS

show :: GExp l -> String

showList :: [GExp l] -> ShowS

data PrettyMode (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)

Methods

showsPrec :: Int -> GAbs l -> ShowS

show :: GAbs l -> String

showList :: [GAbs l] -> ShowS

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)

Methods

showsPrec :: Int -> GArg l -> ShowS

show :: GArg l -> String

showList :: [GArg l] -> ShowS

data PrettyMode (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)

Methods

showsPrec :: Int -> GLets l -> ShowS

show :: GLets l -> String

showList :: [GLets l] -> ShowS

data PrettyMode (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)

Methods

showsPrec :: Int -> GAlt l -> ShowS

show :: GAlt l -> String

showList :: [GAlt l] -> ShowS

data PrettyMode (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 (Type l)) ![GBind l]

Match a data constructor and bind its arguments.

Instances

ShowLanguage l => Show (GPat l)

Methods

showsPrec :: Int -> GPat l -> ShowS

show :: GPat l -> String

showList :: [GPat l] -> ShowS

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)

Methods

showsPrec :: Int -> GCast l -> ShowS

show :: GCast l -> String

showList :: [GCast l] -> ShowS

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)

Methods

showsPrec :: Int -> GWitness l -> ShowS

show :: GWitness l -> String

showList :: [GWitness l] -> ShowS

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)

Methods

showsPrec :: Int -> GWiCon l -> ShowS

show :: GWiCon l -> String

showList :: [GWiCon l] -> ShowS

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

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

Predicates

module DDC.Type.Exp.Simple.Predicates

Atoms

isXVar :: GExp l -> Bool

Check whether an expression is a variable.

isXCon :: GExp l -> Bool

Check whether an expression is a constructor.

isAtomX :: GExp l -> Bool

Check whether an expression is an atomic value, eg an XVar, XCon, or XPrim.

isAtomR :: GArg l -> Bool

Check whether an argument is an atomic value,

isAtomW :: GWitness l -> Bool

Check whether a witness is a WVar or WCon.

Abstractions

isXAbs :: GExp l -> Bool

Check whether an expression is an abstraction.

isXLAM :: GExp l -> Bool

Check whether an expression is a spec abstraction (level-1).

isXLam :: GExp l -> Bool

Check whether an expression is a value or witness abstraction (level-0).

Applications

isXApp :: GExp l -> Bool

Check whether an expression is an XApp.

Let bindings

isXLet :: GExp l -> Bool

Check whether an expression is a XLet.

Patterns

isPDefault :: GPat l -> Bool

Check whether an alternative is a PDefault.

Compounds

module DDC.Type.Exp.Simple.Compounds

Abstractions

makeXAbs :: [GAbs l] -> GExp l -> GExp l

Make some nested abstractions.

takeXAbs :: GExp l -> Maybe ([GAbs l], GExp l)

Split type and value/witness abstractions from the front of an expression, or Nothing if there aren't any.

makeXLAMs :: [GBind l] -> GExp l -> GExp l

Make some nested type lambdas.

takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l)

Split type lambdas from the front of an expression, or Nothing if there aren't any.

makeXLams :: [GBind l] -> GExp l -> GExp l

Make some nested value or witness lambdas.

takeXLams :: GExp l -> Maybe ([GBind l], GExp l)

Split nested value or witness lambdas from the front of an expression, or Nothing if there aren't any.

Applications

makeXApps :: GExp l -> [GArg l] -> GExp l

Build sequence of applications.

takeXApps :: GExp l -> Maybe (GExp l, [GArg l])

Flatten an application into the functional expression and its arguments, or `Nothing if this is not an application.

splitXApps :: GExp l -> (GExp l, [GArg l])

Flatten an application into a functional expression and its arguments, or just return the expression with no arguments if this is not an application.

takeXConApps :: GExp l -> Maybe (DaCon l (Type l), [GArg l])

Flatten an application of a data constructor into the constructor itself and its arguments, or Nothing if this is not an application of a data constructor.

takeXPrimApps :: GExp l -> Maybe (GPrim l, [GArg l])

Flatten an application of a primitive operators into the operator itself and its arguments, or Nothing if this is not an application of a primitive.

Data Constructors

dcUnit :: DaCon n t

The unit data constructor.

takeNameOfDaCon :: DaCon n t -> Maybe n

Take the name of data constructor, if there is one.

takeTypeOfDaCon :: DaCon n (Type n) -> Maybe (Type n)

Take the type annotation of a data constructor, if we know it locally.

Dictionaries

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.