build: ghcid: run even with warnings
[haskell/symantic-parser.git] / src / Symantic / Parser / Machine / Instructions.hs
index 0d0221559574b7d649dd5f0d74dc79355f383f08..80a9f47e68451b830e0bcca5e4e64a824157d49c 100644 (file)
-{-# LANGUAGE ConstraintKinds #-} -- For Executable
+{-# LANGUAGE ConstraintKinds #-} -- For Machine
+{-# LANGUAGE DeriveLift #-} -- For TH.Lift (Failure tok)
 {-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
-{-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
+-- | Semantic of the parsing instructions used
+-- to make the parsing control-flow explicit,
+-- in the convenient tagless-final encoding.
 module Symantic.Parser.Machine.Instructions where
 
 import Data.Bool (Bool(..))
 import Data.Either (Either)
 import Data.Eq (Eq(..))
-import Data.Ord (Ord)
-import Data.Function (($), (.))
+import Data.Function ((.))
 import Data.Kind (Type)
-import System.IO.Unsafe (unsafePerformIO)
+import Data.Set (Set)
 import Text.Show (Show(..))
-import qualified Data.Functor as Functor
+import Data.String (String)
 import qualified Language.Haskell.TH as TH
-import qualified Language.Haskell.TH.Syntax as TH
-import qualified Symantic.Parser.Haskell as H
 
 import Symantic.Parser.Grammar
 import Symantic.Parser.Machine.Input
-import Symantic.Univariant.Trans
+import qualified Symantic.Syntaxes.Classes as Prod
+import qualified Symantic.Semantics.Data as Sym
 
--- * Type 'TermInstr'
-type TermInstr = H.Term TH.CodeQ
+-- * Type 'Splice'
+type Splice = Sym.SomeData TH.CodeQ
 
--- * Type 'Instr'
--- | 'Instr'uctions for the 'Machine'.
-data Instr input valueStack (failStack::Peano) returnValue where
-  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
+-- | Lift a 'TH.CodeQ' into a 'Sym.SomeData'.
+splice :: TH.CodeQ a -> Splice a
+splice x = Sym.SomeData (Sym.Var x)
+
+-- ** Type 'ReprInstr'
+type ReprInstr = {-input-}Type -> {-valueStack-}[Type] -> {-a-}Type -> Type
+
+-- ** Type 'LetName'
+-- | 'TH.Name' of a 'defLet' or 'defJoin'
+-- indexed by the return type of the factorized 'Instr'uctions.
+-- This helps type-inferencing.
+newtype LetName a = LetName { unLetName :: TH.Name }
+  deriving Eq
+  deriving newtype Show
+
+-- ** Class 'InstrComment'
+class InstrComment (repr::ReprInstr) where
+  comment :: String -> repr inp vs a -> repr inp vs a
+
+-- ** Class 'InstrValuable'
+class InstrValuable (repr::ReprInstr) where
+  -- | @('pushValue' x k)@ pushes @(x)@ on the 'valueStack'
   -- and continues with the next 'Instr'uction @(k)@.
-  Push ::
-    TermInstr v ->
-    Instr inp (v ': vs) es ret ->
-    Instr inp vs es ret
-  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
-  Pop ::
-    Instr inp vs es ret ->
-    Instr inp (v ': vs) es ret
-  -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
+  pushValue ::
+    Splice v ->
+    repr inp (v ': vs) a ->
+    repr inp vs a
+  -- | @('popValue' k)@ pushes @(x)@ on the 'valueStack'.
+  popValue ::
+    repr inp vs a ->
+    repr inp (v ': vs) a
+  -- | @('lift2Value' f k)@ pops two values from the 'valueStack',
   -- and pushes the result of @(f)@ applied to them.
-  LiftI2 ::
-    TermInstr (x -> y -> z) ->
-    Instr inp (z : vs) es ret ->
-    Instr inp (y : x : vs) es ret
-  -- | @('Fail')@ raises an error from the 'failStack'.
-  Fail ::
-    [ErrorItem (InputToken inp)] ->
-    Instr inp vs ('Succ es) ret
-  -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
-  -- and continues with the next 'Instr'uction @(k)@.
-  PopFail ::
-    Instr inp vs es ret ->
-    Instr inp vs ('Succ es) ret
-  -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
-  -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
-  -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
-  -- and the control flow goes on with the @(r)@ 'Instr'uction.
-  CatchFail ::
-    Instr inp vs ('Succ es) ret ->
-    Instr inp (Cursor inp ': vs) es ret ->
-    Instr inp vs es ret
-  -- | @('LoadInput' k)@ removes the input from the 'valueStack'
-  -- and continues with the next 'Instr'uction @(k)@ using that input.
-  LoadInput ::
-    Instr inp vs es r ->
-    Instr inp (Cursor inp : vs) es r
-  -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
-  -- and continues with the next 'Instr'uction @(k)@.
-  PushInput ::
-    Instr inp (Cursor inp ': vs) es ret ->
-    Instr inp vs es ret
-  -- | @('Case' l r)@.
-  Case ::
-    Instr inp (x ': vs) es r ->
-    Instr inp (y ': vs) es r ->
-    Instr inp (Either x y ': vs) es r
-  -- | @('Swap' k)@ pops two values on the 'valueStack',
+  lift2Value ::
+    Splice (x -> y -> z) ->
+    repr inp (z ': vs) a ->
+    repr inp (y ': x ': vs) a
+  -- | @('swapValue' k)@ pops two values on the 'valueStack',
   -- pushes the first popped-out, then the second,
   -- and continues with the next 'Instr'uction @(k)@.
-  Swap ::
-    Instr inp (x ': y ': vs) es r ->
-    Instr inp (y ': x ': vs) es r
-  -- | @('Choices' ps bs d)@.
-  Choices ::
-    [TermInstr (v -> Bool)] ->
-    [Instr inp vs es ret] ->
-    Instr inp vs es ret ->
-    Instr inp (v ': vs) es ret
-  -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
+  swapValue ::
+    repr inp (x ': y ': vs) a ->
+    repr inp (y ': x ': vs) a
+  -- | @('mapValue' f k)@.
+  mapValue ::
+    Splice (x -> y) ->
+    repr inp (y ': vs) a ->
+    repr inp (x ': vs) a
+  mapValue f = pushValue f . lift2Value (Prod.flip Prod..@ (Prod.$))
+  -- | @('applyValue' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
+  -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
+  applyValue ::
+    repr inp (y ': vs) a ->
+    repr inp (x ': (x -> y) ': vs) a
+  applyValue = lift2Value (Prod.$)
+
+-- ** Class 'InstrExceptionable'
+class InstrExceptionable (repr::ReprInstr) where
+  -- | @('raise' exn)@ raises 'ExceptionLabel' @(exn)@.
+  raise :: ExceptionLabel -> repr inp vs a
+  -- | @('fail' fs)@ raises 'ExceptionFailure' @(exn)@.
+  -- As a special case, giving an empty 'Set' of failures
+  -- raises 'ExceptionFailure' without using the current position
+  -- to update the farthest error.
+  fail :: Set SomeFailure -> repr inp vs a
+  -- | @('commit' exn k)@ removes the 'OnException'
+  -- from the 'onExceptionStackByLabel' for the given 'Exception' @(exn)@,
+  -- and continues with the next 'Instr'uction @(k)@.
+  commit :: Exception -> repr inp vs a -> repr inp vs a
+  -- | @('catch' exn l r)@ tries the @(l)@ 'Instr'uction
+  -- in a new failure scope such that if @(l)@ raises an exception within @(exn)@, it is caught,
+  -- then the input (and its 'Horizon') is pushed
+  -- as it was before trying @(l)@ on the 'valueStack' (resp. on the 'horizonStack'),
+  -- and the control flow goes on with the @(r)@ 'Instr'uction.
+  catch ::
+    Exception ->
+    {-scope-}repr inp vs ret ->
+    {-onException-}repr inp (InputPosition inp ': vs) ret ->
+    repr inp vs ret
+
+-- ** Class 'InstrBranchable'
+class InstrBranchable (repr::ReprInstr) where
+  -- | @('caseBranch' l r)@.
+  caseBranch ::
+    repr inp (x ': vs) r ->
+    repr inp (y ': vs) r ->
+    repr inp (Either x y ': vs) r
+  -- | @('choicesBranch' ps bs d)@.
+  choicesBranch ::
+    [(Splice (v -> Bool), repr inp vs a)] ->
+    repr inp vs a ->
+    repr inp (v ': vs) a
+  -- | @('ifBranch' ok ko)@ pops a 'Bool' from the 'valueStack'
+  -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
+  -- or @(ko)@ otherwise.
+  ifBranch ::
+    repr inp vs a ->
+    repr inp vs a ->
+    repr inp (Bool ': vs) a
+  ifBranch ok = choicesBranch [(Prod.id, ok)]
+
+-- ** Class 'InstrCallable'
+class InstrCallable (repr::ReprInstr) where
+  -- | @('defLet' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
   -- 'Call's @(n)@ and
   -- continues with the next 'Instr'uction @(k)@.
-  Subroutine ::
-    LetName v -> Instr inp '[] ('Succ 'Zero) v ->
-    Instr inp vs ('Succ es) ret ->
-    Instr inp vs ('Succ es) ret
-  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
-  Jump ::
-    LetName ret ->
-    Instr inp '[] ('Succ es) ret
-  -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
+  defLet ::
+    LetBindings TH.Name (repr inp '[]) ->
+    repr inp vs a ->
+    repr inp vs a
+  -- | @('call' isRec n k)@ pass the control-flow to the 'DefLet' named @(n)@,
   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
-  Call ::
-    LetName v ->
-    Instr inp (v ': vs) ('Succ es) ret ->
-    Instr inp vs ('Succ es) ret
-  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
-  Ret ::
-    Instr inp '[ret] es ret
-  -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
-  -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
-  -- otherwise 'Fail'.
-  Read ::
-    [ErrorItem (InputToken inp)] ->
-    TermInstr (InputToken inp -> Bool) ->
-    Instr inp (InputToken inp ': vs) ('Succ es) ret ->
-    Instr inp vs ('Succ es) ret
-  DefJoin ::
-    LetName v -> Instr inp (v ': vs) es ret ->
-    Instr inp vs es ret ->
-    Instr inp vs es ret
-  RefJoin ::
-    LetName v ->
-    Instr inp (v ': vs) es ret
-
--- ** Type 'LetName'
-newtype LetName a = LetName { unLetName :: TH.Name }
-  deriving (Eq)
-  deriving newtype Show
-
--- * Class 'Executable'
-type Executable repr =
-  ( Stackable repr
-  , Branchable repr
-  , Failable repr
-  , Inputable repr
-  , Routinable repr
-  , Joinable repr
-  )
-
--- ** Class 'Stackable'
-class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
-  push ::
-    TermInstr v ->
-    repr inp (v ': vs) n ret ->
-    repr inp vs n ret
-  pop ::
-    repr inp vs n ret ->
-    repr inp (v ': vs) n ret
-  liftI2 ::
-    TermInstr (x -> y -> z) ->
-    repr inp (z ': vs) es ret ->
-    repr inp (y ': x ': vs) es ret
-  swap ::
-    repr inp (x ': y ': vs) n r ->
-    repr inp (y ': x ': vs) n r
-
--- ** Class 'Branchable'
-class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
-  case_ ::
-    repr inp (x ': vs) n r ->
-    repr inp (y ': vs) n r ->
-    repr inp (Either x y ': vs) n r
-  choices ::
-    [TermInstr (v -> Bool)] ->
-    [repr inp vs es ret] ->
-    repr inp vs es ret ->
-    repr inp (v ': vs) es ret
-
--- ** Class 'Failable'
-class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
-  fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
-  popFail ::
-    repr inp vs es ret ->
-    repr inp vs ('Succ es) ret
-  catchFail ::
-    repr inp vs ('Succ es) ret ->
-    repr inp (Cursor inp ': vs) es ret ->
-    repr inp vs es ret
-
--- ** Class 'Inputable'
-class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
-  loadInput ::
-    repr inp vs es r ->
-    repr inp (Cursor inp ': vs) es r
-  pushInput ::
-    repr inp (Cursor inp ': vs) es ret ->
-    repr inp vs es ret
-
--- ** Class 'Routinable'
-class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
-  subroutine ::
-    LetName v -> repr inp '[] ('Succ 'Zero) v ->
-    repr inp vs ('Succ es) ret ->
-    repr inp vs ('Succ es) ret
   call ::
-    LetName v -> repr inp (v ': vs) ('Succ es) ret ->
-    repr inp vs ('Succ es) ret
+    Bool ->
+    LetName v -> repr inp (v ': vs) a ->
+    repr inp vs a
+  -- | @('ret')@ returns the value stored in a singleton 'valueStack'.
   ret ::
-    repr inp '[ret] es ret
+    repr inp '[a] a
+  -- | @('jump' isRec n k)@ pass the control-flow to the 'DefLet' named @(n)@.
   jump ::
-    LetName ret ->
-    repr inp '[] ('Succ es) ret
+    Bool ->
+    LetName a ->
+    repr inp '[] a
 
--- ** Class 'Joinable'
-class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+-- ** Class 'InstrJoinable'
+class InstrJoinable (repr::ReprInstr) where
   defJoin ::
-    LetName v ->
-    repr inp (v ': vs) es ret ->
-    repr inp vs es ret ->
-    repr inp vs es ret
+    LetName v -> repr inp (v ': vs) a ->
+    repr inp vs a ->
+    repr inp vs a
   refJoin ::
     LetName v ->
-    repr inp (v ': vs) es ret
+    repr inp (v ': vs) a
 
--- ** Class 'Readable'
-class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
+-- ** Class 'InstrInputable'
+class InstrInputable (repr::ReprInstr) where
+  -- | @('saveInput' k)@ pushes the input @(inp)@ on the 'valueStackHead'
+  -- and continues with the next 'Instr'uction @(k)@.
+  saveInput ::
+    repr inp (InputPosition inp ': vs) a ->
+    repr inp vs a
+  -- | @('loadInput' k)@ removes the input from the 'valueStackHead'
+  -- and continues with the next 'Instr'uction @(k)@ using that input.
+  loadInput ::
+    repr inp vs a ->
+    repr inp (InputPosition inp ': vs) a
+
+-- ** Class 'InstrReadable'
+class InstrReadable (tok::Type) (repr::ReprInstr) where
+  -- | @('read' fs p k)@ reads a 'Char' @(c)@ from the input,
+  -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@,
+  -- otherwise 'fail'.
   read ::
     tok ~ InputToken inp =>
-    [ErrorItem tok] ->
-    TermInstr (tok -> Bool) ->
-    repr inp (tok ': vs) ('Succ es) ret ->
-    repr inp vs ('Succ es) ret
-
-instance
-  ( Executable repr
-  , Readable repr (InputToken inp)
-  ) => Trans (Instr inp vs es) (repr inp vs es) where
-  trans = \case
-    Push x k -> push x (trans k)
-    Pop k -> pop (trans k)
-    LiftI2 f k -> liftI2 f (trans k)
-    Fail err -> fail err
-    PopFail k -> popFail (trans k)
-    CatchFail l r -> catchFail (trans l) (trans r)
-    LoadInput k -> loadInput (trans k)
-    PushInput k -> pushInput (trans k)
-    Case l r -> case_ (trans l) (trans r)
-    Swap k -> swap (trans k)
-    Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
-    Subroutine n sub k -> subroutine n (trans sub) (trans k)
-    Jump n -> jump n
-    Call n k -> call n (trans k)
-    Ret -> ret
-    Read es p k -> read es p (trans k)
-    DefJoin n sub k -> defJoin n (trans sub) (trans k)
-    RefJoin n -> refJoin n
-
--- ** Type 'Peano'
--- | Type-level natural numbers, using the Peano recursive encoding.
-data Peano = Zero | Succ Peano
-
--- | @('instrFmap' f k)@.
-instrFmap ::
-  TermInstr (x -> y) ->
-  Instr inp (y ': xs) es ret ->
-  Instr inp (x ': xs) es ret
-instrFmap f k = Push f (LiftI2 (H.flip H..@ (H.$)) k)
-
--- | @('instrApp' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
--- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
-instrApp ::
-  Instr inp (y : vs) es ret ->
-  Instr inp (x : (x -> y) : vs) es ret
-instrApp k = LiftI2 (H.$) k
-
--- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
--- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
--- or @(ko)@ otherwise.
-instrIf ::
-  Instr inp vs es ret ->
-  Instr inp vs es ret ->
-  Instr inp (Bool ': vs) es ret
-instrIf ok ko = Choices [H.id] [ok] ko
-
--- * Type 'Machine'
--- | Making the control-flow explicit.
-data Machine inp v = Machine { unMachine ::
-  forall vs es ret.
-  {-k-}Instr inp (v ': vs) ('Succ es) ret ->
-  Instr inp vs ('Succ es) ret
-  }
-
-runMachine ::
-  forall inp v es repr.
-  Executable repr =>
-  Readable repr (InputToken inp) =>
-  Machine inp v -> repr inp '[] ('Succ es) v
-runMachine (Machine auto) =
-  trans @(Instr inp '[] ('Succ es)) $
-  auto Ret
-
-instance Applicable (Machine inp) where
-  pure x = Machine $ Push (trans x)
-  Machine f <*> Machine x = Machine $ f . x . instrApp
-  liftA2 f (Machine x) (Machine y) = Machine $
-    x . y . LiftI2 (trans f)
-  Machine x *> Machine y = Machine $ x . Pop . y
-  Machine x <* Machine y = Machine $ x . y . Pop
-instance
-  Cursorable (Cursor inp) =>
-  Alternable (Machine inp) where
-  empty = Machine $ \_k -> Fail []
-  Machine l <|> Machine r = Machine $ \k ->
-    makeJoin k $ \j ->
-    CatchFail
-      (l (PopFail j))
-      (instrFailIfConsumed (r j))
-  try (Machine x) = Machine $ \k ->
-    CatchFail (x (PopFail k))
-      -- On exception, reset the input,
-      -- and propagate the failure.
-      (LoadInput (Fail []))
-
--- | If no input has been consumed by the failing alternative
--- then continue with the given continuation.
--- Otherwise, propagate the 'Fail'ure.
-instrFailIfConsumed ::
-  Cursorable (Cursor inp) =>
-  Instr inp vs ('Succ es) ret ->
-  Instr inp (Cursor inp : vs) ('Succ es) ret
-instrFailIfConsumed k = PushInput (LiftI2 (H.Term sameOffset) (instrIf k (Fail [])))
-
--- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
--- by introducing a 'DefJoin' if necessary,
--- and passing the corresponding 'RefJoin' to @(f)@,
--- or @(k)@ as is when factorizing is useless.
-makeJoin ::
-  Instr inp (v : vs) es ret ->
-  (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
-  Instr inp vs es ret
--- Double RefJoin Optimization:
--- If a join-node points directly to another join-node,
--- then reuse it
-makeJoin k@RefJoin{} = ($ k)
--- Terminal RefJoin Optimization:
--- If a join-node points directly to a terminal operation,
--- then it's useless to introduce a join-point.
-makeJoin k@Ret = ($ k)
-makeJoin k =
-  let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
-  \f -> DefJoin joinName k (f (RefJoin joinName))
-
-instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
-  satisfy es p = Machine $ Read es (trans p)
-instance Selectable (Machine inp) where
-  branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
-    makeJoin k $ \j ->
-    lr (Case (l (Swap (instrApp j)))
-             (r (Swap (instrApp j))))
-instance Matchable (Machine inp) where
-  conditional(Machine a) ps bs (Machine default_) = Machine $ \k ->
-    makeJoin k $ \j ->
-    a (Choices (trans Functor.<$> ps)
-               ((\b -> unMachine b j) Functor.<$> bs)
-               (default_ j))
-instance
-  ( Ord (InputToken inp)
-  , Cursorable (Cursor inp)
-  ) => Lookable (Machine inp) where
-  look (Machine x) = Machine $ \k ->
-    PushInput (x (Swap (LoadInput k)))
-  eof = negLook (satisfy [{-discarded by negLook-}] (H.lam1 (\_x -> H.bool True)))
-        -- This sets a better failure message
-        <|> (Machine $ \_k -> Fail [ErrorItemEnd])
-  negLook (Machine x) = Machine $ \k ->
-    CatchFail
-      -- On x success, discard the result,
-      -- and replace this 'CatchFail''s failure handler
-      -- by a 'Fail'ure whose 'farthestExpecting' is negated,
-      -- then a failure is raised from the input
-      -- when entering 'negLook', to avoid odd cases:
-      -- - where the failure that made (negLook x)
-      --   succeed can get the blame for the overall
-      --   failure of the grammar.
-      -- - where the overall failure of
-      --   the grammar might be blamed on something in x
-      --   that, if corrected, still makes x succeed and
-      --   (negLook x) fail.
-      (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
-      -- On x failure, reset the input,
-      -- and go on with the next 'Instr'uctions.
-      (LoadInput (Push H.unit k))
-instance Letable TH.Name (Machine inp) where
-  def n v = Machine $ \k ->
-    Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
-  ref _isRec n = Machine $ \case
-    Ret -> Jump (LetName n)
-    k -> Call (LetName n) k
-instance Cursorable (Cursor inp) => Foldable (Machine inp) where
-  {-
-  chainPre op p = go <*> p
-    where go = (H..) <$> op <*> go <|> pure H.id
-  chainPost p op = p <**> go
-    where go = (H..) <$> op <*> go <|> pure H.id
-  -}
+    Set SomeFailure ->
+    Splice (tok -> Bool) ->
+    repr inp (tok ': vs) a ->
+    repr inp vs a
+
+-- ** Class 'InstrIterable'
+class InstrIterable (repr::ReprInstr) where
+  -- | @('iter' loop done)@.
+  iter ::
+    LetName a ->
+    repr inp '[] a ->
+    repr inp (InputPosition inp ': vs) a ->
+    repr inp vs a
+
+-- ** Class 'InstrRegisterable'
+class InstrRegisterable (repr::ReprInstr) where
+  newRegister ::
+    UnscopedRegister v ->
+    repr inp vs a ->
+    repr inp (v : vs) a
+  readRegister ::
+    UnscopedRegister v ->
+    repr inp (v : vs) a ->
+    repr inp vs a
+  writeRegister ::
+    UnscopedRegister v ->
+    repr inp vs a ->
+    repr inp (v : vs) a
+
+-- | @('modifyRegister' reg k)@
+-- modifies the content of register @(reg)@
+-- with the function at the 'valueStackHead',
+-- then continues with @(k)@.
+modifyRegister ::
+  InstrRegisterable repr =>
+  InstrValuable repr =>
+  UnscopedRegister v -> repr inp vs a -> repr inp ((v -> v) : vs) a
+modifyRegister r = readRegister r . applyValue . writeRegister r