Language.SequentCore.Syntax

Documentation

The AST for Sequent Core, with translations to and from GHC Core.

data Value b

An atomic value. These include literals, lambdas, and variables, as well as types and coercions (see GHC's Expr for the reasoning).

Constructors

Lit Literal

A primitive literal value.

Lam b (Command b)

A function. The body is a computation, that is, a Command.

Type Type

A type. Used to pass a type as an argument to a type-level lambda.

Coercion Coercion

A coercion. Used to pass evidence to the cast operation.

Var Var

A variable.

Instances

OutputableBndr b => Outputable (Value b)

data Frame b

A stack frame. A continuation is simply a list of these. Each represents the outer part of a Haskell expression, with a "hole" where a value can be placed. Computation in the sequent calculus is expressed as the interation of a value with a continuation.

Constructors

App (Command b)

Apply the value to an argument, which may be a computation.

Case b Type [Alt b]

Perform case analysis on the value.

Cast Coercion

Cast the value using the given proof.

Tick (Tickish Id)

Annotate the enclosed frame. Used by the profiler.

Instances

OutputableBndr b => Outputable (Frame b)

type Cont b = [Frame b]

A continuation, expressed as a list of Frames. In terms of the sequent calculus, here nil stands for a free covariable; since Haskell does not allow for control effects, we only allow for one covariable.

data Command b

A general computation. A command brings together a list of bindings, some value, and a continuation saying what to do with that value. The value and continuation comprise a cut in the sequent calculus.

Constructors

Command

Fields

cmdLet :: [Bind b]

Bindings surrounding the computation.

cmdValue :: Value b

The value provided to the continuation.

cmdCont :: Cont b

What to do with the value.

Instances

OutputableBndr b => Outputable (Command b)

data Bind b

A binding. Similar to the Bind datatype from GHC. Can be either a single non-recursive binding or a mutually recursive block.

Constructors

NonRec b (Command b)

Rec [(b, Command b)]

Instances

OutputableBndr b => Outputable (Bind b)

data Alt b

Constructors

Alt AltCon [b] (Command b)

type SeqCoreValue = Value Var

type SeqCoreFrame = Frame Var

type SeqCoreCont = Cont Var

type SeqCoreCommand = Command Var

type SeqCoreBind = Bind Var

type SeqCoreAlt = Alt Var

fromCoreExpr :: Expr b -> Command b

fromCoreBind :: Bind b -> Bind b

fromCoreBinds :: [Bind b] -> [Bind b]

commandToCoreExpr :: Command b -> Expr b

valueToCoreExpr :: Value b -> Expr b

frameToCoreExpr :: Frame b -> Expr b -> Expr b

toCoreBind :: Bind b -> Bind b

toCoreBinds :: [Bind b] -> [Bind b]

toCoreAlt :: Alt b -> Alt b