Language.SequentCore.Syntax

The AST for Sequent Core, with basic operations.

AST Types

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.

Var Id

A term variable. Must not be a nullary constructor; use Cons for this.

Lam b (Command b)

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

Cons DataCon [Command b]

A value formed by a saturated constructor application.

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 for the cast operation to a lambda.

Instances

OutputableBndr b => Outputable (Value b)

HasId b => AlphaEq (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 interaction 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)

HasId b => AlphaEq (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.

Invariant: If cmdValue is a variable representing a constructor, then cmdCont must not begin with as many App frames as the constructor's arity. In other words, the command must not represent a saturated application of a constructor. Such an application should be represented by a Cons value instead. When in doubt, use mkCommand to enforce this invariant.

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)

HasId b => AlphaEq (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)

A single non-recursive binding.

Rec [(b, Command b)]

A block of mutually recursive bindings.

Instances

OutputableBndr b => Outputable (Bind b)

HasId b => AlphaEq (Bind b)

data Alt b

A case alternative. Given by the head constructor (or literal), a list of bound variables (empty for a literal), and the body as a Command.

Constructors

Alt AltCon [b] (Command b)

Instances

OutputableBndr b => Outputable (Alt b)

HasId b => AlphaEq (Alt b)

data AltCon :: *

A case alternative constructor (i.e. pattern match)

Constructors

DataAlt DataCon

LitAlt Literal

A literal: case e of { 1 -> ... } Invariant: always an *unlifted* literal See Note [Literal alternatives]

DEFAULT

Trivial alternative: case e of { _ -> ... }

Instances

Eq AltCon

Data AltCon

Ord AltCon

Outputable AltCon

Typeable * AltCon

type SeqCoreValue = Value Var

Usual instance of Value, with Vars for binders

type SeqCoreFrame = Frame Var

Usual instance of Frame, with Vars for binders

type SeqCoreCont = Cont Var

Usual instance of Cont, with Vars for binders

type SeqCoreCommand = Command Var

Usual instance of Command, with Vars for binders

type SeqCoreBind = Bind Var

Usual instance of Bind, with Vars for binders

type SeqCoreAlt = Alt Var

Usual instance of Alt, with Vars for binders

Constructors

mkCommand :: [Bind b] -> Value b -> Cont b -> Command b

Constructs a command, given let bindings, a value, and a continuation.

This smart constructor enforces the invariant that a saturated constructor invocation is represented as a Cons value rather than using App frames.

valueCommand :: Value b -> Command b

Constructs a command that simply returns a value.

varCommand :: Id -> Command b

Constructs a command that simply returns a variable.

lambdas :: [b] -> Command b -> Command b

Constructs a number of lambdas surrounding a function body.

addLets :: [Bind b] -> Command b -> Command b

Adds the given bindings outside those in the given command.

extendCont :: Command b -> Cont b -> Command b

Adds the given continuation frames to the end of those in the given command.

Deconstructors

collectLambdas :: Command b -> ([b], Command b)

Divide a command into a sequence of lambdas and a body. If c is not a lambda, then collectLambdas c == ([], c).

collectArgs :: Cont b -> ([Command b], Cont b)

Divide a continuation into a sequence of arguments and an outer continuation. If k is not an application continuation, then collectArgs k == ([], k).

isLambda :: Command b -> Bool

True if the given command is a simple lambda, with no let bindings and no continuation.

isTypeArg :: Command b -> Bool

True if the given command simply returns a type as a value. This may only be true of a command appearing as an argument (that is, inside an App frame) or as the body of a let.

isCoArg :: Command b -> Bool

True if the given command simply returns a coercion as a value. This may only be true of a command appearing as an argument (that is, inside an App frame) or as the body of a let.

isErasedArg :: Command b -> Bool

True if the given command simply returns a value that is either a type or a coercion. This may only be true of a command appearing as an argument (that is, inside an App frame) or as the body of a let.

isRuntimeArg :: Command b -> Bool

True if the given command appears at runtime. Types and coercions are erased.

isTypeValue :: Value b -> Bool

True if the given value is a type. See Type.

isCoValue :: Value b -> Bool

True if the given value is a coercion. See Coercion.

isErasedValue :: Value b -> Bool

True if the given value is a type or coercion.

isRuntimeValue :: Value b -> Bool

True if the given value appears at runtime.

isTrivial :: HasId b => Command b -> Bool

True if the given command represents no actual run-time computation or allocation. For this to hold, it must have no let bindings, and its value and its continuation must both be trivial. Equivalent to exprIsTrivial in GHC.

isTrivialValue :: HasId b => Value b -> Bool

True if the given value represents no actual run-time computation. Some literals are not trivial, and a lambda whose argument is not erased or whose body is non-trivial is also non-trivial.

isTrivialCont :: Cont b -> Bool

True if the given continuation represents no actual run-time computation. This holds if all of its frames are trivial (perhaps because it is the empty continuation).

isTrivialFrame :: Frame b -> Bool

True if the given continuation represents no actual run-time computation. This is true of casts and of applications of erased arguments (types and coercions). Ticks are not considered trivial, since this would cause them to be inlined.

commandAsSaturatedCall :: Command b -> Maybe (Value b, [Command b], Cont b)

If a command represents a saturated call to some function, splits it into the function, the arguments, and the remaining continuation after the arguments.

asSaturatedCall :: Value b -> Cont b -> Maybe ([Command b], Cont b)

If the given value is a function, and the given continuation would provide enough arguments to saturate it, returns the arguments and the remainder of the continuation.

asValueCommand :: Command b -> Maybe (Value b)

If a command does nothing but provide a value, returns that value.

Calculations

valueArity :: Value b -> Int

Compute (a conservative estimate of) the arity of a value. If the value is a variable, this may be a lower bound.

commandType :: SeqCoreCommand -> Type

Compute the type of a command.

Alpha-equivalence

(=~=) :: AlphaEq a => a -> a -> Bool infix 4

True if the two given terms are the same, up to renaming of bound variables.

class AlphaEq a where

The class of types that can be compared up to alpha-equivalence.

Minimal complete definition

aeqIn

Methods

aeq :: a -> a -> Bool infix 4

True if the two given terms are the same, up to renaming of bound variables.

aeqIn :: AlphaEnv -> a -> a -> Bool

True if the two given terms are the same, up to renaming of bound variables and the specified equivalences between free variables.

Instances

AlphaEq Coercion

AlphaEq Type

AlphaEq a => AlphaEq [a]

HasId b => AlphaEq (Alt b)

HasId b => AlphaEq (Bind b)

HasId b => AlphaEq (Command b)

HasId b => AlphaEq (Frame b)

HasId b => AlphaEq (Value b)

type AlphaEnv = RnEnv2

The type of the environment of an alpha-equivalence comparison. Only needed by user code if two terms need to be compared under some assumed correspondences between free variables. See GHC's VarEnv module for operations.

class HasId a where

A class of types that contain an identifier. Useful so that we can compare, say, elements of Command b for any b that wraps an identifier with additional information.

Methods

identifier :: a -> Id

The identifier contained by the type a.

Instances

HasId Var