Maintainer | maurerl@cs.uoregon.edu |
---|---|

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

The AST for Sequent Core, with basic operations.

- data Value b
- data Cont b
- data Command b = Command {}
- data Bind b
- data Alt b = Alt AltCon [b] (Command b)
- data AltCon :: *
- type SeqCoreValue = Value Var
- type SeqCoreCont = Cont Var
- type SeqCoreCommand = Command Var
- type SeqCoreBind = Bind Var
- type SeqCoreBndr = Var
- type SeqCoreAlt = Alt Var
- mkCommand :: [Bind b] -> Value b -> Cont b -> Command b
- valueCommand :: Value b -> Command b
- varCommand :: Id -> Command b
- mkCompute :: Command b -> Value b
- lambdas :: [b] -> Command b -> Value b
- addLets :: [Bind b] -> Command b -> Command b
- collectLambdas :: Value b -> ([b], Command b)
- collectArgs :: Cont b -> ([Value b], Cont b)
- collectTypeArgs :: Cont b -> ([KindOrType], Cont b)
- collectTypeAndOtherArgs :: Cont b -> ([KindOrType], [Value b], Cont b)
- partitionTypes :: [Value b] -> ([KindOrType], [Value b])
- isLambda :: Command b -> Bool
- isTypeValue :: Value b -> Bool
- isCoValue :: Value b -> Bool
- isErasedValue :: Value b -> Bool
- isRuntimeValue :: Value b -> Bool
- isTrivial :: HasId b => Command b -> Bool
- isTrivialValue :: HasId b => Value b -> Bool
- isTrivialCont :: Cont b -> Bool
- isReturnCont :: Cont b -> Bool
- commandAsSaturatedCall :: Command b -> Maybe (Value b, [Value b], Cont b)
- asSaturatedCall :: Value b -> Cont b -> Maybe ([Value b], Cont b)
- asValueCommand :: Command b -> Maybe (Value b)
- valueArity :: Value b -> Int
- valueType :: SeqCoreValue -> Type
- contOuterType :: Type -> SeqCoreCont -> Type
- commandType :: SeqCoreCommand -> Type
- contIdTag :: Char
- isContId :: Id -> Bool
- asContId :: Id -> ContId
- (=~=) :: AlphaEq a => a -> a -> Bool
- class AlphaEq a where
- type AlphaEnv = RnEnv2
- class HasId a where
- identifier :: a -> Id

# AST Types

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.

Lit Literal | A primitive literal value. |

Var Id | A term variable. Must |

Lam b (Command b) | A function. Binds both an argument and a continuation. The body is a command. |

Cons DataCon [Value b] | A value formed by a saturated constructor application. |

Compute (Command b) | A value produced by a computation. Binds the current continuation. |

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 |

Cont (Cont b) | A continuation. Allowed |

OutputableBndr b => Outputable (Value b) | |

HasId b => AlphaEq (Value b) |

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.

App (Value b) (Cont b) | Apply the value to an argument. |

Case b Type [Alt b] (Cont b) | Perform case analysis on the value. |

Cast Coercion (Cont b) | Cast the value using the given coercion. |

Tick (Tickish Id) (Cont b) | Annotate the enclosed frame. Used by the profiler. |

Jump ContId | Reference to a bound continuation. |

Return | Top-level continuation. |

OutputableBndr b => Outputable (Cont b) | |

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

OutputableBndr b => Outputable (Command b) | |

HasId b => AlphaEq (Command b) |

A binding. Similar to the `Bind`

datatype from GHC. Can be either a single
non-recursive binding or a mutually recursive block.

NonRec b (Value b) | A single non-recursive binding. |

Rec [(b, Value b)] | A block of mutually recursive bindings. |

OutputableBndr b => Outputable (Bind b) | |

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

.

OutputableBndr b => Outputable (Alt b) | |

HasId b => AlphaEq (Alt b) |

data AltCon :: *

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

type SeqCoreBndr = Var Source

Usual binders for Sequent Core terms

# Constructors

valueCommand :: Value b -> Command b Source

Constructs a command that simply returns a value. If the value is a computation, returns that computation instead.

varCommand :: Id -> Command b Source

Constructs a command that simply returns a variable.

mkCompute :: Command b -> Value b Source

Wraps a command in a value using `Compute`

. If the command is a value
command (see `asValueCommand`

), unwraps it instead.

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

Constructs a number of lambdas surrounding a function body.

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

Adds the given bindings outside those in the given command.

# Deconstructors

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

Divide a value into a sequence of lambdas and a body. If `c`

is not a
lambda, then `collectLambdas v == ([], valueCommand v)`

.

collectArgs :: Cont b -> ([Value b], Cont b) Source

Divide a continuation into a sequence of arguments and an outer
continuation. If `k`

is not an application continuation, then
`collectArgs k == ([], k)`

.

collectTypeArgs :: Cont b -> ([KindOrType], Cont b) Source

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)`

.

collectTypeAndOtherArgs :: Cont b -> ([KindOrType], [Value b], Cont b) Source

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)`

.

partitionTypes :: [Value b] -> ([KindOrType], [Value b]) Source

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

isLambda :: Command b -> Bool Source

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

isTypeValue :: Value b -> Bool Source

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

.

isErasedValue :: Value b -> Bool Source

True if the given value is a type or coercion.

isRuntimeValue :: Value b -> Bool Source

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

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

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 Source

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 Source

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.

isReturnCont :: Cont b -> Bool Source

True if the given continuation is the return continuation, `Return`

.

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

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 ([Value b], Cont b) Source

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) Source

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

# Calculations

valueArity :: Value b -> Int Source

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

valueType :: SeqCoreValue -> Type Source

Compute the type of a value.

contOuterType :: Type -> SeqCoreCont -> Type Source

Compute the outer type of a continuation, that is, the type of the value it eventually yields to the environment. Requires the inner type as an argument.

commandType :: SeqCoreCommand -> Type Source

Compute the type that a command yields to its outer context.

# Continuation ids

asContId :: Id -> ContId Source

Tag an id as a continuation id. This changes the unique of the id, so the returned id is always distinct from the argument in comparisons.

# Alpha-equivalence

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

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.