-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Alternative Core language for GHC plugins
--   
@package sequent-core
@version 0.3


-- | The AST for Sequent Core, with basic operations.
module Language.SequentCore.Syntax

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

-- | A primitive literal value.
Lit :: Literal -> Value b

-- | A term variable. Must <i>not</i> be a nullary constructor; use
--   <a>Cons</a> for this.
Var :: Id -> Value b

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

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

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

-- | A type. Used to pass a type as an argument to a type-level lambda.
Type :: Type -> Value b

-- | A coercion. Used to pass evidence for the <tt>cast</tt> operation to a
--   lambda.
Coercion :: Coercion -> Value b

-- | A continuation. Allowed <i>only</i> as the body of a non-recursive
--   <tt>let</tt>.
Cont :: (Cont b) -> 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.
data Cont b

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

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

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

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

-- | Reference to a bound continuation.
Jump :: ContId -> Cont b

-- | Top-level continuation.
Return :: Cont b

-- | A general computation. A command brings together a list of bindings,
--   some value, and a <i>continuation</i> saying what to do with that
--   value. The value and continuation comprise a <i>cut</i> in the sequent
--   calculus.
--   
--   <b>Invariant</b>: If <a>cmdValue</a> is a variable representing a
--   constructor, then <a>cmdCont</a> must <i>not</i> begin with as many
--   <a>App</a> 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 <a>Cons</a> value
--   instead. When in doubt, use <a>mkCommand</a> to enforce this
--   invariant.
data Command b
Command :: [Bind b] -> Value b -> Cont b -> Command b

-- | Bindings surrounding the computation.
cmdLet :: Command b -> [Bind b]

-- | The value provided to the continuation.
cmdValue :: Command b -> Value b

-- | What to do with the value.
cmdCont :: Command b -> Cont b

-- | A binding. Similar to the <tt>Bind</tt> datatype from GHC. Can be
--   either a single non-recursive binding or a mutually recursive block.
data Bind b

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

-- | A block of mutually recursive bindings.
Rec :: [(b, Value b)] -> 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
--   <a>Command</a>.
data Alt b
Alt :: AltCon -> [b] -> (Command b) -> Alt b

-- | A case alternative constructor (i.e. pattern match)
data AltCon :: *
DataAlt :: DataCon -> AltCon

-- | A literal: <tt>case e of { 1 -&gt; ... }</tt> Invariant: always an
--   *unlifted* literal See Note [Literal alternatives]
LitAlt :: Literal -> AltCon

-- | Trivial alternative: <tt>case e of { _ -&gt; ... }</tt>
DEFAULT :: AltCon

-- | Usual instance of <a>Value</a>, with <a>Var</a>s for binders
type SeqCoreValue = Value Var

-- | Usual instance of <a>Cont</a>, with <a>Var</a>s for binders
type SeqCoreCont = Cont Var

-- | Usual instance of <a>Command</a>, with <a>Var</a>s for binders
type SeqCoreCommand = Command Var

-- | Usual instance of <a>Bind</a>, with <a>Var</a>s for binders
type SeqCoreBind = Bind Var

-- | Usual binders for Sequent Core terms
type SeqCoreBndr = Var

-- | Usual instance of <a>Alt</a>, with <a>Var</a>s for binders
type SeqCoreAlt = Alt Var

-- | Constructs a command, given <tt>let</tt> bindings, a value, and a
--   continuation.
--   
--   This smart constructor enforces the invariant that a saturated
--   constructor invocation is represented as a <a>Cons</a> value rather
--   than using <a>App</a> frames.
mkCommand :: [Bind b] -> Value b -> Cont b -> Command b

-- | Constructs a command that simply returns a value. If the value is a
--   computation, returns that computation instead.
valueCommand :: Value b -> Command b

-- | Constructs a command that simply returns a variable.
varCommand :: Id -> Command b

-- | Wraps a command in a value using <a>Compute</a>. If the command is a
--   value command (see <a>asValueCommand</a>), unwraps it instead.
mkCompute :: Command b -> Value b

-- | Constructs a number of lambdas surrounding a function body.
lambdas :: [b] -> Command b -> Value b

-- | Adds the given bindings outside those in the given command.
addLets :: [Bind b] -> Command b -> Command b

