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


-- | Linear scan register allocator, formally verified in Coq
--   
--   The <tt>linearscan</tt> library is an implementation -- in Coq,
--   extracted to Haskell -- of a register allocation algorithm developed
--   by Christian Wimmer. It is described in detail in his Masters thesis,
--   which can be found at
--   <a>http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf</a>.
--   A Java implementation of this same algorithm, by that author, is used
--   in Oracle's Graal project.
--   
--   This version of the algorithm was written and verified in Coq,
--   containing over 130 proved lemmas, at over 5K LOC. It was funded as a
--   research project by BAE Systems (<a>http://www.baesystems.com</a>), to
--   be used in an in-house compiler written in Haskell.
--   
--   In order for the Coq code to be usable from Haskell, it is first
--   extracted from Coq as a Haskell library, during which many of Coq's
--   fundamental types are mapped directly onto counterparts in the Haskell
--   Prelude. Thus, it should be within the performance range of an
--   equivalent implementation written directly in Haskell.
--   
--   Note that not every conceivable property of this library has been
--   proven. For some of the lower layers this is true, because the
--   algebraic constraints on these components could be exhaustively
--   described in the context of their use. However, higher-level
--   components represent a great variety of use cases, and not every one
--   of these cases has been proven correct. This represents an ongoing
--   effort, with the hope that proofs will entirely replace the necessity
--   for ad hoc unit testing, and that at some point we can know that any
--   allocation produced by this library must either fail, or be
--   mathematically sound.
--   
--   This library's sole entry point is the <a>LinearScan.allocate</a>
--   function, which takes a list of information about basic blocks to an
--   equivalent list, with annotations indicating allocation choices.
@package linearscan
@version 0.11.1

module LinearScan

-- | Transform a list of basic blocks containing variable references, into
--   an equivalent list where each reference is associated with a register
--   allocation. Artificial save and restore instructions may also be
--   inserted into blocks to indicate spilling and reloading of variables.
--   
--   In order to call this function, the caller must provide records that
--   allow viewing and mutating of the original program graph.
--   
--   If allocation is found to be impossible -- for example if there are
--   simply not enough registers -- a <a>Left</a> value is returned, with a
--   string describing the error.
allocate :: (Functor m, Applicative m, Monad m) => Int -> BlockInfo m blk1 blk2 op1 op2 -> OpInfo m op1 op2 -> UseVerifier -> [blk1] -> m (String, Either [String] [blk2])

-- | From the point of view of this library, a basic block is nothing more
--   than an ordered sequence of operations.
data BlockInfo m blk1 blk2 op1 op2
BlockInfo :: (blk1 -> Int) -> (blk1 -> [Int]) -> (blk1 -> blk1 -> m (blk1, blk1)) -> (blk1 -> ([op1], [op1], [op1])) -> (blk1 -> [op2] -> [op2] -> [op2] -> blk2) -> BlockInfo m blk1 blk2 op1 op2
[blockId] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> Int
[blockSuccessors] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> [Int]
[splitCriticalEdge] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> blk1 -> m (blk1, blk1)
[blockOps] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> ([op1], [op1], [op1])
[setBlockOps] :: BlockInfo m blk1 blk2 op1 op2 -> blk1 -> [op2] -> [op2] -> [op2] -> blk2
data UseVerifier
VerifyDisabled :: UseVerifier
VerifyEnabled :: UseVerifier
VerifyEnabledStrict :: UseVerifier

-- | Every operation may reference multiple variables and/or specific
--   physical registers. If a physical register is referenced, then that
--   register is considered unavailable for allocation over the range of
--   such references.
--   
--   Certain operations have special significance as to how basic blocks
--   are organized, and the lifetime of allocations. Thus, if an operation
--   begins or ends a loop, or represents a method call, it should be
--   indicated using the <a>OpKind</a> field. Indication of calls is
--   necessary in order to save and restore all registers around a call,
--   but indication of loops is optional, as it's merely avoids reloading
--   of spilled variables inside loop bodies.
data OpInfo m op1 op2
OpInfo :: (op1 -> OpKind) -> (op1 -> [VarInfo]) -> (PhysReg -> VarId -> PhysReg -> m [op2]) -> (PhysReg -> VarId -> m [op2]) -> (VarId -> PhysReg -> m [op2]) -> (op1 -> [((VarId, VarKind), PhysReg)] -> m [op2]) -> (op1 -> String) -> OpInfo m op1 op2
[opKind] :: OpInfo m op1 op2 -> op1 -> OpKind
[opRefs] :: OpInfo m op1 op2 -> op1 -> [VarInfo]
[moveOp] :: OpInfo m op1 op2 -> PhysReg -> VarId -> PhysReg -> m [op2]
[saveOp] :: OpInfo m op1 op2 -> PhysReg -> VarId -> m [op2]
[restoreOp] :: OpInfo m op1 op2 -> VarId -> PhysReg -> m [op2]
[applyAllocs] :: OpInfo m op1 op2 -> op1 -> [((VarId, VarKind), PhysReg)] -> m [op2]
[showOp1] :: OpInfo m op1 op2 -> op1 -> String
data OpKind
IsNormal :: OpKind
IsCall :: OpKind
IsBranch :: OpKind
type VarId = Int

-- | Each variable has associated allocation details, and a flag to
--   indicate whether it must be loaded into a register at its point of
--   use. Variables are also distinguished by their kind, which allows for
--   restricting the scope of their lifetime. For example, output variables
--   are not needed in a basic block until the first point of use, while
--   the lifetime of input variables extends until their final use.
data VarInfo
VarInfo :: Either PhysReg VarId -> VarKind -> Bool -> VarInfo
[varId] :: VarInfo -> Either PhysReg VarId
[varKind] :: VarInfo -> VarKind
[regRequired] :: VarInfo -> Bool
data VarKind
Input :: VarKind
InputOutput :: VarKind
Temp :: VarKind
Output :: VarKind
type PhysReg = Int
instance GHC.Classes.Eq LinearScan.UsePos.VarKind
instance GHC.Classes.Eq LinearScan.Blocks.OpKind
instance GHC.Show.Show LinearScan.Blocks.OpKind
instance GHC.Show.Show LinearScan.Verify.AllocError
instance GHC.Show.Show LinearScan.Main.FinalStage
instance GHC.Show.Show LinearScan.LiveSets.BlockLiveSets
instance GHC.Show.Show LinearScan.Trace.SSTrace
instance GHC.Show.Show LinearScan.ScanStateDesc
instance GHC.Show.Show LinearScan.LoopState
instance GHC.Show.Show LinearScan.Verify.RegStateDescSet
instance GHC.Show.Show LinearScan.Resolve.ResolvingMoveSet
instance GHC.Show.Show LinearScan.Trace.SpillConditionT
instance GHC.Show.Show LinearScan.Trace.SplitPositionT