diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -55,3 +55,37 @@
   to 20% performance improvement
 * Code restructuring and refactoring
 * Added copious amounts of documentation
+
+## 1.5.0.0 -- 2021-08-12
+Infrastructure for improved handler analysis:
+
+* Refactored `LetBinding` to include more generic metadata.
+* Added metadata to `StaSubroutine` and introduced `StaSubroutine#` and associated functions.
+* Fed metadata through `letRec`'s `genBinding` and into `buildRec`.
+* Added an `Amount` to `Offset`, which also takes into account a multiplicity, used to track unknown
+  but non-zero quantities.
+* Added `callCC` and modified the API for `suspend` to allow for abstracted `Offset` creation. The
+  `callCC` operation promises to utilise static input consumption from the subroutine to refine the
+  input to the return continuation (making use of the multiplicity above).
+* Refactored the `CombinatorAnalyser` into an `Analysis.Cut` module (and moved `Dependencies` there too)
+* Refactored the `InstructionAnalyser` into an `Analysis.Coins` and `Analysis.Relevancy` modules
+* More documentation
+
+Input Reclamation:
+
+* Added `Machine.Types.Coins`, which separates coins for length checks from input reclamation.
+* `Analysis.Coins` now deals wiith the `Coins` type, as do the instructions.
+* Added `Common.RewindQueue` to handle rewindable input caching.
+* Added `Common.QueueLike` to abstract both queue's common operations.
+* Moved the implementation of `Queue` into a `Queue.Impl` submodule, for `RewindQueue` and testing.
+* Added `GiveBursary` instruction to implement a variant of `RefundCoins`.
+* Added `PrefetchChar` instruction for future prefetching on branches.
+* Added `canAfford` to `Context` and removed the broken `liquidate`.
+* Improved the input factoring for join points.
+
+Misc:
+
+* Removed the unneeded `genDefuncX` operations in `Core.Defunc`, and `ap`, hid others.
+* Added type to `next` in `CharList`.
+* Added auxilliary information parameter to `sat`.
+* Added `fetch` and broke it out of `sat`.
diff --git a/parsley-core.cabal b/parsley-core.cabal
--- a/parsley-core.cabal
+++ b/parsley-core.cabal
@@ -5,7 +5,7 @@
 --                   | +------- breaking internal API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             1.4.0.0
+version:             1.5.0.0
 synopsis:            A fast parser combinator library backed by Typed Template Haskell
 description:         This package contains the internals of the @parsley@ package.
                      .
@@ -39,11 +39,17 @@
                        Parsley.Internal.Common,
                        Parsley.Internal.Common.Fresh,
                        Parsley.Internal.Common.Indexed,
-                       Parsley.Internal.Common.Queue,
+                       Parsley.Internal.Common.QueueLike,
                        Parsley.Internal.Common.State,
                        Parsley.Internal.Common.Utils,
                        Parsley.Internal.Common.Vec,
 
+                       Parsley.Internal.Common.Queue,
+                       Parsley.Internal.Common.Queue.Impl,
+
+                       Parsley.Internal.Common.RewindQueue,
+                       Parsley.Internal.Common.RewindQueue.Impl,
+
                        Parsley.Internal.Core,
                        Parsley.Internal.Core.CombinatorAST,
                        Parsley.Internal.Core.Defunc,
@@ -53,16 +59,22 @@
                        Parsley.Internal.Core.Primitives,
 
                        Parsley.Internal.Frontend,
-                       Parsley.Internal.Frontend.CombinatorAnalyser,
                        Parsley.Internal.Frontend.Compiler,
-                       Parsley.Internal.Frontend.Dependencies,
                        Parsley.Internal.Frontend.Optimiser,
 
+                       Parsley.Internal.Frontend.Analysis,
+                       Parsley.Internal.Frontend.Analysis.Cut,
+                       Parsley.Internal.Frontend.Analysis.Dependencies,
+                       Parsley.Internal.Frontend.Analysis.Flags,
+
                        Parsley.Internal.Backend,
                        Parsley.Internal.Backend.CodeGenerator,
-                       Parsley.Internal.Backend.InstructionAnalyser,
-                       Parsley.Internal.Backend.Optimiser,
+                       --Parsley.Internal.Backend.Optimiser,
 
+                       Parsley.Internal.Backend.Analysis,
+                       Parsley.Internal.Backend.Analysis.Coins,
+                       Parsley.Internal.Backend.Analysis.Relevancy,
+
                        Parsley.Internal.Backend.Machine,
                        Parsley.Internal.Backend.Machine.Defunc,
                        Parsley.Internal.Backend.Machine.Eval,
@@ -75,6 +87,7 @@
                        Parsley.Internal.Backend.Machine.Ops,
 
                        Parsley.Internal.Backend.Machine.Types,
+                       Parsley.Internal.Backend.Machine.Types.Coins,
                        Parsley.Internal.Backend.Machine.Types.State
 
   if impl(ghc >= 8.10)
@@ -140,6 +153,20 @@
     ghc-options:       -Wno-missing-safe-haskell-mode
                        -Wno-prepositive-qualified-module
                        -Wno-unused-packages
+
+common test-common
+  build-depends:       base >=4.10 && <5,
+                       parsley-core,
+                       tasty
+  hs-source-dirs:      test
+  default-language:    Haskell2010
+
+test-suite common-test
+  import:              test-common
+  type:                exitcode-stdio-1.0
+  build-depends:       tasty-hunit, tasty-quickcheck
+  main-is:             CommonTest.hs
+  other-modules:       CommonTest.Queue, CommonTest.RewindQueue
 
 source-repository head
   type:                git
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine.hs
@@ -9,6 +9,7 @@
 -}
 module Parsley.Internal.Backend.Machine (
     Input, eval,
+    module Parsley.Internal.Backend.Machine.Types.Coins,
     module Parsley.Internal.Backend.Machine.Instructions,
     module Parsley.Internal.Backend.Machine.Defunc,
     module Parsley.Internal.Backend.Machine.Identifiers,
@@ -23,8 +24,9 @@
 import Parsley.Internal.Backend.Machine.Identifiers
 import Parsley.Internal.Backend.Machine.InputOps     (InputPrep(..))
 import Parsley.Internal.Backend.Machine.Instructions
-import Parsley.Internal.Backend.Machine.LetBindings  (LetBinding, makeLetBinding)
+import Parsley.Internal.Backend.Machine.LetBindings  (LetBinding, makeLetBinding, newMeta)
 import Parsley.Internal.Backend.Machine.Ops          (Ops)
+import Parsley.Internal.Backend.Machine.Types.Coins  (Coins(..), zero, minCoins, maxCoins, plus, plus1, minus, plusNotReclaim)
 import Parsley.Internal.Common.Utils                 (Code)
 import Parsley.Internal.Core.InputTypes
 import Parsley.Internal.Trace                        (Trace)
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Eval.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Eval.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Eval.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Eval.hs
@@ -20,20 +20,21 @@
 import Data.Dependent.Map                             (DMap)
 import Data.Functor                                   ((<&>))
 import Data.Void                                      (Void)
-import Control.Monad                                  (forM, liftM2, liftM3)
-import Control.Monad.Reader                           (ask, asks, local)
+import Control.Monad                                  (forM, liftM2, liftM3, when)
+import Control.Monad.Reader                           (ask, asks, reader, local)
 import Control.Monad.ST                               (runST)
 import Parsley.Internal.Backend.Machine.Defunc        (Defunc(OFFSET), pattern FREEVAR, genDefunc, ap, ap2, _if)
 import Parsley.Internal.Backend.Machine.Identifiers   (MVar(..), ΦVar, ΣVar)
 import Parsley.Internal.Backend.Machine.InputOps      (InputDependant, InputOps(InputOps))
 import Parsley.Internal.Backend.Machine.InputRep      (Rep)
 import Parsley.Internal.Backend.Machine.Instructions  (Instr(..), MetaInstr(..), Access(..), Handler(..))
-import Parsley.Internal.Backend.Machine.LetBindings   (LetBinding(..))
+import Parsley.Internal.Backend.Machine.LetBindings   (LetBinding(body))
 import Parsley.Internal.Backend.Machine.LetRecBuilder (letRec)
+import Parsley.Internal.Backend.Machine.Ops
 import Parsley.Internal.Backend.Machine.Types         (MachineMonad, Machine(..), run)
 import Parsley.Internal.Backend.Machine.Types.Context
+import Parsley.Internal.Backend.Machine.Types.Coins   (willConsume, int)
 import Parsley.Internal.Backend.Machine.Types.Offset  (mkOffset, offset)
-import Parsley.Internal.Backend.Machine.Ops
 import Parsley.Internal.Backend.Machine.Types.State   (Γ(..), OpStack(..))
 import Parsley.Internal.Common                        (Fix4, cata4, One, Code, Vec(..), Nat(..))
 import Parsley.Internal.Trace                         (Trace(trace))
@@ -46,18 +47,18 @@
 
 @since 1.0.0.0
 -}
-eval :: forall o a. (Trace, Ops o) 
+eval :: forall o a. (Trace, Ops o)
      => Code (InputDependant (Rep o)) -- ^ The input as provided by the user.
      -> LetBinding o a a              -- ^ The binding to be generated.
      -> DMap MVar (LetBinding o a)    -- ^ The map of all other required bindings.
      -> Code (Maybe a)                -- ^ The code for this parser.