-- | Divide a value into a sequence of lambdas and a body. If <tt>c</tt> is
--   not a lambda, then <tt>collectLambdas v == ([], valueCommand v)</tt>.
collectLambdas :: Value b -> ([b], Command b)

-- | Divide a continuation into a sequence of arguments and an outer
--   continuation. If <tt>k</tt> is not an application continuation, then
--   <tt>collectArgs k == ([], k)</tt>.
collectArgs :: Cont b -> ([Value b], Cont b)

-- | Divide a continuation into a sequence of type arguments and an outer
--   continuation. If <tt>k</tt> is not an application continuation or only
--   applies non-type arguments, then <tt>collectTypeArgs k == ([],
--   k)</tt>.
collectTypeArgs :: Cont b -> ([KindOrType], Cont b)

-- | Divide a continuation into a sequence of type arguments, then a
--   sequence of non-type arguments, then an outer continuation. If
--   <tt>k</tt> is not an application continuation, then
--   <tt>collectTypeAndOtherArgs k == ([], [], k)</tt>.
collectTypeAndOtherArgs :: Cont b -> ([KindOrType], [Value b], Cont b)

-- | Divide a list of values into an initial sublist of types and the
--   remaining values.
partitionTypes :: [Value b] -> ([KindOrType], [Value b])

-- | True if the given command is a simple lambda, with no let bindings and
--   no continuation.
isLambda :: Command b -> Bool

-- | True if the given value is a type. See <a>Type</a>.
isTypeValue :: Value b -> Bool

-- | True if the given value is a coercion. See <a>Coercion</a>.
isCoValue :: Value b -> Bool

-- | True if the given value is a type or coercion.
isErasedValue :: Value b -> Bool

-- | True if the given value appears at runtime, i.e. is neither a type nor
--   a coercion.
isRuntimeValue :: Value b -> Bool

-- | True if the given command represents no actual run-time computation or
--   allocation. For this to hold, it must have no <tt>let</tt> bindings,
--   and its value and its continuation must both be trivial. Equivalent to
--   <a>exprIsTrivial</a> in GHC.
isTrivial :: HasId b => Command 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.
isTrivialValue :: HasId b => Value 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.
isTrivialCont :: Cont b -> Bool

-- | True if the given continuation is the return continuation,
--   <a>Return</a>.
isReturnCont :: Cont b -> Bool

