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 not be a
nullary constructor; use |
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 only as the
body of a non-recursive |
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.