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

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

The AST for Sequent Core, with basic operations.

- data Term b
- data Cont b
- data Command b = Command {}
- data Bind b
- data Alt b = Alt AltCon [b] (Command b)
- data AltCon :: *
- data Expr a
- type Program a = [Bind a]
- type ContId = Id
- type SeqCoreTerm = Term Var
- type SeqCoreCont = Cont Var
- type SeqCoreCommand = Command Var
- type SeqCoreBind = Bind Var
- type SeqCoreBndr = Var
- type SeqCoreAlt = Alt Var
- type SeqCoreExpr = Expr Var
- type SeqCoreProgram = Program Var
- mkCommand :: HasId b => [Bind b] -> Term b -> Cont b -> Command b
- mkCompute :: HasId b => b -> Command b -> Term b
- addLets :: [Bind b] -> Command b -> Command b
- addNonRec :: HasId b => b -> Term b -> Command b -> Command b
- lambdas :: Term b -> ([b], Maybe (b, Command b))
- collectArgs :: Cont b -> ([Term b], Cont b)
- collectTypeArgs :: Cont b -> ([KindOrType], Cont b)
- collectTypeAndOtherArgs :: Cont b -> ([KindOrType], [Term b], Cont b)
- collectArgsUpTo :: Int -> Cont b -> ([Term b], Cont b)
- partitionTypes :: [Term b] -> ([KindOrType], [Term b])
- isLambda :: Command b -> Bool
- isValueArg :: Term b -> Bool
- isTypeTerm :: Term b -> Bool
- isCoTerm :: Term b -> Bool
- isErasedTerm :: Term b -> Bool
- isRuntimeTerm :: Term b -> Bool
- isProperTerm :: Term b -> Bool
- isTrivial :: HasId b => Command b -> Bool
- isTrivialTerm :: HasId b => Term b -> Bool
- isTrivialCont :: Cont b -> Bool
- isReturnCont :: Cont b -> Bool
- commandAsSaturatedCall :: HasId b => Command b -> Maybe (Term b, [Term b], Cont b)
- asSaturatedCall :: HasId b => Term b -> Cont b -> Maybe ([Term b], Cont b)
- asValueCommand :: ContId -> Command b -> Maybe (Term b)
- flattenBind :: Bind b -> [(b, Term b)]
- flattenBinds :: [Bind b] -> [(b, Term b)]
- bindersOf :: Bind b -> [b]
- bindersOfBinds :: [Bind b] -> [b]
- termArity :: HasId b => Term b -> Int
- termType :: HasId b => Term b -> Type
- contType :: HasId b => Cont b -> Type
- termIsBottom :: Term b -> Bool
- commandIsBottom :: Command b -> Bool
- needsCaseBinding :: Type -> Term b -> Bool
- termOkForSpeculation :: Term b -> Bool
- commandOkForSpeculation :: Command b -> Bool
- contOkForSpeculation :: Cont b -> Bool
- termOkForSideEffects :: Term b -> Bool
- commandOkForSideEffects :: Command b -> Bool
- contOkForSideEffects :: Cont b -> Bool
- termIsCheap :: HasId b => Term b -> Bool
- contIsCheap :: HasId b => Cont b -> Bool
- commandIsCheap :: HasId b => Command b -> Bool
- termIsExpandable :: HasId b => Term b -> Bool
- contIsExpandable :: HasId b => Cont b -> Bool
- commandIsExpandable :: HasId b => Command b -> Bool
- isContId :: Id -> Bool
- asContId :: Id -> ContId
- mkContTy :: Type -> Type
- contTyArg :: Type -> Type
- (=~=) :: 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] b (Command b) | A function. Binds some arguments and a continuation. The body is a command. |

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

Compute b (Command b) | A value produced by a computation. Binds a 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 (Term b) | |

HasId b => AlphaEq (Term 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 (Term b) (Cont b) | Apply the value to an argument. |

Case b [Alt 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. |

Return ContId | Reference to a bound continuation. |

OutputableBndr b => Outputable (Cont b) | |

HasId b => AlphaEq (Cont b) |

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.

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 (Term b) | A single non-recursive binding. |

Rec [(b, Term 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)

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

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

type SeqCoreBndr = Var Source

Usual binders for Sequent Core terms

# Constructors

mkCompute :: HasId b => b -> Command b -> Term b Source

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.

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

Adds the given bindings outside those in the given command.

addNonRec :: HasId b => b -> Term b -> Command b -> Command b Source

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

# Deconstructors

collectArgs :: Cont b -> ([Term 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], [Term 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)`

.

collectArgsUpTo :: Int -> Cont b -> ([Term b], Cont b) Source

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

.

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

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

isLambda :: Command b -> Bool Source

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

isValueArg :: Term b -> Bool Source

isTypeTerm :: Term b -> Bool Source

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

.

isErasedTerm :: Term b -> Bool Source

True if the given term is a type or coercion.

isRuntimeTerm :: Term b -> Bool Source

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

isProperTerm :: Term b -> Bool Source

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.

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

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.

isTrivialTerm :: HasId b => Term b -> Bool Source

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.

isTrivialCont :: Cont b -> Bool Source

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.

isReturnCont :: Cont b -> Bool Source

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

.

commandAsSaturatedCall :: HasId b => Command b -> Maybe (Term b, [Term 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 :: HasId b => Term b -> Cont b -> Maybe ([Term b], Cont b) Source

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.

asValueCommand :: ContId -> Command b -> Maybe (Term b) Source

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

flattenBind :: Bind b -> [(b, Term b)] Source

flattenBinds :: [Bind b] -> [(b, Term b)] Source

bindersOfBinds :: [Bind b] -> [b] Source

# Calculations

termArity :: HasId b => Term b -> Int Source

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

contType :: HasId b => Cont b -> Type Source

Compute the type a continuation accepts. If `contType cont`

is Foo and `cont`

is bound
to `k`

, then `k`

's `idType`

will be `!Foo`

.

termIsBottom :: Term b -> Bool Source

Find whether an expression is definitely bottom.

commandIsBottom :: Command b -> Bool Source

Find whether a command definitely evaluates to bottom.

needsCaseBinding :: Type -> Term b -> Bool Source

Decide whether a term should be bound using `case`

rather than `let`

.
See `needsCaseBinding`

.

termOkForSpeculation :: Term b -> Bool Source

commandOkForSpeculation :: Command b -> Bool Source

contOkForSpeculation :: Cont b -> Bool Source

termOkForSideEffects :: Term b -> Bool Source

commandOkForSideEffects :: Command b -> Bool Source

contOkForSideEffects :: Cont b -> Bool Source

termIsCheap :: HasId b => Term b -> Bool Source

contIsCheap :: HasId b => Cont b -> Bool Source

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

termIsExpandable :: HasId b => Term b -> Bool Source

contIsExpandable :: HasId b => Cont b -> Bool Source

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

# Continuation ids

# 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.