-eval input (LetBinding !p _) fs = trace "EVALUATING TOP LEVEL" [|| runST $
+eval input binding fs = trace "EVALUATING TOP LEVEL" [|| runST $
   do let !(# next, more, offset #) = $$input
      $$(let ?ops = InputOps [||more||] [||next||]
         in letRec fs
              nameLet
              (\μ exp rs names -> buildRec μ rs (emptyCtx names) (readyMachine exp))
-             (run (readyMachine p) (Γ Empty halt (mkOffset [||offset||] 0) (VCons fatal VNil)) . nextUnique . emptyCtx))
+             (run (readyMachine (body binding)) (Γ Empty halt (mkOffset [||offset||] 0) (VCons fatal VNil)) . nextUnique . emptyCtx))
   ||]
   where
     nameLet :: MVar x -> String
@@ -97,7 +98,7 @@
 evalRet = return $! retCont >>= resume
 
 evalCall :: forall s o a x xs n r. MarshalOps o => MVar x -> Machine s o (x : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
-evalCall μ (Machine k) = freshUnique $ \u -> liftM2 (\mk sub γ@Γ{..} -> callWithContinuation @o sub (suspend mk γ u) (offset input) handlers) k (askSub μ)
+evalCall μ (Machine k) = freshUnique $ \u -> liftM2 (callCC u) (askSub μ) k
 
 evalJump :: forall s o a x n. MarshalOps o => MVar x -> MachineMonad s o '[] (Succ n) x a
 evalJump μ = askSub μ <&> \sub Γ{..} -> callWithContinuation @o sub retCont (offset input) handlers
@@ -112,18 +113,34 @@
 evalLift2 f (Machine k) = k <&> \m γ -> m (γ {operands = let Op y (Op x xs) = operands γ in Op (ap2 f x y) xs})
 
 evalSat :: (?ops :: InputOps (Rep o), PositionOps (Rep o), Trace) => Defunc (Char -> Bool) -> Machine s o (Char : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
-evalSat p (Machine k) = do
+evalSat p k@(Machine k') = do
   bankrupt <- asks isBankrupt
   hasChange <- asks hasCoin
-  if | bankrupt -> maybeEmitCheck (Just 1) <$> k
-     | hasChange -> maybeEmitCheck Nothing <$> local spendCoin k
-     | otherwise -> trace "I have a piggy :)" $ local breakPiggy (asks ((maybeEmitCheck . Just) . coins) <*> local spendCoin k)
+  if | bankrupt -> emitCheckAndFetch 1 k
+     | hasChange -> local spendCoin (satFetch k)
+     | otherwise -> trace "I have a piggy :)" $
+        local breakPiggy $
+          do check <- asks (emitCheckAndFetch . coins)
+             check (Machine (local spendCoin k'))
   where
-    maybeEmitCheck Nothing mk γ = sat (ap p) mk (raise γ) γ
-    maybeEmitCheck (Just n) mk γ =
-      --[|| let bad = $$(raise γ) in $$(emitLengthCheck n (sat (ap p) mk [||bad||]) [||bad||] γ)||]
-      emitLengthCheck n (sat (ap p) mk (raise γ) γ) (raise γ) (input γ)
+    satFetch :: (?ops :: InputOps (Rep o))
+             => Machine s o (Char : xs) (Succ n) r a
+             -> MachineMonad s o xs (Succ n) r a
+    satFetch mk = reader $ \ctx γ ->
+      sat (ap p) (readChar ctx (fetch (input γ)))
+                 (continue mk γ)
+                 (raise γ)
 
+    emitCheckAndFetch :: (?ops :: InputOps (Rep o), PositionOps (Rep o))
+                      => Int
+                      -> Machine s o (Char : xs) (Succ n) r a
+                      -> MachineMonad s o xs (Succ n) r a
+    emitCheckAndFetch n mk = do
+      sat <- satFetch mk
+      return $ \γ -> emitLengthCheck n (sat γ) (raise γ) (input γ)
+
+    continue mk γ c input' = run mk (γ {input = input', operands = Op c (operands γ)})
+
 evalEmpt :: MachineMonad s o xs (Succ n) r a
 evalEmpt = return $! raise
 
@@ -185,15 +202,15 @@
   in dup x $ \dupx -> mk (γ {operands = Op dupx (Op dupx xs)})
 
 evalMake :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
-evalMake σ a k = asks $ \ctx γ ->
+evalMake σ a k = reader $ \ctx γ ->
   let Op x xs = operands γ
   in newΣ σ a x (run k (γ {operands = xs})) ctx
 
 evalGet :: ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
-evalGet σ a k = asks $ \ctx γ -> readΣ σ a (\x -> run k (γ {operands = Op x (operands γ)})) ctx
+evalGet σ a k = reader $ \ctx γ -> readΣ σ a (\x -> run k (γ {operands = Op x (operands γ)})) ctx
 
 evalPut :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
-evalPut σ a k = asks $ \ctx γ ->
+evalPut σ a k = reader $ \ctx γ ->
   let Op x xs = operands γ
   in writeΣ σ a x (run k (γ {operands = xs})) ctx
 
@@ -214,6 +231,21 @@
 evalMeta (AddCoins coins) (Machine k) =
   do requiresPiggy <- asks hasCoin
      if requiresPiggy then local (storePiggy coins) k
-     else local (giveCoins coins) k <&> \mk γ -> emitLengthCheck coins (mk γ) (raise γ) (input γ)
-evalMeta (RefundCoins coins) (Machine k) = local (giveCoins coins) k
-evalMeta (DrainCoins coins) (Machine k) = liftM2 (\n mk γ -> emitLengthCheck n (mk γ) (raise γ) (input γ)) (asks ((coins -) . liquidate)) k
+     else local (giveCoins coins) k <&> \mk γ -> emitLengthCheck (willConsume coins) (mk γ) (raise γ) (input γ)
+evalMeta (RefundCoins coins) (Machine k) = local (refundCoins coins) k
+-- No interaction with input reclamation here!
+evalMeta (DrainCoins coins) (Machine k) =
+  -- If there are enough coins left to cover the cost, no length check is required
+  -- Otherwise, the full length check is required (partial doesn't work until the right offset is reached)
+  liftM2 (\canAfford mk γ -> if canAfford then mk γ else emitLengthCheck (willConsume coins) (mk γ) (raise γ) (input γ))
+         (asks (canAfford (willConsume coins)))
+         k
+evalMeta (GiveBursary coins) (Machine k) = local (giveCoins coins) k
+evalMeta (PrefetchChar check) k =
+  do bankrupt <- asks isBankrupt
+     when (not bankrupt && check) (error "must be bankrupt to generate a prefetch check")
+     mkCheck check (reader $ \ctx γ -> prefetch (input γ) ctx (run k γ))
+  where
+    mkCheck True  k = local (giveCoins (int 1)) k <&> \mk γ -> emitLengthCheck 1 (mk γ) (raise γ) (input γ)
+    mkCheck False k = k
+    prefetch o ctx k = fetch o (\c o' -> k (addChar c o' ctx))
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputOps.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputOps.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputOps.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputOps.hs
@@ -29,9 +29,12 @@
 import GHC.Exts                                  (Int(..), Char(..), TYPE, Int#)
 import GHC.ForeignPtr                            (ForeignPtr(..))
 import GHC.Prim                                  (indexWideCharArray#, indexWord16Array#, readWord8OffAddr#, word2Int#, chr#, touch#, realWorld#, plusAddr#, (+#), (-#))
-import Parsley.Internal.Backend.Machine.InputRep
+import Parsley.Internal.Backend.Machine.InputRep (Stream(..), CharList(..), Text16(..), Rep, UnpackedLazyByteString,
+                                                  offWith, emptyUnpackedLazyByteString, intSame, intLess,
+                                                  offsetText, offWithSame, offWithShiftRight, dropStream,
+                                                  textShiftRight, textShiftLeft, byteStringShiftRight,
+                                                  byteStringShiftLeft, max#)
 import Parsley.Internal.Common.Utils             (Code)
-import Parsley.Internal.Core.InputTypes
 
 import qualified Data.ByteString.Lazy.Internal as Lazy (ByteString(..))
 --import qualified Data.Text                     as Text (length, index)
@@ -126,7 +129,7 @@
                                          , _next       :: Code (rep -> (# Char, rep #)) -- ^ Read the next character (without checking existence)
                                          }
 {-|
-Wraps around `InputOps` and `_more`. 
+Wraps around `InputOps` and `_more`.
 
 Queries the input to see if another character may be consumed.
 
@@ -180,6 +183,7 @@
 instance InputPrep CharList where
   prepare qinput = [||
       let CharList input = $$qinput
+          next :: (# Int#, [Char] #) -> (# Char, (# Int#, [Char] #) #)
           next (# i#, c:cs #) = (# c, (# i# +# 1#, cs #) #)
           more :: (# Int#, [Char] #) -> Bool
           more (# _, [] #) = False
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputRep.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputRep.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputRep.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/InputRep.hs
@@ -29,16 +29,18 @@
     -- * @LazyByteString@ Operations
     UnpackedLazyByteString, emptyUnpackedLazyByteString,
     -- * @Stream@ Operations
-    Stream, dropStream,
+    dropStream,
     -- * @Text@ Operations
     offsetText,
     -- * Crucial Exposed Functions
-    {- | 
+    {- |
     These functions must be exposed, since they can appear
     in the generated code.
     -}
     textShiftRight, textShiftLeft,
-    byteStringShiftRight, byteStringShiftLeft
+    byteStringShiftRight, byteStringShiftLeft,
+    -- * Re-exports
+    module Parsley.Internal.Core.InputTypes
   ) where
 
 import Data.Array.Unboxed                (UArray)
@@ -50,7 +52,7 @@
 import GHC.ForeignPtr                    (ForeignPtr(..), ForeignPtrContents)
 import GHC.Prim                          (Int#, Addr#, nullAddr#)
 import Parsley.Internal.Common.Utils     (Code)
-import Parsley.Internal.Core.InputTypes  (Text16, CharList, Stream(..))
+import Parsley.Internal.Core.InputTypes  (Text16(..), CharList(..), Stream(..))
 
 import qualified Data.ByteString.Lazy.Internal as Lazy (ByteString(..))
 
@@ -107,7 +109,7 @@
 -}
 type RepKind :: Type -> RuntimeRep
 type family RepKind input where
-  RepKind [Char] = IntRep 
+  RepKind [Char] = IntRep
   RepKind (UArray Int Char) = IntRep
   RepKind Text16 = IntRep
   RepKind ByteString = IntRep
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Ops.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Ops.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Ops.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Ops.hs
@@ -26,7 +26,7 @@
     -- * Core Machine Operations
     dup, returnST,
     -- ** Abstracted Input Operations
-    sat, emitLengthCheck,
+    sat, emitLengthCheck, fetch,
     -- ** Register Operations
     newΣ, writeΣ, readΣ,
     -- ** Handler Operations
@@ -39,7 +39,7 @@
     -- ** Continuation Operations
     -- *** Basic continuations and operations
     halt, noreturn,
-    resume, callWithContinuation,
+    resume, callWithContinuation, callCC,
     -- *** Continuation preparation
     suspend,
     -- ** Join Point Operations
@@ -73,16 +73,17 @@
 import Parsley.Internal.Backend.Machine.InputOps       (PositionOps(..), LogOps(..), InputOps, next, more)
 import Parsley.Internal.Backend.Machine.InputRep       (Rep)
 import Parsley.Internal.Backend.Machine.Instructions   (Access(..))
-import Parsley.Internal.Backend.Machine.LetBindings    (Regs(..))
+import Parsley.Internal.Backend.Machine.LetBindings    (Regs(..), Metadata(failureInputCharacteristic, successInputCharacteristic), InputCharacteristic(..))
 import Parsley.Internal.Backend.Machine.Types          (MachineMonad, Machine(..), run)
 import Parsley.Internal.Backend.Machine.Types.Context
 import Parsley.Internal.Backend.Machine.Types.Dynamics (DynFunc, DynCont, DynHandler)
-import Parsley.Internal.Backend.Machine.Types.Offset   (Offset(..), moveOne, mkOffset)
 import Parsley.Internal.Backend.Machine.Types.State    (Γ(..), OpStack(..))
 import Parsley.Internal.Backend.Machine.Types.Statics
 import Parsley.Internal.Common                         (One, Code, Vec(..), Nat(..))
 import System.Console.Pretty                           (color, Color(Green, White, Red, Blue))
 
+import Parsley.Internal.Backend.Machine.Types.Offset as Offset (Offset(..), moveOne, mkOffset, moveN)
+
 {- General Operations -}
 {-|
 Creates a let-binding that allows the same value to be
@@ -113,17 +114,25 @@
 from the input within @γ@, executing the failure code if it does not
 exist or does not match.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-sat :: (?ops :: InputOps (Rep o))
-    => (Defunc Char -> Defunc Bool)        -- ^ Predicate to test the character with.
-    -> (Γ s o (Char : xs) n r a -> Code b) -- ^ Code to execute with updated state on success.
-    -> Code b                              -- ^ Code to execute on any failure.
-    -> Γ s o xs n r a                      -- ^ State @γ@ which contains the input.
+sat :: (Defunc Char -> Defunc Bool)                         -- ^ Predicate to test the character with.
+    -> ((Code Char -> Offset o -> aux -> Code b) -> Code b) -- ^ The source of the character
+    -> (Defunc Char -> Offset o -> aux -> Code b)           -- ^ Code to execute on success.
+    -> Code b                                               -- ^ Code to execute on failure.
     -> Code b
-sat p k bad γ@Γ{..} = next (offset input) $ \c offset' -> let v = FREEVAR c in _if (p v) (k (γ {operands = Op v operands, input = moveOne input offset'})) bad
+sat p src good bad = src $ \c input' aux -> let v = FREEVAR c in _if (p v) (good v input' aux) bad
 
 {-|
+Consumes the next character and adjusts the offset to match.
+
+@since 1.5.0.0
+-}
+fetch :: (?ops :: InputOps (Rep o))
+      => Offset o -> (Code Char -> Offset o -> Code b) -> Code b
+fetch input k = next (offset input) $ \c offset' -> k c (moveOne input offset')
+
+{-|
 Emits a length check for a number of characters \(n\) in the most efficient
 way it can. It takes two continuations a @good@ and a @bad@: the @good@ is used
 when the \(n\) characters are available and the @bad@ when they are not.
@@ -240,6 +249,8 @@
 
 @since 1.4.0.0
 -}
+--TODO: annoyingly, a `try` on its own binds a handler, even though it's footprint is negligable
+--      we should introduce a `noBinding` flag to the Always handler to mitigate this.
 bindAlwaysHandler :: forall s o xs n r a b. HandlerOps o
                   => Γ s o xs n r a                    -- ^ The state from which to capture the offset.
                   -> StaHandlerBuilder s o a           -- ^ The handler waiting to receive the captured offset and be bound.
@@ -315,21 +326,43 @@
                      -> Code (Rep o)                    -- ^ The input to feed to @sub@.
                      -> Vec (Succ n) (StaHandler s o a) -- ^ The stack from which to obtain the handler to pass to @sub@.
                      -> Code (ST s (Maybe a))
-callWithContinuation sub ret input (VCons h _) = sub (dynCont ret) input (dynHandler h)
+callWithContinuation sub ret input (VCons h _) = staSubroutine# sub (dynCont ret) input (dynHandler h (failureInputCharacteristic (meta sub)))
 
 -- Continuation preparation
 {-|
 Converts a partial parser into a return continuation in a manner similar
 to `buildHandler`.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
 suspend :: (Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -- ^ The partial parser to turn into a return continuation.
         -> Γ s o xs n r a                                  -- ^ The state to execute the continuation with.
-        -> Word                                            -- ^ The unique identifier to assign to the continuation's input.
+        -> (Code (Rep o) -> Offset o)                      -- ^ Function used to generate the offset
         -> StaCont s o a x
-suspend m γ u = mkStaCont $ \x o# -> m (γ {operands = Op (FREEVAR x) (operands γ), input = mkOffset o# u})
+suspend m γ off = mkStaCont $ \x o# -> m (γ {operands = Op (FREEVAR x) (operands γ), input = off o#})
 
+{-|
+Combines `suspend` and `callWithContinuation`, simultaneously performing
+an optimisation on the offset if the subroutine has known input characteristics.
+
+@since 1.5.0.0
+-}
+callCC :: forall s o xs n r a x. MarshalOps o
+       => Word                                                   --
+       -> StaSubroutine s o a x                                  -- ^ The subroutine @sub@ that will be called.
+       -> (Γ s o (x : xs) (Succ n) r a -> Code (ST s (Maybe a))) -- ^ The return continuation to generate
+       -> Γ s o xs (Succ n) r a                                  --
+       -> Code (ST s (Maybe a))
+callCC u sub k γ = callWithContinuation sub (suspend k γ (chooseOffset (successInputCharacteristic (meta sub)) o)) (offset o) (handlers γ)
+  where
+    o :: Offset o
+    o = input γ
+
+    chooseOffset :: InputCharacteristic -> Offset o -> Code (Rep o) -> Offset o
+    chooseOffset (AlwaysConsumes n) o qo# = moveN n o qo#
+    chooseOffset NeverConsumes      o qo# = o {offset = qo#}
+    chooseOffset MayConsume         _ qo# = mkOffset qo# u
+
 {- Join Point Operations -}
 {-|
 Wraps around `setupJoinPoint#` to make a join point and register it
@@ -371,7 +404,7 @@
     bindIter# @o (offset o) $ \qloop qo# ->
       let off = mkOffset qo# u
       in run l (Γ Empty noreturn off (VCons (mkStaHandlerDyn (Just off) [||$$qhandler $$(qo#)||]) VNil))
-               (voidCoins (insertSub μ (\_ o# _ -> [|| $$qloop $$(o#) ||]) ctx))
+               (voidCoins (insertSub μ (mkStaSubroutine $ \_ o# _ -> [|| $$qloop $$(o#) ||]) ctx))
 
 {-|
 Similar to `buildIterAlways`, but builds a handler that performs in
@@ -397,7 +430,7 @@
         bindIter# @o (offset o) $ \qloop qo# ->
           let off = mkOffset qo# u
           in run l (Γ Empty noreturn off (VCons (mkStaHandlerFull off [||$$qhandler $$(qo#)||] [||$$qyes $$(qo#)||] [||$$qno $$(qo#)||]) VNil))
-                   (voidCoins (insertSub μ (\_ o# _ -> [|| $$qloop $$(o#) ||]) ctx))
+                   (voidCoins (insertSub μ (mkStaSubroutine $ \_ o# _ -> [|| $$qloop $$(o#) ||]) ctx))
 
 {- Recursion Operations -}
 {-|
@@ -406,30 +439,34 @@
 This eliminates recursive calls from having to pass all of the same registers
 each time round.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
 buildRec :: forall rs s o a r. RecBuilder o
          => MVar r                  -- ^ The name of the binding.
          -> Regs rs                 -- ^ The registered required by the binding.
          -> Ctx s o a               -- ^ The context to re-insert the register-less binding
          -> Machine s o '[] One r a -- ^ The body of the binding.
+         -> Metadata                -- ^ The metadata associated with the binding
          -> DynFunc rs s o a r
-buildRec μ rs ctx k =
+buildRec μ rs ctx k meta =
   takeFreeRegisters rs ctx $ \ctx ->
     bindRec# @o $ \qself qret qo# qh ->
       run k (Γ Empty (mkStaContDyn qret) (mkOffset qo# 0) (VCons (mkStaHandlerDyn Nothing qh) VNil))
-            (insertSub μ (\k o# h -> [|| $$qself $$k $$(o#) $$h ||]) (nextUnique ctx))
+            (insertSub μ (mkStaSubroutineMeta meta $ \k o# h -> [|| $$qself $$k $$(o#) $$h ||]) (nextUnique ctx))
 
 {- Marshalling Operations -}
 {-|
 Wraps around `dynHandler#`, but ensures that if the `StaHandler`
 originated from a `DynHandler` itself, that no work is performed.
 
-@since 1.4.0.0
+Takes in an `InputCharacteristic`, which is used to refine the
+handler given knowledge about how it might be used.
+
+@since 1.5.0.0
 -}
-dynHandler :: forall s o a. MarshalOps o => StaHandler s o a -> DynHandler s o a
-dynHandler sh@(StaHandler _ _ Nothing) = dynHandler# @o (staHandler# sh)
-dynHandler (StaHandler _ _ (Just dh))  = dh
+dynHandler :: forall s o a. MarshalOps o => StaHandler s o a -> InputCharacteristic -> DynHandler s o a
+dynHandler (StaHandler _ sh Nothing)  = dynHandler# @o . staHandlerCharacteristicSta sh
+dynHandler (StaHandler _ _ (Just dh)) = staHandlerCharacteristicDyn dh (dynHandler# @o . const)
 
 {-|
 Wraps around `dynCont#`, but ensures that if the `StaCont`
@@ -468,7 +505,7 @@
               -> Code String
 preludeString name dir γ ctx ends = [|| concat [$$prelude, $$eof, ends, '\n' : $$caretSpace, color Blue "^"] ||]
   where
-    Offset {offset} = input γ
+    offset          = Offset.offset (input γ)
     indent          = replicate (debugLevel ctx * 2) ' '
     start           = shiftLeft offset [||5#||]
     end             = shiftRight offset [||5#||]
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Context.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Context.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Context.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Context.hs
@@ -31,8 +31,8 @@
     -- $reg-doc
 
     -- ** Putters
-    insertNewΣ, cacheΣ, 
-    -- ** Getters 
+    insertNewΣ, cacheΣ,
+    -- ** Getters
     concreteΣ, cachedΣ,
     takeFreeRegisters,
 
@@ -48,9 +48,11 @@
     -- $piggy-doc
 
     -- ** Modifiers
-    storePiggy, breakPiggy, spendCoin, giveCoins, voidCoins, 
+    storePiggy, breakPiggy, spendCoin, giveCoins, refundCoins, voidCoins,
     -- ** Getters
-    coins, hasCoin, isBankrupt, liquidate
+    coins, hasCoin, isBankrupt, canAfford,
+    -- ** Input Reclamation
+    addChar, readChar
   ) where
 
 import Control.Exception                               (Exception, throw)
@@ -62,12 +64,15 @@
 import Parsley.Internal.Backend.Machine.Defunc         (Defunc)
 import Parsley.Internal.Backend.Machine.Identifiers    (MVar(..), ΣVar(..), ΦVar, IMVar, IΣVar)
 import Parsley.Internal.Backend.Machine.LetBindings    (Regs(..))
+import Parsley.Internal.Backend.Machine.Types.Coins    (Coins, willConsume, canReclaim)
 import Parsley.Internal.Backend.Machine.Types.Dynamics (DynFunc, DynSubroutine)
+import Parsley.Internal.Backend.Machine.Types.Offset   (Offset)
 import Parsley.Internal.Backend.Machine.Types.Statics  (QSubroutine(..), StaFunc, StaSubroutine, StaCont)
-import Parsley.Internal.Common                         (Queue, enqueue, dequeue, Code)
+import Parsley.Internal.Common                         (Queue, enqueue, dequeue, Code, RewindQueue)
 
-import qualified Data.Dependent.Map as DMap             ((!), insert, empty, lookup)
-import qualified Parsley.Internal.Common.Queue as Queue (empty, null, foldr)
+import qualified Data.Dependent.Map                           as DMap  ((!), insert, empty, lookup)
+import qualified Parsley.Internal.Common.QueueLike            as Queue (empty, null)
+import qualified Parsley.Internal.Common.RewindQueue          as Queue (rewind)
 
 -- Core Data-types
 {-|
@@ -77,13 +82,14 @@
 
 @since 1.0.0.0
 -}
-data Ctx s o a = Ctx { μs         :: DMap MVar (QSubroutine s o a) -- ^ Map of subroutine bindings.
-                     , φs         :: DMap ΦVar (QJoin s o a)       -- ^ Map of join point bindings.
-                     , σs         :: DMap ΣVar (Reg s)             -- ^ Map of available registers.
-                     , debugLevel :: Int                           -- ^ Approximate depth of debug combinator.
-                     , coins      :: Int                           -- ^ Number of tokens free to consume without length check.
-                     , offsetUniq :: Word                          -- ^ Next unique offset identifier.
-                     , piggies    :: Queue Int                     -- ^ Queue of future length check credit.
+data Ctx s o a = Ctx { μs         :: DMap MVar (QSubroutine s o a)     -- ^ Map of subroutine bindings.
+                     , φs         :: DMap ΦVar (QJoin s o a)           -- ^ Map of join point bindings.
+                     , σs         :: DMap ΣVar (Reg s)                 -- ^ Map of available registers.
+                     , debugLevel :: Int                               -- ^ Approximate depth of debug combinator.
+                     , coins      :: Int                               -- ^ Number of tokens free to consume without length check.
+                     , offsetUniq :: Word                              -- ^ Next unique offset identifier.
+                     , piggies    :: Queue Coins                       -- ^ Queue of future length check credit.
+                     , knownChars :: RewindQueue (Code Char, Offset o) -- ^ Characters that can be reclaimed on backtrack.
                      }
 
 {-|
@@ -101,7 +107,7 @@
 @since 1.0.0.0
 -}
 emptyCtx :: DMap MVar (QSubroutine s o a) -> Ctx s o a
-emptyCtx μs = Ctx μs DMap.empty DMap.empty 0 0 0 Queue.empty
+emptyCtx μs = Ctx μs DMap.empty DMap.empty 0 0 0 Queue.empty Queue.empty
 
 -- Subroutines
 {- $sub-doc
@@ -173,10 +179,10 @@
 Across recursion and call-boundaries, these materialise as @STRef@s. These are stored
 in the `Ctx` and can be looked up when required.
 
-However, parsley does not mandate that registers /must/ exist in this form. Registers 
-can be subject to caching, where a register's static "most-recently known" may be 
+However, parsley does not mandate that registers /must/ exist in this form. Registers
+can be subject to caching, where a register's static "most-recently known" may be
 stored within the `Ctx` in addition to the "true" binding. This can, in effect, mean
-that registers do not exist at runtime. Both forms of register data can be extracted, 
+that registers do not exist at runtime. Both forms of register data can be extracted,
 however exceptions will guard against mis-management.
 -}
 data Reg s x = Reg { getReg    :: Maybe (Code (STRef s x)) -- ^ The "true" register
@@ -318,7 +324,7 @@
   a length check for value of the coins in the bank
 * When all the piggy-banks are exhausted, a length check must be generated for each
   token that is consumed.
-* When adding coins into the system, if the `Ctx` is bankrupt, then the coins are added 
+* When adding coins into the system, if the `Ctx` is bankrupt, then the coins are added
   immediately along with a length check, otherwise a piggy-bank is added.
 
 These are the basic principles behind this system, and it works effectively. There are some
@@ -326,14 +332,18 @@
 reason why piggy-banks are stored in the context and /not/ consumed immediately to add to
 the coin count is so that length checks are delayed to the last possible moment: you should
 have used all of your current allocation before asking for more!
+
+In addition to this above system, Parsley stores previously read characters in a rewind queue:
+this means that when backtracking is performed (i.e. when looking ahead) the characters can be
+statically rewound and made available for free.
 -}
 {-|
 Place a piggy-bank into the reserve, delaying the corresponding length check until it is
 broken.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-storePiggy :: Int -> Ctx s o a -> Ctx s o a
+storePiggy :: Coins -> Ctx s o a -> Ctx s o a
 storePiggy coins ctx = ctx {piggies = enqueue coins (piggies ctx)}
 
 {-|
@@ -344,7 +354,7 @@
 @since 1.0.0.0
 -}
 breakPiggy :: Ctx s o a -> Ctx s o a
-breakPiggy ctx = let (coins, piggies') = dequeue (piggies ctx) in ctx {coins = coins, piggies = piggies'}
+breakPiggy ctx = let (coins, piggies') = dequeue (piggies ctx) in ctx {coins = willConsume coins, piggies = piggies'}
 
 {-|
 Does the context have coins available?
@@ -352,7 +362,7 @@
 @since 1.0.0.0
 -}
 hasCoin :: Ctx s o a -> Bool
-hasCoin = (> 0) . coins
+hasCoin = canAfford 1
 
 {-|
 Is it the case that there are no coins /and/ no piggy-banks remaining?
@@ -373,29 +383,66 @@
 {-|
 Adds coins into the current supply.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-giveCoins :: Int -> Ctx s o a -> Ctx s o a
-giveCoins c ctx = ctx {coins = coins ctx + c}
+giveCoins :: Coins -> Ctx s o a -> Ctx s o a
+giveCoins c ctx = ctx {coins = coins ctx + willConsume c}
 
 {-|
+Adds coins into the current supply.
+
+@since 1.5.0.0
+-}
+refundCoins :: Coins -> Ctx s o a -> Ctx s o a
+refundCoins c ctx = ctx { coins = coins ctx + willConsume c
+                        , knownChars = Queue.rewind (canReclaim c) (knownChars ctx)
+                        }
+
+{-|
 Removes all coins and piggy-banks, such that @isBankrupt == True@.
 
 @since 1.0.0.0
 -}
 voidCoins :: Ctx s o a -> Ctx s o a
-voidCoins ctx = ctx {coins = 0, piggies = Queue.empty}
+voidCoins ctx = ctx {coins = 0, piggies = Queue.empty, knownChars = Queue.empty}
 
 {-|
-Collect all coins and the value of every piggy bank.
+Asks if the current coin total can afford a charge of \(n\) characters.
 
-This is used when a join-point is called, so that a length check can be
-generated to cover the cost of the binding.
+This is used by `DrainCoins`, which will have to emit a full length check
+of size \(n\) if this quota cannot be reached.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-liquidate :: Ctx s o a -> Int
-liquidate ctx = Queue.foldr (+) (coins ctx) (piggies ctx)
+canAfford :: Int -> Ctx s o a -> Bool
+canAfford n = (>= n) . coins
+
+{-|
+Caches a known character and the next offset into the context so that it
+can be retrieved later.
+
+@since 1.5.0.0
+-}
+addChar :: Code Char -> Offset o -> Ctx s o a -> Ctx s o a
+addChar c o ctx = ctx { knownChars = enqueue (c, o) (knownChars ctx) }
+
+{-|
+Reads a character from the context's retrieval queue if one exists.
+If not, reads a character from another given source (and adds it to the
+rewind buffer).
+
+@since 1.5.0.0
+-}
+readChar :: Ctx s o a                                      -- ^ The original context.
+         -> ((Code Char -> Offset o -> Code b) -> Code b)  -- ^ The fallback source of input.
+         -> (Code Char -> Offset o -> Ctx s o a -> Code b) -- ^ The continuation that needs the read characters and updated context.
+         -> Code b
+readChar ctx fallback k
+  | reclaimable = unsafeReadChar ctx k
+  | otherwise   = fallback $ \c o -> unsafeReadChar (addChar c o ctx) k
+  where
+    reclaimable = not (Queue.null (knownChars ctx))
+    unsafeReadChar ctx k = let ((c, o), q) = dequeue (knownChars ctx) in k c o (ctx { knownChars = q })
 
 -- Exceptions
 newtype MissingDependency = MissingDependency IMVar deriving anyclass Exception
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Offset.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Offset.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Offset.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Offset.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DerivingStrategies #-}
 {-|
 Module      : Parsley.Internal.Backend.Machine.Types.Offset
 Description : Statically refined offsets.
@@ -11,7 +12,9 @@
 
 @since 1.4.0.0
 -}
-module Parsley.Internal.Backend.Machine.Types.Offset (module Parsley.Internal.Backend.Machine.Types.Offset) where
+module Parsley.Internal.Backend.Machine.Types.Offset (
+    Offset, mkOffset, offset, moveOne, moveN, same
+  ) where
 
 import Parsley.Internal.Backend.Machine.InputRep    (Rep)
 import Parsley.Internal.Common.Utils                (Code)
@@ -19,10 +22,10 @@
 {-|
 Augments a regular @'Code' ('Rep' o)@ with information about its origins and
 how much input is known to have been consumed since it came into existence.
-This can be used to statically evaluate handlers (see 
+This can be used to statically evaluate handlers (see
 `Parsley.Internal.Backend.Machine.Types.Statics.staHandlerEval`).
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
 data Offset o = Offset {
     -- | The underlying code that represents the current offset into the input.
@@ -30,10 +33,12 @@
     -- | The unique identifier that determines where this offset originated from.
     unique :: Word,
     -- | The amount of input that has been consumed on this offset since it was born.
-    moved  :: Word
+    moved  :: Amount
   }
-instance Show (Offset o) where show o = show (unique o) ++ "+" ++ show (moved o)
 
+data Amount = Amount Word {- ^ The multiplicity. -} Word {- ^ The additive offset. -}
+  deriving stock Eq
+
 {-|
 Given two `Offset`s, this determines whether or not they represent the same
 offset into the input stream at runtime. This comparison only makes sense when
@@ -53,13 +58,43 @@
 @since 1.4.0.0
 -}
 moveOne :: Offset o -> Code (Rep o) -> Offset o
-moveOne off o = off { offset = o, moved = moved off + 1 }
+moveOne = moveN (Just 1)
 
 {-|
+Updates an `Offset` with its new underlying representation of a real
+runtime offset and records that several more characters have been consumed.
+Here, `Nothing` represents an unknown but non-zero amount of characters.
+
+@since 1.5.0.0
+-}
+moveN :: Maybe Word -> Offset o -> Code (Rep o) -> Offset o
+moveN n off o = off { offset = o, moved = moved off `add` toAmount n }
+  where
+    toAmount :: Maybe Word -> Amount
+    toAmount Nothing = Amount 1 0
+    toAmount (Just n) = Amount 0 n
+
+{-|
 Makes a fresh `Offset` that has not had any input consumed off of it
 yet.
 
 @since 1.4.0.0
 -}
 mkOffset :: Code (Rep o) -> Word -> Offset o
-mkOffset offset unique = Offset offset unique 0
+mkOffset offset unique = Offset offset unique (Amount 0 0)
+
+add :: Amount -> Amount -> Amount
+add a1@(Amount n i) a2@(Amount m j)
+  -- If the multiplicites don't match then this is _even_ more unknowable
+  | n /= m, n /= 0, m /= 0 = Amount (n + m) 0
+  -- This is a funny case, it shouldn't happen and it's not really clear what happens if it does
+  | n /= 0, m /= 0         = error ("adding " ++ show a1 ++ " and " ++ show a2 ++ " makes no sense?")
+  -- If one of the multiplicites is 0 then the offset can be added
+  | otherwise              = Amount (max n m) (i + j)
+
+-- Instances
+instance Show (Offset o) where
+  show o = show (unique o) ++ "+" ++ show (moved o)
+
+instance Show Amount where
+  show (Amount n m) = show n ++ "*n+" ++ show m
diff --git a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Statics.hs b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Statics.hs
--- a/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Statics.hs
+++ b/src/ghc-8.10+/Parsley/Internal/Backend/Machine/Types/Statics.hs
@@ -17,15 +17,16 @@
 -}
 module Parsley.Internal.Backend.Machine.Types.Statics (
     -- * Handlers
-    StaHandler#, StaHandler(..),
+    StaHandler#, StaHandler(..), StaHandlerCase, WStaHandler#, WDynHandler,
 
     -- ** @StaHandler@ Builders
     -- | The following functions are builders of `StaHandler`.
-    mkStaHandler, mkStaHandlerNoOffset, mkStaHandlerDyn, mkStaHandlerFull, 
-    
+    mkStaHandler, mkStaHandlerNoOffset, mkStaHandlerDyn, mkStaHandlerFull,
+
     -- ** @StaHandler@ Interpreters
     -- | The following functions interpret or extract information from `StaHandler`.
     staHandler#, staHandlerEval,
+    staHandlerCharacteristicSta, staHandlerCharacteristicDyn,
 
     -- * Return Continuations
     StaCont#, StaCont(..),
@@ -33,8 +34,12 @@
     staCont#,
 
     -- * Subroutines
-    QSubroutine(..), StaSubroutine, StaFunc,
-    qSubroutine
+    QSubroutine(..), StaSubroutine, StaSubroutine#, StaFunc,
+    -- ** Subroutine Builders
+    qSubroutine, mkStaSubroutine, mkStaSubroutineMeta,
+
+    -- ** Subroutine Extractors
+    staSubroutine#, meta,
   ) where
 
 import Control.Monad.ST                                (ST)
@@ -42,7 +47,7 @@
 import Data.Kind                                       (Type)
 import Data.Maybe                                      (fromMaybe)
 import Parsley.Internal.Backend.Machine.InputRep       (Rep)
-import Parsley.Internal.Backend.Machine.LetBindings    (Regs(..))
+import Parsley.Internal.Backend.Machine.LetBindings    (Regs(..), Metadata, newMeta, InputCharacteristic(..))
 import Parsley.Internal.Backend.Machine.Types.Dynamics (DynCont, DynHandler, DynFunc)
 import Parsley.Internal.Backend.Machine.Types.Offset   (Offset(offset), same)
 import Parsley.Internal.Common.Utils                   (Code)
@@ -61,22 +66,18 @@
 mkStaHandler# dh qo# = [||$$dh $$(qo#)||]
 
 {-|
-Compared with `StaHandler#`, this type allows for the encoding of various static 
+Compared with `StaHandler#`, this type allows for the encoding of various static
 properties of handlers which can be carried around during the lifetime of the handlers.
-This information allows the engine to optimise more aggressively, leveraging 
+This information allows the engine to optimise more aggressively, leveraging
 domain-specific optimisation data.
 
-Note that @StaHandlerCase@ is not exposed, but is potentially three handlers: one for
-unknown offset cases, one for offset known to be the same, and another for offset known
-to be different (see `mkStaHandlerFull`).
-
-@since 1.4.0.0
+@since 1.5.0.0
 -}
 data StaHandler s o a =
   StaHandler
-    (Maybe (Offset o))                     -- ^ The statically bound offset for this handler, if available.
-    {-# UNPACK #-} !(StaHandlerCase s o a) -- ^ The static function representing this handler when offsets are incomparable.
-    (Maybe (DynHandler s o a))             -- ^ The dynamic handler that has been wrapped in this handler, if available.
+    (Maybe (Offset o))                         -- ^ The statically bound offset for this handler, if available.
+    (StaHandlerCase WStaHandler# s o a)        -- ^ The static function representing this handler when offsets are incomparable.
+    (Maybe (StaHandlerCase WDynHandler s o a)) -- ^ The dynamic handler that has been wrapped in this handler, if available.
 
 {-|
 Given a static handler, extracts the underlying handler which
@@ -86,10 +87,10 @@
 @since 1.4.0.0
 -}
 staHandler# :: StaHandler s o a -> StaHandler# s o a
-staHandler# (StaHandler _ sh _) = unknown sh
+staHandler# (StaHandler _ sh _) = unWrapSta (unknown sh)
 
 _mkStaHandler :: Maybe (Offset o) -> StaHandler# s o a -> StaHandler s o a
-_mkStaHandler o sh = StaHandler o (mkUnknown sh) Nothing
+_mkStaHandler o sh = StaHandler o (mkUnknownSta sh) Nothing
 
 {-|
 Augments a `StaHandler#` with information about what the offset is that
@@ -112,7 +113,7 @@
 mkStaHandlerNoOffset = _mkStaHandler Nothing
 
 {-|
-Converts a `Parsley.Internal.Machine.Types.Dynamics.DynHandler` into a 
+Converts a `Parsley.Internal.Machine.Types.Dynamics.DynHandler` into a
 `StaHandler` taking into account the possibility that captured offset
 information is available. The dynamic handler used to construct this
 static handler is maintained as the origin of the handler. This means
@@ -121,11 +122,11 @@
 @since 1.4.0.0
 -}
 mkStaHandlerDyn :: forall s o a. Maybe (Offset o) -> DynHandler s o a -> StaHandler s o a
-mkStaHandlerDyn c dh = StaHandler c (mkUnknown (mkStaHandler# @o dh)) (Just dh)
+mkStaHandlerDyn c dh = StaHandler c (mkUnknownSta (mkStaHandler# @o dh)) (Just (mkUnknownDyn dh))
 
 {-|
 When the behaviours of a handler given input that matches or does not match
-its captured offset are known, this function can be used to construct a 
+its captured offset are known, this function can be used to construct a
 `StaHandler` that stores this information. This can in turn be used in
 conjunction with `staHandlerEval` to statically refine the application of
 a handler to its argument.
@@ -138,10 +139,10 @@
                  -> DynHandler s o a       -- ^ The handler to be executed when offsets are known not to match.
                  -> StaHandler s o a       -- ^ A handler that carries this information around for later refinement.
 mkStaHandlerFull c handler yes no = StaHandler (Just c)
-  (mkFull (mkStaHandler# @o handler)
-          yes
-          (mkStaHandler# @o no))
-  (Just handler)
+  (mkFullSta (mkStaHandler# @o handler)
+             yes
+             (mkStaHandler# @o no))
+  (Just (mkFullDyn handler yes no))
 
 {-|
 Unlike `staHandler#`, which returns a handler that accepts @'Code' ('Rep' o)@, this
@@ -160,25 +161,84 @@
 -}
 staHandlerEval :: StaHandler s o a -> Offset o -> Code (ST s (Maybe a))
 staHandlerEval (StaHandler (Just c) sh _) o
-  | Just True <- same c o            = maybe (unknown sh) const (yesSame sh) (offset o)
-  | Just False <- same c o           = fromMaybe (unknown sh) (notSame sh) (offset o)
-staHandlerEval (StaHandler _ sh _) o = unknown sh (offset o)
+  | Just True <- same c o            = maybe (unWrapSta (unknown sh)) const (yesSame sh) (offset o)
+  | Just False <- same c o           = unWrapSta (fromMaybe (unknown sh) (notSame sh)) (offset o)
+staHandlerEval (StaHandler _ sh _) o = unWrapSta (unknown sh) (offset o)
 
-data StaHandlerCase s o a = StaHandlerCase {
+staHandlerCharacteristic :: StaHandlerCase h s o a -> (Code (ST s (Maybe a)) -> h s o a) -> InputCharacteristic -> h s o a
+staHandlerCharacteristic sh conv NeverConsumes      = maybe (unknown sh) conv (yesSame sh)
+staHandlerCharacteristic sh _    (AlwaysConsumes _) = fromMaybe (unknown sh) (notSame sh)
+staHandlerCharacteristic sh _    MayConsume         = unknown sh
+
+{-|
+Selects the correct case out of a `StaHandlerCase` depending on what the `InputCharacteristic` that
+governs the use of the handler is. This means that it can select any of the three cases.
+
+@since 1.5.0.0
+-}
+staHandlerCharacteristicSta :: StaHandlerCase WStaHandler# s o a -> InputCharacteristic -> StaHandler# s o a
+staHandlerCharacteristicSta h = unWrapSta . staHandlerCharacteristic h (WrapSta . const)
+
+{-|
+Selects the correct case out of a `StaHandlerCase` depending on what the `InputCharacteristic` that
+governs the use of the handler is. This means that it can select any of the three cases.
+
+@since 1.5.0.0
+-}
+staHandlerCharacteristicDyn :: StaHandlerCase WDynHandler s o a
+                            -> (Code (ST s (Maybe a)) -> DynHandler s o a) -- ^ How to convert the input-same case to a `DynHandler`.
+                            -> InputCharacteristic
+                            -> DynHandler s o a
+staHandlerCharacteristicDyn h conv = unWrapDyn . staHandlerCharacteristic h (WrapDyn . conv)
+
+{-|
+Represents potentially three handlers: one for unknown offset cases, one for offset known to be
+the same, and another for offset known to be different (see `mkStaHandlerFull`). Parameterised by
+a generic handler type, which is instantiated to one of `WStaHandler#` or `WDynHandler`.
+
+@since 1.5.0.0
+-}
+data StaHandlerCase h s (o :: Type) a = StaHandlerCase {
   -- | The static function representing this handler when offsets are incomparable.
-  unknown :: StaHandler# s o a,
+  unknown :: h s o a,
   -- | The static value representing this handler when offsets are known to match, if available.
   yesSame :: Maybe (Code (ST s (Maybe a))),
   -- | The static function representing this handler when offsets are known not to match, if available.
-  notSame :: Maybe (StaHandler# s o a)
+  notSame :: Maybe (h s o a)
 }
 
-mkUnknown :: StaHandler# s o a -> StaHandlerCase s o a
+{-|
+Wraps a `StaHandler#`.
+
+@since 1.5.0.0
+-}
+newtype WStaHandler# s o a = WrapSta { unWrapSta :: StaHandler# s o a }
+
+{-|
+Wraps a `DynHandler`.
+
+@since 1.5.0.0
+-}
+newtype WDynHandler s o a = WrapDyn { unWrapDyn :: DynHandler s o a }
+
+mkUnknown :: h s o a -> StaHandlerCase h s o a
 mkUnknown h = StaHandlerCase h Nothing Nothing
 
-mkFull :: StaHandler# s o a -> Code (ST s (Maybe a)) -> StaHandler# s o a -> StaHandlerCase s o a
+mkUnknownSta :: StaHandler# s o a -> StaHandlerCase WStaHandler# s o a
+mkUnknownSta = mkUnknown . WrapSta
+
+mkUnknownDyn :: DynHandler s o a -> StaHandlerCase WDynHandler s o a
+mkUnknownDyn = mkUnknown . WrapDyn
+
+mkFull :: h s o a -> Code (ST s (Maybe a)) -> h s o a -> StaHandlerCase h s o a
 mkFull h yes no = StaHandlerCase h (Just yes) (Just no)
 
+mkFullSta :: StaHandler# s o a -> Code (ST s (Maybe a)) -> StaHandler# s o a -> StaHandlerCase WStaHandler# s o a
+mkFullSta h yes no = mkFull (WrapSta h) yes (WrapSta no)
+
+mkFullDyn :: DynHandler s o a -> Code (ST s (Maybe a)) -> DynHandler s o a -> StaHandlerCase WDynHandler s o a
+mkFullDyn h yes no = mkFull (WrapDyn h) yes (WrapDyn no)
+
 -- Continuations
 {-|
 This represents the translation of `Parsley.Internal.Backend.Machine.Types.Base.Cont#`
@@ -198,7 +258,7 @@
 data StaCont s o a x = StaCont (StaCont# s o a x) (Maybe (DynCont s o a x))
 
 {-|
-Converts a `Parsley.Internal.Machine.Types.Dynamics.DynCont` into a 
+Converts a `Parsley.Internal.Machine.Types.Dynamics.DynCont` into a
 `StaCont`. The dynamic continuation used to construct this
 static continuation is maintained as the origin of the continuation. This means
 if it is converted back the conversion is free.
@@ -233,11 +293,40 @@
 but where the static function structure has been exposed. This allows for β-reduction
 on subroutines, a simple form of inlining optimisation: useful for iteration.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
-type StaSubroutine s o a x = DynCont s o a x -> Code (Rep o) -> DynHandler s o a -> Code (ST s (Maybe a))
+type StaSubroutine# s o a x = DynCont s o a x -> Code (Rep o) -> DynHandler s o a -> Code (ST s (Maybe a))
 
 {-|
+Packages a `StaSubroutine#` along with statically determined metadata that describes it derived from
+static analysis.
+
+@since 1.5.0.0
+-}
+data StaSubroutine s o a x = StaSubroutine {
+    -- | Extracts the underlying subroutine.
+    staSubroutine# :: StaSubroutine# s o a x,
+    -- | Extracts the metadata from a subroutine.
+    meta :: Metadata
+  }
+
+{-|
+Converts a `StaSubroutine#` into a `StaSubroutine` by providing the empty meta.
+
+@since 1.5.0.0
+-}
+mkStaSubroutine :: StaSubroutine# s o a x -> StaSubroutine s o a x
+mkStaSubroutine = mkStaSubroutineMeta newMeta
+
+{-|
+Converts a `StaSubroutine#` into a `StaSubroutine` by providing its metadata.
+
+@since 1.5.0.0
+-}
+mkStaSubroutineMeta :: Metadata -> StaSubroutine# s o a x -> StaSubroutine s o a x
+mkStaSubroutineMeta = flip StaSubroutine
+
+{-|
 This represents the translation of `Parsley.Internal.Backend.Machine.Types.Base.Func`
 but where the static function structure has been exposed. This allows for β-reduction
 on subroutines with registers, a simple form of inlining optimisation.
@@ -260,11 +349,11 @@
 on zero or more free registers into a `QSubroutine`, where the registers are
 existentially bounds to the function.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
-qSubroutine :: forall s o a x rs. DynFunc rs s o a x -> Regs rs -> QSubroutine s o a x
-qSubroutine func frees = QSubroutine (staFunc frees func) frees
+qSubroutine :: forall s o a x rs. DynFunc rs s o a x -> Regs rs -> Metadata -> QSubroutine s o a x
+qSubroutine func frees meta = QSubroutine (staFunc frees func) frees
   where
     staFunc :: forall rs. Regs rs -> DynFunc rs s o a x -> StaFunc rs s o a x
-    staFunc NoRegs func = \dk o# dh -> [|| $$func $$dk $$(o#) $$dh ||]
+    staFunc NoRegs func = StaSubroutine (\dk o# dh -> [|| $$func $$dk $$(o#) $$dh ||]) meta
     staFunc (FreeReg _ witness) func = \r -> staFunc witness [|| $$func $$r ||]
diff --git a/src/ghc-8.6+/Parsley/Internal/Backend/Machine.hs b/src/ghc-8.6+/Parsley/Internal/Backend/Machine.hs
--- a/src/ghc-8.6+/Parsley/Internal/Backend/Machine.hs
+++ b/src/ghc-8.6+/Parsley/Internal/Backend/Machine.hs
@@ -9,6 +9,7 @@
 -}
 module Parsley.Internal.Backend.Machine (
     Input, eval,
+    module Parsley.Internal.Backend.Machine.Types.Coins,
     module Parsley.Internal.Backend.Machine.Instructions,
     module Parsley.Internal.Backend.Machine.Defunc,
     module Parsley.Internal.Backend.Machine.Identifiers,
@@ -24,8 +25,9 @@
 import Parsley.Internal.Backend.Machine.InputOps     (InputPrep(..))
 import Parsley.Internal.Backend.Machine.InputRep     (Rep)
 import Parsley.Internal.Backend.Machine.Instructions
-import Parsley.Internal.Backend.Machine.LetBindings  (LetBinding, makeLetBinding)
+import Parsley.Internal.Backend.Machine.LetBindings  (LetBinding, makeLetBinding, newMeta)
 import Parsley.Internal.Backend.Machine.Ops          (Ops)
+import Parsley.Internal.Backend.Machine.Types.Coins  (Coins(..), zero, minCoins, maxCoins, plus, plus1, minus, plusNotReclaim)
 import Parsley.Internal.Common.Utils                 (Code)
 import Parsley.Internal.Core.InputTypes
 import Parsley.Internal.Trace                        (Trace)
diff --git a/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Eval.hs b/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Eval.hs
--- a/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Eval.hs
+++ b/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Eval.hs
@@ -18,6 +18,7 @@
 import Parsley.Internal.Backend.Machine.LetBindings   (LetBinding(..))
 import Parsley.Internal.Backend.Machine.LetRecBuilder
 import Parsley.Internal.Backend.Machine.Ops
+import Parsley.Internal.Backend.Machine.Types.Coins   (willConsume)
 import Parsley.Internal.Backend.Machine.Types.State
 import Parsley.Internal.Common                        (Fix4, cata4, One, Code, Vec(..), Nat(..))
 import Parsley.Internal.Trace                         (Trace(trace))
@@ -29,13 +30,13 @@
 import qualified Parsley.Internal.Backend.Machine.Instructions as Instructions (Handler(..))
 
 eval :: forall o a. (Trace, Ops o) => Code (InputDependant o) -> LetBinding o a a -> DMap MVar (LetBinding o a) -> Code (Maybe a)
-eval input (LetBinding !p _) fs = trace "EVALUATING TOP LEVEL" [|| runST $
+eval input binding fs = trace "EVALUATING TOP LEVEL" [|| runST $
   do let !(InputDependant next more offset) = $$input
      $$(let ?ops = InputOps [||more||] [||next||]
         in letRec fs
              nameLet
-             (\μ exp rs names -> buildRec μ rs (emptyCtx names) (readyMachine exp))
-             (run (readyMachine p) (Γ Empty (halt @o) [||offset||] (VCons (fatal @o) VNil)) . emptyCtx))
+             (\μ exp rs names _meta -> buildRec μ rs (emptyCtx names) (readyMachine exp))
+             (run (readyMachine (body binding)) (Γ Empty (halt @o) [||offset||] (VCons (fatal @o) VNil)) . emptyCtx))
   ||]
   where
     nameLet :: MVar x -> String
@@ -184,9 +185,21 @@
     ask
 
 evalMeta :: (?ops :: InputOps o, PositionOps o, BoxOps o, HandlerOps o) => MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
-evalMeta (AddCoins coins) (Machine k) =
+evalMeta (AddCoins coins') (Machine k) =
   do requiresPiggy <- asks hasCoin
+     let coins = willConsume coins'
      if requiresPiggy then local (storePiggy coins) k
      else local (giveCoins coins) k <&> \mk γ -> emitLengthCheck coins mk (raise γ) γ
-evalMeta (RefundCoins coins) (Machine k) = local (giveCoins coins) k
-evalMeta (DrainCoins coins) (Machine k) = liftM2 (\n mk γ -> emitLengthCheck n mk (raise γ) γ) (asks ((coins -) . liquidate)) k
+evalMeta (RefundCoins coins) (Machine k) = local (giveCoins (willConsume coins)) k
+evalMeta (DrainCoins coins) (Machine k) =
+  -- If there are enough coins left to cover the cost, no length check is required
+  -- Otherwise, the full length check is required (partial doesn't work until the right offset is reached)
+  liftM2 (\canAfford mk γ -> if canAfford then mk γ else emitLengthCheck (willConsume coins) mk (raise γ) γ)
+         (asks (canAfford (willConsume coins)))
+         k
+evalMeta (GiveBursary coins) (Machine k) = local (giveCoins (willConsume coins)) k
+evalMeta (PrefetchChar check) (Machine k) =
+  do requiresPiggy <- asks hasCoin
+     if | not check     -> k
+        | requiresPiggy -> local (storePiggy 1) k
+        | otherwise     -> local (giveCoins 1) k <&> \mk γ -> emitLengthCheck 1 mk (raise γ) γ
diff --git a/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Types/State.hs b/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Types/State.hs
--- a/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Types/State.hs
+++ b/src/ghc-8.6+/Parsley/Internal/Backend/Machine/Types/State.hs
@@ -12,7 +12,7 @@
     askSub, askΦ,
     debugUp, debugDown, debugLevel,
     storePiggy, breakPiggy, spendCoin, giveCoins, voidCoins, coins,
-    hasCoin, isBankrupt, liquidate
+    hasCoin, isBankrupt, canAfford
   ) where
 
 import Control.Exception                            (Exception, throw)
@@ -26,11 +26,11 @@
 import Parsley.Internal.Backend.Machine.Defunc      (Defunc)
 import Parsley.Internal.Backend.Machine.Identifiers (MVar(..), ΣVar(..), ΦVar, IMVar, IΣVar)
 import Parsley.Internal.Backend.Machine.InputRep    (Unboxed)
-import Parsley.Internal.Backend.Machine.LetBindings (Regs(..))
+import Parsley.Internal.Backend.Machine.LetBindings (Regs(..), Metadata)
 import Parsley.Internal.Common                      (Queue, enqueue, dequeue, Code, Vec)
 
 import qualified Data.Dependent.Map as DMap             ((!), insert, empty, lookup)
-import qualified Parsley.Internal.Common.Queue as Queue (empty, null, foldr)
+import qualified Parsley.Internal.Common.Queue as Queue (empty, null)
 
 type HandlerStack n s o a = Vec n (Code (Handler s o a))
 type Handler s o a = Unboxed o -> ST s (Maybe a)
@@ -44,8 +44,8 @@
 
 data QSubroutine s o a x = forall rs. QSubroutine  (Code (Func rs s o a x)) (Regs rs)
 
-qSubroutine :: Code (Func rs s o a x) -> Regs rs -> QSubroutine s o a x
-qSubroutine = QSubroutine
+qSubroutine :: Code (Func rs s o a x) -> Regs rs -> Metadata -> QSubroutine s o a x
+qSubroutine body frees _ = QSubroutine body frees
 
 newtype QJoin s o a x = QJoin { unwrapJoin :: Code (Cont s o a x) }
 newtype Machine s o xs n r a = Machine { getMachine :: MachineMonad s o xs n r a }
@@ -127,7 +127,7 @@
 breakPiggy ctx = let (coins, piggies') = dequeue (piggies ctx) in ctx {coins = coins, piggies = piggies'}
 
 hasCoin :: Ctx s o a -> Bool
-hasCoin = (> 0) . coins
+hasCoin = canAfford 1
 
 isBankrupt :: Ctx s o a -> Bool
 isBankrupt = liftM2 (&&) (not . hasCoin) (Queue.null . piggies)
@@ -141,8 +141,8 @@
 voidCoins :: Ctx s o a -> Ctx s o a
 voidCoins ctx = ctx {coins = 0, piggies = Queue.empty}
 
-liquidate :: Ctx s o a -> Int
-liquidate ctx = Queue.foldr (+) (coins ctx) (piggies ctx)
+canAfford :: Int -> Ctx s o a -> Bool
+canAfford n = (>= n) . coins
 
 newtype MissingDependency = MissingDependency IMVar deriving anyclass Exception
 newtype OutOfScopeRegister = OutOfScopeRegister IΣVar deriving anyclass Exception
diff --git a/src/ghc/Parsley/Internal/Backend/Analysis.hs b/src/ghc/Parsley/Internal/Backend/Analysis.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Backend/Analysis.hs
@@ -0,0 +1,57 @@
+{-|
+Module      : Parsley.Internal.Backend.Analysis
+Description : Exposes various analysis passes.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes the analysis passes defined within the analysis submodules. See
+the extended documentation in the submodules.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Backend.Analysis (
+    coinsNeeded,
+    relevancy
+  ) where
+
+import Parsley.Internal.Backend.Analysis.Coins (coinsNeeded)
+import Parsley.Internal.Backend.Analysis.Relevancy (relevancy)
+
+{- TODO
+  Live Value Analysis
+  -------------------
+
+  This analysis is designed to clean up dead registers:
+    * Instead of the state laws on the Combinator AST, this should catch these cases
+    * By performing it here we have ready access to the control flow information
+    * We'll perform global register analysis
+
+  State Laws:
+    * get *> get = get = get <* get
+    * put (pure x) *> get = put (pure x) *> pure x
+    * put get = pure ()
+    * put x *> put (pure y) = x *> put (pure y) = put x <* put (pure y)
+    -->
+    * Get . Pop . Get = Get = Get . Get . Pop -- Captured by relevancy analysis
+    * Get . Get = Get . Dup Subsumes the above (Dup . Pop = id, Dup . Swap = Dup)
+    * px . Put . Push () . Pop . Get = px . Dup . Put . Push () . Pop -- ??? (this law is better than above)
+    * Get . Put . Push () = Push () -- ??? Improved relevancy analysis?
+    * px . Put . Push () . Pop . py . Put . Push () = px . Pop . Push () . Pop . py . Put . Push () = px . Put . Push () . py . Put . Push () . Pop -- Captured by dead register analysis
+
+  Best case scenario is that we can capture all of the above optimisations
+  without a need to explicitly implement them.
+
+  Idea 1) recurse through the machine and mark branches with their liveIn set
+          if a register is not liveIn after a Put instruction it can be removed
+          Get r gens r
+          Put r kills r
+  Idea 2) recurse through the machine and collect relevancy data:
+          a value on the stack is relevant if it is consumed by `Lift2` or `Case`, etc
+          it is irrelevant if consumed by Pop
+          if Get produces an irrelevant operand, it can be replaced by Push BOTTOM
+          Dup disjoins the relevancy of the top two elements of the stack
+          Swap switches the relevancy of the top two elements of the stack
+  Idea 3) recurse through the machine and collect everUsed information
+          if a register is never used, then the Make instruction can be removed
+-}
diff --git a/src/ghc/Parsley/Internal/Backend/Analysis/Coins.hs b/src/ghc/Parsley/Internal/Backend/Analysis/Coins.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Backend/Analysis/Coins.hs
@@ -0,0 +1,81 @@
+{-|
+Module      : Parsley.Internal.Backend.Analysis.Coins
+Description : Coins analysis.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Implements the analysis path required to determine how many tokens of input a given parser
+is known to consume at /least/ in order to successfully execute. This provides the needed
+metadata to perform the piggybank algorithm in the machine (see
+"Parsley.Internal.Backend.Machine.Types.Context" for more information.)
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Backend.Analysis.Coins (coinsNeeded) where
+
+import Parsley.Internal.Backend.Machine (Instr(..), MetaInstr(..), Handler(..), Coins, plus1, minCoins, zero, minus, plusNotReclaim, willConsume)
+import Parsley.Internal.Common.Indexed  (cata4, Fix4, Const4(..))
+
+{-|
+Calculate the number of tokens that will be consumed by a given machine.
+
+@since 1.5.0.0
+-}
+coinsNeeded :: Fix4 (Instr o) xs n r a -> Coins
+coinsNeeded = fst . getConst4 . cata4 (Const4 . alg)
+
+first :: (a -> b) -> (a, x) -> (b, x)
+first = flip bimap id
+
+second :: (a -> b) -> (x, a) -> (x, b)
+second = bimap id
+
+bimap :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
+bimap = curry (bilift2 ($) ($))
+
+bilift2 :: (a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
+bilift2 f g (x1, y1) (x2, y2) = (f x1 x2, g y1 y2)
+
+algCatch :: (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
+algCatch k (_, True) = k
+algCatch (_, True) k = k
+algCatch (k1, _) (k2, _) = (minCoins k1 k2, False)
+
+-- Bool represents if an empty is found in a branch (of a Catch)
+-- This helps to get rid of `min` being used for `Try` where min is always 0
+-- (The input is needed to /succeed/, so if one branch is doomed to fail it doesn't care about coins)
+alg :: Instr o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
+alg Ret                                     = (zero, False)
+alg (Push _ k)                              = getConst4 k -- was const False on the second parameter, I think that's probably right but a bit presumptive
+alg (Pop k)                                 = getConst4 k
+alg (Lift2 _ k)                             = getConst4 k
+alg (Sat _ (Const4 k))                      = first plus1 k
+alg (Call _ (Const4 k))                     = first (const zero) k
+alg (Jump _)                                = (zero, False)
+alg Empt                                    = (zero, True)
+alg (Commit k)                              = getConst4 k
+alg (Catch k h)                             = algCatch (getConst4 k) (algHandler h)
+alg (Tell k)                                = getConst4 k
+alg (Seek k)                                = getConst4 k
+alg (Case p q)                              = algCatch (getConst4 p) (getConst4 q)
+alg (Choices _ ks def)                      = foldr (algCatch . getConst4) (getConst4 def) ks
+alg (Iter _ _ h)                            = first (const zero) (algHandler h)
+alg (Join _)                                = (zero, False)
+alg (MkJoin _ (Const4 b) (Const4 k))        = bilift2 (flip plusNotReclaim . willConsume) (||) b k
+alg (Swap k)                                = getConst4 k
+alg (Dup k)                                 = getConst4 k
+alg (Make _ _ k)                            = getConst4 k
+alg (Get _ _ k)                             = getConst4 k
+alg (Put _ _ k)                             = getConst4 k
+alg (LogEnter _ k)                          = getConst4 k
+alg (LogExit _ k)                           = getConst4 k
+alg (MetaInstr (AddCoins _) (Const4 k))     = k
+alg (MetaInstr (RefundCoins n) (Const4 k))  = first (minCoins zero . (`minus` n)) k -- These were refunded, so deduct
+alg (MetaInstr (DrainCoins _) (Const4 k))   = second (const False) k
+alg (MetaInstr (GiveBursary n) (Const4 _))  = (n, False)                            -- We know that `n` is the required for `k`
+alg (MetaInstr (PrefetchChar _) (Const4 k)) = k
+
+algHandler :: Handler o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
+algHandler (Same yes no) = algCatch (getConst4 yes) (getConst4 no)
+algHandler (Always k) = getConst4 k
diff --git a/src/ghc/Parsley/Internal/Backend/Analysis/Relevancy.hs b/src/ghc/Parsley/Internal/Backend/Analysis/Relevancy.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Backend/Analysis/Relevancy.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE MultiParamTypeClasses,
+             TypeFamilies,
+             UndecidableInstances #-}
+{-|
+Module      : Parsley.Internal.Backend.Analysis.Relevancy
+Description : Value relevancy analysis.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes an analysis that can determine whether each of the values present on the stack for a
+given machine are actually used or not. This information may be useful in the future to calculate
+whether a register is "dead" or not.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Backend.Analysis.Relevancy (relevancy, Length) where
+
+import Data.Kind                        (Type)
+import Parsley.Internal.Backend.Machine (Instr(..), Handler(..))
+import Parsley.Internal.Common.Indexed  (cata4, Fix4)
+import Parsley.Internal.Common.Vec      (Vec(..), Nat(..), SNat(..), SingNat(..), zipWithVec, replicateVec)
+
+{-|
+Provides a conservative estimate on whether or not each of the elements of the stack on
+entry to a machine are actually used in the computation.
+
+@since 1.5.0.0
+-}
+relevancy :: SingNat (Length xs) => Fix4 (Instr o) xs n r a -> Vec (Length xs) Bool
+relevancy = ($ sing) . getStack . cata4 (RelevancyStack . alg)
+
+{-|
+Computes the length of a type-level list. Used to index a `Vec`.
+
+@since 1.5.0.0
+-}
+type family Length (xs :: [Type]) :: Nat where
+  Length '[] = Zero
+  Length (_ : xs) = Succ (Length xs)
+
+newtype RelevancyStack xs (n :: Nat) r a = RelevancyStack { getStack :: SNat (Length xs) -> Vec (Length xs) Bool }
+
+zipRelevancy :: Vec n Bool -> Vec n Bool -> Vec n Bool
+zipRelevancy = zipWithVec (||)
+
+-- This algorithm is over-approximating: join and ret aren't _always_ relevant
+alg :: Instr o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
+alg Ret                _         = VCons True VNil
+alg (Push _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
+alg (Pop k)            (SSucc n) = VCons False (getStack k n)
+alg (Lift2 _ k)        (SSucc n) = let VCons rel xs = getStack k n in VCons rel (VCons rel xs)
+alg (Sat _ k)          n         = let VCons _ xs = getStack k (SSucc n) in xs
+alg (Call _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
+alg (Jump _)           _         = VNil
+alg Empt               n         = replicateVec n False
+alg (Commit k)         n         = getStack k n
+alg (Catch k _)        n         = getStack k n
+alg (Tell k)           n         = let VCons _ xs = getStack k (SSucc n) in xs
+alg (Seek k)           (SSucc n) = VCons True (getStack k n)
+alg (Case p q)         n         = VCons True (let VCons _ xs = zipRelevancy (getStack p n) (getStack q n) in xs)
+alg (Choices _ ks def) (SSucc n) = VCons True (foldr (zipRelevancy . (`getStack` n)) (getStack def n) ks)
+alg (Iter _ _ h)       n         = let VCons _ xs = algHandler h (SSucc n) in xs
+alg (Join _)           (SSucc n) = VCons True (replicateVec n False)
+alg (MkJoin _ b _)     n         = let VCons _ xs = getStack b (SSucc n) in xs
+alg (Swap k)           n         = let VCons rel1 (VCons rel2 xs) = getStack k n in VCons rel2 (VCons rel1 xs)
+alg (Dup k)            n         = let VCons rel1 (VCons rel2 xs) = getStack k (SSucc n) in VCons (rel1 || rel2) xs
+alg (Make _ _ k)       (SSucc n) = VCons False (getStack k n)
+alg (Get _ _ k)        n         = let VCons _ xs = getStack k (SSucc n) in xs
+alg (Put _ _ k)        (SSucc n) = VCons False (getStack k n)
+alg (LogEnter _ k)     n         = getStack k n
+alg (LogExit _ k)      n         = getStack k n
+alg (MetaInstr _ k)    n         = getStack k n
+
+algHandler :: Handler o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
+algHandler (Same yes no) (SSucc n) = VCons True (let VCons _ xs = zipRelevancy (VCons False (getStack yes n)) (getStack no (SSucc n)) in xs)
+algHandler (Always k) n = getStack k n
diff --git a/src/ghc/Parsley/Internal/Backend/CodeGenerator.hs b/src/ghc/Parsley/Internal/Backend/CodeGenerator.hs
--- a/src/ghc/Parsley/Internal/Backend/CodeGenerator.hs
+++ b/src/ghc/Parsley/Internal/Backend/CodeGenerator.hs
@@ -14,21 +14,22 @@
 -}
 module Parsley.Internal.Backend.CodeGenerator (codeGen) where
 
-import Data.Maybe                                    (isJust)
-import Data.Set                                      (Set, elems)
-import Control.Monad.Trans                           (lift)
-import Parsley.Internal.Backend.Machine              (user, userBool, LetBinding, makeLetBinding, Instr(..), Handler(..),
-                                                      _Fmap, _App, _Modify, _Get, _Put, _Make,
-                                                      addCoins, refundCoins, drainCoins,
-                                                      IMVar, IΦVar, IΣVar, MVar(..), ΦVar(..), ΣVar(..), SomeΣVar)
-import Parsley.Internal.Backend.InstructionAnalyser  (coinsNeeded)
-import Parsley.Internal.Common.Fresh                 (VFreshT, HFresh, evalFreshT, evalFresh, construct, MonadFresh(..), mapVFreshT)
-import Parsley.Internal.Common.Indexed               (Fix, Fix4(In4), Cofree(..), Nat(..), imap, histo, extract, (|>))
-import Parsley.Internal.Core.CombinatorAST           (Combinator(..), MetaCombinator(..))
-import Parsley.Internal.Core.Defunc                  (Defunc(COMPOSE, ID), pattern FLIP_H, pattern UNIT)
-import Parsley.Internal.Trace                        (Trace(trace))
+import Data.Maybe                          (isJust)
+import Data.Set                            (Set, elems)
+import Control.Monad.Trans                 (lift)
+import Parsley.Internal.Backend.Machine    (user, userBool, LetBinding, makeLetBinding, newMeta, Instr(..), Handler(..),
+                                            _Fmap, _App, _Modify, _Get, _Put, _Make,
+                                            addCoins, refundCoins, drainCoins, giveBursary,
+                                            minus, minCoins, maxCoins, zero,
+                                            IMVar, IΦVar, IΣVar, MVar(..), ΦVar(..), ΣVar(..), SomeΣVar)
+import Parsley.Internal.Backend.Analysis   (coinsNeeded)
+import Parsley.Internal.Common.Fresh       (VFreshT, HFresh, evalFreshT, evalFresh, construct, MonadFresh(..), mapVFreshT)
+import Parsley.Internal.Common.Indexed     (Fix, Fix4(In4), Cofree(..), Nat(..), imap, histo, extract, (|>))
+import Parsley.Internal.Core.CombinatorAST (Combinator(..), MetaCombinator(..))
+import Parsley.Internal.Core.Defunc        (Defunc(COMPOSE, ID), pattern FLIP_H, pattern UNIT)
+import Parsley.Internal.Trace              (Trace(trace))
 
-import Parsley.Internal.Core.Defunc as Core          (Defunc)
+import Parsley.Internal.Core.Defunc as Core (Defunc)
 
 type CodeGenStack a = VFreshT IΦVar (VFreshT IMVar (HFresh IΣVar)) a
 runCodeGenStack :: CodeGenStack a -> IMVar -> IΦVar -> IΣVar -> a
@@ -50,7 +51,7 @@
         -> IMVar            -- ^ The binding identifier to start name generation from.
         -> IΣVar            -- ^ The register identifier to start name generation from.
         -> LetBinding o a x
-codeGen letBound p rs μ0 σ0 = trace ("GENERATING " ++ name ++ ": " ++ show p ++ "\nMACHINE: " ++ show (elems rs) ++ " => " ++ show m) $ makeLetBinding m rs
+codeGen letBound p rs μ0 σ0 = trace ("GENERATING " ++ name ++ ": " ++ show p ++ "\nMACHINE: " ++ show (elems rs) ++ " => " ++ show m) $ makeLetBinding m rs newMeta
   where
     name = maybe "TOP LEVEL" show letBound
     m = finalise (histo alg p)
@@ -58,6 +59,9 @@
     alg = deep |> (\x -> CodeGen (shallow (imap extract x)))
     finalise cg =
       let m = runCodeGenStack (runCodeGen cg (In4 Ret)) μ0 0 σ0
+      -- let-bound things are not safe to factor length checks out of
+      -- This is because we do not know the cut characteristics of every caller
+      -- In theory this /could/ be computed as the union of every call site
       in if isJust letBound then m else addCoins (coinsNeeded m) m
 
 pattern (:<$>:) :: Core.Defunc (a -> b) -> Cofree Combinator k a -> Combinator (Cofree Combinator k) b
@@ -83,8 +87,8 @@
      qc <- freshΦ (runCodeGen q φ)
      let np = coinsNeeded pc
      let nq = coinsNeeded qc
-     let dp = np - min np nq
-     let dq = nq - min np nq
+     let dp = np `minus` minCoins np nq
+     let dq = nq `minus` minCoins np nq
      return $! binder (In4 (Catch (addCoins dp pc) (handler (addCoins dq qc))))
 
 chainPreCompile :: CodeGen o a (x -> x) -> CodeGen o a x
@@ -136,27 +140,28 @@
 shallow (p :<|>: q)   m = do altNoCutCompile p q parsecHandler id m
 shallow (Try p)       m = do fmap (In4 . flip Catch rollbackHandler) (runCodeGen p (deadCommitOptimisation m))
 shallow (LookAhead p) m =
-  do n <- fmap coinsNeeded (runCodeGen p (In4 Empt)) -- Dodgy hack, but oh well
+  do n <- fmap coinsNeeded (runCodeGen p (In4 Ret)) -- Dodgy hack, but oh well
      fmap (In4 . Tell) (runCodeGen p (In4 (Swap (In4 (Seek (refundCoins n m))))))
 shallow (NotFollowedBy p) m =
   do pc <- runCodeGen p (In4 (Pop (In4 (Seek (In4 (Commit (In4 Empt)))))))
      let np = coinsNeeded pc
      let nm = coinsNeeded m
-     return $! In4 (Catch (addCoins (max (np - nm) 0) (In4 (Tell pc))) (Always (In4 (Seek (In4 (Push (user UNIT) m))))))
+     -- The minus here is used because the shared coins are propagated out front, neat.
+     return $! In4 (Catch (addCoins (maxCoins (np `minus` nm) zero) (In4 (Tell pc))) (Always (In4 (Seek (In4 (Push (user UNIT) m))))))
 shallow (Branch b p q) m =
   do (binder, φ) <- makeΦ m
      pc <- freshΦ (runCodeGen p (In4 (Swap (In4 (_App φ)))))
      qc <- freshΦ (runCodeGen q (In4 (Swap (In4 (_App φ)))))
      let minc = coinsNeeded (In4 (Case pc qc))
-     let dp = max 0 (coinsNeeded pc - minc)
-     let dq = max 0 (coinsNeeded qc - minc)
+     let dp = maxCoins zero (coinsNeeded pc `minus` minc)
+     let dq = maxCoins zero (coinsNeeded qc `minus` minc)
      fmap binder (runCodeGen b (In4 (Case (addCoins dp pc) (addCoins dq qc))))
 shallow (Match p fs qs def) m =
   do (binder, φ) <- makeΦ m
      qcs <- traverse (\q -> freshΦ (runCodeGen q φ)) qs
      defc <- freshΦ (runCodeGen def φ)
      let minc = coinsNeeded (In4 (Choices (map userBool fs) qcs defc))
-     let defc':qcs' = map (max 0 . subtract minc . coinsNeeded >>= addCoins) (defc:qcs)
+     let defc':qcs' = map (maxCoins zero . (`minus` minc) . coinsNeeded >>= addCoins) (defc:qcs)
      fmap binder (runCodeGen p (In4 (Choices (map user fs) qcs' defc')))
 shallow (Let _ μ _)            m = do return $! tailCallOptimise μ m
 shallow (ChainPre op p)        m = do chainPreCompile op p addCoinsNeeded id m
@@ -190,19 +195,23 @@
 freshΦ :: CodeGenStack a -> CodeGenStack a
 freshΦ = newScope
 
+-- TODO: We can inline anything that is /pure/ and has no large code foot-print, at the moment this
+--       is tripped up by lots of `Push` and `Pop`s.
 makeΦ :: Fix4 (Instr o) (x ': xs) (Succ n) r a -> CodeGenStack (Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a, Fix4 (Instr o) (x : xs) (Succ n) r a)
 makeΦ m | elidable m = return (id, m)
   where
     elidable :: Fix4 (Instr o) (x ': xs) (Succ n) r a -> Bool
     -- This is double-φ optimisation:   If a φ-node points shallowly to another φ-node, then it can be elided
     elidable (In4 (Join _))             = True
+    elidable (In4 (Pop (In4 (Join _)))) = True
     -- This is terminal-φ optimisation: If a φ-node points shallowly to a terminal operation, then it can be elided
     elidable (In4 Ret)                  = True
+    elidable (In4 (Pop (In4 Ret)))      = True
     -- This is a form of double-φ optimisation: If a φ-node points shallowly to a jump, then it can be elided and the jump used instead
     -- Note that this should NOT be done for non-tail calls, as they may generate a large continuation
     elidable (In4 (Pop (In4 (Jump _)))) = True
     elidable _                          = False
-makeΦ m = let n = coinsNeeded m in fmap (\φ -> (In4 . MkJoin φ (addCoins n m), drainCoins n (In4 (Join φ)))) askΦ
+makeΦ m = let n = coinsNeeded m in fmap (\φ -> (In4 . MkJoin φ (giveBursary n m), drainCoins n (In4 (Join φ)))) askΦ
 
 freshΣ :: CodeGenStack (ΣVar a)
 freshΣ = lift (lift (construct ΣVar))
diff --git a/src/ghc/Parsley/Internal/Backend/InstructionAnalyser.hs b/src/ghc/Parsley/Internal/Backend/InstructionAnalyser.hs
deleted file mode 100644
--- a/src/ghc/Parsley/Internal/Backend/InstructionAnalyser.hs
+++ /dev/null
@@ -1,134 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses,
-             TypeFamilies,
-             UndecidableInstances #-}
-module Parsley.Internal.Backend.InstructionAnalyser (coinsNeeded, relevancy, Length) where
-
-import Data.Kind                        (Type)
-import Parsley.Internal.Backend.Machine (Instr(..), MetaInstr(..), Handler(..))
-import Parsley.Internal.Common.Indexed  (cata4, Fix4, Const4(..))
-import Parsley.Internal.Common.Vec      (Vec(..), Nat(..), SNat(..), SingNat(..), zipWithVec, replicateVec)
-
-coinsNeeded :: Fix4 (Instr o) xs n r a -> Int
-coinsNeeded = fst . getConst4 . cata4 (Const4 . alg)
-  where
-    algCatch :: (Int, Bool) -> (Int, Bool) -> (Int, Bool)
-    algCatch k (_, True) = k
-    algCatch (_, True) k = k
-    algCatch (k1, _) (k2, _) = (min k1 k2, False)
-
-    -- Bool represents if an empty is found in a branch (of a Catch)
-    -- This helps to get rid of `min` being used for `Try` where min is always 0
-    -- (The input is needed to _succeed_, so if one branch is doomed to fail it doesn't care about coins)
-    alg :: Instr o (Const4 (Int, Bool)) xs n r a -> (Int, Bool)
-    alg Ret                                    = (0, False)
-    alg (Push _ k)                             = getConst4 k -- was const False on the second parameter, I think that's probably right but a bit presumptive
-    alg (Pop k)                                = getConst4 k
-    alg (Lift2 _ k)                            = getConst4 k
-    alg (Sat _ (Const4 k))                     = (fst k + 1, snd k)
-    alg (Call _ (Const4 k))                    = (0, snd k)
-    alg (Jump _)                               = (0, False)
-    alg Empt                                   = (0, True)
-    alg (Commit k)                             = getConst4 k
-    alg (Catch k h)                            = algCatch (getConst4 k) (algHandler h)
-    alg (Tell k)                               = getConst4 k
-    alg (Seek k)                               = getConst4 k
-    alg (Case p q)                             = algCatch (getConst4 p) (getConst4 q)
-    alg (Choices _ ks def)                     = foldr (algCatch . getConst4) (getConst4 def) ks
-    alg (Iter _ _ h)                           = (0, snd (algHandler h))
-    alg (Join _)                               = (0, False)
-    alg (MkJoin _ (Const4 b) (Const4 k))       = (fst k + fst b, snd k || snd b)
-    alg (Swap k)                               = getConst4 k
-    alg (Dup k)                                = getConst4 k
-    alg (Make _ _ k)                           = getConst4 k
-    alg (Get _ _ k)                            = getConst4 k
-    alg (Put _ _ k)                            = getConst4 k
-    alg (LogEnter _ k)                         = getConst4 k
-    alg (LogExit _ k)                          = getConst4 k
-    alg (MetaInstr (AddCoins _) (Const4 k))    = k
-    alg (MetaInstr (RefundCoins n) (Const4 k)) = (max (fst k - n) 0, snd k) -- These were refunded, so deduct
-    alg (MetaInstr (DrainCoins _) (Const4 k))  = (fst k, False)
-
-    algHandler :: Handler o (Const4 (Int, Bool)) xs n r a -> (Int, Bool)
-    algHandler (Same yes no) = algCatch (getConst4 yes) (getConst4 no)
-    algHandler (Always k) = getConst4 k
-
-{- TODO
-  Live Value Analysis
-  -------------------
-
-  This analysis is designed to clean up dead registers:
-    * Instead of the state laws on the Combinator AST, this should catch these cases
-    * By performing it here we have ready access to the control flow information
-    * We'll perform global register analysis
-
-  State Laws:
-    * get *> get = get = get <* get
-    * put (pure x) *> get = put (pure x) *> pure x
-    * put get = pure ()
-    * put x *> put (pure y) = x *> put (pure y) = put x <* put (pure y)
-    -->
-    * Get . Pop . Get = Get = Get . Get . Pop -- Captured by relevancy analysis
-    * Get . Get = Get . Dup Subsumes the above (Dup . Pop = id, Dup . Swap = Dup)
-    * px . Put . Push () . Pop . Get = px . Dup . Put . Push () . Pop -- ??? (this law is better than above)
-    * Get . Put . Push () = Push () -- ??? Improved relevancy analysis?
-    * px . Put . Push () . Pop . py . Put . Push () = px . Pop . Push () . Pop . py . Put . Push () = px . Put . Push () . py . Put . Push () . Pop -- Captured by dead register analysis
-
-  Best case scenario is that we can capture all of the above optimisations
-  without a need to explicitly implement them.
-
-  Idea 1) recurse through the machine and mark branches with their liveIn set
-          if a register is not liveIn after a Put instruction it can be removed
-          Get r gens r
-          Put r kills r
-  Idea 2) recurse through the machine and collect relevancy data:
-          a value on the stack is relevant if it is consumed by `Lift2` or `Case`, etc
-          it is irrelevant if consumed by Pop
-          if Get produces an irrelevant operand, it can be replaced by Push BOTTOM
-          Dup disjoins the relevancy of the top two elements of the stack
-          Swap switches the relevancy of the top two elements of the stack
-  Idea 3) recurse through the machine and collect everUsed information
-          if a register is never used, then the Make instruction can be removed
--}
-
-type family Length (xs :: [Type]) :: Nat where
-  Length '[] = Zero
-  Length (_ : xs) = Succ (Length xs)
-
-newtype RelevancyStack xs (n :: Nat) r a = RelevancyStack { getStack :: SNat (Length xs) -> Vec (Length xs) Bool }
-
-relevancy :: SingNat (Length xs) => Fix4 (Instr o) xs n r a -> Vec (Length xs) Bool
-relevancy = ($ sing) . getStack . cata4 (RelevancyStack . alg)
-  where
-    zipRelevancy = zipWithVec (||)
-
-    -- This algorithm is over-approximating: join and ret aren't _always_ relevant
-    alg :: Instr o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
-    alg Ret                _         = VCons True VNil
-    alg (Push _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
-    alg (Pop k)            (SSucc n) = VCons False (getStack k n)
-    alg (Lift2 _ k)        (SSucc n) = let VCons rel xs = getStack k n in VCons rel (VCons rel xs)
-    alg (Sat _ k)          n         = let VCons _ xs = getStack k (SSucc n) in xs
-    alg (Call _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
-    alg (Jump _)           _         = VNil
-    alg Empt               n         = replicateVec n False
-    alg (Commit k)         n         = getStack k n
-    alg (Catch k _)        n         = getStack k n
-    alg (Tell k)           n         = let VCons _ xs = getStack k (SSucc n) in xs
-    alg (Seek k)           (SSucc n) = VCons True (getStack k n)
-    alg (Case p q)         n         = VCons True (let VCons _ xs = zipRelevancy (getStack p n) (getStack q n) in xs)
-    alg (Choices _ ks def) (SSucc n) = VCons True (foldr (zipRelevancy . (`getStack` n)) (getStack def n) ks)
-    alg (Iter _ _ h)       n         = let VCons _ xs = algHandler h (SSucc n) in xs
-    alg (Join _)           (SSucc n) = VCons True (replicateVec n False)
-    alg (MkJoin _ b _)     n         = let VCons _ xs = getStack b (SSucc n) in xs
-    alg (Swap k)           n         = let VCons rel1 (VCons rel2 xs) = getStack k n in VCons rel2 (VCons rel1 xs)
-    alg (Dup k)            n         = let VCons rel1 (VCons rel2 xs) = getStack k (SSucc n) in VCons (rel1 || rel2) xs
-    alg (Make _ _ k)       (SSucc n) = VCons False (getStack k n)
-    alg (Get _ _ k)        n         = let VCons _ xs = getStack k (SSucc n) in xs
-    alg (Put _ _ k)        (SSucc n) = VCons False (getStack k n)
-    alg (LogEnter _ k)     n         = getStack k n
-    alg (LogExit _ k)      n         = getStack k n
-    alg (MetaInstr _ k)    n         = getStack k n
-
-    algHandler :: Handler o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
-    algHandler (Same yes no) (SSucc n) = VCons True (let VCons _ xs = zipRelevancy (VCons False (getStack yes n)) (getStack no (SSucc n)) in xs)
-    algHandler (Always k) n = getStack k n
diff --git a/src/ghc/Parsley/Internal/Backend/Machine/Identifiers.hs b/src/ghc/Parsley/Internal/Backend/Machine/Identifiers.hs
--- a/src/ghc/Parsley/Internal/Backend/Machine/Identifiers.hs
+++ b/src/ghc/Parsley/Internal/Backend/Machine/Identifiers.hs
@@ -27,8 +27,8 @@
 import Unsafe.Coerce                     (unsafeCoerce)
 
 {-|
-Represents a join point which requires an argument
-of type @a@. 
+Represents a join point which requires an argument.
+of type @a@.
 
 @since 1.0.0.0
 -}
diff --git a/src/ghc/Parsley/Internal/Backend/Machine/Instructions.hs b/src/ghc/Parsley/Internal/Backend/Machine/Instructions.hs
--- a/src/ghc/Parsley/Internal/Backend/Machine/Instructions.hs
+++ b/src/ghc/Parsley/Internal/Backend/Machine/Instructions.hs
@@ -24,12 +24,13 @@
     -- * Smart Instructions
     _App, _Fmap, _Modify, _Make, _Put, _Get,
     -- * Smart Meta-Instructions
-    addCoins, refundCoins, drainCoins
+    addCoins, refundCoins, drainCoins, giveBursary, prefetchChar
   ) where
 
 import Data.Kind                                    (Type)
 import Data.Void                                    (Void)
 import Parsley.Internal.Backend.Machine.Identifiers (MVar, ΦVar, ΣVar)
+import Parsley.Internal.Backend.Machine.Types.Coins (Coins(Coins))
 import Parsley.Internal.Common                      (IFunctor4, Fix4(In4), Const4(..), imap4, cata4, Nat(..), One, intercalateDiff)
 
 import Parsley.Internal.Backend.Machine.Defunc as Machine (Defunc, user)
@@ -64,20 +65,20 @@
   {-| Applies a function to the top two elements of the stack, converting them to something else and pushing it back on.
 
   @since 1.0.0.0 -}
-  Lift2     :: Machine.Defunc (x -> y -> z) {- ^ Function to apply. -} 
-            -> k (z : xs) n r a             {- ^ Machine requiring new value. -} 
+  Lift2     :: Machine.Defunc (x -> y -> z) {- ^ Function to apply. -}
+            -> k (z : xs) n r a             {- ^ Machine requiring new value. -}
             -> Instr o k (y : x : xs) n r a
   {-| Reads a character so long as it matches a given predicate. If it does not, or no input is available, this instruction fails.
 
   @since 1.0.0.0 -}
-  Sat       :: Machine.Defunc (Char -> Bool) {- ^ Predicate to apply. -} 
-            -> k (Char : xs) (Succ n) r a    {- ^ Machine requiring read character. -} 
+  Sat       :: Machine.Defunc (Char -> Bool) {- ^ Predicate to apply. -}
+            -> k (Char : xs) (Succ n) r a    {- ^ Machine requiring read character. -}
             -> Instr o k xs (Succ n) r a
   {-| Calls another let-bound parser.
 
   @since 1.0.0.0 -}
-  Call      :: MVar x                  {- ^ The binding to invoke. -} 
-            -> k (x : xs) (Succ n) r a {- ^ Continuation to do after the call. -} 
+  Call      :: MVar x                  {- ^ The binding to invoke. -}
+            -> k (x : xs) (Succ n) r a {- ^ Continuation to do after the call. -}
             -> Instr o k xs (Succ n) r a
   {-| Jumps to another let-bound parser tail-recursively.
 
@@ -94,8 +95,8 @@
   {-| Registers a handler to deal with possible failure in the given machine.
 
   @since 1.4.0.0 -}
-  Catch     :: k xs (Succ n) r a          {- ^ Machine where failure is handled by the handler. -} 
-            -> Handler o k (o : xs) n r a {- ^ The handler to register. -} 
+  Catch     :: k xs (Succ n) r a          {- ^ Machine where failure is handled by the handler. -}
+            -> Handler o k (o : xs) n r a {- ^ The handler to register. -}
             -> Instr o k xs n r a
   {-| Pushes the current input offset onto the stack.
 
@@ -108,24 +109,24 @@
   {-| Picks one of two continuations based on whether a `Left` or `Right` is on the stack.
 
   @since 1.0.0.0 -}
-  Case      :: k (x : xs) n r a {- ^ Machine to execute if `Left` on stack. -} 
-            -> k (y : xs) n r a {- ^ Machine to execute if `Right` on stack. -} 
+  Case      :: k (x : xs) n r a {- ^ Machine to execute if `Left` on stack. -}
+            -> k (y : xs) n r a {- ^ Machine to execute if `Right` on stack. -}
             -> Instr o k (Either x y : xs) n r a
   {-| Given a collection of predicates and machines, this instruction will execute the first machine
       for which the corresponding predicate returns true for the value on the top of the stack.
 
   @since 1.0.0.0 -}
-  Choices   :: [Machine.Defunc (x -> Bool)] {- ^ A list of predicates to try. -} 
-            -> [k xs n r a]                 {- ^ A corresponding list of machines. -} 
+  Choices   :: [Machine.Defunc (x -> Bool)] {- ^ A list of predicates to try. -}
+            -> [k xs n r a]                 {- ^ A corresponding list of machines. -}
             -> k xs n r a                   {- ^ A default machine to execute if no predicates match. -}
             -> Instr o k (x : xs) n r a
   {-| Sets up an iteration, where the second argument is executed repeatedly until it fails, which is
       handled by the given handler. The use of `Void` indicates that `Ret` is illegal within the loop.
 
   @since 1.0.0.0 -}
-  Iter      :: MVar Void                  {- ^ The name of the binding. -} 
-            -> k '[] One Void a           {- ^ The body of the loop: it cannot return "normally". -} 
-            -> Handler o k (o : xs) n r a {- ^ The handler for the loop's exit. -} 
+  Iter      :: MVar Void                  {- ^ The name of the binding. -}
+            -> k '[] One Void a           {- ^ The body of the loop: it cannot return "normally". -}
+            -> Handler o k (o : xs) n r a {- ^ The handler for the loop's exit. -}
             -> Instr o k xs n r a
   {-| Jumps to a given join point.
 
@@ -134,9 +135,9 @@
   {-| Sets up a new join point binding.
 
   @since 1.0.0.0 -}
-  MkJoin    :: ΦVar x           {- ^ The name of the binding that can be referred to later. -} 
-            -> k (x : xs) n r a {- ^ The body of the join point binding. -} 
-            -> k xs n r a       {- ^ The scope within which the binding is valid.  -} 
+  MkJoin    :: ΦVar x           {- ^ The name of the binding that can be referred to later. -}
+            -> k (x : xs) n r a {- ^ The body of the join point binding. -}
+            -> k xs n r a       {- ^ The scope within which the binding is valid.  -}
             -> Instr o k xs n r a
   {-| Swaps the top two elements on the stack
 
@@ -149,44 +150,44 @@
   {-| Initialises a new register for use within the continuation. Initial value is on the stack.
 
   @since 1.0.0.0 -}
-  Make      :: ΣVar x     {- ^ The name of the new register. -} 
-            -> Access     {- ^ Whether or not the register is "concrete". -} 
-            -> k xs n r a {- ^ The scope within which the register is accessible. -} 
+  Make      :: ΣVar x     {- ^ The name of the new register. -}
+            -> Access     {- ^ Whether or not the register is "concrete". -}
+            -> k xs n r a {- ^ The scope within which the register is accessible. -}
             -> Instr o k (x : xs) n r a
   {-| Pushes the value contained within a register onto the stack.
 
   @since 1.0.0.0 -}
-  Get       :: ΣVar x           {- ^ Name of the register to read. -} 
-            -> Access           {- ^ Whether or not the value is cached. -} 
-            -> k (x : xs) n r a {- ^ The machine that requires the value. -} 
+  Get       :: ΣVar x           {- ^ Name of the register to read. -}
+            -> Access           {- ^ Whether or not the value is cached. -}
+            -> k (x : xs) n r a {- ^ The machine that requires the value. -}
             -> Instr o k xs n r a
   {-| Places the value on the top of the stack into a given register.
 
   @since 1.0.0.0 -}
-  Put       :: ΣVar x     {- ^ Name of the register to update. -} 
-            -> Access     {- ^ Whether or not the value needs to be stored in a concrete register. -} 
-            -> k xs n r a 
+  Put       :: ΣVar x     {- ^ Name of the register to update. -}
+            -> Access     {- ^ Whether or not the value needs to be stored in a concrete register. -}
+            -> k xs n r a
             -> Instr o k (x : xs) n r a
   {-| Begins a debugging scope, the inner scope requires /two/ handlers,
       the first is the log handler itself, and then the second is the
       "real" fail handler for when the log handler is executed.
 
   @since 1.0.0.0 -}
-  LogEnter  :: String                   {- ^ The message to be printed. -} 
-            -> k xs (Succ (Succ n)) r a {- ^ The machine to be debugged. -} 
+  LogEnter  :: String                   {- ^ The message to be printed. -}
+            -> k xs (Succ (Succ n)) r a {- ^ The machine to be debugged. -}
             -> Instr o k xs (Succ n) r a
   {-| Ends the log scope after a succesful execution.
 
   @since 1.0.0.0 -}
-  LogExit   :: String     {- ^ The message to be printed. -} 
-            -> k xs n r a {- ^ The machine that follows. -} 
+  LogExit   :: String     {- ^ The message to be printed. -}
+            -> k xs n r a {- ^ The machine that follows. -}
             -> Instr o k xs n r a
   {-| Executes a meta-instruction, which is interacting with
       implementation specific static information.
 
   @since 1.0.0.0 -}
-  MetaInstr :: MetaInstr n {- ^ A meta-instruction to perform. -} 
-            -> k xs n r a  {- ^ The machine that follows. -} 
+  MetaInstr :: MetaInstr n {- ^ A meta-instruction to perform. -}
+            -> k xs n r a  {- ^ The machine that follows. -}
             -> Instr o k xs n r a
 
 {-|
@@ -233,51 +234,78 @@
 
       A handler is required, in case the length check fails.
 
-  @since 1.0.0.0 -}
-  AddCoins    :: Int -> MetaInstr (Succ n)
+  @since 1.5.0.0 -}
+  AddCoins    :: Coins -> MetaInstr (Succ n)
   {-| Refunds to the piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information).
       This always happens for free, and is added straight to the coins.
 
-  @since 1.0.0.0 -}
-  RefundCoins :: Int -> MetaInstr n
+  @since 1.5.0.0 -}
+  RefundCoins :: Coins -> MetaInstr n
   {-| Remove coins from piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information)
       This is used to pay for more expensive calls to bindings with known required input.
 
       A handler is required, as there may not be enough coins to pay the cost and a length check causes a failure.
 
-  @since 1.0.0.0 -}
-  DrainCoins  :: Int -> MetaInstr (Succ n)
+  @since 1.5.0.0 -}
+  DrainCoins  :: Coins -> MetaInstr (Succ n)
+  {-| Refunds to the piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information).
+      This always happens for free, and is added straight to the coins. Unlike `RefundCoins` this cannot reclaim
+      input, nor is is subtractive in the analysis.
 
+  @since 1.5.0.0 -}
+  GiveBursary :: Coins -> MetaInstr n
+  {-| Fetches a character to read in advance. This is used to factor out a common token from alternatives.
+      The boolean argument represents whether or not the read is covered by a factored length check, or
+      requires its own.
 
-mkCoin :: (Int -> MetaInstr n) -> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
-mkCoin _    0 = id
-mkCoin meta n = In4 . MetaInstr (meta n)
+  @since 1.5.0.0 -}
+  PrefetchChar :: Bool -> MetaInstr (Succ n)
 
+mkCoin :: (Coins -> MetaInstr n) -> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
+mkCoin _    (Coins 0 0) = id
+mkCoin meta n           = In4 . MetaInstr (meta n)
+
 {-|
 Smart-constuctor around `AddCoins`.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-addCoins :: Int -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
+addCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
 addCoins = mkCoin AddCoins
 
 {-|
 Smart-constuctor around `RefundCoins`.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-refundCoins :: Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
+refundCoins :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
 refundCoins = mkCoin RefundCoins
 
 {-|
 Smart-constuctor around `DrainCoins`.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-drainCoins :: Int -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
+drainCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
 drainCoins = mkCoin DrainCoins
 
 {-|
+Smart-constuctor around `RefundCoins`.
+
+@since 1.5.0.0
+-}
+giveBursary :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
+giveBursary = mkCoin GiveBursary
+
+{-|
+Smart-constructor around `PrefetchChar`.
+
+@since 1.5.0.0 
+-}
+prefetchChar :: Bool -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
+prefetchChar check = In4 . MetaInstr (PrefetchChar check)
+
+{-|
 Applies a value on the top of the stack to a function on the second-most top of the stack.
 
 @since 1.0.0.0
@@ -392,6 +420,8 @@
   show (Always k)    = getConst4 k ""
 
 instance Show (MetaInstr n) where
-  show (AddCoins n)    = "Add " ++ show n ++ " coins"
-  show (RefundCoins n) = "Refund " ++ show n ++ " coins"
-  show (DrainCoins n)  = "Using " ++ show n ++ " coins"
+  show (AddCoins n)     = "Add " ++ show n ++ " coins"
+  show (RefundCoins n)  = "Refund " ++ show n ++ " coins"
+  show (DrainCoins n)   = "Using " ++ show n ++ " coins"
+  show (GiveBursary n)  = "Bursary of " ++ show n ++ " coins"
+  show (PrefetchChar b) = "Prefetch character " ++ (if b then "with" else "without") ++ " length-check"
diff --git a/src/ghc/Parsley/Internal/Backend/Machine/LetBindings.hs b/src/ghc/Parsley/Internal/Backend/Machine/LetBindings.hs
--- a/src/ghc/Parsley/Internal/Backend/Machine/LetBindings.hs
+++ b/src/ghc/Parsley/Internal/Backend/Machine/LetBindings.hs
@@ -12,9 +12,10 @@
 @since 1.0.0.0
 -}
 module Parsley.Internal.Backend.Machine.LetBindings (
-    LetBinding(..),
+    LetBinding(..), Metadata, InputCharacteristic(..),
     Regs(..),
-    makeLetBinding,
+    makeLetBinding, newMeta,
+    successInputCharacteristic, failureInputCharacteristic,
     Binding
   ) where
 
@@ -40,20 +41,78 @@
 Packages a binding along with its free registers that are required
 for it, which are left existential. This is possible since the `Regs`
 datatype serves as a singleton-style witness of the original registers
-and their types.
+and their types. It also requires `Metadata` to be provided, sourced
+from analysis.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
-data LetBinding o a x = LetBinding (Binding o a x) (Some Regs)
+data LetBinding o a x = LetBinding {
+    body :: Binding o a x,
+    freeRegs :: Some Regs,
+    meta :: Metadata
+  }
 
+{- |
+This is used to store useful static information that can be
+used to guide code generation.
+
+See `successInputCharacteristic`, and `failureInputCharacteristic`.
+
+@since 1.5.0.0
+-}
+data Metadata = Metadata {
+    {- |
+    Characterises the way that a binding consumes input on success.
+
+    @since 1.5.0.0
+    -}
+    successInputCharacteristic :: InputCharacteristic,
+    {- |
+    Characterises the way that a binding consumes input on failure.
+
+    @since 1.5.0.0
+    -}
+    failureInputCharacteristic :: InputCharacteristic
+  }
+
 {-|
-Given a `Binding` and a set of existential `ΣVar`s, produces a
+Provides a way to describe how input is consumed in certain circumstances:
+
+* The input may be always the same on all paths
+* The input may always be consumed, but not the same on all paths
+* The input may never be consumed in any path
+* It may be inconsistent
+
+@since 1.5.0.0
+-}
+data InputCharacteristic = AlwaysConsumes (Maybe Word)
+                         -- ^ On all paths, input must be consumed: `Nothing` when the extact
+                         --   amount is inconsistent across paths.
+                         | NeverConsumes
+                         -- ^ On all paths, no input is consumed.
+                         | MayConsume
+                         -- ^ The input characteristic is unknown or inconsistent.
+
+{-|
+Given a `Binding` , a set of existential `ΣVar`s, and some `Metadata`, produces a
 `LetBinding` instance.
 
-@since 1.4.0.0
+@since 1.5.0.0
 -}
-makeLetBinding :: Binding o a x -> Set SomeΣVar -> LetBinding o a x
+makeLetBinding :: Binding o a x -> Set SomeΣVar -> Metadata -> LetBinding o a x
 makeLetBinding m rs = LetBinding m (makeRegs rs)
+
+{-|
+Produces a new `Metadata` object, with fields initialised to sensible conservative
+defaults.
+
+@since 1.5.0.0
+-}
+newMeta :: Metadata
+newMeta = Metadata {
+    successInputCharacteristic = MayConsume,
+    failureInputCharacteristic = MayConsume
+  }
 
 {-|
 Represents a collection of free registers, preserving their type
diff --git a/src/ghc/Parsley/Internal/Backend/Machine/LetRecBuilder.hs b/src/ghc/Parsley/Internal/Backend/Machine/LetRecBuilder.hs
--- a/src/ghc/Parsley/Internal/Backend/Machine/LetRecBuilder.hs
+++ b/src/ghc/Parsley/Internal/Backend/Machine/LetRecBuilder.hs
@@ -24,7 +24,7 @@
 #else
 import Language.Haskell.TH.Syntax                   (unTypeCode, unsafeCodeCoerce, Exp(VarE, LetE), Dec(FunD), Clause(Clause), Body(NormalB))
 #endif
-import Parsley.Internal.Backend.Machine.LetBindings (LetBinding(..), Binding, Regs)
+import Parsley.Internal.Backend.Machine.LetBindings (LetBinding(..), Metadata, Binding, Regs)
 import Parsley.Internal.Backend.Machine.Types       (QSubroutine, qSubroutine, Func)
 
 import Parsley.Internal.Common.Utils                (Code)
@@ -42,25 +42,25 @@
 Given a collection of bindings, generates a recursive binding group where each is allowed to
 refer to every other. These are then in scope for the top-level parser.
 
-@since 1.0.0.0
+@since 1.5.0.0
 -}
-letRec :: GCompare key 
+letRec :: GCompare key
        => {-bindings-}  DMap key (LetBinding o a)   -- ^ The bindings that should form part of the recursive group
       -> {-nameof-}     (forall x. key x -> String) -- ^ A function which can give a name to a key in the map
-      -> {-genBinding-} (forall x rs. key x -> Binding o a x -> Regs rs -> DMap key (QSubroutine s o a) -> Code (Func rs s o a x)) 
+      -> {-genBinding-} (forall x rs. key x -> Binding o a x -> Regs rs -> DMap key (QSubroutine s o a) -> Metadata -> Code (Func rs s o a x))
       -- ^ How a binding - and their free registers - should be converted into code
-      -> {-expr-}       (DMap key (QSubroutine s o a) -> Code b) 
+      -> {-expr-}       (DMap key (QSubroutine s o a) -> Code b)
       -- ^ How to produce the top-level binding given the compiled bindings, i.e. the @in@ for the @let@
       -> Code b
 letRec bindings nameOf genBinding expr = unsafeCodeCoerce $
   do -- Make a bunch of names
-     names <- traverseWithKey (\k (LetBinding _ rs) -> Const . (, rs) <$> newName (nameOf k)) bindings
+     names <- traverseWithKey (\k (LetBinding _ rs meta) -> Const . (, rs, meta) <$> newName (nameOf k)) bindings
      -- Wrap them up so that they are valid typed template haskell names
      let typedNames = DMap.map makeTypedName names
      -- Generate each binding providing them with the names
-     let makeDecl (k :=> LetBinding body (Some frees)) =
-          do let Const (name, _) = names ! k
-             func <- unTypeCode (genBinding k body frees typedNames)
+     let makeDecl (k :=> LetBinding body (Some frees) _) =
+          do let Const (name, _, meta) = names ! k
+             func <- unTypeCode (genBinding k body frees typedNames meta)
              return (FunD name [Clause [] (NormalB func) []])
      decls <- traverse makeDecl (toList bindings)
      -- Generate the main expression using the same names
@@ -68,5 +68,5 @@
      -- Construct the let expression
      return (LetE decls exp)
   where
-     makeTypedName :: Const (Name, Some Regs) x -> QSubroutine s o a x
-     makeTypedName (Const (name, Some frees)) = qSubroutine (unsafeCodeCoerce (return (VarE name))) frees
+     makeTypedName :: Const (Name, Some Regs, Metadata) x -> QSubroutine s o a x
+     makeTypedName (Const (name, Some frees, meta)) = qSubroutine (unsafeCodeCoerce (return (VarE name))) frees meta
diff --git a/src/ghc/Parsley/Internal/Backend/Machine/Types/Coins.hs b/src/ghc/Parsley/Internal/Backend/Machine/Types/Coins.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Backend/Machine/Types/Coins.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-|
+Module      : Parsley.Internal.Backend.Machine.Types.Coins
+Description : Meta-data associated with input consumption optimisations.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : unstable
+
+This module exposes `Coins` and the relevant operations. These are used by
+constant input analysis to side-step unnecessary length checks and character
+reads (in the case of lookahead).
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Backend.Machine.Types.Coins (
+    Coins(..),
+    int, zero,
+    minCoins, maxCoins,
+    plus1, plus, minus,
+    plusNotReclaim,
+  ) where
+
+{-|
+Packages together the known input that can be consumed after a length-check with the number of
+characters that can be rewound on a lookahead backtrack.
+
+@since 1.5.0.0
+-}
+data Coins = Coins {
+    -- | The number of tokens we know must be consumed along the path to succeed.
+    willConsume :: Int,
+    -- | The number of tokens we can reclaim if the parser backtracks.
+    canReclaim :: Int
+  } deriving stock Show
+
+{-|
+Makes a `Coins` value with equal quantities of coins and characters.
+
+@since 1.5.0.0
+-}
+int :: Int -> Coins
+int n = Coins n n
+
+{-|
+Makes a `Coins` value of 0.
+
+@since 1.5.0.0
+-}
+zero :: Coins
+zero = int 0
+
+zipCoins :: (Int -> Int -> Int) -> Coins -> Coins -> Coins
+zipCoins f (Coins k1 r1) (Coins k2 r2) = Coins (f k1 k2) (f r1 r2)
+
+{-|
+Takes the pairwise min of two `Coins` values.
+
+@since 1.5.0.0
+-}
+minCoins :: Coins -> Coins -> Coins
+minCoins = zipCoins min
+
+{-|
+Takes the pairwise max of two `Coins` values.
+
+@since 1.5.0.0
+-}
+maxCoins :: Coins -> Coins -> Coins
+maxCoins = zipCoins max
+
+{-|
+Adds 1 to all the `Coins` values.
+
+@since 1.5.0.0
+-}
+plus1 :: Coins -> Coins
+plus1 = plus (Coins 1 1)
+
+{-|
+Performs the pairwise addition of two `Coins` values.
+
+@since 1.5.0.0
+-}
+plus :: Coins -> Coins -> Coins
+plus = zipCoins (+)
+
+{-|
+Performs the pairwise subtraction of two `Coins` values.
+
+@since 1.5.0.0
+-}
+minus :: Coins -> Coins -> Coins
+minus = zipCoins (-)
+
+{-|
+A verson of plus where the reclaim value remains constant.
+
+@since 1.5.0.0
+-}
+plusNotReclaim :: Coins -> Int -> Coins
+plusNotReclaim (Coins k r) n = Coins (k + n) r
diff --git a/src/ghc/Parsley/Internal/Backend/Optimiser.hs b/src/ghc/Parsley/Internal/Backend/Optimiser.hs
deleted file mode 100644
--- a/src/ghc/Parsley/Internal/Backend/Optimiser.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-module Parsley.Internal.Backend.Optimiser (optimise) where
-
-import Data.GADT.Compare                (geq)
-import Data.Typeable                    ((:~:)(Refl))
-import Parsley.Internal.Backend.Machine
-import Parsley.Internal.Common.Indexed
-
--- We'll come back here later ;)
-optimise :: Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
-optimise (Push _ (In4 (Pop m))) = m
-optimise (Get _ _ (In4 (Pop m))) = m
-optimise (Dup (In4 (Pop m))) = m
-optimise (Dup (In4 (Swap m))) = In4 (Dup m)
-optimise (Get r1 a (In4 (Get r2 _ m))) | Just Refl <- r1 `geq` r2 = In4 (Get r1 a (In4 (Dup m)))
-optimise (Put r1 a (In4 (Get r2 _ m))) | Just Refl <- r1 `geq` r2 = In4 (Dup (In4 (Put r1 a m)))
-optimise (Get r1 _ (In4 (Put r2 _ m))) | Just Refl <- r1 `geq` r2 = m
-optimise m = In4 m
diff --git a/src/ghc/Parsley/Internal/Common.hs b/src/ghc/Parsley/Internal/Common.hs
--- a/src/ghc/Parsley/Internal/Common.hs
+++ b/src/ghc/Parsley/Internal/Common.hs
@@ -10,13 +10,15 @@
 module Parsley.Internal.Common (
     module Parsley.Internal.Common.Fresh,
     module Parsley.Internal.Common.Indexed,
-    module Parsley.Internal.Common.Queue,
+    module Parsley.Internal.Common.QueueLike, Queue, RewindQueue,
     module Parsley.Internal.Common.Utils,
     module Parsley.Internal.Common.Vec
   ) where
 
 import Parsley.Internal.Common.Fresh
 import Parsley.Internal.Common.Indexed
-import Parsley.Internal.Common.Queue
+import Parsley.Internal.Common.QueueLike
+import Parsley.Internal.Common.Queue (Queue)
+import Parsley.Internal.Common.RewindQueue (RewindQueue)
 import Parsley.Internal.Common.Utils
 import Parsley.Internal.Common.Vec
diff --git a/src/ghc/Parsley/Internal/Common/Queue.hs b/src/ghc/Parsley/Internal/Common/Queue.hs
--- a/src/ghc/Parsley/Internal/Common/Queue.hs
+++ b/src/ghc/Parsley/Internal/Common/Queue.hs
@@ -1,41 +1,26 @@
-{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
-{-# LANGUAGE ViewPatterns,
-             DerivingStrategies #-}
-module Parsley.Internal.Common.Queue (Queue, empty, enqueue, dequeue, null, size, foldr) where
-
-import Prelude hiding (null, foldr)
-
-import qualified Prelude (foldr)
-
-data Queue a = Queue {
-  outsz :: Int,
-  outs  :: [a],
-  insz  :: Int,
-  ins   :: [a]
-} deriving stock Eq
-
-empty :: Queue a
-empty = Queue 0 [] 0 []
-
-enqueue :: a -> Queue a -> Queue a
-enqueue x q = q {insz = insz q + 1, ins = x : ins q}
-
-dequeue :: Queue a -> (a, Queue a)
-dequeue q@(outs -> (x:outs')) = (x, q {outsz = outsz q - 1, outs = outs'})
-dequeue q@(outs -> [])        = dequeue (Queue (insz q) (reverse (ins q)) 0 [])
-
-null :: Queue a -> Bool
-null (Queue 0 [] 0 []) = True
-null _ = False
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-|
+Module      : Parsley.Internal.Common.Queue
+Description : Queue operations.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
 
-size :: Queue a -> Int
-size q = insz q + outsz q
+Exposes the instance of `QueueLike` for `Queue`.
 
-toList :: Queue a -> [a]
-toList q = outs q ++ reverse (ins q)
+@since 1.5.0.0
+-}
+module Parsley.Internal.Common.Queue (module Queue) where
 
-foldr :: (a -> b -> b) -> b -> Queue a -> b
-foldr f k = Prelude.foldr f k . toList
+import Parsley.Internal.Common.Queue.Impl as Queue (
+    Queue, empty, enqueue, dequeue, null, size, foldr, enqueueAll
+  )
+import Parsley.Internal.Common.QueueLike  (QueueLike(empty, null, size, enqueue, dequeue, enqueueAll))
 
-instance Show a => Show (Queue a) where
-  show = show . toList
+instance QueueLike Queue where
+  empty      = Queue.empty
+  null       = Queue.null
+  size       = Queue.size
+  enqueue    = Queue.enqueue
+  dequeue    = Queue.dequeue
+  enqueueAll = Queue.enqueueAll
diff --git a/src/ghc/Parsley/Internal/Common/Queue/Impl.hs b/src/ghc/Parsley/Internal/Common/Queue/Impl.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Common/Queue/Impl.hs
@@ -0,0 +1,104 @@
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+{-# LANGUAGE DerivingStrategies, ViewPatterns #-}
+{-|
+Module      : Parsley.Internal.Common.Queue.Impl
+Description : Implementation of a queue.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Implementation of a FIFO queue structure, with amortized operations.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Common.Queue.Impl (
+    module Parsley.Internal.Common.Queue.Impl
+  ) where
+
+import Prelude hiding (null, foldr)
+import Data.List (foldl')
+
+import qualified Prelude (foldr)
+
+{-|
+Concrete FIFO Queue, with amortized constant operations.
+
+@since 1.5.0.0
+-}
+data Queue a = Queue {
+  outsz :: Int,
+  outs  :: [a],
+  insz  :: Int,
+  ins   :: [a]
+} deriving stock Eq
+
+{-|
+Construct an empty queue.
+
+@since 1.5.0.0
+-}
+empty :: Queue a
+empty = Queue 0 [] 0 []
+
+{-|
+Adds an element onto the end of the queue.
+
+@since 1.5.0.0
+-}
+enqueue :: a -> Queue a -> Queue a
+enqueue x q = q {insz = insz q + 1, ins = x : ins q}
+
+{-|
+Adds each of the elements onto the queue, from left-to-right.
+
+@since 1.5.0.0
+-}
+enqueueAll :: [a] -> Queue a -> Queue a
+enqueueAll xs q = q { insz = insz q + length xs, ins = foldl' (flip (:)) (ins q) xs }
+
+{-|
+Removes an element from the front of the queue.
+
+@since 1.5.0.0
+-}
+dequeue :: Queue a -> (a, Queue a)
+dequeue q@(outs -> (x:outs')) = (x, q {outsz = outsz q - 1, outs = outs'})
+dequeue q@(outs -> [])
+  | insz q /= 0 = dequeue (Queue (insz q) (reverse (ins q)) 0 [])
+  | otherwise   = error "dequeue of empty queue"
+
+{-|
+Is the queue empty?
+
+@since 1.5.0.0
+-}
+null :: Queue a -> Bool
+null (Queue 0 [] 0 []) = True
+null _ = False
+
+{-|
+Returns how many elements are in the queue.
+
+@since 1.5.0.0
+-}
+size :: Queue a -> Int
+size q = insz q + outsz q
+
+{-|
+Folds the values in the queue.
+
+@since 1.5.0.0
+-}
+foldr :: (a -> b -> b) -> b -> Queue a -> b
+foldr f k = Prelude.foldr f k . toList
+
+instance Show a => Show (Queue a) where
+  show = show . toList
+
+{-|
+Converts this queue into a list.
+
+@since 1.5.0.0
+-}
+toList :: Queue a -> [a]
+toList q = outs q ++ reverse (ins q)
diff --git a/src/ghc/Parsley/Internal/Common/QueueLike.hs b/src/ghc/Parsley/Internal/Common/QueueLike.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Common/QueueLike.hs
@@ -0,0 +1,56 @@
+{-|
+Module      : Parsley.Internal.Common.QueueLike
+Description : Operations to work with Queue-like things.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes the core shared operations of queue implementations.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Common.QueueLike (module Parsley.Internal.Common.QueueLike) where
+
+{-|
+Operations on a queue-like structure @q@. These operations should be
+efficient, with amortized constant complexity for all of them except `enqueueAll`.
+
+@since 1.5.0.0
+-}
+class QueueLike q where
+  {-|
+  Construct an empty queue.
+
+  @since 1.5.0.0
+  -}
+  empty      :: q a
+  {-|
+  Is the queue empty?
+
+  @since 1.5.0.0
+  -}
+  null       :: q a -> Bool
+  {-|
+  Returns how many elements are in the queue.
+
+  @since 1.5.0.0
+  -}
+  size       :: q a -> Int
+  {-|
+  Adds an element onto the end of the queue.
+
+  @since 1.5.0.0
+  -}
+  enqueue    :: a -> q a -> q a
+  {-|
+  Removes an element from the front of the queue.
+
+  @since 1.5.0.0
+  -}
+  dequeue    :: q a -> (a, q a)
+  {-|
+  Adds each of the elements onto the queue, from left-to-right.
+
+  @since 1.5.0.0
+  -}
+  enqueueAll :: [a] -> q a -> q a
diff --git a/src/ghc/Parsley/Internal/Common/RewindQueue.hs b/src/ghc/Parsley/Internal/Common/RewindQueue.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Common/RewindQueue.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-|
+Module      : Parsley.Internal.Common.RewindQueue
+Description : RewindQueue operations.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes the instance of `QueueLike` for `RewindQueue`.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Common.RewindQueue (module RewindQueue) where
+
+import Parsley.Internal.Common.RewindQueue.Impl as RewindQueue (
+    RewindQueue, empty, enqueue, dequeue, rewind, null, size, foldr, enqueueAll
+  )
+import Parsley.Internal.Common.QueueLike  (QueueLike(empty, null, size, enqueue, dequeue, enqueueAll))
+
+instance QueueLike RewindQueue where
+  empty      = RewindQueue.empty
+  null       = RewindQueue.null
+  size       = RewindQueue.size
+  enqueue    = RewindQueue.enqueue
+  dequeue    = RewindQueue.dequeue
+  enqueueAll = RewindQueue.enqueueAll
diff --git a/src/ghc/Parsley/Internal/Common/RewindQueue/Impl.hs b/src/ghc/Parsley/Internal/Common/RewindQueue/Impl.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Common/RewindQueue/Impl.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE DerivingStrategies, RecordWildCards #-}
+{-|
+Module      : Parsley.Internal.Common.Queue.Impl
+Description : Implementation of a queue which can be rewound.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Implementation of a FIFO queue structure, with amortized operations that also supports a rewinding
+operation backed by a LIFO stack.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Common.RewindQueue.Impl (module Parsley.Internal.Common.RewindQueue.Impl) where
+
+import Prelude hiding (null, foldr)
+import Data.List (foldl')
+import Parsley.Internal.Common.Queue.Impl as Queue (Queue(..), toList)
+
+import qualified Parsley.Internal.Common.Queue.Impl as Queue (
+    empty, enqueue, enqueueAll, dequeue, null, size, foldr
+  )
+
+{-|
+Concrete FIFO Queue, with amortized constant operations.
+
+Also keeps history of dequeued values, which can be undone
+in a LIFO manner.
+
+@since 1.5.0.0
+-}
+data RewindQueue a = RewindQueue {
+    queue :: Queue a,
+    undo :: [a],
+    undosz :: Int
+  } deriving stock (Eq, Show)
+
+{-|
+Construct an empty queue.
+
+@since 1.5.0.0
+-}
+empty :: RewindQueue a
+empty = RewindQueue Queue.empty [] 0
+
+{-|
+Adds an element onto the end of the queue.
+
+@since 1.5.0.0
+-}
+enqueue :: a -> RewindQueue a -> RewindQueue a
+enqueue x q = q { queue = Queue.enqueue x (queue q) }
+
+{-|
+Adds each of the elements onto the queue, from left-to-right.
+
+@since 1.5.0.0
+-}
+enqueueAll :: [a] -> RewindQueue a -> RewindQueue a
+enqueueAll xs q = q { queue = Queue.enqueueAll xs (queue q) }
+
+{-|
+Removes an element from the front of the queue.
+
+@since 1.5.0.0
+-}
+dequeue :: RewindQueue a -> (a, RewindQueue a)
+dequeue RewindQueue{..} =
+  let (x, queue') = Queue.dequeue queue
+  in (x, RewindQueue { queue = queue', undo = x : undo, undosz = undosz + 1 })
+
+{-|
+Undoes the last \(n\) `dequeue` operations but /only/ if there are that many
+available undos. Otherwise, it will throw an error.
+
+@since 1.5.0.0
+-}
+rewind :: Int -> RewindQueue a -> RewindQueue a
+rewind n RewindQueue{..}
+  | n <= undosz = let (rs, undo') = splitAt n undo
+                  in RewindQueue { queue = queue { outsz = outsz queue + length rs,
+                                                   outs = foldl' (flip (:)) (outs queue) rs },
+                                   undo = undo',
+                                   undosz = undosz - n }
+  | otherwise   = error $ "Cannot rewind more than " ++ show undosz ++ " elements, but tried " ++ show n
+
+{-|
+Is the queue empty?
+
+@since 1.5.0.0
+-}
+null :: RewindQueue a -> Bool
+null = Queue.null . queue
+
+{-|
+Returns how many elements are in the queue.
+
+@since 1.5.0.0
+-}
+size :: RewindQueue a -> Int
+size = Queue.size . queue
+
+{-|
+Folds the values in the queue. Undo history is not included.
+
+@since 1.5.0.0
+-}
+foldr :: (a -> b -> b) -> b -> RewindQueue a -> b
+foldr f k = Queue.foldr f k . queue
+
+{-|
+Converts this queue into a list. Undo history is discarded.
+
+@since 1.5.0.0
+-}
+toList :: RewindQueue a -> [a]
+toList = Queue.toList . queue
diff --git a/src/ghc/Parsley/Internal/Core.hs b/src/ghc/Parsley/Internal/Core.hs
--- a/src/ghc/Parsley/Internal/Core.hs
+++ b/src/ghc/Parsley/Internal/Core.hs
@@ -14,6 +14,6 @@
     module Parsley.Internal.Core.InputTypes
   ) where
 
-import Parsley.Internal.Core.Defunc hiding (genDefunc, genDefunc1, genDefunc2, ap, unsafeBLACK, lamTerm, lamTermBool, adaptLam)
+import Parsley.Internal.Core.Defunc hiding (lamTerm, lamTermBool)
 import Parsley.Internal.Core.InputTypes
 import Parsley.Internal.Core.Primitives (Parser, ParserOps)
diff --git a/src/ghc/Parsley/Internal/Core/Defunc.hs b/src/ghc/Parsley/Internal/Core/Defunc.hs
--- a/src/ghc/Parsley/Internal/Core/Defunc.hs
+++ b/src/ghc/Parsley/Internal/Core/Defunc.hs
@@ -1,6 +1,22 @@
 {-# LANGUAGE PatternSynonyms, TypeApplications #-}
-module Parsley.Internal.Core.Defunc (module Parsley.Internal.Core.Defunc) where
+{-|
+Module      : Parsley.Internal.Core.Defunc
+Description : Combinator-level defunctionalisation
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
 
+This module contains the infrastructure and definitions of defunctionalised
+terms that can be used by the user and the frontend.
+
+@since 1.0.0.0
+-}
+module Parsley.Internal.Core.Defunc (
+    Defunc(..),
+    pattern COMPOSE_H, pattern FLIP_H, pattern FLIP_CONST, pattern UNIT,
+    lamTerm, lamTermBool
+  ) where
+
 --import Data.Typeable                 (Typeable, (:~:)(Refl), eqT)
 import Language.Haskell.TH.Syntax    (Lift(..))
 import Parsley.Internal.Common.Utils (WQ(..), Code, Quapplicative(..))
@@ -13,7 +29,6 @@
   This will come in parsley-2.0.0.0.
 -}
 
-
 {-|
 This datatype is useful for providing an /inspectable/ representation of common Haskell functions.
 These can be provided in place of `WQ` to any combinator that requires it. The only difference is
@@ -28,40 +43,40 @@
 data Defunc a where
   -- | Corresponds to the standard @id@ function
   ID      :: Defunc (a -> a)
-  -- | Corresponds to the standard @(.)@ function applied to no arguments
+  -- | Corresponds to the standard @(.)@ function applied to no arguments.
   COMPOSE :: Defunc ((b -> c) -> (a -> b) -> (a -> c))
-  -- | Corresponds to the standard @flip@ function applied to no arguments
+  -- | Corresponds to the standard @flip@ function applied to no arguments.
   FLIP    :: Defunc ((a -> b -> c) -> b -> a -> c)
-  -- | Corresponds to function application of two other `Defunc` values
+  -- | Corresponds to function application of two other `Defunc` values.
   APP_H   :: Defunc (a -> b) -> Defunc a -> Defunc b
-  -- | Corresponds to the partially applied @(== x)@ for some `Defunc` value @x@
+  -- | Corresponds to the partially applied @(== x)@ for some `Defunc` value @x@.
   EQ_H    :: Eq a => Defunc a -> Defunc (a -> Bool)
-  -- | Represents a liftable, showable value
+  -- | Represents a liftable, showable value.
   LIFTED  :: (Show a, Lift a{-, Typeable a-}) => a -> Defunc a
-  -- | Represents the standard @(:)@ function applied to no arguments
+  -- | Represents the standard @(:)@ function applied to no arguments.
   CONS    :: Defunc (a -> [a] -> [a])
-  -- | Represents the standard @const@ function applied to no arguments
+  -- | Represents the standard @const@ function applied to no arguments.
   CONST   :: Defunc (a -> b -> a)
-  -- | Represents the empty list @[]@
+  -- | Represents the empty list @[]@.
   EMPTY   :: Defunc [a]
-  -- | Wraps up any value of type `WQ`
+  -- | Wraps up any value of type `WQ`.
   BLACK   :: WQ a -> Defunc a
 
   -- Syntax constructors
   {-|
-  Represents the regular Haskell @if@ syntax
+  Represents the regular Haskell @if@ syntax.
 
   @since 0.1.1.0
   -}
   IF_S    :: Defunc Bool -> Defunc a -> Defunc a -> Defunc a
   {-|
-  Represents a Haskell lambda abstraction
+  Represents a Haskell lambda abstraction.
 
   @since 0.1.1.0
   -}
   LAM_S   :: (Defunc a -> Defunc b) -> Defunc (a -> b)
   {-|
-  Represents a Haskell let binding
+  Represents a Haskell let binding.
 
   @since 0.1.1.0
   -}
@@ -77,9 +92,9 @@
   _val ID           = id
   _val COMPOSE      = (.)
   _val FLIP         = flip
-  _val (APP_H f x)  = (_val f) (_val x)
+  _val (APP_H f x)  = _val f (_val x)
   _val (LIFTED x)   = x
-  _val (EQ_H x)     = ((_val x) ==)
+  _val (EQ_H x)     = (_val x ==)
   _val CONS         = (:)
   _val CONST        = const
   _val EMPTY        = []
@@ -92,44 +107,53 @@
   (>*<) = APP_H
 
 {-|
-This pattern represents fully applied composition of two `Defunc` values
+This pattern represents fully applied composition of two `Defunc` values.
 
 @since 0.1.0.0
 -}
 pattern COMPOSE_H     :: () => ((x -> y -> z) ~ ((b -> c) -> (a -> b) -> a -> c)) => Defunc x -> Defunc y -> Defunc z
 pattern COMPOSE_H f g = APP_H (APP_H COMPOSE f) g
 {-|
-This pattern corresponds to the standard @flip@ function applied to a single argument
+This pattern corresponds to the standard @flip@ function applied to a single argument.
 
 @since 0.1.0.0
 -}
 pattern FLIP_H        :: () => ((x -> y) ~ ((a -> b -> c) -> b -> a -> c)) => Defunc x -> Defunc y
 pattern FLIP_H f      = APP_H FLIP f
 {-|
-Represents the flipped standard @const@ function applied to no arguments
+Represents the flipped standard @const@ function applied to no arguments.
 
 @since 0.1.0.0
 -}
 pattern FLIP_CONST    :: () => (x ~ (a -> b -> b)) => Defunc x
 pattern FLIP_CONST    = FLIP_H CONST
 {-|
-This pattern represents the unit value @()@
+This pattern represents the unit value @()@.
 
 @since 0.1.0.0
 -}
 pattern UNIT          :: Defunc ()
 pattern UNIT          = LIFTED ()
 
-ap :: Defunc (a -> b) -> Defunc a -> Defunc b
-ap = APP_H
-
 -- TODO: This is deprecated in favour of Typeable as of parsley 2.0.0.0
+{-|
+Specialised conversion for functions returning `Bool`. This will go
+as soon as `Defunc` has a `Typeable` constraint in parsley 2.
+
+@since 1.0.1.0
+-}
 lamTermBool :: Defunc (a -> Bool) -> Lam (a -> Bool)
 lamTermBool (APP_H CONST (LIFTED True)) = Abs (const T)
 lamTermBool (APP_H CONST (LIFTED False)) = Abs (const F)
 lamTermBool f = lamTerm f
 
-lamTerm :: forall a. Defunc a -> Lam a
+{-|
+Converts a `Defunc` value into an equivalent `Lam` value, discarding
+the inspectivity of functions.
+
+@since 1.0.1.0
+-}
+lamTerm :: {-forall a.-} Defunc a -> Lam a
 lamTerm ID = Abs id
 lamTerm COMPOSE = Abs (\f -> Abs (\g -> Abs (App f . App g)))
 lamTerm FLIP = Abs (\f -> Abs (\x -> Abs (\y -> App (App f y) x)))
@@ -158,15 +182,6 @@
     defuncTerm (Let x f)  = LET_S (defuncTerm x) (defuncTerm . f . lamTerm)
     defuncTerm T          = LIFTED True
     defuncTerm F          = LIFTED False
-
-genDefunc :: Defunc a -> Code a
-genDefunc = normaliseGen . lamTerm
-
-genDefunc1 :: Defunc (a -> b) -> Code a -> Code b
-genDefunc1 f x = genDefunc (APP_H f (unsafeBLACK x))
-
-genDefunc2 :: Defunc (a -> b -> c) -> Code a -> Code b -> Code c
-genDefunc2 f x y = genDefunc (APP_H (APP_H f (unsafeBLACK x)) (unsafeBLACK y))
 
 unsafeBLACK :: Code a -> Defunc a
 unsafeBLACK = BLACK . WQ undefined
diff --git a/src/ghc/Parsley/Internal/Core/Identifiers.hs b/src/ghc/Parsley/Internal/Core/Identifiers.hs
--- a/src/ghc/Parsley/Internal/Core/Identifiers.hs
+++ b/src/ghc/Parsley/Internal/Core/Identifiers.hs
@@ -1,6 +1,18 @@
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 {-# LANGUAGE DerivingStrategies,
              GeneralizedNewtypeDeriving #-}
+{-|
+Module      : Parsley.Internal.Backend.Machine.Identifiers
+Description : frontend specific identifiers.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+This module defines "identifiers", which are used to uniquely identify different
+nodes in the combinator tree (and abstract machine).
+
+@since 1.0.0.0
+-}
 module Parsley.Internal.Core.Identifiers (
     MVar(..), IMVar,
     ΣVar(..), IΣVar, SomeΣVar(..), getIΣVar
@@ -14,9 +26,31 @@
 import Data.Word         (Word64)
 import Unsafe.Coerce     (unsafeCoerce)
 
+{-|
+An identifier representing concrete registers and mutable state.
+
+@since 0.1.0.0
+-}
 newtype ΣVar (a :: Type) = ΣVar IΣVar
+{-|
+An identifier representing let-bound parsers, recursion, and iteration.
+
+@since 0.1.0.0
+-}
 newtype MVar (a :: Type) = MVar IMVar
+
+{-|
+Underlying untyped identifier, which is numeric but otherwise opaque.
+
+@since 0.1.0.0
+-}
 newtype IMVar = IMVar Word64 deriving newtype (Ord, Eq, Num, Enum, Show, Ix)
+
+{-|
+Underlying untyped identifier, which is numeric but otherwise opaque.
+
+@since 0.1.0.0
+-}
 newtype IΣVar = IΣVar Word64 deriving newtype (Ord, Eq, Num, Enum, Show, Ix)
 
 instance Show (MVar a) where show (MVar μ) = "μ" ++ show μ
@@ -33,11 +67,21 @@
     EQ -> case geq σ1 σ2 of Just Refl -> GEQ
     GT -> GGT
 
+{-|
+An identifier representing some concrete register, but where the type is existential.
+
+@since 0.1.0.0
+-}
 data SomeΣVar = forall r. SomeΣVar (ΣVar r)
 instance Eq SomeΣVar where (==) = (==) `on` getIΣVar
 instance Ord SomeΣVar where compare = compare `on` getIΣVar
 instance Show SomeΣVar where show (SomeΣVar σ) = show σ
 
+{-|
+Fetch the untyped identifier from under the existential.
+
+@since 0.1.0.0
+-}
 getIΣVar :: SomeΣVar -> IΣVar
 getIΣVar (SomeΣVar (ΣVar σ)) = σ
 
diff --git a/src/ghc/Parsley/Internal/Core/InputTypes.hs b/src/ghc/Parsley/Internal/Core/InputTypes.hs
--- a/src/ghc/Parsley/Internal/Core/InputTypes.hs
+++ b/src/ghc/Parsley/Internal/Core/InputTypes.hs
@@ -1,3 +1,14 @@
+{-|
+Module      : Parsley.Internal.Core.InputTypes
+Description : Auxilliary input types.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Extra types of input specialised for specific scenarios.
+
+@since 1.0.0.0
+-}
 module Parsley.Internal.Core.InputTypes (module Parsley.Internal.Core.InputTypes) where
 
 import Data.Text (Text)
@@ -6,7 +17,7 @@
 By wrapping a regular @Text@ input with this newtype, Parsley will assume that all
 of the characters fit into exactly one 16-bit chunk. This allows the consumption of
 characters in the datatype to be consumed much faster, but does not support multi-word
-characters. 
+characters.
 
 @since 0.1.0.0
 -}
diff --git a/src/ghc/Parsley/Internal/Core/Lam.hs b/src/ghc/Parsley/Internal/Core/Lam.hs
--- a/src/ghc/Parsley/Internal/Core/Lam.hs
+++ b/src/ghc/Parsley/Internal/Core/Lam.hs
@@ -1,16 +1,49 @@
+{-|
+Module      : Parsley.Internal.Core.Lam
+Description : Generic defunctionalised abstraction.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+This module contains `Lam`, which is a defunctionalised lambda calculus.
+This serves as a more easy to work with form of defunctionalisation moving
+into the backend and machine where it is no longer necessary to inspect function
+values. It permits for the generation of efficient terms, with some inspection
+of values.
+
+@since 1.0.1.0
+-}
 module Parsley.Internal.Core.Lam (normaliseGen, normalise, Lam(..)) where
 
 import Parsley.Internal.Common.Utils (Code)
 
+{-|
+Defunctionalised lambda calculus in HOAS form. Supports basic inspection
+of values, but not functions.
+
+@since 1.0.1.0
+-}
 data Lam a where
+    -- | Function abstraction.
     Abs :: (Lam a -> Lam b) -> Lam (a -> b)
+    -- | Function application.
     App :: Lam (a -> b) -> Lam a -> Lam b
+    -- | Variable. The boolean represents whether it is "simple" or "complex", i.e. the size of the term.
     Var :: Bool {- Simple -} -> Code a -> Lam a
+    -- | Conditional expression.
     If  :: Lam Bool -> Lam a -> Lam a -> Lam a
+    -- | Let-binding.
     Let :: Lam a -> (Lam a -> Lam b) -> Lam b
+    -- | Value representing true.
     T   :: Lam Bool
+    -- | Value representing false.
     F   :: Lam Bool
 
+{-|
+Optimises a `Lam` expression, reducing it until the outmost lambda, let, or if statement.
+
+@since 1.0.1.0
+-}
 normalise :: Lam a -> Lam a
 normalise x = if normal x then x else reduce x
   where
@@ -46,6 +79,12 @@
 generate T          = [||True||]
 generate F          = [||False||]
 
+{-|
+Generates Haskell code that represents a `Lam` value, but normalising it first to ensure the
+term is minimal.
+
+@since 1.0.1.0
+-}
 normaliseGen :: Lam a -> Code a
 normaliseGen = generate . normalise
 
diff --git a/src/ghc/Parsley/Internal/Frontend/Analysis.hs b/src/ghc/Parsley/Internal/Frontend/Analysis.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Frontend/Analysis.hs
@@ -0,0 +1,30 @@
+{-|
+Module      : Parsley.Internal.Frontend.Analysis
+Description : Exposes various analysis passes.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes the analysis passes defined within the analysis submodules via `analyse`.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Frontend.Analysis (
+    analyse, dependencyAnalysis,
+    module Flags
+  ) where
+
+import Parsley.Internal.Common.Indexed                 (Fix)
+import Parsley.Internal.Core.CombinatorAST             (Combinator)
+import Parsley.Internal.Frontend.Analysis.Cut          (cutAnalysis)
+import Parsley.Internal.Frontend.Analysis.Dependencies (dependencyAnalysis)
+
+import Parsley.Internal.Frontend.Analysis.Flags as Flags (emptyFlags, AnalysisFlags(letBound))
+
+{-|
+Performs Cut-Analysis on the combinator tree (See "Parsley.Internal.Frontend.Analysis.Cut")
+
+@since 1.5.0.0
+-}
+analyse :: AnalysisFlags -> Fix Combinator a -> Fix Combinator a
+analyse flags = cutAnalysis (letBound flags)
diff --git a/src/ghc/Parsley/Internal/Frontend/Analysis/Cut.hs b/src/ghc/Parsley/Internal/Frontend/Analysis/Cut.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Frontend/Analysis/Cut.hs
@@ -0,0 +1,137 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-|
+Module      : Parsley.Internal.Frontend.Analysis.Cut
+Description : Marks cut points in the parser.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes a transformation that annotates the parts of the grammar where cuts occur: these are places
+where backtracking is not allowed to occur. This information is used to help with correct allocation
+of coins used for "Parsley.Internal.Backend.Analysis.Coins": the combinator tree has access to scoping
+information lost in the machine.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Frontend.Analysis.Cut (cutAnalysis) where
+
+import Data.Coerce                         (coerce)
+import Data.Kind                           (Type)
+import Parsley.Internal.Common.Indexed     (Fix(..), zygo, (:*:)(..), ifst)
+import Parsley.Internal.Core.CombinatorAST (Combinator(..), MetaCombinator(..))
+
+{-|
+Annotate a tree with its cut-points. We assume a cut for let-bound parsers.
+
+@since 1.5.0.0
+-}
+cutAnalysis :: Bool -- ^ Whether or not the parser in question is a let-bound parser.
+            -> Fix Combinator a -> Fix Combinator a
+cutAnalysis letBound = fst . ($ letBound) . doCut . zygo (CutAnalysis . cutAlg) compliance
+
+data Compliance (k :: Type) = DomComp | NonComp | Comp | FullPure deriving stock (Show, Eq)
+newtype CutAnalysis a = CutAnalysis { doCut :: Bool -> (Fix Combinator a, Bool) }
+
+seqCompliance :: Compliance a -> Compliance b -> Compliance c
+seqCompliance c FullPure = coerce c
+seqCompliance FullPure c = coerce c
+seqCompliance Comp _     = Comp
+seqCompliance _ _        = NonComp
+
+caseCompliance :: Compliance a -> Compliance b -> Compliance c
+caseCompliance c FullPure              = coerce c
+caseCompliance FullPure c              = coerce c
+caseCompliance c1 c2 | c1 == coerce c2 = coerce c1
+caseCompliance _ _                     = NonComp
+
+{-# INLINE compliance #-}
+compliance :: Combinator Compliance a -> Compliance a
+compliance (Pure _)                 = FullPure
+compliance (Satisfy _)              = NonComp
+compliance Empty                    = FullPure
+compliance Let{}                    = DomComp
+compliance (Try _)                  = DomComp
+compliance (NonComp :<|>: FullPure) = Comp
+compliance (_ :<|>: _)              = NonComp
+compliance (l :<*>: r)              = seqCompliance l r
+compliance (l :<*: r)               = seqCompliance l r
+compliance (l :*>: r)               = seqCompliance l r
+compliance (LookAhead c)            = c -- Lookahead will consume input on failure, so its compliance matches that which is beneath it
+compliance (NotFollowedBy _)        = FullPure
+compliance (Debug _ c)              = c
+compliance (ChainPre NonComp p)     = seqCompliance Comp p
+compliance (ChainPre _ p)           = seqCompliance NonComp p
+compliance (ChainPost p NonComp)    = seqCompliance p Comp
+compliance (ChainPost p _)          = seqCompliance p NonComp
+compliance (Branch b p q)           = seqCompliance b (caseCompliance p q)
+compliance (Match p _ qs def)       = seqCompliance p (foldr1 caseCompliance (def:qs))
+compliance (MakeRegister _ l r)     = seqCompliance l r
+compliance (GetRegister _)          = FullPure
+compliance (PutRegister _ c)        = coerce c
+compliance (MetaCombinator _ c)     = c
+
+cutAlg :: Combinator (CutAnalysis :*: Compliance) a -> Bool -> (Fix Combinator a, Bool)
+cutAlg (Pure x) _ = (In (Pure x), False)
+cutAlg (Satisfy f) cut = (mkCut cut (In (Satisfy f)), True)
+cutAlg Empty _ = (In Empty, False)
+cutAlg (Let r μ p) cut = (mkCut (not cut) (In (Let r μ (fst (doCut (ifst p) True)))), False) -- If there is no cut, we generate a piggy for the continuation
+cutAlg (Try p) _ = False <$ rewrap Try False (ifst p)
+cutAlg ((p :*: NonComp) :<|>: (q :*: FullPure)) _ = (requiresCut (In (fst (doCut p True) :<|>: fst (doCut q False))), True)
+cutAlg (p :<|>: q) cut =
+  let (q', handled) = doCut (ifst q) cut
+  in (In (fst (doCut (ifst p) False) :<|>: q'), handled)
+cutAlg (l :<*>: r) cut = seqCutAlg (:<*>:) cut (ifst l) (ifst r)
+cutAlg (l :<*: r) cut = seqCutAlg (:<*:) cut (ifst l) (ifst r)
+cutAlg (l :*>: r) cut = seqCutAlg (:*>:) cut (ifst l) (ifst r)
+cutAlg (LookAhead p) cut = rewrap LookAhead cut (ifst p)
+cutAlg (NotFollowedBy p) _ = False <$ rewrap NotFollowedBy False (ifst p)
+cutAlg (Debug msg p) cut = rewrap (Debug msg) cut (ifst p)
+cutAlg (ChainPre (op :*: NonComp) p) _ =
+  let (op', _) = doCut op True
+      (p', _) = doCut (ifst p) False
+  in (requiresCut (In (ChainPre op' p')), True)
+cutAlg (ChainPre op p) cut =
+  let (op', _) = doCut (ifst op) False
+      (p', handled) = doCut (ifst p) cut
+  in (mkCut (not cut) (In (ChainPre op' p')), handled)
+cutAlg (ChainPost p (op :*: NonComp)) cut =
+  let (p', _) = doCut (ifst p) cut
+      (op', _) = doCut op True
+  in (requiresCut (In (ChainPost p' op')), True)
+cutAlg (ChainPost p op) cut =
+  let (p', handled) = doCut (ifst p) cut
+      (op', _) = doCut (ifst op) False
+  in (mkCut (cut && handled) (In (ChainPost p' op')), handled)
+cutAlg (Branch b p q) cut =
+  let (b', handled) = doCut (ifst b) cut
+      (p', handled') = doCut (ifst p) (cut && not handled)
+      (q', handled'') = doCut (ifst q) (cut && not handled)
+  in (In (Branch b' p' q'), handled || (handled' && handled''))
+cutAlg (Match p f qs def) cut =
+  let (p', handled) = doCut (ifst p) cut
+      (def', handled') = doCut (ifst def) (cut && not handled)
+      (qs', handled'') = foldr (\q -> biliftA2 (:) (&&) (doCut (ifst q) (cut && not handled))) ([], handled') qs
+  in (In (Match p' f qs' def'), handled || handled'')
+cutAlg (MakeRegister σ l r) cut = seqCutAlg (MakeRegister σ) cut (ifst l) (ifst r)
+cutAlg (GetRegister σ) _ = (In (GetRegister σ), False)
+cutAlg (PutRegister σ p) cut = rewrap (PutRegister σ) cut (ifst p)
+cutAlg (MetaCombinator m p) cut = rewrap (MetaCombinator m) cut (ifst p)
+
+mkCut :: Bool -> Fix Combinator a -> Fix Combinator a
+mkCut True = In . MetaCombinator Cut
+mkCut False = id
+
+requiresCut :: Fix Combinator a -> Fix Combinator a
+requiresCut = In . MetaCombinator RequiresCut
+
+seqCutAlg :: (Fix Combinator a -> Fix Combinator b -> Combinator (Fix Combinator) c) -> Bool -> CutAnalysis a -> CutAnalysis b -> (Fix Combinator c, Bool)
+seqCutAlg con cut l r =
+  let (l', handled) = doCut l cut
+      (r', handled') = doCut r (cut && not handled)
+  in (In (con l' r'), handled || handled')
+
+rewrap :: (Fix Combinator a -> Combinator (Fix Combinator) b) -> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
+rewrap con cut p = let (p', handled) = doCut p cut in (In (con p'), handled)
+
+biliftA2 :: (a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
+biliftA2 f g (x1, y1) (x2, y2) = (f x1 x2, g y1 y2)
diff --git a/src/ghc/Parsley/Internal/Frontend/Analysis/Dependencies.hs b/src/ghc/Parsley/Internal/Frontend/Analysis/Dependencies.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Frontend/Analysis/Dependencies.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE RecordWildCards #-}
+{-|
+Module      : Parsley.Internal.Frontend.Analysis.Dependencies
+Description : Calculate dependencies of a collection of bindings.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes `dependencyAnalysis`, which is used to calculate information
+regarding the dependencies of each let-bound parser, as well as their
+free-registers.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Frontend.Analysis.Dependencies (dependencyAnalysis) where
+
+import Control.Arrow                        (first, second)
+import Control.Monad                        (unless, forM_)
+import Data.Array                           (Array, (!), listArray)
+import Data.Array.MArray                    (readArray, writeArray, newArray)
+import Data.Array.ST                        (runSTUArray)
+import Data.Array.Unboxed                   (assocs)
+import Data.Dependent.Map                   (DMap)
+import Data.List                            (foldl', partition, sortOn)
+import Data.Map.Strict                      (Map)
+import Data.Set                             (Set, insert, (\\), union, notMember, empty)
+import Data.STRef                           (newSTRef, readSTRef, writeSTRef)
+import Parsley.Internal.Common.Indexed      (Fix, cata, Const1(..), (:*:)(..), zipper)
+import Parsley.Internal.Common.State        (State, MonadState, execState, modify')
+import Parsley.Internal.Core.CombinatorAST  (Combinator(..), traverseCombinator)
+import Parsley.Internal.Core.Identifiers    (IMVar, MVar(..), IΣVar, ΣVar, SomeΣVar(..), getIΣVar)
+
+import qualified Data.Dependent.Map as DMap (foldrWithKey, filterWithKey)
+import qualified Data.Map.Strict    as Map  ((!), empty, insert, mapMaybeWithKey, findMax, elems, lookup, foldMapWithKey)
+import qualified Data.Set           as Set  (elems, empty, insert, lookupMax)
+
+type Graph = Array IMVar [IMVar]
+
+{-|
+Given a top-level parser and a collection of its let-bound subjects performs the following tasks:
+
+* Determines which parser depend on which others.
+* Use the previous information to remove any dead bindings.
+* Calculate the direct free registers for each binding.
+* Propogate the free registers according to transitive need via the dependency graph.
+
+Returns the non-dead bindings, the information about each bindings free registers, and the next
+free index for any registers created in code generation.
+
+@since 1.5.0.0
+-}
+-- TODO This actually should be in the backend... dead bindings and the topological ordering can be computed here
+--      but the register stuff should come after register optimisation and instruction peephole
+dependencyAnalysis :: Fix Combinator a -> DMap MVar (Fix Combinator) -> (DMap MVar (Fix Combinator), Map IMVar (Set SomeΣVar), IΣVar)
+dependencyAnalysis toplevel μs =
+  let -- Step 1: find roots of the toplevel
+      roots = directDependencies toplevel
+      -- Step 2: build immediate dependencies
+      DependencyMaps{..} = buildDependencyMaps μs
+      -- Step 3: find the largest name
+      n = fst (Map.findMax immediateDependencies)
+      -- Step 4: Build a dependency graph
+      graph = buildGraph n immediateDependencies
+      -- Step 5: construct the seen set (dfnum)
+      -- Step 6: dfs from toplevel (via roots) all with same seen set
+      -- Step 7: elems of seen set with dfnum 0 are dead, otherwise they are collected into a list in descending order
+      (topo, dead) = topoOrdering roots n graph
+      -- Step 8: perform a dfs on each of the topo, with a new seen set for each,
+      --         building the flattened dependency map. If the current focus has
+      --         already been computed, add all its deps to the seen set and skip.
+      --         The end seen set becomes out flattened deps.
+      trueDeps = flattenDependencies topo (minMax topo) graph
+      -- Step 8: Compute the new registers, and remove dead ones
+      addNewRegs v uses
+        | notMember v dead = let deps = trueDeps Map.! v
+                                 defs = definedRegisters Map.! v
+                                 subUses = foldMap (usedRegisters Map.!) deps
+                                 subDefs = foldMap (definedRegisters Map.!) deps
+                             in Just $ (uses \\ defs) `union` (subUses \\ subDefs)
+        | otherwise        = Nothing
+      trueRegs = Map.mapMaybeWithKey addNewRegs usedRegisters
+      largestRegister = maybe (-1) getIΣVar (Set.lookupMax (Map.foldMapWithKey (const id) definedRegisters))
+  in (DMap.filterWithKey (\(MVar v) _ -> notMember v dead) μs, trueRegs, largestRegister)
+
+minMax :: Ord a => [a] -> (a, a)
+minMax []     = error "cannot find minimum or maximum of empty list"
+minMax (x:xs) = foldl' (\(small, big) x -> (min small x, max big x)) (x, x) xs
+
+buildGraph :: IMVar -> Map IMVar (Set IMVar) -> Graph
+buildGraph n = listArray (0, n) . map Set.elems . Map.elems
+
+topoOrdering :: Set IMVar -> IMVar -> Graph -> ([IMVar], Set IMVar)
+topoOrdering roots n graph =
+  let dfnums = runSTUArray $ do
+        dfnums <- newArray (0, n) (0 :: Int)
+        nextDfnum <- newSTRef 1
+        let hasSeen v = (/= 0) <$> readArray dfnums v
+        let setSeen v = do dfnum <- readSTRef nextDfnum
+                           writeArray dfnums v dfnum
+                           writeSTRef nextDfnum (dfnum + 1)
+        forM_ roots (dfs hasSeen setSeen graph)
+        return dfnums
+      (lives, deads) = partition ((/= 0) . snd) (assocs dfnums)
+  in (reverseMap fst (sortOn snd lives), foldl' (\ds v0 -> Set.insert (fst v0) ds) Set.empty deads)
+
+reverseMap :: (a -> b) -> [a] -> [b]
+reverseMap f = foldl' (\xs x -> f x : xs) []
+
+flattenDependencies :: [IMVar] -> (IMVar, IMVar) -> Graph -> Map IMVar (Set IMVar)
+flattenDependencies topo range graph = foldl' reachable Map.empty topo
+  where
+    reachable :: Map IMVar (Set IMVar) -> IMVar -> Map IMVar (Set IMVar)
+    reachable deps root =
+      let seen = runSTUArray $ do
+            seen <- newArray range False
+            let setSeen v = writeArray seen v True
+            let seenOrSkip v = case Map.lookup v deps of
+                  Nothing -> readArray seen v
+                  Just ds -> setSeen v >> forM_ ds setSeen >> return True
+            dfs seenOrSkip setSeen graph root
+            return seen
+          ds = foldl' (\ds (v, b) -> if b then Set.insert v ds else ds) Set.empty (assocs seen)
+      in Map.insert root ds deps
+
+dfs :: Monad m => (IMVar -> m Bool) -> (IMVar -> m ()) -> Graph -> IMVar -> m ()
+dfs hasSeen setSeen graph = go
+  where
+    go v = do seen <- hasSeen v
+              unless seen $
+                do setSeen v
+                   forM_ (graph ! v) go
+
+-- IMMEDIATE DEPENDENCY MAPS
+data DependencyMaps = DependencyMaps {
+  usedRegisters         :: Map IMVar (Set SomeΣVar), -- Leave Lazy
+  immediateDependencies :: Map IMVar (Set IMVar), -- Could be Strict
+  definedRegisters      :: Map IMVar (Set SomeΣVar)
+}
+
+buildDependencyMaps :: DMap MVar (Fix Combinator) -> DependencyMaps
+buildDependencyMaps = DMap.foldrWithKey (\(MVar v) p deps@DependencyMaps{..} ->
+  let (frs, defs, ds) = freeRegistersAndDependencies v p
+  in deps { usedRegisters = Map.insert v frs usedRegisters
+          , immediateDependencies = Map.insert v ds immediateDependencies
+          , definedRegisters = Map.insert v defs definedRegisters}) (DependencyMaps Map.empty Map.empty Map.empty)
+
+freeRegistersAndDependencies :: IMVar -> Fix Combinator a -> (Set SomeΣVar,  Set SomeΣVar, Set IMVar)
+freeRegistersAndDependencies v p =
+  let frsm :*: depsm = zipper freeRegistersAlg (dependenciesAlg (Just v)) p
+      (frs, defs) = runFreeRegisters frsm
+      ds = runDependencies depsm
+  in (frs, defs, ds)
+
+-- DEPENDENCY ANALYSIS
+newtype Dependencies a = Dependencies { doDependencies :: State (Set IMVar) () }
+runDependencies :: Dependencies a -> Set IMVar
+runDependencies = flip execState empty. doDependencies
+
+directDependencies :: Fix Combinator a -> Set IMVar
+directDependencies = runDependencies . cata (dependenciesAlg Nothing)
+
+{-# INLINE dependenciesAlg #-}
+dependenciesAlg :: Maybe IMVar -> Combinator Dependencies a -> Dependencies a
+dependenciesAlg (Just v) (Let _ μ@(MVar u) _) = Dependencies $ do unless (u == v) (dependsOn μ)
+dependenciesAlg Nothing  (Let _ μ _)          = Dependencies $ do dependsOn μ
+dependenciesAlg _ p                           = Dependencies $ do traverseCombinator (fmap Const1 . doDependencies) p; return ()
+
+dependsOn :: MonadState (Set IMVar) m => MVar a -> m ()
+dependsOn (MVar v) = modify' (insert v)
+
+-- FREE REGISTER ANALYSIS
+newtype FreeRegisters a = FreeRegisters { doFreeRegisters :: State (Set SomeΣVar, Set SomeΣVar) () }
+runFreeRegisters :: FreeRegisters a -> (Set SomeΣVar, Set SomeΣVar)
+runFreeRegisters = flip execState (empty, empty) . doFreeRegisters
+
+{-# INLINE freeRegistersAlg #-}
+freeRegistersAlg :: Combinator FreeRegisters a -> FreeRegisters a
+freeRegistersAlg (GetRegister σ)      = FreeRegisters $ do uses σ
+freeRegistersAlg (PutRegister σ p)    = FreeRegisters $ do uses σ; doFreeRegisters p
+freeRegistersAlg (MakeRegister σ p q) = FreeRegisters $ do defs σ; doFreeRegisters p; doFreeRegisters q
+freeRegistersAlg Let{}                = FreeRegisters $ do return () -- TODO This can be removed when Let doesn't have the body in it...
+freeRegistersAlg p                    = FreeRegisters $ do traverseCombinator (fmap Const1 . doFreeRegisters) p; return ()
+
+uses :: MonadState (Set SomeΣVar, vs) m => ΣVar a -> m ()
+uses σ = modify' (first (insert (SomeΣVar σ)))
+
+defs :: MonadState (vs, Set SomeΣVar) m => ΣVar a -> m ()
+defs σ = modify' (second (insert (SomeΣVar σ)))
diff --git a/src/ghc/Parsley/Internal/Frontend/Analysis/Flags.hs b/src/ghc/Parsley/Internal/Frontend/Analysis/Flags.hs
new file mode 100644
--- /dev/null
+++ b/src/ghc/Parsley/Internal/Frontend/Analysis/Flags.hs
@@ -0,0 +1,34 @@
+{-|
+Module      : Parsley.Internal.Frontend.Analysis.Flags
+Description : Flags needed to control analysis.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Contains flags that can control how analysis should proceed.
+
+@since 1.5.0.0
+-}
+module Parsley.Internal.Frontend.Analysis.Flags (AnalysisFlags(letBound), emptyFlags) where
+
+{-|
+The packaged flags object.
+
+@since 1.5.0.0
+-}
+newtype AnalysisFlags = AnalysisFlags {
+  {-|
+  Is the binding used in this analysis let-bound?
+
+  @since 1.5.0.0
+  -}
+  letBound :: Bool
+}
+
+{-|
+An empty `AnalysisFlags` instance populated with sensible default values.
+
+@since 1.5.0.0
+-}
+emptyFlags :: AnalysisFlags
+emptyFlags = AnalysisFlags False
diff --git a/src/ghc/Parsley/Internal/Frontend/CombinatorAnalyser.hs b/src/ghc/Parsley/Internal/Frontend/CombinatorAnalyser.hs
deleted file mode 100644
--- a/src/ghc/Parsley/Internal/Frontend/CombinatorAnalyser.hs
+++ /dev/null
@@ -1,241 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-module Parsley.Internal.Frontend.CombinatorAnalyser (analyse, compliance, Compliance(..), emptyFlags, AnalysisFlags(..)) where
-
---import Control.Applicative                 (liftA2)
---import Control.Monad.Reader                (ReaderT, ask, runReaderT, local)
---import Control.Monad.State.Strict          (State, get, put, evalState)
-import Data.Coerce                         (coerce)
-import Data.Kind                           (Type)
---import Data.Map.Strict                     (Map)
---import Data.Set                            (Set)
-import Parsley.Internal.Common.Indexed     (Fix(..){-, imap, cata-}, zygo, (:*:)(..), ifst)
-import Parsley.Internal.Core.CombinatorAST (Combinator(..), MetaCombinator(..))
---import Parsley.Internal.Core.Identifiers   (IMVar, MVar(..))
-
---import qualified Data.Map.Strict as Map
---import qualified Data.Set        as Set
-
-newtype AnalysisFlags = AnalysisFlags {
-  letBound :: Bool
-}
-emptyFlags :: AnalysisFlags
-emptyFlags = AnalysisFlags False
-
-analyse :: AnalysisFlags -> Fix Combinator a -> Fix Combinator a
-analyse flags = cutAnalysis (letBound flags) {-. terminationAnalysis-}
-
-data Compliance (k :: Type) = DomComp | NonComp | Comp | FullPure deriving stock (Show, Eq)
-
-seqCompliance :: Compliance a -> Compliance b -> Compliance c
-seqCompliance c FullPure = coerce c
-seqCompliance FullPure c = coerce c
-seqCompliance Comp _     = Comp
-seqCompliance _ _        = NonComp
-
-caseCompliance :: Compliance a -> Compliance b -> Compliance c
-caseCompliance c FullPure              = coerce c
-caseCompliance FullPure c              = coerce c
-caseCompliance c1 c2 | c1 == coerce c2 = coerce c1
-caseCompliance _ _                     = NonComp
-
-{-# INLINE compliance #-}
-compliance :: Combinator Compliance a -> Compliance a
-compliance (Pure _)                 = FullPure
-compliance (Satisfy _)              = NonComp
-compliance Empty                    = FullPure
-compliance Let{}                    = DomComp
-compliance (Try _)                  = DomComp
-compliance (NonComp :<|>: FullPure) = Comp
-compliance (_ :<|>: _)              = NonComp
-compliance (l :<*>: r)              = seqCompliance l r
-compliance (l :<*: r)               = seqCompliance l r
-compliance (l :*>: r)               = seqCompliance l r
-compliance (LookAhead c)            = c -- Lookahead will consume input on failure, so its compliance matches that which is beneath it
-compliance (NotFollowedBy _)        = FullPure
-compliance (Debug _ c)              = c
-compliance (ChainPre NonComp p)     = seqCompliance Comp p
-compliance (ChainPre _ p)           = seqCompliance NonComp p
-compliance (ChainPost p NonComp)    = seqCompliance p Comp
-compliance (ChainPost p _)          = seqCompliance p NonComp
-compliance (Branch b p q)           = seqCompliance b (caseCompliance p q)
-compliance (Match p _ qs def)       = seqCompliance p (foldr1 caseCompliance (def:qs))
-compliance (MakeRegister _ l r)     = seqCompliance l r
-compliance (GetRegister _)          = FullPure
-compliance (PutRegister _ c)        = coerce c
-compliance (MetaCombinator _ c)     = c
-
-newtype CutAnalysis a = CutAnalysis {doCut :: Bool -> (Fix Combinator a, Bool)}
-
-biliftA2 :: (a -> b -> c) -> (x -> y -> z) -> (a, x) -> (b, y) -> (c, z)
-biliftA2 f g (x1, y1) (x2, y2) = (f x1 x2, g y1 y2)
-
-cutAnalysis :: Bool -> Fix Combinator a -> Fix Combinator a
-cutAnalysis letBound = fst . ($ letBound) . doCut . zygo (CutAnalysis . alg) compliance
-  where
-    mkCut True = In . MetaCombinator Cut
-    mkCut False = id
-
-    requiresCut = In . MetaCombinator RequiresCut
-
-    seqAlg :: (Fix Combinator a -> Fix Combinator b -> Combinator (Fix Combinator) c) -> Bool -> CutAnalysis a -> CutAnalysis b -> (Fix Combinator c, Bool)
-    seqAlg con cut l r =
-      let (l', handled) = doCut l cut
-          (r', handled') = doCut r (cut && not handled)
-      in (In (con l' r'), handled || handled')
-
-    rewrap :: (Fix Combinator a -> Combinator (Fix Combinator) b) -> Bool -> CutAnalysis a -> (Fix Combinator b, Bool)
-    rewrap con cut p = let (p', handled) = doCut p cut in (In (con p'), handled)
-
-    alg :: Combinator (CutAnalysis :*: Compliance) a -> Bool -> (Fix Combinator a, Bool)
-    alg (Pure x) _ = (In (Pure x), False)
-    alg (Satisfy f) cut = (mkCut cut (In (Satisfy f)), True)
-    alg Empty _ = (In Empty, False)
-    alg (Let r μ p) cut = (mkCut (not cut) (In (Let r μ (fst (doCut (ifst p) True)))), False) -- If there is no cut, we generate a piggy for the continuation
-    alg (Try p) _ = False <$ rewrap Try False (ifst p)
-    alg ((p :*: NonComp) :<|>: (q :*: FullPure)) _ = (requiresCut (In (fst (doCut p True) :<|>: fst (doCut q False))), True)
-    alg (p :<|>: q) cut =
-      let (q', handled) = doCut (ifst q) cut
-      in (In (fst (doCut (ifst p) False) :<|>: q'), handled)
-    alg (l :<*>: r) cut = seqAlg (:<*>:) cut (ifst l) (ifst r)
-    alg (l :<*: r) cut = seqAlg (:<*:) cut (ifst l) (ifst r)
-    alg (l :*>: r) cut = seqAlg (:*>:) cut (ifst l) (ifst r)
-    alg (LookAhead p) cut = rewrap LookAhead cut (ifst p)
-    alg (NotFollowedBy p) _ = False <$ rewrap NotFollowedBy False (ifst p)
-    alg (Debug msg p) cut = rewrap (Debug msg) cut (ifst p)
-    alg (ChainPre (op :*: NonComp) p) _ =
-      let (op', _) = doCut op True
-          (p', _) = doCut (ifst p) False
-      in (requiresCut (In (ChainPre op' p')), True)
-    alg (ChainPre op p) cut =
-      let (op', _) = doCut (ifst op) False
-          (p', handled) = doCut (ifst p) cut
-      in (mkCut (not cut) (In (ChainPre op' p')), handled)
-    alg (ChainPost p (op :*: NonComp)) cut =
-      let (p', _) = doCut (ifst p) cut
-          (op', _) = doCut op True
-      in (requiresCut (In (ChainPost p' op')), True)
-    alg (ChainPost p op) cut =
-      let (p', handled) = doCut (ifst p) cut
-          (op', _) = doCut (ifst op) False
-      in (mkCut (cut && handled) (In (ChainPost p' op')), handled)
-    alg (Branch b p q) cut =
-      let (b', handled) = doCut (ifst b) cut
-          (p', handled') = doCut (ifst p) (cut && not handled)
-          (q', handled'') = doCut (ifst q) (cut && not handled)
-      in (In (Branch b' p' q'), handled || (handled' && handled''))
-    alg (Match p f qs def) cut =
-      let (p', handled) = doCut (ifst p) cut
-          (def', handled') = doCut (ifst def) (cut && not handled)
-          (qs', handled'') = foldr (\q -> biliftA2 (:) (&&) (doCut (ifst q) (cut && not handled))) ([], handled') qs
-      in (In (Match p' f qs' def'), handled || handled'')
-    alg (MakeRegister σ l r) cut = seqAlg (MakeRegister σ) cut (ifst l) (ifst r)
-    alg (GetRegister σ) _ = (In (GetRegister σ), False)
-    alg (PutRegister σ p) cut = rewrap (PutRegister σ) cut (ifst p)
-    alg (MetaCombinator m p) cut = rewrap (MetaCombinator m) cut (ifst p)
-
--- Termination Analysis (Generalised left-recursion checker)
-{-data Consumption = Some | None | Never
-data Prop = Prop {success :: Consumption, fails :: Consumption, indisputable :: Bool} | Unknown
-
-looping (Prop Never Never _)          = True
-looping _                             = False
-strongLooping (Prop Never Never True) = True
-strongLooping _                       = False
-neverSucceeds (Prop Never _ _)        = True
-neverSucceeds _                       = False
-neverFails (Prop _ Never _)           = True
-neverFails _                          = False
-
-Never ||| _     = Never
-_     ||| Never = Never
-Some  ||| _     = Some
-None  ||| p     = p
-
-Some  &&& _    = Some
-_     &&& Some = Some
-None  &&& _    = None
-Never &&& p    = p
-
-Never ^^^ _     = Never
-_     ^^^ Never = Never
-None  ^^^ _     = None
-Some  ^^^ p     = p
-
-(==>) :: Prop -> Prop -> Prop
-p ==> _ | neverSucceeds p            = p
-_ ==> Prop Never Never True          = Prop Never Never True
-Prop None _ _ ==> Prop Never Never _ = Prop Never Never False
-Prop s1 f1 b1 ==> Prop s2 f2 b2      = Prop (s1 ||| s2) (f1 &&& (s1 ||| f2)) (b1 && b2)
-
-branching :: Prop -> [Prop] -> Prop
-branching b ps
-  | neverSucceeds b = b
-  | any strongLooping ps = Prop Never Never True
-branching (Prop None f _) ps
-  | any looping ps = Prop Never Never False
-  | otherwise      = Prop (foldr1 (|||) (map success ps)) (f &&& (foldr1 (^^^) (map fails ps))) False
-branching (Prop Some f _) ps = Prop (foldr (|||) Some (map success ps)) f False
-
---data InferredTerm = Loops | Safe | Undecidable
-newtype Termination a = Termination {runTerm :: ReaderT (Set IMVar) (State (Map IMVar Prop)) Prop}
-terminationAnalysis :: Fix Combinator a -> Fix Combinator a
-terminationAnalysis p = if not (looping (evalState (runReaderT (runTerm (cata (Termination . alg) p)) Set.empty) Map.empty)) then p
-                        else error "Parser will loop indefinitely: either it is left-recursive or iterates over pure computations"
-  where
-    alg :: Combinator Termination a -> ReaderT (Set IMVar) (State (Map IMVar Prop)) Prop
-    alg (Satisfy _)                          = return $! Prop Some None True
-    alg (Pure _)                             = return $! Prop None Never True
-    alg Empty                                = return $! Prop Never None True
-    alg (Try p)                              =
-      do x <- runTerm p
-         return $! if looping x then x
-                   else Prop (success x) None (indisputable x)
-    alg (LookAhead p)                        =
-      do x <- runTerm p
-         return $! if looping x then x
-                   else Prop None (fails x) (indisputable x)
-    alg (NotFollowedBy p)                    =
-      do x <- runTerm p
-         return $! if looping x then x
-                   else Prop None None True
-    alg (p :<*>: q)                          = liftA2 (==>) (runTerm p) (runTerm q)
-    alg (p :*>: q)                           = liftA2 (==>) (runTerm p) (runTerm q)
-    alg (p :<*: q)                           = liftA2 (==>) (runTerm p) (runTerm q)
-    alg (p :<|>: q)                          =
-      do x <- runTerm p; case x of
-           -- If we fail without consuming input then q governs behaviour
-           Prop _ None _       -> runTerm q
-           -- If p never fails then q is irrelevant
-           x | neverFails x    -> return $! x
-           -- If p never succeeds then q governs
-           x | neverSucceeds x -> runTerm q
-           Prop s1 Some i1     -> do ~(Prop s2 f i2) <- runTerm q; return $! Prop (s1 &&& s2) (Some ||| f) (i1 && i2)
-    alg (Branch b p q)                       = liftA2 branching (runTerm b) (sequence [runTerm p, runTerm q])
-    alg (Match p _ qs def)                   = liftA2 branching (runTerm p) (traverse runTerm (def:qs))
-    alg (ChainPre op p)                      =
-      do x <- runTerm op; case x of
-           -- Never failing implies you must either loop or not consume input
-           Prop _ Never _ -> return $! Prop Never Never True
-           -- Reaching p can take a route that consumes no input, if op failed
-           _ -> do y <- runTerm p
-                   return $! if looping y then y
-                             else y -- TODO Verify!
-    alg (ChainPost p op)                     =
-      do y <- runTerm op; case y of
-           Prop None _ _ -> return $! Prop Never Never True
-           y -> do x <- runTerm p; case (x, y) of
-                     (Prop Some f _, Prop _ Never _) -> return $! Prop Some f False
-                     (x, y)                          -> return $! Prop (success x) (fails x &&& fails y) False -- TODO Verify
-    alg (Let True (MVar v) p)                =
-      do props <- get
-         seen <- ask
-         case Map.lookup v props of
-           Just prop -> return $! prop
-           Nothing | Set.member v seen -> return $! Prop Never Never False
-           Nothing -> do prop <- local (Set.insert v) (runTerm p)
-                         let prop' = if looping prop then Prop Never Never True else prop
-                         put (Map.insert v prop' props)
-                         return $! prop'
-    alg (Debug _ p)                          = runTerm p
-    --alg _                                    = return $! Unknown
--}
diff --git a/src/ghc/Parsley/Internal/Frontend/Compiler.hs b/src/ghc/Parsley/Internal/Frontend/Compiler.hs
--- a/src/ghc/Parsley/Internal/Frontend/Compiler.hs
+++ b/src/ghc/Parsley/Internal/Frontend/Compiler.hs
@@ -19,31 +19,30 @@
 module Parsley.Internal.Frontend.Compiler (compile) where
 
 import Prelude hiding (pred)
-import Data.Dependent.Map                           (DMap)
-import Data.Hashable                                (Hashable, hashWithSalt, hash)
-import Data.HashMap.Strict                          (HashMap)
-import Data.HashSet                                 (HashSet)
-import Data.IORef                                   (IORef, newIORef, readIORef, writeIORef)
-import Data.Kind                                    (Type)
-import Data.Maybe                                   (isJust)
-import Data.Set                                     (Set)
-import Control.Arrow                                (first, second)
-import Control.Monad                                (void, when)
-import Control.Monad.Reader                         (ReaderT, runReaderT, local, ask, MonadReader)
-import GHC.Exts                                     (Int(..), unsafeCoerce#)
-import GHC.Prim                                     (StableName#)
-import GHC.StableName                               (StableName(..), makeStableName, hashStableName, eqStableName)
-import Numeric                                      (showHex)
-import Parsley.Internal.Core.CombinatorAST          (Combinator(..), ScopeRegister(..), Reg(..), Parser(..), traverseCombinator)
-import Parsley.Internal.Core.Identifiers            (IMVar, MVar(..), IΣVar, ΣVar(..), SomeΣVar)
-import Parsley.Internal.Common.Fresh                (HFreshT, newVar, runFreshT)
-import Parsley.Internal.Common.Indexed              (Fix(In), cata, cata', IFunctor(imap), (:+:)(..), (\/), Const1(..))
-import Parsley.Internal.Common.State                (State, get, gets, runState, execState, modify', MonadState)
-import Parsley.Internal.Frontend.Optimiser          (optimise)
-import Parsley.Internal.Frontend.CombinatorAnalyser (analyse, emptyFlags, AnalysisFlags(..))
-import Parsley.Internal.Frontend.Dependencies       (dependencyAnalysis)
-import Parsley.Internal.Trace                       (Trace(trace))
-import System.IO.Unsafe                             (unsafePerformIO)
+import Data.Dependent.Map                  (DMap)
+import Data.Hashable                       (Hashable, hashWithSalt, hash)
+import Data.HashMap.Strict                 (HashMap)
+import Data.HashSet                        (HashSet)
+import Data.IORef                          (IORef, newIORef, readIORef, writeIORef)
+import Data.Kind                           (Type)
+import Data.Maybe                          (isJust)
+import Data.Set                            (Set)
+import Control.Arrow                       (first, second)
+import Control.Monad                       (void, when)
+import Control.Monad.Reader                (ReaderT, runReaderT, local, ask, MonadReader)
+import GHC.Exts                            (Int(..), unsafeCoerce#)
+import GHC.Prim                            (StableName#)
+import GHC.StableName                      (StableName(..), makeStableName, hashStableName, eqStableName)
+import Numeric                             (showHex)
+import Parsley.Internal.Core.CombinatorAST (Combinator(..), ScopeRegister(..), Reg(..), Parser(..), traverseCombinator)
+import Parsley.Internal.Core.Identifiers   (IMVar, MVar(..), IΣVar, ΣVar(..), SomeΣVar)
+import Parsley.Internal.Common.Fresh       (HFreshT, newVar, runFreshT)
+import Parsley.Internal.Common.Indexed     (Fix(In), cata, cata', IFunctor(imap), (:+:)(..), (\/), Const1(..))
+import Parsley.Internal.Common.State       (State, get, gets, runState, execState, modify', MonadState)
+import Parsley.Internal.Frontend.Optimiser (optimise)
+import Parsley.Internal.Frontend.Analysis  (analyse, emptyFlags, letBound, dependencyAnalysis)
+import Parsley.Internal.Trace              (Trace(trace))
+import System.IO.Unsafe                    (unsafePerformIO)
 
 import qualified Data.Dependent.Map  as DMap    ((!), empty, insert, mapWithKey, size)
 import qualified Data.HashMap.Strict as HashMap (lookup, insert, empty, insertWith, foldrWithKey, (!))
diff --git a/src/ghc/Parsley/Internal/Frontend/Dependencies.hs b/src/ghc/Parsley/Internal/Frontend/Dependencies.hs
deleted file mode 100644
--- a/src/ghc/Parsley/Internal/Frontend/Dependencies.hs
+++ /dev/null
@@ -1,163 +0,0 @@
-{-# LANGUAGE RecordWildCards #-}
-module Parsley.Internal.Frontend.Dependencies (dependencyAnalysis) where
-
-import Control.Arrow                        (first, second)
-import Control.Monad                        (unless, forM_)
-import Data.Array                           (Array, (!), listArray)
-import Data.Array.MArray                    (readArray, writeArray, newArray)
-import Data.Array.ST                        (runSTUArray)
-import Data.Array.Unboxed                   (assocs)
-import Data.Dependent.Map                   (DMap)
-import Data.List                            (foldl', partition, sortOn)
-import Data.Map.Strict                      (Map)
-import Data.Set                             (Set, insert, (\\), union, notMember, empty)
-import Data.STRef                           (newSTRef, readSTRef, writeSTRef)
-import Parsley.Internal.Common.Indexed      (Fix, cata, Const1(..), (:*:)(..), zipper)
-import Parsley.Internal.Common.State        (State, MonadState, execState, modify')
-import Parsley.Internal.Core.CombinatorAST  (Combinator(..), traverseCombinator)
-import Parsley.Internal.Core.Identifiers    (IMVar, MVar(..), IΣVar, ΣVar, SomeΣVar(..), getIΣVar)
-
-import qualified Data.Dependent.Map as DMap (foldrWithKey, filterWithKey)
-import qualified Data.Map.Strict    as Map  ((!), empty, insert, mapMaybeWithKey, findMax, elems, lookup, foldMapWithKey)
-import qualified Data.Set           as Set  (elems, empty, insert, lookupMax)
-
-type Graph = Array IMVar [IMVar]
-
--- TODO This actually should be in the backend... dead bindings and the topological ordering can be computed here
---      but the register stuff should come after register optimisation and instruction peephole
-
-dependencyAnalysis :: Fix Combinator a -> DMap MVar (Fix Combinator) -> (DMap MVar (Fix Combinator), Map IMVar (Set SomeΣVar), IΣVar)
-dependencyAnalysis toplevel μs =
-  let -- Step 1: find roots of the toplevel
-      roots = directDependencies toplevel
-      -- Step 2: build immediate dependencies
-      DependencyMaps{..} = buildDependencyMaps μs
-      -- Step 3: find the largest name
-      n = fst (Map.findMax immediateDependencies)
-      -- Step 4: Build a dependency graph
-      graph = buildGraph n immediateDependencies
-      -- Step 5: construct the seen set (dfnum)
-      -- Step 6: dfs from toplevel (via roots) all with same seen set
-      -- Step 7: elems of seen set with dfnum 0 are dead, otherwise they are collected into a list in descending order
-      (topo, dead) = topoOrdering roots n graph
-      -- Step 8: perform a dfs on each of the topo, with a new seen set for each,
-      --         building the flattened dependency map. If the current focus has
-      --         already been computed, add all its deps to the seen set and skip.
-      --         The end seen set becomes out flattened deps.
-      trueDeps = flattenDependencies topo (minMax topo) graph
-      -- Step 8: Compute the new registers, and remove dead ones
-      addNewRegs v uses
-        | notMember v dead = let deps = trueDeps Map.! v
-                                 defs = definedRegisters Map.! v
-                                 subUses = foldMap (usedRegisters Map.!) deps
-                                 subDefs = foldMap (definedRegisters Map.!) deps
-                             in Just $ (uses \\ defs) `union` (subUses \\ subDefs)
-        | otherwise        = Nothing
-      trueRegs = Map.mapMaybeWithKey addNewRegs usedRegisters
-      largestRegister = maybe (-1) getIΣVar (Set.lookupMax (Map.foldMapWithKey (const id) definedRegisters))
-  in (DMap.filterWithKey (\(MVar v) _ -> notMember v dead) μs, trueRegs, largestRegister)
-
-minMax :: Ord a => [a] -> (a, a)
-minMax []     = error "cannot find minimum or maximum of empty list"
-minMax (x:xs) = foldl' (\(small, big) x -> (min small x, max big x)) (x, x) xs
-
-buildGraph :: IMVar -> Map IMVar (Set IMVar) -> Graph
-buildGraph n = listArray (0, n) . map Set.elems . Map.elems
-
-topoOrdering :: Set IMVar -> IMVar -> Graph -> ([IMVar], Set IMVar)
-topoOrdering roots n graph =
-  let dfnums = runSTUArray $ do
-        dfnums <- newArray (0, n) (0 :: Int)
-        nextDfnum <- newSTRef 1
-        let hasSeen v = (/= 0) <$> readArray dfnums v
-        let setSeen v = do dfnum <- readSTRef nextDfnum
-                           writeArray dfnums v dfnum
-                           writeSTRef nextDfnum (dfnum + 1)
-        forM_ roots (dfs hasSeen setSeen graph)
-        return dfnums
-      (lives, deads) = partition ((/= 0) . snd) (assocs dfnums)
-  in (reverseMap fst (sortOn snd lives), foldl' (\ds v0 -> Set.insert (fst v0) ds) Set.empty deads)
-
-reverseMap :: (a -> b) -> [a] -> [b]
-reverseMap f = foldl' (\xs x -> f x : xs) []
-
-flattenDependencies :: [IMVar] -> (IMVar, IMVar) -> Graph -> Map IMVar (Set IMVar)
-flattenDependencies topo range graph = foldl' reachable Map.empty topo
-  where
-    reachable :: Map IMVar (Set IMVar) -> IMVar -> Map IMVar (Set IMVar)
-    reachable deps root =
-      let seen = runSTUArray $ do
-            seen <- newArray range False
-            let setSeen v = writeArray seen v True
-            let seenOrSkip v = case Map.lookup v deps of
-                  Nothing -> readArray seen v
-                  Just ds -> setSeen v >> forM_ ds setSeen >> return True
-            dfs seenOrSkip setSeen graph root
-            return seen
-          ds = foldl' (\ds (v, b) -> if b then Set.insert v ds else ds) Set.empty (assocs seen)
-      in Map.insert root ds deps
-
-dfs :: Monad m => (IMVar -> m Bool) -> (IMVar -> m ()) -> Graph -> IMVar -> m ()
-dfs hasSeen setSeen graph = go
-  where
-    go v = do seen <- hasSeen v
-              unless seen $
-                do setSeen v
-                   forM_ (graph ! v) go
-
--- IMMEDIATE DEPENDENCY MAPS
-data DependencyMaps = DependencyMaps {
-  usedRegisters         :: Map IMVar (Set SomeΣVar), -- Leave Lazy
-  immediateDependencies :: Map IMVar (Set IMVar), -- Could be Strict
-  definedRegisters      :: Map IMVar (Set SomeΣVar)
-}
-
-buildDependencyMaps :: DMap MVar (Fix Combinator) -> DependencyMaps
-buildDependencyMaps = DMap.foldrWithKey (\(MVar v) p deps@DependencyMaps{..} ->
-  let (frs, defs, ds) = freeRegistersAndDependencies v p
-  in deps { usedRegisters = Map.insert v frs usedRegisters
-          , immediateDependencies = Map.insert v ds immediateDependencies
-          , definedRegisters = Map.insert v defs definedRegisters}) (DependencyMaps Map.empty Map.empty Map.empty)
-
-freeRegistersAndDependencies :: IMVar -> Fix Combinator a -> (Set SomeΣVar,  Set SomeΣVar, Set IMVar)
-freeRegistersAndDependencies v p =
-  let frsm :*: depsm = zipper freeRegistersAlg (dependenciesAlg (Just v)) p
-      (frs, defs) = runFreeRegisters frsm
-      ds = runDependencies depsm
-  in (frs, defs, ds)
-
--- DEPENDENCY ANALYSIS
-newtype Dependencies a = Dependencies { doDependencies :: State (Set IMVar) () }
-runDependencies :: Dependencies a -> Set IMVar
-runDependencies = flip execState empty. doDependencies
-
-directDependencies :: Fix Combinator a -> Set IMVar
-directDependencies = runDependencies . cata (dependenciesAlg Nothing)
-
-{-# INLINE dependenciesAlg #-}
-dependenciesAlg :: Maybe IMVar -> Combinator Dependencies a -> Dependencies a
-dependenciesAlg (Just v) (Let _ μ@(MVar u) _) = Dependencies $ do unless (u == v) (dependsOn μ)
-dependenciesAlg Nothing  (Let _ μ _)          = Dependencies $ do dependsOn μ
-dependenciesAlg _ p                           = Dependencies $ do traverseCombinator (fmap Const1 . doDependencies) p; return ()
-
-dependsOn :: MonadState (Set IMVar) m => MVar a -> m ()
-dependsOn (MVar v) = modify' (insert v)
-
--- FREE REGISTER ANALYSIS
-newtype FreeRegisters a = FreeRegisters { doFreeRegisters :: State (Set SomeΣVar, Set SomeΣVar) () }
-runFreeRegisters :: FreeRegisters a -> (Set SomeΣVar, Set SomeΣVar)
-runFreeRegisters = flip execState (empty, empty) . doFreeRegisters
-
-{-# INLINE freeRegistersAlg #-}
-freeRegistersAlg :: Combinator FreeRegisters a -> FreeRegisters a
-freeRegistersAlg (GetRegister σ)      = FreeRegisters $ do uses σ
-freeRegistersAlg (PutRegister σ p)    = FreeRegisters $ do uses σ; doFreeRegisters p
-freeRegistersAlg (MakeRegister σ p q) = FreeRegisters $ do defs σ; doFreeRegisters p; doFreeRegisters q
-freeRegistersAlg Let{}                = FreeRegisters $ do return () -- TODO This can be removed when Let doesn't have the body in it...
-freeRegistersAlg p                    = FreeRegisters $ do traverseCombinator (fmap Const1 . doFreeRegisters) p; return ()
-
-uses :: MonadState (Set SomeΣVar, vs) m => ΣVar a -> m ()
-uses σ = modify' (first (insert (SomeΣVar σ)))
-
-defs :: MonadState (vs, Set SomeΣVar) m => ΣVar a -> m ()
-defs σ = modify' (second (insert (SomeΣVar σ)))
diff --git a/src/ghc/Parsley/Internal/Frontend/Optimiser.hs b/src/ghc/Parsley/Internal/Frontend/Optimiser.hs
--- a/src/ghc/Parsley/Internal/Frontend/Optimiser.hs
+++ b/src/ghc/Parsley/Internal/Frontend/Optimiser.hs
@@ -1,6 +1,17 @@
 {-# LANGUAGE LambdaCase,
              PatternSynonyms,
              ViewPatterns #-}
+{-|
+Module      : Parsley.Internal.Frontend.Optimiser
+Description : Combinator law optimisation.
+License     : BSD-3-Clause
+Maintainer  : Jamie Willis
+Stability   : experimental
+
+Exposes the `optimise` algebra, which is used for optimisations based on the laws of parsers.
+
+@since 1.0.0.0
+-}
 module Parsley.Internal.Frontend.Optimiser (optimise) where
 
 import Prelude hiding                      ((<$>))
@@ -15,6 +26,12 @@
 pattern (:<$:) :: Defunc a -> Fix Combinator b -> Combinator (Fix Combinator) a
 pattern x :<$: p = In (Pure x) :<*: p
 
+{-|
+Optimises a `Combinator` tree according to the various laws of parsers. See the source
+for which laws are being utilised.
+
+@since 1.0.0.0
+-}
 optimise :: Combinator (Fix Combinator) a -> Fix Combinator a
 -- DESTRUCTIVE OPTIMISATION
 -- Right Absorption Law: empty <*> u                    = empty
@@ -149,14 +166,6 @@
 optimise (f :<$>: In (Branch b p q))                     = optimise (Branch b (optimise (APP_H COMPOSE f :<$>: p)) (optimise (APP_H COMPOSE f :<$>: q)))
 -- pure Match law: match vs (pure x) f def               = if elem x vs then f x else def
 optimise (Match (In (Pure x)) fs qs def)                 = foldr (\(f, q) k -> if _val f (_val x) then q else k) def (zip fs qs)
--- TODO I'm not actually sure this one is a good optimisation? might have some size constraint on it
--- Generalised Identity Match law: match vs p (pure . f) def = f <$> (p >?> flip elem vs) <|> def
-{-optimise (Match p fs qs def)
-  | all (\case {In (Pure _) -> True; _ -> False}) qs     = optimise (optimise (makeQ apply qapply :<$>: (p >?> (makeQ validate qvalidate))) :<|>: def)
-    where apply x    = foldr (\(f, In (Pure y)) k -> if _val f x then _val y else k) (error "whoopsie") (zip fs qs)
-          qapply     = [||\x -> $$(foldr (\(f, In (Pure y)) k -> [||if $$(_code f) x then $$(_code y) else $$k||]) ([||error "whoopsie"||]) (zip fs qs))||]
-          validate x = foldr (\f b -> _val f x || b) False fs
-          qvalidate  = [||\x -> $$(foldr (\f k -> [||$$(_code f) x || $$k||]) [||False||] fs)||]-}
 -- Distributivity Law: f <$> match vs p g def            = match vs p ((f <$>) . g) (f <$> def)
 optimise (f :<$>: (In (Match p fs qs def)))              = In (Match p fs (map (optimise . (f :<$>:)) qs) (optimise (f :<$>: def)))
 -- Trivial let-bindings - NOTE: These will get moved when Let nodes no longer have the "source" in them
@@ -167,11 +176,3 @@
 optimise (Let False _ p@(In (GetRegister _)))                        = p
 optimise (Let False _ p@(In (In (Pure _) :<*>: In (GetRegister _)))) = p
 optimise p                                                           = In p
-
--- try (lookAhead p *> p *> lookAhead q) = lookAhead (p *> q) <* try p
-
-{-(>?>) :: Fix Combinator a -> Defunc (a -> Bool) -> Fix Combinator a
-p >?> f = In (Branch (In (makeQ g qg :<$>: p)) (In Empty) (In (Pure ID)))
-  where
-    g x = if _val f x then Right x else Left ()
-    qg = [||\x -> if $$(_code f) x then Right x else Left ()||]-}
diff --git a/test/CommonTest.hs b/test/CommonTest.hs
new file mode 100644
--- /dev/null
+++ b/test/CommonTest.hs
@@ -0,0 +1,13 @@
+module Main where
+
+import Test.Tasty
+import qualified CommonTest.Queue as QueueTest
+import qualified CommonTest.RewindQueue as RewindQueueTest
+
+main :: IO ()
+main = defaultMain tests
+
+tests :: TestTree
+tests = testGroup "Common Tests" [ QueueTest.tests
+                                 , RewindQueueTest.tests
+                                 ]
diff --git a/test/CommonTest/Queue.hs b/test/CommonTest/Queue.hs
new file mode 100644
--- /dev/null
+++ b/test/CommonTest/Queue.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE FlexibleInstances, AllowAmbiguousTypes, TypeApplications, RankNTypes, ScopedTypeVariables, ConstraintKinds #-}
+module CommonTest.Queue where
+import Test.Tasty (testGroup, TestTree)
+import Test.Tasty.HUnit ( testCase, (@?=) )
+import Test.Tasty.QuickCheck
+  ( listOf,
+    (===),
+    (==>),
+    (.&&.),
+    testProperty,
+    Arbitrary(arbitrary),
+    Property )
+
+import Prelude hiding (null)
+import Parsley.Internal.Common.QueueLike  (QueueLike(empty, null, size, enqueue, dequeue, enqueueAll))
+import Parsley.Internal.Common.Queue ()
+import Parsley.Internal.Common.Queue.Impl (Queue(..))
+import qualified Parsley.Internal.Common.Queue.Impl as Queue
+
+instance Arbitrary a => Arbitrary (Queue a) where
+  arbitrary = do ins <- listOf arbitrary
+                 outs <- listOf arbitrary
+                 return $ Queue { ins = ins, insz = length ins
+                                , outs = outs, outsz = length outs
+                                }
+
+class QueueLike q => QueueLikeImpl q where
+  toList :: q a -> [a]
+
+instance QueueLikeImpl Queue where
+  toList = Queue.toList
+
+type TestContext q = (Arbitrary (q Integer), QueueLikeImpl q, Show (q Integer))
+
+tests :: TestTree
+tests = testGroup "Queue" (genTests @Queue)
+
+genTests :: forall q. TestContext q => [TestTree]
+genTests = [ emptyTests @q
+           , enqueueTests @q
+           , testProperty "toList should roundtrip with enqueueAll" $ toListRound @q
+           , dequeueTests @q
+           ]
+
+emptyTests :: forall q. TestContext q => TestTree
+emptyTests = testGroup "empty should" [
+    testCase "be null" $ null @q empty @?= True,
+    testCase "have size 0" $ size @q empty @?= 0
+  ]
+
+enqueueTests :: forall q. TestContext q => TestTree
+enqueueTests = testGroup "enqueue should" [
+    testProperty "increase size by one" $ uncurry (enqueueSizeBy1 @q),
+    testProperty "render empty non-null" $ flip (enqueueNonNull @q) empty,
+    testProperty "render any other queue non-null" $ uncurry (enqueueNonNull @q),
+    testProperty "behave like snoc" $ uncurry (enqueueIsSnoc @q),
+    testProperty "serve as a model for enqueueAll" $ uncurry (enqueueAllModelsEnqueue @q)
+  ]
+
+enqueueSizeBy1 :: forall q. TestContext q => Integer -> q Integer -> Property
+enqueueSizeBy1 x q = size q + 1 === size (enqueue x q)
+
+enqueueNonNull :: forall q. TestContext q => Integer -> Queue Integer -> Bool
+enqueueNonNull x = not . Queue.null . Queue.enqueue x
+
+enqueueIsSnoc :: forall q. TestContext q => Integer -> Queue Integer -> Property
+enqueueIsSnoc x q = Queue.toList q ++ [x] === Queue.toList (Queue.enqueue x q)
+
+enqueueAllModelsEnqueue :: forall q. TestContext q => [Integer] -> Queue Integer -> Property
+enqueueAllModelsEnqueue xs q = Queue.enqueueAll xs q === foldl (flip Queue.enqueue) q xs
+
+dequeueTests :: forall q. TestContext q => TestTree
+dequeueTests = testGroup "dequeue should" [
+    testProperty "decrease size by one when non-empty" $ dequeueSizeBy1 @q,
+    testProperty "behave like tail" $ dequeueIsTail @q
+  ]
+
+dequeueSizeBy1 :: forall q. TestContext q => Queue Integer -> Property
+dequeueSizeBy1 q = not (Queue.null q) ==> Queue.size q === Queue.size (snd (Queue.dequeue q)) + 1
+
+dequeueIsTail :: forall q. TestContext q => Queue Integer -> Property
+dequeueIsTail q = not (Queue.null q) ==>
+  let (x, q') = Queue.dequeue q
+  in Queue.toList q === x : Queue.toList q'
+
+toListRound :: forall q. TestContext q => [Integer] -> Property
+toListRound xs = toList @q (enqueueAll xs empty) === xs
diff --git a/test/CommonTest/RewindQueue.hs b/test/CommonTest/RewindQueue.hs
new file mode 100644
--- /dev/null
+++ b/test/CommonTest/RewindQueue.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeApplications #-}
+module CommonTest.RewindQueue where
+
+import Test.Tasty (testGroup, TestTree)
+import Test.Tasty.QuickCheck
+  ( listOf,
+    (===),
+    (==>),
+    conjoin,
+    testProperty,
+    forAll,
+    elements,
+    resize,
+    Arbitrary(arbitrary),
+    Property )
+import CommonTest.Queue as QueueTest (genTests, QueueLikeImpl(..))
+
+import Prelude hiding (null)
+
+import Parsley.Internal.Common.QueueLike  (QueueLike(empty, null, size, enqueue, dequeue, enqueueAll))
+import Parsley.Internal.Common.RewindQueue ()
+import Parsley.Internal.Common.RewindQueue.Impl (RewindQueue(..))
+import qualified Parsley.Internal.Common.RewindQueue.Impl as Rewind
+
+tests :: TestTree
+tests = testGroup "RewindQueue" [
+    testGroup "should behave like Queue" (QueueTest.genTests @RewindQueue),
+    testProperty "rewind should reverse dequeue" rewindRoundtrip
+  ]
+
+rewindRoundtrip :: RewindQueue Integer -> Property
+rewindRoundtrip rq = conjoin (map prop [0..size rq])
+  where
+    prop i = let rq' = iterate (snd . dequeue) rq !! i
+             in toList (Rewind.rewind i rq') === toList rq
+
+instance Arbitrary a => Arbitrary (RewindQueue a) where
+  arbitrary = do undo <- listOf arbitrary
+                 queue <- arbitrary
+                 return $ RewindQueue queue undo (length undo)
+
+instance QueueTest.QueueLikeImpl RewindQueue where
+  toList = Rewind.toList