An expression producing a value. These include literals, lambdas, and variables, as well as types and coercions (see GHC's Expr for the reasoning). They also include computed values, which bind the current continuation in the body of a command.

A continuation, representing a strict context of a Haskell expression. Computation in the sequent calculus is expressed as the interaction of a value with a continuation.

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

Invariant: If cmdTerm 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.

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

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.

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

Some expression -- a term, a command, or a continuation. Useful for writing mutually recursive functions.

An entire program.

The identifier for a covariable, which is like a variable but it binds a continuation.

Usual instance of Term, with Vars for binders

Usual instance of Cont, with Vars for binders

Usual instance of Command, with Vars for binders

Usual instance of Bind, with Vars for binders

Usual binders for Sequent Core terms

Usual instance of Alt, with Vars for binders

Usual instance of Expr, with Vars for binders

Usual instance of Term, with Vars for binders

Constructs a command, given let bindings, a term, 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.

Wraps a command that returns to the given continuation id in a term using Compute. If the command is a value command (see asValueCommand), unwraps it instead.

Adds the given bindings outside those in the given command.

Adds the given binding outside the given command, possibly using a case binding rather than a let. See CoreSyn on the let/app invariant.

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

Divide a continuation into a sequence of type arguments and an outer continuation. If k is not an application continuation or only applies non-type arguments, then collectTypeArgs k == ([], k).

Divide a continuation into a sequence of type arguments, then a sequence of non-type arguments, then an outer continuation. If k is not an application continuation, then collectTypeAndOtherArgs k == ([], [], k).

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

Divide a list of terms into an initial sublist of types and the remaining terms.

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

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

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

True if the given term is a type or coercion.

True if the given term appears at runtime, i.e. is neither a type nor a coercion.

True if the given term can appear in an expression without restriction. Not true if the term is a type, coercion, or continuation; these can only appear on the RHS of a let or (except for continuations) as an argument in a function call.

True if the given command is so simple we can duplicate it freely. This means it has no bindings and its term and continuation are both trivial.

True if the given term is so simple we can duplicate it freely. Some literals are not trivial, and a lambda whose argument is not erased or whose body is non-trivial is also non-trivial.

True if the given continuation is so simple we can duplicate it freely. 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.

True if the given continuation is a return continuation, Return _.

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

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

If a command does nothing but provide a value to the given continuation id, returns that value.

Compute (a conservative estimate of) the arity of a term.

Compute the type of a term.

Compute the type a continuation accepts. If contType cont is Foo and cont is bound to k, then k's idType will be !Foo.

Find whether an expression is definitely bottom.

Find whether a command definitely evaluates to bottom.

Decide whether a term should be bound using case rather than let. See needsCaseBinding.

Find whether an id is a continuation id.

Tag an id as a continuation id.

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

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

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.

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.