{-# LANGUAGE ConstraintKinds #-} -- For Executable
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
{-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
{-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
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.Kind (Type)
import System.IO.Unsafe (unsafePerformIO)
import Text.Show (Show(..), showString)
import qualified Data.Functor as Functor
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

-- * Type 'Instr'
-- | 'Instr'uctions for the 'Machine'.
data Instr input valueStack (failStack::Peano) returnValue where
  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  Push ::
    InstrPure 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',
  -- and pushes the result of @(f)@ applied to them.
  LiftI2 ::
    InstrPure (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',
  -- 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 ::
    [InstrPure (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)@,
  -- '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)@,
  -- 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)] ->
    InstrPure (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 'InstrPure'
data InstrPure a where
  InstrPureHaskell :: H.Haskell a -> InstrPure a
  InstrPureSameOffset :: Cursorable cur => InstrPure (cur -> cur -> Bool)

instance Show (InstrPure a) where
  showsPrec :: Int -> InstrPure a -> ShowS
showsPrec Int
p = \case
    InstrPureHaskell Haskell a
x -> Int -> Haskell a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Haskell a
x
    InstrPure a
InstrPureSameOffset -> String -> ShowS
showString String
"InstrPureSameOffset"
instance Trans InstrPure TH.CodeQ where
  trans :: forall a. InstrPure a -> CodeQ a
trans = \case
    InstrPureHaskell Haskell a
x -> Haskell a -> CodeQ a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Haskell a
x
    InstrPure a
InstrPureSameOffset -> CodeQ a
forall cur. Cursorable cur => CodeQ (cur -> cur -> Bool)
sameOffset

-- ** Type 'LetName'
newtype LetName a = LetName { forall a. LetName a -> Name
unLetName :: TH.Name }
  deriving (LetName a -> LetName a -> Bool
(LetName a -> LetName a -> Bool)
-> (LetName a -> LetName a -> Bool) -> Eq (LetName a)
forall a. LetName a -> LetName a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LetName a -> LetName a -> Bool
$c/= :: forall a. LetName a -> LetName a -> Bool
== :: LetName a -> LetName a -> Bool
$c== :: forall a. LetName a -> LetName a -> Bool
Eq)
  deriving newtype Int -> LetName a -> ShowS
[LetName a] -> ShowS
LetName a -> String
(Int -> LetName a -> ShowS)
-> (LetName a -> String)
-> ([LetName a] -> ShowS)
-> Show (LetName a)
forall a. Int -> LetName a -> ShowS
forall a. [LetName a] -> ShowS
forall a. LetName a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LetName a] -> ShowS
$cshowList :: forall a. [LetName a] -> ShowS
show :: LetName a -> String
$cshow :: forall a. LetName a -> String
showsPrec :: Int -> LetName a -> ShowS
$cshowsPrec :: forall a. Int -> LetName a -> ShowS
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 ::
    InstrPure 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 ::
    InstrPure (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 ::
    [InstrPure (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
  ret ::
    repr inp '[ret] es ret
  jump ::
    LetName ret ->
    repr inp '[] ('Succ es) ret

-- ** Class 'Joinable'
class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
  defJoin ::
    LetName v ->
    repr inp (v ': vs) es ret ->
    repr inp vs es ret ->
    repr inp vs es ret
  refJoin ::
    LetName v ->
    repr inp (v ': vs) es ret

-- ** Class 'Readable'
class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
  read ::
    tok ~ InputToken inp =>
    [ErrorItem tok] ->
    InstrPure (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 :: forall a. Instr inp vs es a -> repr inp vs es a
trans = \case
    Push InstrPure v
x Instr inp (v : vs) es a
k -> InstrPure v -> repr inp (v : vs) es a -> repr inp vs es a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (n :: Peano) ret.
Stackable repr =>
InstrPure v -> repr inp (v : vs) n ret -> repr inp vs n ret
push InstrPure v
x (Instr inp (v : vs) es a -> repr inp (v : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (v : vs) es a
k)
    Pop Instr inp vs es a
k -> repr inp vs es a -> repr inp (v : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (n :: Peano) ret v.
Stackable repr =>
repr inp vs n ret -> repr inp (v : vs) n ret
pop (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs es a
k)
    LiftI2 InstrPure (x -> y -> z)
f Instr inp (z : vs) es a
k -> InstrPure (x -> y -> z)
-> repr inp (z : vs) es a -> repr inp (y : x : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) x y z inp (vs :: [*])
       (es :: Peano) ret.
Stackable repr =>
InstrPure (x -> y -> z)
-> repr inp (z : vs) es ret -> repr inp (y : x : vs) es ret
liftI2 InstrPure (x -> y -> z)
f (Instr inp (z : vs) es a -> repr inp (z : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (z : vs) es a
k)
    Fail [ErrorItem (InputToken inp)]
err -> [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (es :: Peano) ret.
Failable repr =>
[ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
fail [ErrorItem (InputToken inp)]
err
    PopFail Instr inp vs es a
k -> repr inp vs es a -> repr inp vs ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (es :: Peano) ret.
Failable repr =>
repr inp vs es ret -> repr inp vs ('Succ es) ret
popFail (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs es a
k)
    CatchFail Instr inp vs ('Succ es) a
l Instr inp (Cursor inp : vs) es a
r -> repr inp vs ('Succ es) a
-> repr inp (Cursor inp : vs) es a -> repr inp vs es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (es :: Peano) ret.
Failable repr =>
repr inp vs ('Succ es) ret
-> repr inp (Cursor inp : vs) es ret -> repr inp vs es ret
catchFail (Instr inp vs ('Succ es) a -> repr inp vs ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs ('Succ es) a
l) (Instr inp (Cursor inp : vs) es a -> repr inp (Cursor inp : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (Cursor inp : vs) es a
r)
    LoadInput Instr inp vs es a
k -> repr inp vs es a -> repr inp (Cursor inp : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (es :: Peano) r.
Inputable repr =>
repr inp vs es r -> repr inp (Cursor inp : vs) es r
loadInput (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs es a
k)
    PushInput Instr inp (Cursor inp : vs) es a
k -> repr inp (Cursor inp : vs) es a -> repr inp vs es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp (vs :: [*])
       (es :: Peano) ret.
Inputable repr =>
repr inp (Cursor inp : vs) es ret -> repr inp vs es ret
pushInput (Instr inp (Cursor inp : vs) es a -> repr inp (Cursor inp : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (Cursor inp : vs) es a
k)
    Case Instr inp (x : vs) es a
l Instr inp (y : vs) es a
r -> repr inp (x : vs) es a
-> repr inp (y : vs) es a -> repr inp (Either x y : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp x (vs :: [*])
       (n :: Peano) r y.
Branchable repr =>
repr inp (x : vs) n r
-> repr inp (y : vs) n r -> repr inp (Either x y : vs) n r
case_ (Instr inp (x : vs) es a -> repr inp (x : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (x : vs) es a
l) (Instr inp (y : vs) es a -> repr inp (y : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (y : vs) es a
r)
    Swap Instr inp (x : y : vs) es a
k -> repr inp (x : y : vs) es a -> repr inp (y : x : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp x y (vs :: [*])
       (n :: Peano) r.
Stackable repr =>
repr inp (x : y : vs) n r -> repr inp (y : x : vs) n r
swap (Instr inp (x : y : vs) es a -> repr inp (x : y : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (x : y : vs) es a
k)
    Choices [InstrPure (v -> Bool)]
ps [Instr inp vs es a]
bs Instr inp vs es a
d -> [InstrPure (v -> Bool)]
-> [repr inp vs es a] -> repr inp vs es a -> repr inp (v : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (es :: Peano) ret.
Branchable repr =>
[InstrPure (v -> Bool)]
-> [repr inp vs es ret]
-> repr inp vs es ret
-> repr inp (v : vs) es ret
choices [InstrPure (v -> Bool)]
ps (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Instr inp vs es a -> repr inp vs es a)
-> [Instr inp vs es a] -> [repr inp vs es a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [Instr inp vs es a]
bs) (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs es a
d)
    Subroutine LetName v
n Instr inp '[] ('Succ 'Zero) v
sub Instr inp vs ('Succ es) a
k -> LetName v
-> repr inp '[] ('Succ 'Zero) v
-> repr inp vs ('Succ es) a
-> repr inp vs ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (es :: Peano) ret.
Routinable repr =>
LetName v
-> repr inp '[] ('Succ 'Zero) v
-> repr inp vs ('Succ es) ret
-> repr inp vs ('Succ es) ret
subroutine LetName v
n (Instr inp '[] ('Succ 'Zero) v -> repr inp '[] ('Succ 'Zero) v
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp '[] ('Succ 'Zero) v
sub) (Instr inp vs ('Succ es) a -> repr inp vs ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs ('Succ es) a
k)
    Jump LetName a
n -> LetName a -> repr inp '[] ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) ret inp (es :: Peano).
Routinable repr =>
LetName ret -> repr inp '[] ('Succ es) ret
jump LetName a
n
    Call LetName v
n Instr inp (v : vs) ('Succ es) a
k -> LetName v
-> repr inp (v : vs) ('Succ es) a -> repr inp vs ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (es :: Peano) ret.
Routinable repr =>
LetName v
-> repr inp (v : vs) ('Succ es) ret -> repr inp vs ('Succ es) ret
call LetName v
n (Instr inp (v : vs) ('Succ es) a -> repr inp (v : vs) ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (v : vs) ('Succ es) a
k)
    Instr inp vs es a
Ret -> repr inp vs es a
forall (repr :: * -> [*] -> Peano -> * -> *) inp ret (es :: Peano).
Routinable repr =>
repr inp '[ret] es ret
ret
    Read [ErrorItem (InputToken inp)]
es InstrPure (InputToken inp -> Bool)
p Instr inp (InputToken inp : vs) ('Succ es) a
k -> [ErrorItem (InputToken inp)]
-> InstrPure (InputToken inp -> Bool)
-> repr inp (InputToken inp : vs) ('Succ es) a
-> repr inp vs ('Succ es) a
forall (repr :: * -> [*] -> Peano -> * -> *) tok inp (vs :: [*])
       (es :: Peano) ret.
(Readable repr tok, tok ~ InputToken inp) =>
[ErrorItem tok]
-> InstrPure (tok -> Bool)
-> repr inp (tok : vs) ('Succ es) ret
-> repr inp vs ('Succ es) ret
read [ErrorItem (InputToken inp)]
es InstrPure (InputToken inp -> Bool)
p (Instr inp (InputToken inp : vs) ('Succ es) a
-> repr inp (InputToken inp : vs) ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (InputToken inp : vs) ('Succ es) a
k)
    DefJoin LetName v
n Instr inp (v : vs) es a
sub Instr inp vs es a
k -> LetName v
-> repr inp (v : vs) es a -> repr inp vs es a -> repr inp vs es a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (es :: Peano) ret.
Joinable repr =>
LetName v
-> repr inp (v : vs) es ret
-> repr inp vs es ret
-> repr inp vs es ret
defJoin LetName v
n (Instr inp (v : vs) es a -> repr inp (v : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp (v : vs) es a
sub) (Instr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr inp vs es a
k)
    RefJoin LetName v
n -> LetName v -> repr inp (v : vs) es a
forall (repr :: * -> [*] -> Peano -> * -> *) v inp (vs :: [*])
       (es :: Peano) ret.
Joinable repr =>
LetName v -> repr inp (v : vs) es ret
refJoin LetName v
n

-- ** Type 'Peano'
-- | Type-level natural numbers, using the Peano recursive encoding.
data Peano = Zero | Succ Peano

-- | @('Fmap' f k)@.
pattern Fmap ::
  InstrPure (x -> y) ->
  Instr inp (y ': xs) es ret ->
  Instr inp (x ': xs) es ret
pattern $bFmap :: forall x inp (xs :: [*]) (es :: Peano) ret y.
InstrPure (x -> y)
-> Instr inp (y : xs) es ret -> Instr inp (x : xs) es ret
$mFmap :: forall {r} {x} {inp} {xs :: [*]} {es :: Peano} {ret}.
Instr inp (x : xs) es ret
-> (forall {y}.
    InstrPure (x -> y) -> Instr inp (y : xs) es ret -> r)
-> (Void# -> r)
-> r
Fmap f k = Push f (LiftI2 (InstrPureHaskell (H.Flip H.:@ (H.:$))) k)

-- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
-- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
pattern App ::
  Instr inp (y : vs) es ret ->
  Instr inp (x : (x -> y) : vs) es ret
pattern $bApp :: forall inp y (vs :: [*]) (es :: Peano) ret x.
Instr inp (y : vs) es ret -> Instr inp (x : (x -> y) : vs) es ret
$mApp :: forall {r} {inp} {y} {vs :: [*]} {es :: Peano} {ret} {x}.
Instr inp (x : (x -> y) : vs) es ret
-> (Instr inp (y : vs) es ret -> r) -> (Void# -> r) -> r
App k = LiftI2 (InstrPureHaskell (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.
pattern If ::
  Instr inp vs es ret ->
  Instr inp vs es ret ->
  Instr inp (Bool ': vs) es ret
pattern $bIf :: forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs es ret
-> Instr inp vs es ret -> Instr inp (Bool : vs) es ret
$mIf :: forall {r} {inp} {vs :: [*]} {es :: Peano} {ret}.
Instr inp (Bool : vs) es ret
-> (Instr inp vs es ret -> Instr inp vs es ret -> r)
-> (Void# -> r)
-> r
If ok ko = Choices [InstrPureHaskell H.Id] [ok] ko

-- * Type 'Machine'
-- | Making the control-flow explicit.
data Machine inp v = Machine { forall inp v.
Machine inp v
-> forall (vs :: [*]) (es :: Peano) ret.
   Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
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 :: forall inp v (es :: Peano) (repr :: * -> [*] -> Peano -> * -> *).
(Executable repr, Readable repr (InputToken inp)) =>
Machine inp v -> repr inp '[] ('Succ es) v
runMachine (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
auto) =
  forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans @(Instr inp '[] ('Succ es)) (Instr inp '[] ('Succ es) v -> repr inp '[] ('Succ es) v)
-> Instr inp '[] ('Succ es) v -> repr inp '[] ('Succ es) v
forall a b. (a -> b) -> a -> b
$
  Instr inp '[v] ('Succ es) v -> Instr inp '[] ('Succ es) v
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
auto Instr inp '[v] ('Succ es) v
forall inp ret (es :: Peano). Instr inp '[ret] es ret
Ret

instance Applicable (Machine inp) where
  pure :: forall a. Haskell a -> Machine inp a
pure Haskell a
x = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ InstrPure a
-> Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall es inp (vs :: [*]) (es :: Peano) ret.
InstrPure es -> Instr inp (es : vs) es ret -> Instr inp vs es ret
Push (Haskell a -> InstrPure a
forall a. Haskell a -> InstrPure a
InstrPureHaskell Haskell a
x)
  Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((a -> b) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
f <*> :: forall a b. Machine inp (a -> b) -> Machine inp a -> Machine inp b
<*> Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp b)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall a b. (a -> b) -> a -> b
$ Instr inp ((a -> b) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((a -> b) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
f (Instr inp ((a -> b) : vs) ('Succ es) ret
 -> Instr inp vs ('Succ es) ret)
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp ((a -> b) : vs) ('Succ es) ret)
-> Instr inp (b : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (a : (a -> b) : vs) ('Succ es) ret
-> Instr inp ((a -> b) : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (a : (a -> b) : vs) ('Succ es) ret
 -> Instr inp ((a -> b) : vs) ('Succ es) ret)
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp (a : (a -> b) : vs) ('Succ es) ret)
-> Instr inp (b : vs) ('Succ es) ret
-> Instr inp ((a -> b) : vs) ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (b : vs) ('Succ es) ret
-> Instr inp (a : (a -> b) : vs) ('Succ es) ret
forall inp y (vs :: [*]) (es :: Peano) ret x.
Instr inp (y : vs) es ret -> Instr inp (x : (x -> y) : vs) es ret
App
  liftA2 :: forall a b c.
Haskell (a -> b -> c)
-> Machine inp a -> Machine inp b -> Machine inp c
liftA2 Haskell (a -> b -> c)
f (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x) (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp c
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp c)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp c
forall a b. (a -> b) -> a -> b
$
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> (Instr inp (c : vs) ('Succ es) ret
    -> Instr inp (a : vs) ('Succ es) ret)
-> Instr inp (c : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (b : a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y (Instr inp (b : a : vs) ('Succ es) ret
 -> Instr inp (a : vs) ('Succ es) ret)
-> (Instr inp (c : vs) ('Succ es) ret
    -> Instr inp (b : a : vs) ('Succ es) ret)
-> Instr inp (c : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstrPure (a -> b -> c)
-> Instr inp (c : vs) ('Succ es) ret
-> Instr inp (b : a : vs) ('Succ es) ret
forall es es vs inp (vs :: [*]) (es :: Peano) ret.
InstrPure (es -> es -> vs)
-> Instr inp (vs : vs) es ret -> Instr inp (es : es : vs) es ret
LiftI2 (Haskell (a -> b -> c) -> InstrPure (a -> b -> c)
forall a. Haskell a -> InstrPure a
InstrPureHaskell Haskell (a -> b -> c)
f)
  Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x *> :: forall a b. Machine inp a -> Machine inp b -> Machine inp b
*> Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp b)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall a b. (a -> b) -> a -> b
$ Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp (a : vs) ('Succ es) ret)
-> Instr inp (b : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp vs ('Succ es) ret -> Instr inp (a : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) ret es.
Instr inp es es ret -> Instr inp (es : es) es ret
Pop (Instr inp vs ('Succ es) ret -> Instr inp (a : vs) ('Succ es) ret)
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp (b : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y
  Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x <* :: forall a b. Machine inp a -> Machine inp b -> Machine inp a
<* Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> (Instr inp (a : vs) ('Succ es) ret
    -> Instr inp (a : vs) ('Succ es) ret)
-> Instr inp (a : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (b : a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
y (Instr inp (b : a : vs) ('Succ es) ret
 -> Instr inp (a : vs) ('Succ es) ret)
-> (Instr inp (a : vs) ('Succ es) ret
    -> Instr inp (b : a : vs) ('Succ es) ret)
-> Instr inp (a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr inp (a : vs) ('Succ es) ret
-> Instr inp (b : a : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) ret es.
Instr inp es es ret -> Instr inp (es : es) es ret
Pop
instance
  Cursorable (Cursor inp) =>
  Alternable (Machine inp) where
  empty :: forall a. Machine inp a
empty = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
_k -> [ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
Fail []
  Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
l <|> :: forall a. Machine inp a -> Machine inp a -> Machine inp a
<|> Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
r = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
k ->
    Instr inp (a : vs) ('Succ es) ret
-> (Instr inp (a : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall inp v (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) es ret
-> (Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp vs es ret
makeJoin Instr inp (a : vs) ('Succ es) ret
k ((Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Instr inp vs ('Succ es) ret)
-> (Instr inp (a : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
j ->
    Instr inp vs ('Succ ('Succ es)) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
CatchFail
      (Instr inp (a : vs) ('Succ ('Succ es)) ret
-> Instr inp vs ('Succ ('Succ es)) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
l (Instr inp (a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ ('Succ es)) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs es ret -> Instr inp vs ('Succ es) ret
PopFail Instr inp (a : vs) ('Succ es) ret
j))
      (Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Cursorable (Cursor inp) =>
Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
failIfConsumed (Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
r Instr inp (a : vs) ('Succ es) ret
j))
  try :: forall a. Machine inp a -> Machine inp a
try (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
k ->
    Instr inp vs ('Succ ('Succ es)) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
CatchFail (Instr inp (a : vs) ('Succ ('Succ es)) ret
-> Instr inp vs ('Succ ('Succ es)) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ ('Succ es)) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs es ret -> Instr inp vs ('Succ es) ret
PopFail Instr inp (a : vs) ('Succ es) ret
k))
      -- On exception, reset the input,
      -- and propagate the failure.
      (Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) r.
Instr inp es es r -> Instr inp (Cursor inp : es) es r
LoadInput ([ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
Fail []))

-- | If no input has been consumed by the failing alternative
-- then continue with the given continuation.
-- Otherwise, propagate the 'Fail'ure.
failIfConsumed ::
  Cursorable (Cursor inp) =>
  Instr inp vs ('Succ es) ret ->
  Instr inp (Cursor inp : vs) ('Succ es) ret
failIfConsumed :: forall inp (vs :: [*]) (es :: Peano) ret.
Cursorable (Cursor inp) =>
Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
failIfConsumed Instr inp vs ('Succ es) ret
k = Instr inp (Cursor inp : Cursor inp : vs) ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
PushInput (InstrPure (Cursor inp -> Cursor inp -> Bool)
-> Instr inp (Bool : vs) ('Succ es) ret
-> Instr inp (Cursor inp : Cursor inp : vs) ('Succ es) ret
forall es es vs inp (vs :: [*]) (es :: Peano) ret.
InstrPure (es -> es -> vs)
-> Instr inp (vs : vs) es ret -> Instr inp (es : es : vs) es ret
LiftI2 InstrPure (Cursor inp -> Cursor inp -> Bool)
forall es. Cursorable es => InstrPure (es -> es -> Bool)
InstrPureSameOffset (Instr inp vs ('Succ es) ret
-> Instr inp vs ('Succ es) ret
-> Instr inp (Bool : vs) ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs es ret
-> Instr inp vs es ret -> Instr inp (Bool : vs) es ret
If Instr inp vs ('Succ es) ret
k ([ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
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 :: forall inp v (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) es ret
-> (Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp vs es ret
makeJoin k :: Instr inp (v : vs) es ret
k@RefJoin{} = ((Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp (v : vs) es ret -> Instr inp vs es ret
forall a b. (a -> b) -> a -> b
$ Instr inp (v : vs) es ret
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 :: Instr inp (v : vs) es ret
k@Instr inp (v : vs) es ret
Ret = ((Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp (v : vs) es ret -> Instr inp vs es ret
forall a b. (a -> b) -> a -> b
$ Instr inp (v : vs) es ret
k)
makeJoin Instr inp (v : vs) es ret
k =
  let joinName :: LetName a
joinName = Name -> LetName a
forall a. Name -> LetName a
LetName (Name -> LetName a) -> Name -> LetName a
forall a b. (a -> b) -> a -> b
$ IO Name -> Name
forall a. IO a -> a
unsafePerformIO (IO Name -> Name) -> IO Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> IO Name
forall (m :: * -> *). Quasi m => String -> m Name
TH.qNewName String
"join" in
  \Instr inp (v : vs) es ret -> Instr inp vs es ret
f -> LetName v
-> Instr inp (v : vs) es ret
-> Instr inp vs es ret
-> Instr inp vs es ret
forall es inp (vs :: [*]) (es :: Peano) ret.
LetName es
-> Instr inp (es : vs) es ret
-> Instr inp vs es ret
-> Instr inp vs es ret
DefJoin LetName v
forall {a}. LetName a
joinName Instr inp (v : vs) es ret
k (Instr inp (v : vs) es ret -> Instr inp vs es ret
f (LetName v -> Instr inp (v : vs) es ret
forall es inp (es :: [*]) (es :: Peano) ret.
LetName es -> Instr inp (es : es) es ret
RefJoin LetName v
forall {a}. LetName a
joinName))

instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
  satisfy :: [ErrorItem tok] -> Haskell (tok -> Bool) -> Machine inp tok
satisfy [ErrorItem tok]
es Haskell (tok -> Bool)
p = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (tok : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp tok
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (tok : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp tok)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (tok : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp tok
forall a b. (a -> b) -> a -> b
$ [ErrorItem (InputToken inp)]
-> InstrPure (InputToken inp -> Bool)
-> Instr inp (InputToken inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)]
-> InstrPure (InputToken inp -> Bool)
-> Instr inp (InputToken inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
Read [ErrorItem tok]
[ErrorItem (InputToken inp)]
es (Haskell (tok -> Bool) -> InstrPure (tok -> Bool)
forall a. Haskell a -> InstrPure a
InstrPureHaskell Haskell (tok -> Bool)
p)
instance Selectable (Machine inp) where
  branch :: forall a b c.
Machine inp (Either a b)
-> Machine inp (a -> c) -> Machine inp (b -> c) -> Machine inp c
branch (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (Either a b : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
lr) (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((a -> c) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
l) (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((b -> c) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
r) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp c
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp c)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp c
forall a b. (a -> b) -> a -> b
$ \Instr inp (c : vs) ('Succ es) ret
k ->
    Instr inp (c : vs) ('Succ es) ret
-> (Instr inp (c : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall inp v (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) es ret
-> (Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp vs es ret
makeJoin Instr inp (c : vs) ('Succ es) ret
k ((Instr inp (c : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Instr inp vs ('Succ es) ret)
-> (Instr inp (c : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall a b. (a -> b) -> a -> b
$ \Instr inp (c : vs) ('Succ es) ret
j ->
    Instr inp (Either a b : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (Either a b : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
lr (Instr inp (a : vs) ('Succ es) ret
-> Instr inp (b : vs) ('Succ es) ret
-> Instr inp (Either a b : vs) ('Succ es) ret
forall inp es (es :: [*]) (es :: Peano) r vs.
Instr inp (es : es) es r
-> Instr inp (vs : es) es r -> Instr inp (Either es vs : es) es r
Case (Instr inp ((a -> c) : a : vs) ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((a -> c) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
l (Instr inp (a : (a -> c) : vs) ('Succ es) ret
-> Instr inp ((a -> c) : a : vs) ('Succ es) ret
forall inp es es (vs :: [*]) (es :: Peano) r.
Instr inp (es : es : vs) es r -> Instr inp (es : es : vs) es r
Swap (Instr inp (c : vs) ('Succ es) ret
-> Instr inp (a : (a -> c) : vs) ('Succ es) ret
forall inp y (vs :: [*]) (es :: Peano) ret x.
Instr inp (y : vs) es ret -> Instr inp (x : (x -> y) : vs) es ret
App Instr inp (c : vs) ('Succ es) ret
j)))
             (Instr inp ((b -> c) : b : vs) ('Succ es) ret
-> Instr inp (b : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp ((b -> c) : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
r (Instr inp (b : (b -> c) : vs) ('Succ es) ret
-> Instr inp ((b -> c) : b : vs) ('Succ es) ret
forall inp es es (vs :: [*]) (es :: Peano) r.
Instr inp (es : es : vs) es r -> Instr inp (es : es : vs) es r
Swap (Instr inp (c : vs) ('Succ es) ret
-> Instr inp (b : (b -> c) : vs) ('Succ es) ret
forall inp y (vs :: [*]) (es :: Peano) ret x.
Instr inp (y : vs) es ret -> Instr inp (x : (x -> y) : vs) es ret
App Instr inp (c : vs) ('Succ es) ret
j))))
instance Matchable (Machine inp) where
  conditional :: forall a b.
Eq a =>
[Haskell (a -> Bool)]
-> [Machine inp b]
-> Machine inp a
-> Machine inp b
-> Machine inp b
conditional [Haskell (a -> Bool)]
ps [Machine inp b]
bs (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
m) (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
default_) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp b)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp b
forall a b. (a -> b) -> a -> b
$ \Instr inp (b : vs) ('Succ es) ret
k ->
    Instr inp (b : vs) ('Succ es) ret
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall inp v (vs :: [*]) (es :: Peano) ret.
Instr inp (v : vs) es ret
-> (Instr inp (v : vs) es ret -> Instr inp vs es ret)
-> Instr inp vs es ret
makeJoin Instr inp (b : vs) ('Succ es) ret
k ((Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Instr inp vs ('Succ es) ret)
-> (Instr inp (b : vs) ('Succ es) ret
    -> Instr inp vs ('Succ es) ret)
-> Instr inp vs ('Succ es) ret
forall a b. (a -> b) -> a -> b
$ \Instr inp (b : vs) ('Succ es) ret
j ->
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
m ([InstrPure (a -> Bool)]
-> [Instr inp vs ('Succ es) ret]
-> Instr inp vs ('Succ es) ret
-> Instr inp (a : vs) ('Succ es) ret
forall es inp (es :: [*]) (es :: Peano) ret.
[InstrPure (es -> Bool)]
-> [Instr inp es es ret]
-> Instr inp es es ret
-> Instr inp (es : es) es ret
Choices (Haskell (a -> Bool) -> InstrPure (a -> Bool)
forall a. Haskell a -> InstrPure a
InstrPureHaskell (Haskell (a -> Bool) -> InstrPure (a -> Bool))
-> [Haskell (a -> Bool)] -> [InstrPure (a -> Bool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [Haskell (a -> Bool)]
ps)
               ((\Machine inp b
b -> Machine inp b
-> forall (vs :: [*]) (es :: Peano) ret.
   Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall inp v.
Machine inp v
-> forall (vs :: [*]) (es :: Peano) ret.
   Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
unMachine Machine inp b
b Instr inp (b : vs) ('Succ es) ret
j) (Machine inp b -> Instr inp vs ('Succ es) ret)
-> [Machine inp b] -> [Instr inp vs ('Succ es) ret]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [Machine inp b]
bs)
               (Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (b : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
default_ Instr inp (b : vs) ('Succ es) ret
j))
instance
  ( Ord (InputToken inp)
  , Cursorable (Cursor inp)
  ) => Lookable (Machine inp) where
  look :: forall a. Machine inp a -> Machine inp a
look (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
k ->
    Instr inp (Cursor inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
PushInput (Instr inp (a : Cursor inp : vs) ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (Cursor inp : a : vs) ('Succ es) ret
-> Instr inp (a : Cursor inp : vs) ('Succ es) ret
forall inp es es (vs :: [*]) (es :: Peano) r.
Instr inp (es : es : vs) es r -> Instr inp (es : es : vs) es r
Swap (Instr inp (a : vs) ('Succ es) ret
-> Instr inp (Cursor inp : a : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) r.
Instr inp es es r -> Instr inp (Cursor inp : es) es r
LoadInput Instr inp (a : vs) ('Succ es) ret
k)))
  eof :: Machine inp ()
eof = Machine inp (InputToken inp) -> Machine inp ()
forall (repr :: * -> *) a. Lookable repr => repr a -> repr ()
negLook ([ErrorItem (InputToken inp)]
-> Haskell (InputToken inp -> Bool) -> Machine inp (InputToken inp)
forall (repr :: * -> *) tok.
Satisfiable repr tok =>
[ErrorItem tok] -> Haskell (tok -> Bool) -> repr tok
satisfy [{-discarded by negLook-}] (Haskell (Bool -> InputToken inp -> Bool)
forall (repr :: * -> *) a b. Haskellable repr => repr (a -> b -> a)
H.const Haskell (Bool -> InputToken inp -> Bool)
-> Haskell Bool -> Haskell (InputToken inp -> Bool)
forall (repr :: * -> *) a b.
Haskellable repr =>
repr (a -> b) -> repr a -> repr b
H..@ Bool -> Haskell Bool
forall (repr :: * -> *). Haskellable repr => Bool -> repr Bool
H.bool Bool
True))
        -- Set a better failure message
        Machine inp () -> Machine inp () -> Machine inp ()
forall (repr :: * -> *) a.
Alternable repr =>
repr a -> repr a -> repr a
<|> ((forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp ()
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp ())
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp ()
forall a b. (a -> b) -> a -> b
$ \Instr inp (() : vs) ('Succ es) ret
_k -> [ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
Fail [ErrorItem (InputToken inp)
forall tok. ErrorItem tok
ErrorItemEnd])
  negLook :: forall a. Machine inp a -> Machine inp ()
negLook (Machine forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x) = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp ()
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp ())
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (() : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp ()
forall a b. (a -> b) -> a -> b
$ \Instr inp (() : vs) ('Succ es) ret
k ->
    Instr inp vs ('Succ ('Succ es)) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
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.
      (Instr inp (Cursor inp : vs) ('Succ ('Succ es)) ret
-> Instr inp vs ('Succ ('Succ es)) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp (Cursor inp : vs) es ret -> Instr inp vs es ret
PushInput (Instr inp (a : Cursor inp : vs) ('Succ ('Succ es)) ret
-> Instr inp (Cursor inp : vs) ('Succ ('Succ es)) ret
forall (vs :: [*]) (es :: Peano) ret.
Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
x (Instr inp (Cursor inp : vs) ('Succ ('Succ es)) ret
-> Instr inp (a : Cursor inp : vs) ('Succ ('Succ es)) ret
forall inp (es :: [*]) (es :: Peano) ret es.
Instr inp es es ret -> Instr inp (es : es) es ret
Pop (Instr inp (Cursor inp : vs) ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ ('Succ es)) ret
forall inp (vs :: [*]) (es :: Peano) ret.
Instr inp vs es ret -> Instr inp vs ('Succ es) ret
PopFail (Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) r.
Instr inp es es r -> Instr inp (Cursor inp : es) es r
LoadInput ([ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
forall inp (vs :: [*]) (es :: Peano) ret.
[ErrorItem (InputToken inp)] -> Instr inp vs ('Succ es) ret
Fail []))))))
      -- On x failure, reset the input,
      -- and go on with the next 'Instr'uctions.
      (Instr inp vs ('Succ es) ret
-> Instr inp (Cursor inp : vs) ('Succ es) ret
forall inp (es :: [*]) (es :: Peano) r.
Instr inp es es r -> Instr inp (Cursor inp : es) es r
LoadInput (InstrPure ()
-> Instr inp (() : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall es inp (vs :: [*]) (es :: Peano) ret.
InstrPure es -> Instr inp (es : vs) es ret -> Instr inp vs es ret
Push (Haskell () -> InstrPure ()
forall a. Haskell a -> InstrPure a
InstrPureHaskell Haskell ()
forall (repr :: * -> *). Haskellable repr => repr ()
H.unit) Instr inp (() : vs) ('Succ es) ret
k))
instance Letable TH.Name (Machine inp) where
  def :: forall a. Name -> Machine inp a -> Machine inp a
def Name
n Machine inp a
v = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \Instr inp (a : vs) ('Succ es) ret
k ->
    LetName a
-> Instr inp '[] ('Succ 'Zero) a
-> Instr inp vs ('Succ es) ret
-> Instr inp vs ('Succ es) ret
forall es inp (vs :: [*]) (es :: Peano) ret.
LetName es
-> Instr inp '[] ('Succ 'Zero) es
-> Instr inp vs ('Succ es) ret
-> Instr inp vs ('Succ es) ret
Subroutine (Name -> LetName a
forall a. Name -> LetName a
LetName Name
n) (Machine inp a
-> forall (vs :: [*]) (es :: Peano) ret.
   Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall inp v.
Machine inp v
-> forall (vs :: [*]) (es :: Peano) ret.
   Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
unMachine Machine inp a
v Instr inp '[a] ('Succ 'Zero) a
forall inp ret (es :: Peano). Instr inp '[ret] es ret
Ret) (LetName a
-> Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall es inp (vs :: [*]) (es :: Peano) ret.
LetName es
-> Instr inp (es : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
Call (Name -> LetName a
forall a. Name -> LetName a
LetName Name
n) Instr inp (a : vs) ('Succ es) ret
k)
  ref :: forall a. Bool -> Name -> Machine inp a
ref Bool
_isRec Name
n = (forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall inp v.
(forall (vs :: [*]) (es :: Peano) ret.
 Instr inp (v : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp v
Machine ((forall (vs :: [*]) (es :: Peano) ret.
  Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
 -> Machine inp a)
-> (forall (vs :: [*]) (es :: Peano) ret.
    Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret)
-> Machine inp a
forall a b. (a -> b) -> a -> b
$ \case
    Instr inp (a : vs) ('Succ es) ret
Ret -> LetName ret -> Instr inp '[] ('Succ es) ret
forall ret inp (es :: Peano).
LetName ret -> Instr inp '[] ('Succ es) ret
Jump (Name -> LetName ret
forall a. Name -> LetName a
LetName Name
n)
    Instr inp (a : vs) ('Succ es) ret
k -> LetName a
-> Instr inp (a : vs) ('Succ es) ret -> Instr inp vs ('Succ es) ret
forall es inp (vs :: [*]) (es :: Peano) ret.
LetName es
-> Instr inp (es : vs) ('Succ es) ret
-> Instr inp vs ('Succ es) ret
Call (Name -> LetName a
forall a. Name -> LetName a
LetName Name
n) Instr inp (a : vs) ('Succ es) ret
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
  -}