-- | If a command represents a saturated call to some function, splits it
--   into the function, the arguments, and the remaining continuation after
--   the arguments.
commandAsSaturatedCall :: Command b -> Maybe (Value b, [Value 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.
asSaturatedCall :: Value b -> Cont b -> Maybe ([Value b], Cont b)

-- | If a command does nothing but provide a value, returns that value.
asValueCommand :: Command b -> Maybe (Value b)

-- | Compute (a conservative estimate of) the arity of a value. If the
--   value is a variable, this may be a lower bound.
valueArity :: Value b -> Int

-- | Compute the type of a value.
valueType :: SeqCoreValue -> Type

-- | 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.
contOuterType :: Type -> SeqCoreCont -> Type

-- | Compute the type that a command yields to its outer context.
commandType :: SeqCoreCommand -> Type

-- | INTERNAL USE ONLY.
contIdTag :: Char

-- | Find whether an id is a continuation id.
isContId :: Id -> Bool

-- | 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.
asContId :: Id -> ContId

-- | True if the two given terms are the same, up to renaming of bound
--   variables.
(=~=) :: AlphaEq a => a -> a -> Bool

-- | The class of types that can be compared up to alpha-equivalence.
class AlphaEq a where aeq = aeqIn emptyAlphaEnv
aeq :: AlphaEq a => a -> a -> Bool
aeqIn :: AlphaEq a => AlphaEnv -> a -> a -> Bool

-- | 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
--   <a>VarEnv</a> module for operations.
type AlphaEnv = RnEnv2

-- | A class of types that contain an identifier. Useful so that we can
--   compare, say, elements of <tt>Command b</tt> for any <tt>b</tt> that
--   wraps an identifier with additional information.
class HasId a
identifier :: HasId a => a -> Id
instance HasId b => AlphaEq (Bind b)
instance AlphaEq a => AlphaEq [a]
instance AlphaEq Coercion
instance AlphaEq Type
instance HasId b => AlphaEq (Alt b)
instance HasId b => AlphaEq (Command b)
instance HasId b => AlphaEq (Cont b)
instance HasId b => AlphaEq (Value b)
instance HasId Var


-- | Instances and functions for pretty-printing Sequent Core terms using
--   GHC's built-in pretty printer.
module Language.SequentCore.Pretty

-- | Print the given bindings as a sequence of top-level bindings.
pprTopLevelBinds :: OutputableBndr b => [Bind b] -> SDoc
instance OutputableBndr b => Outputable (Alt b)
instance OutputableBndr b => Outputable (Cont b)
instance OutputableBndr b => Outputable (Command b)
instance OutputableBndr b => Outputable (Value b)
instance OutputableBndr b => Outputable (Bind b)


-- | Translation between Sequent Core and native GHC Core.
module Language.SequentCore.Translate

-- | Translates a Core expression into Sequent Core.
fromCoreExpr :: CoreExpr -> SeqCoreCommand

-- | Translates a Core binding into Sequent Core.
fromCoreBind :: CoreBind -> SeqCoreBind

-- | Translates a list of Core bindings into Sequent Core.
fromCoreBinds :: [CoreBind] -> [SeqCoreBind]

-- | Translates a Core case alternative into Sequent Core.
fromCoreAlt :: CoreAlt -> SeqCoreAlt

-- | Translates a command into Core.
commandToCoreExpr :: SeqCoreCommand -> CoreExpr

-- | Translates a value into Core.
valueToCoreExpr :: SeqCoreValue -> CoreExpr

-- | Translates a continuation into a function that will wrap a Core
--   expression with a fragment of context (an argument to apply to, a case
--   expression to run, etc.).
contToCoreExpr :: SeqCoreCont -> (CoreExpr -> CoreExpr)

-- | Translates a binding into Core.
bindToCore :: SeqCoreBind -> CoreBind

-- | Translates a list of bindings into Core.
bindsToCore :: [SeqCoreBind] -> [CoreBind]

-- | Translates a case alternative into Core.
altToCore :: SeqCoreAlt -> CoreAlt


-- | Tools for writing a GHC plugin using the Sequent Core language in
--   place of GHC Core.
module Language.SequentCore.Plugin

-- | Given a function that processes a module's bindings as Sequent Core
--   terms, perform the same processing as a Core-to-Core pass usable from
--   a GHC plugin. Intended to be passed to the <tt>CoreDoPluginPass</tt>
--   constructor as part of your plugin's <tt>installCoreToDos</tt>
--   function. See <a>Language.SequentCore.Dump</a> for an example and the
--   GHC manual for more details.
sequentPass :: ([SeqCoreBind] -> CoreM [SeqCoreBind]) -> (ModGuts -> CoreM ModGuts)


-- | An example GHC optimizer plugin using Sequent Core. Simply translates
--   the given Core code to Sequent Core, dumps it to the screen, then
--   translates back. This allows inspection of the Sequent Core code for a
--   module and also tests the translation functions.
--   
--   Note that translating to Sequent Core and back should give an
--   <i>equivalent</i> program, but it may vary slightly. The effects
--   should be benign, such as a <tt>let</tt> floating around in an
--   expression (but never across a lambda).
module Language.SequentCore.Dump

-- | The plugin. A GHC plugin is a module that exports a value called
--   <tt>plugin</tt> with the type <a>Plugin</a>.
plugin :: Plugin


-- | A proof of concept to demonstrate that the Sequent Core syntax can be
--   used for basic optimization in the style of GHC's simplifier. In some
--   ways, it is easier to use Sequent Core for these, as the continuations
--   are expressed directly in the program syntax rather than needing to be
--   built up on the fly.
module Language.SequentCore.Simpl

-- | Plugin data. The initializer replaces all instances of the original
--   simplifier with the new one.
plugin :: Plugin


-- | A simple reimplementation of the SpecConstr pass using Sequent Core.
--   
--   Based on <a>Call-pattern specialization for Haskell programs</a>,
--   Simon Peyton Jones, submitted to ICFP 2007.
module Language.SequentCore.SpecConstr

-- | Plugin data. The initialization code replaces the built-in SpecConstr
--   pass in the Core-to-Core pipeline.
plugin :: Plugin
instance Outputable Spec
instance Outputable CallPat
instance Monoid ScUsage
instance Outputable HowBound
instance Outputable ScUsage
instance Outputable ScEnv


module Language.SequentCore