{-# LANGUAGE PatternSynonyms #-} -- For Instr
{-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
{-# LANGUAGE UndecidableInstances #-}
-- | Initial encoding with bottom-up optimizations of 'Instr'uctions,
-- re-optimizing downward as needed after each optimization.
-- There is only one optimization (for 'push') so far,
-- but the introspection enabled by the 'Instr' data-type
-- is also useful to optimize with more context in the 'Machine'.
module Symantic.Parser.Machine.Optimize where

import Data.Bool (Bool(..))
import Data.Either (Either)
import Data.Maybe (Maybe(..))
import Data.Function ((.))
import Data.Kind (Constraint)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
import qualified Data.Functor as Functor

import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
import Symantic.Parser.Machine.Instructions
import Symantic.Univariant.Trans

-- * Data family 'Instr'
-- | 'Instr'uctions of the 'Machine'.
-- This is an extensible data-type.
data family Instr
  (instr :: ReprInstr -> Constraint)
  (repr :: ReprInstr)
  :: ReprInstr

-- | Convenient utility to pattern-match a 'SomeInstr'.
pattern Instr :: Typeable comb =>
  Instr comb repr inp vs es a ->
  SomeInstr repr inp vs es a
pattern $mInstr :: forall {r} {comb :: ReprInstr -> Constraint} {repr :: ReprInstr}
       {inp} {vs :: [*]} {es :: Peano} {a}.
Typeable comb =>
SomeInstr repr inp vs es a
-> (Instr comb repr inp vs es a -> r) -> (Void# -> r) -> r
Instr x <- (unSomeInstr -> Just x)

-- ** Type 'SomeInstr'
-- | Some 'Instr'uction existantialized over the actual instruction symantic class.
-- Useful to handle a list of 'Instr'uctions
-- without requiring impredicative quantification.
-- Must be used by pattern-matching
-- on the 'SomeInstr' data-constructor,
-- to bring the constraints in scope.
--
-- As in 'SomeComb', a first pass of optimizations
-- is directly applied in it
-- to avoid introducing an extra newtype,
-- this also give a more comprehensible code.
data SomeInstr repr inp vs es a =
  forall instr.
  (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
  SomeInstr (Instr instr repr inp vs es a)

instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
  trans :: forall a. SomeInstr repr inp vs es a -> repr inp vs es a
trans (SomeInstr Instr instr repr inp vs es a
x) = Instr instr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Instr instr repr inp vs es a
x

-- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
-- extract the data-constructor from the given 'SomeInstr'
-- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
unSomeInstr ::
  forall instr repr inp vs es a.
  Typeable instr =>
  SomeInstr repr inp vs es a ->
  Maybe (Instr instr repr inp vs es a)
unSomeInstr :: forall (instr :: ReprInstr -> Constraint) (repr :: ReprInstr) inp
       (vs :: [*]) (es :: Peano) a.
Typeable instr =>
SomeInstr repr inp vs es a -> Maybe (Instr instr repr inp vs es a)
unSomeInstr (SomeInstr (Instr instr repr inp vs es a
i::Instr i repr inp vs es a)) =
  case forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: ReprInstr -> Constraint). Typeable a => TypeRep a
typeRep @instr TypeRep instr -> TypeRep instr -> Maybe (instr :~~: instr)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: ReprInstr -> Constraint). Typeable a => TypeRep a
typeRep @i of
    Just instr :~~: instr
HRefl -> Instr instr repr inp vs es a
-> Maybe (Instr instr repr inp vs es a)
forall a. a -> Maybe a
Just Instr instr repr inp vs es a
i
    Maybe (instr :~~: instr)
Nothing -> Maybe (Instr instr repr inp vs es a)
forall a. Maybe a
Nothing

-- Stackable
data instance Instr Stackable repr inp vs fs a where
  -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  Push ::
    TermInstr v ->
    SomeInstr repr inp (v ': vs) es a ->
    Instr Stackable repr inp vs es a
  -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
  Pop ::
    SomeInstr repr inp vs es a ->
    Instr Stackable repr inp (v ': vs) es a
  -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
  -- and pushes the result of @(f)@ applied to them.
  LiftI2 ::
    TermInstr (x -> y -> z) ->
    SomeInstr repr inp (z : vs) es a ->
    Instr Stackable repr inp (y : x : vs) es a
  -- | @('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 ::
    SomeInstr repr inp (x ': y ': vs) es a ->
    Instr Stackable repr inp (y ': x ': vs) es a
instance Stackable repr => Trans (Instr Stackable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Stackable repr inp vs es a -> repr inp vs es a
trans = \case
    Push TermInstr v
x SomeInstr repr inp (v : vs) es a
k -> TermInstr v -> repr inp (v : vs) es a -> repr inp vs es a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Stackable repr =>
TermInstr v -> repr inp (v : vs) es a -> repr inp vs es a
push TermInstr v
x (SomeInstr repr inp (v : vs) es a -> repr inp (v : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (v : vs) es a
k)
    Pop SomeInstr repr inp vs es a
k -> repr inp vs es a -> repr inp (v : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a v.
Stackable repr =>
repr inp vs es a -> repr inp (v : vs) es a
pop (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs es a
k)
    LiftI2 TermInstr (x -> y -> z)
f SomeInstr repr inp (z : vs) es a
k -> TermInstr (x -> y -> z)
-> repr inp (z : vs) es a -> repr inp (y : x : vs) es a
forall (repr :: ReprInstr) x y z inp (vs :: [*]) (es :: Peano) a.
Stackable repr =>
TermInstr (x -> y -> z)
-> repr inp (z : vs) es a -> repr inp (y : x : vs) es a
liftI2 TermInstr (x -> y -> z)
f (SomeInstr repr inp (z : vs) es a -> repr inp (z : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (z : vs) es a
k)
    Swap SomeInstr repr inp (x : y : vs) es a
k -> repr inp (x : y : vs) es a -> repr inp (y : x : vs) es a
forall (repr :: ReprInstr) inp x y (vs :: [*]) (es :: Peano) a.
Stackable repr =>
repr inp (x : y : vs) es a -> repr inp (y : x : vs) es a
swap (SomeInstr repr 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 SomeInstr repr inp (x : y : vs) es a
k)
instance Stackable repr => Stackable (SomeInstr repr) where
  push :: forall v inp (vs :: [*]) (es :: Peano) a.
TermInstr v
-> SomeInstr repr inp (v : vs) es a -> SomeInstr repr inp vs es a
push TermInstr v
_v (Instr (Pop SomeInstr repr inp vs es a
i)) = SomeInstr repr inp vs es a
SomeInstr repr inp vs es a
i
  push TermInstr v
v SomeInstr repr inp (v : vs) es a
i = Instr Stackable repr inp vs es a -> SomeInstr repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (TermInstr v
-> SomeInstr repr inp (v : vs) es a
-> Instr Stackable repr inp vs es a
forall es (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
TermInstr es
-> SomeInstr repr inp (es : vs) es a
-> Instr Stackable repr inp vs es a
Push TermInstr v
v SomeInstr repr inp (v : vs) es a
i)
  pop :: forall inp (vs :: [*]) (es :: Peano) a v.
SomeInstr repr inp vs es a -> SomeInstr repr inp (v : vs) es a
pop = Instr Stackable repr inp (v : vs) es a
-> SomeInstr repr inp (v : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Stackable repr inp (v : vs) es a
 -> SomeInstr repr inp (v : vs) es a)
-> (SomeInstr repr inp vs es a
    -> Instr Stackable repr inp (v : vs) es a)
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp (v : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp vs es a
-> Instr Stackable repr inp (v : vs) es a
forall (repr :: ReprInstr) inp (es :: [*]) (es :: Peano) a vs.
SomeInstr repr inp es es a
-> Instr Stackable repr inp (vs : es) es a
Pop
  liftI2 :: forall x y z inp (vs :: [*]) (es :: Peano) a.
TermInstr (x -> y -> z)
-> SomeInstr repr inp (z : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
liftI2 TermInstr (x -> y -> z)
f = Instr Stackable repr inp (y : x : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Stackable repr inp (y : x : vs) es a
 -> SomeInstr repr inp (y : x : vs) es a)
-> (SomeInstr repr inp (z : vs) es a
    -> Instr Stackable repr inp (y : x : vs) es a)
-> SomeInstr repr inp (z : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermInstr (x -> y -> z)
-> SomeInstr repr inp (z : vs) es a
-> Instr Stackable repr inp (y : x : vs) es a
forall es vs y (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
TermInstr (es -> vs -> y)
-> SomeInstr repr inp (y : vs) es a
-> Instr Stackable repr inp (vs : es : vs) es a
LiftI2 TermInstr (x -> y -> z)
f
  swap :: forall inp x y (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp (x : y : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
swap = Instr Stackable repr inp (y : x : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Stackable repr inp (y : x : vs) es a
 -> SomeInstr repr inp (y : x : vs) es a)
-> (SomeInstr repr inp (x : y : vs) es a
    -> Instr Stackable repr inp (y : x : vs) es a)
-> SomeInstr repr inp (x : y : vs) es a
-> SomeInstr repr inp (y : x : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp (x : y : vs) es a
-> Instr Stackable repr inp (y : x : vs) es a
forall (repr :: ReprInstr) inp es vs (y :: [*]) (es :: Peano) a.
SomeInstr repr inp (es : vs : y) es a
-> Instr Stackable repr inp (vs : es : y) es a
Swap

-- Routinable
data instance Instr Routinable repr inp vs fs a where
  -- | @('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 ->
    SomeInstr repr inp '[] ('Succ 'Zero) v ->
    SomeInstr repr inp vs ('Succ es) a ->
    Instr Routinable repr inp vs ('Succ es) a
  -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  Jump ::
    LetName a ->
    Instr Routinable repr inp '[] ('Succ es) a
  -- | @('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 ->
    SomeInstr repr inp (v ': vs) ('Succ es) a ->
    Instr Routinable repr inp vs ('Succ es) a
  -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
  Ret ::
    Instr Routinable repr inp '[a] es a
instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Routinable repr inp vs es a -> repr inp vs es a
trans = \case
    Subroutine LetName v
n SomeInstr repr inp '[] ('Succ 'Zero) v
sub SomeInstr repr 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 :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Routinable repr =>
LetName v
-> repr inp '[] ('Succ 'Zero) v
-> repr inp vs ('Succ es) a
-> repr inp vs ('Succ es) a
subroutine LetName v
n (SomeInstr repr inp '[] ('Succ 'Zero) v
-> repr inp '[] ('Succ 'Zero) v
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp '[] ('Succ 'Zero) v
sub) (SomeInstr repr inp vs ('Succ es) a -> repr inp vs ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs ('Succ es) a
k)
    Jump LetName a
n -> LetName a -> repr inp '[] ('Succ es) a
forall (repr :: ReprInstr) a inp (es :: Peano).
Routinable repr =>
LetName a -> repr inp '[] ('Succ es) a
jump LetName a
n
    Call LetName v
n SomeInstr repr inp (v : vs) ('Succ es) a
k -> LetName v
-> repr inp (v : vs) ('Succ es) a -> repr inp vs ('Succ es) a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Routinable repr =>
LetName v
-> repr inp (v : vs) ('Succ es) a -> repr inp vs ('Succ es) a
call LetName v
n (SomeInstr repr 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 SomeInstr repr inp (v : vs) ('Succ es) a
k)
    Instr Routinable repr inp vs es a
R:InstrRoutinablereprinpvsfsa repr inp vs es a
Ret -> repr inp vs es a
forall (repr :: ReprInstr) inp a (es :: Peano).
Routinable repr =>
repr inp '[a] es a
ret
instance Routinable repr => Routinable (SomeInstr repr) where
  subroutine :: forall v inp (vs :: [*]) (es :: Peano) a.
LetName v
-> SomeInstr repr inp '[] ('Succ 'Zero) v
-> SomeInstr repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
subroutine LetName v
n SomeInstr repr inp '[] ('Succ 'Zero) v
sub = Instr Routinable repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Routinable repr inp vs ('Succ es) a
 -> SomeInstr repr inp vs ('Succ es) a)
-> (SomeInstr repr inp vs ('Succ es) a
    -> Instr Routinable repr inp vs ('Succ es) a)
-> SomeInstr repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetName v
-> SomeInstr repr inp '[] ('Succ 'Zero) v
-> SomeInstr repr inp vs ('Succ es) a
-> Instr Routinable repr inp vs ('Succ es) a
forall es (repr :: ReprInstr) inp (vs :: [*]) (vs :: Peano) a.
LetName es
-> SomeInstr repr inp '[] ('Succ 'Zero) es
-> SomeInstr repr inp vs ('Succ vs) a
-> Instr Routinable repr inp vs ('Succ vs) a
Subroutine LetName v
n SomeInstr repr inp '[] ('Succ 'Zero) v
sub
  jump :: forall a inp (es :: Peano).
LetName a -> SomeInstr repr inp '[] ('Succ es) a
jump = Instr Routinable repr inp '[] ('Succ es) a
-> SomeInstr repr inp '[] ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Routinable repr inp '[] ('Succ es) a
 -> SomeInstr repr inp '[] ('Succ es) a)
-> (LetName a -> Instr Routinable repr inp '[] ('Succ es) a)
-> LetName a
-> SomeInstr repr inp '[] ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetName a -> Instr Routinable repr inp '[] ('Succ es) a
forall a (repr :: ReprInstr) inp (es :: Peano).
LetName a -> Instr Routinable repr inp '[] ('Succ es) a
Jump
  call :: forall v inp (vs :: [*]) (es :: Peano) a.
LetName v
-> SomeInstr repr inp (v : vs) ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
call LetName v
n = Instr Routinable repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Routinable repr inp vs ('Succ es) a
 -> SomeInstr repr inp vs ('Succ es) a)
-> (SomeInstr repr inp (v : vs) ('Succ es) a
    -> Instr Routinable repr inp vs ('Succ es) a)
-> SomeInstr repr inp (v : vs) ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetName v
-> SomeInstr repr inp (v : vs) ('Succ es) a
-> Instr Routinable repr inp vs ('Succ es) a
forall es (repr :: ReprInstr) inp (vs :: [*]) (vs :: Peano) a.
LetName es
-> SomeInstr repr inp (es : vs) ('Succ vs) a
-> Instr Routinable repr inp vs ('Succ vs) a
Call LetName v
n
  ret :: forall inp a (es :: Peano). SomeInstr repr inp '[a] es a
ret = Instr Routinable repr inp '[a] es a -> SomeInstr repr inp '[a] es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr Instr Routinable repr inp '[a] es a
forall (repr :: ReprInstr) inp a (es :: Peano).
Instr Routinable repr inp '[a] es a
Ret

-- Branchable
data instance Instr Branchable repr inp vs fs a where
  -- | @('Case' l r)@.
  Case ::
    SomeInstr repr inp (x ': vs) es a ->
    SomeInstr repr inp (y ': vs) es a ->
    Instr Branchable repr inp (Either x y ': vs) es a
  -- | @('Choices' ps bs d)@.
  Choices ::
    [TermInstr (v -> Bool)] ->
    [SomeInstr repr inp vs es a] ->
    SomeInstr repr inp vs es a ->
    Instr Branchable repr inp (v ': vs) es a
instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Branchable repr inp vs es a -> repr inp vs es a
trans = \case
    Case SomeInstr repr inp (x : vs) es a
l SomeInstr repr 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 :: ReprInstr) inp x (vs :: [*]) (es :: Peano) r y.
Branchable repr =>
repr inp (x : vs) es r
-> repr inp (y : vs) es r -> repr inp (Either x y : vs) es r
caseI (SomeInstr repr inp (x : vs) es a -> repr inp (x : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (x : vs) es a
l) (SomeInstr repr inp (y : vs) es a -> repr inp (y : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (y : vs) es a
r)
    Choices [TermInstr (v -> Bool)]
ps [SomeInstr repr inp vs es a]
bs SomeInstr repr inp vs es a
d -> [TermInstr (v -> Bool)]
-> [repr inp vs es a] -> repr inp vs es a -> repr inp (v : vs) es a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Branchable repr =>
[TermInstr (v -> Bool)]
-> [repr inp vs es a] -> repr inp vs es a -> repr inp (v : vs) es a
choices [TermInstr (v -> Bool)]
ps (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (SomeInstr repr inp vs es a -> repr inp vs es a)
-> [SomeInstr repr inp vs es a] -> [repr inp vs es a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
Functor.<$> [SomeInstr repr inp vs es a]
bs) (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs es a
d)
instance Branchable repr => Branchable (SomeInstr repr) where
  caseI :: forall inp x (vs :: [*]) (es :: Peano) r y.
SomeInstr repr inp (x : vs) es r
-> SomeInstr repr inp (y : vs) es r
-> SomeInstr repr inp (Either x y : vs) es r
caseI SomeInstr repr inp (x : vs) es r
l = Instr Branchable repr inp (Either x y : vs) es r
-> SomeInstr repr inp (Either x y : vs) es r
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Branchable repr inp (Either x y : vs) es r
 -> SomeInstr repr inp (Either x y : vs) es r)
-> (SomeInstr repr inp (y : vs) es r
    -> Instr Branchable repr inp (Either x y : vs) es r)
-> SomeInstr repr inp (y : vs) es r
-> SomeInstr repr inp (Either x y : vs) es r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp (x : vs) es r
-> SomeInstr repr inp (y : vs) es r
-> Instr Branchable repr inp (Either x y : vs) es r
forall (repr :: ReprInstr) inp es (vs :: [*]) (es :: Peano) a y.
SomeInstr repr inp (es : vs) es a
-> SomeInstr repr inp (y : vs) es a
-> Instr Branchable repr inp (Either es y : vs) es a
Case SomeInstr repr inp (x : vs) es r
l
  choices :: forall v inp (vs :: [*]) (es :: Peano) a.
[TermInstr (v -> Bool)]
-> [SomeInstr repr inp vs es a]
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp (v : vs) es a
choices [TermInstr (v -> Bool)]
ps [SomeInstr repr inp vs es a]
bs = Instr Branchable repr inp (v : vs) es a
-> SomeInstr repr inp (v : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Branchable repr inp (v : vs) es a
 -> SomeInstr repr inp (v : vs) es a)
-> (SomeInstr repr inp vs es a
    -> Instr Branchable repr inp (v : vs) es a)
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp (v : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TermInstr (v -> Bool)]
-> [SomeInstr repr inp vs es a]
-> SomeInstr repr inp vs es a
-> Instr Branchable repr inp (v : vs) es a
forall es (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
[TermInstr (es -> Bool)]
-> [SomeInstr repr inp vs es a]
-> SomeInstr repr inp vs es a
-> Instr Branchable repr inp (es : vs) es a
Choices [TermInstr (v -> Bool)]
ps [SomeInstr repr inp vs es a]
bs

-- Failable
data instance Instr Failable repr inp vs fs a where
  -- | @('Fail')@ raises an error from the 'failStack'.
  Fail ::
    [ErrorItem (InputToken inp)] ->
    Instr Failable repr inp vs ('Succ es) a
  -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PopFail ::
    SomeInstr repr inp vs es ret ->
    Instr Failable repr 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 ::
    SomeInstr repr inp vs ('Succ es) ret ->
    SomeInstr repr inp (Cursor inp ': vs) es ret ->
    Instr Failable repr inp vs es ret
instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Failable repr inp vs es a -> repr inp vs es a
trans = \case
    Fail [ErrorItem (InputToken inp)]
err -> [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
Failable repr =>
[ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) a
fail [ErrorItem (InputToken inp)]
err
    PopFail SomeInstr repr inp vs es a
k -> repr inp vs es a -> repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
Failable repr =>
repr inp vs es a -> repr inp vs ('Succ es) a
popFail (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs es a
k)
    CatchFail SomeInstr repr inp vs ('Succ es) a
l SomeInstr repr 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 :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
Failable repr =>
repr inp vs ('Succ es) a
-> repr inp (Cursor inp : vs) es a -> repr inp vs es a
catchFail (SomeInstr repr inp vs ('Succ es) a -> repr inp vs ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs ('Succ es) a
l) (SomeInstr repr 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 SomeInstr repr inp (Cursor inp : vs) es a
r)
instance Failable repr => Failable (SomeInstr repr) where
  fail :: forall inp (vs :: [*]) (es :: Peano) a.
[ErrorItem (InputToken inp)] -> SomeInstr repr inp vs ('Succ es) a
fail = Instr Failable repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Failable repr inp vs ('Succ es) a
 -> SomeInstr repr inp vs ('Succ es) a)
-> ([ErrorItem (InputToken inp)]
    -> Instr Failable repr inp vs ('Succ es) a)
-> [ErrorItem (InputToken inp)]
-> SomeInstr repr inp vs ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ErrorItem (InputToken inp)]
-> Instr Failable repr inp vs ('Succ es) a
forall inp (repr :: ReprInstr) (vs :: [*]) (es :: Peano) a.
[ErrorItem (InputToken inp)]
-> Instr Failable repr inp vs ('Succ es) a
Fail
  popFail :: forall inp (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp vs es a -> SomeInstr repr inp vs ('Succ es) a
popFail = Instr Failable repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Failable repr inp vs ('Succ es) a
 -> SomeInstr repr inp vs ('Succ es) a)
-> (SomeInstr repr inp vs es a
    -> Instr Failable repr inp vs ('Succ es) a)
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp vs ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp vs es a
-> Instr Failable repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) ret.
SomeInstr repr inp vs es ret
-> Instr Failable repr inp vs ('Succ es) ret
PopFail
  catchFail :: forall inp (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp vs ('Succ es) a
-> SomeInstr repr inp (Cursor inp : vs) es a
-> SomeInstr repr inp vs es a
catchFail SomeInstr repr inp vs ('Succ es) a
x = Instr Failable repr inp vs es a -> SomeInstr repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Failable repr inp vs es a -> SomeInstr repr inp vs es a)
-> (SomeInstr repr inp (Cursor inp : vs) es a
    -> Instr Failable repr inp vs es a)
-> SomeInstr repr inp (Cursor inp : vs) es a
-> SomeInstr repr inp vs es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp vs ('Succ es) a
-> SomeInstr repr inp (Cursor inp : vs) es a
-> Instr Failable repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) ret.
SomeInstr repr inp vs ('Succ es) ret
-> SomeInstr repr inp (Cursor inp : vs) es ret
-> Instr Failable repr inp vs es ret
CatchFail SomeInstr repr inp vs ('Succ es) a
x

-- Inputable
data instance Instr Inputable repr inp vs fs a where
  -- | @('LoadInput' k)@ removes the input from the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@ using that input.
  LoadInput ::
    SomeInstr repr inp vs es a ->
    Instr Inputable repr inp (Cursor inp : vs) es a
  -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
  -- and continues with the next 'Instr'uction @(k)@.
  PushInput ::
    SomeInstr repr inp (Cursor inp ': vs) es a ->
    Instr Inputable repr inp vs es a
instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Inputable repr inp vs es a -> repr inp vs es a
trans = \case
    LoadInput SomeInstr repr inp vs es a
k -> repr inp vs es a -> repr inp (Cursor inp : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
Inputable repr =>
repr inp vs es a -> repr inp (Cursor inp : vs) es a
loadInput (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs es a
k)
    PushInput SomeInstr repr inp (Cursor inp : vs) es a
k -> repr inp (Cursor inp : vs) es a -> repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
Inputable repr =>
repr inp (Cursor inp : vs) es a -> repr inp vs es a
pushInput (SomeInstr repr 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 SomeInstr repr inp (Cursor inp : vs) es a
k)
instance Inputable repr => Inputable (SomeInstr repr) where
  loadInput :: forall inp (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp vs es a
-> SomeInstr repr inp (Cursor inp : vs) es a
loadInput = Instr Inputable repr inp (Cursor inp : vs) es a
-> SomeInstr repr inp (Cursor inp : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Inputable repr inp (Cursor inp : vs) es a
 -> SomeInstr repr inp (Cursor inp : vs) es a)
-> (SomeInstr repr inp vs es a
    -> Instr Inputable repr inp (Cursor inp : vs) es a)
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp (Cursor inp : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp vs es a
-> Instr Inputable repr inp (Cursor inp : vs) es a
forall (repr :: ReprInstr) inp (es :: [*]) (es :: Peano) a.
SomeInstr repr inp es es a
-> Instr Inputable repr inp (Cursor inp : es) es a
LoadInput
  pushInput :: forall inp (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp (Cursor inp : vs) es a
-> SomeInstr repr inp vs es a
pushInput = Instr Inputable repr inp vs es a -> SomeInstr repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Inputable repr inp vs es a -> SomeInstr repr inp vs es a)
-> (SomeInstr repr inp (Cursor inp : vs) es a
    -> Instr Inputable repr inp vs es a)
-> SomeInstr repr inp (Cursor inp : vs) es a
-> SomeInstr repr inp vs es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeInstr repr inp (Cursor inp : vs) es a
-> Instr Inputable repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
SomeInstr repr inp (Cursor inp : vs) es a
-> Instr Inputable repr inp vs es a
PushInput

-- Joinable
data instance Instr Joinable repr inp vs fs a where
  DefJoin ::
    LetName v ->
    SomeInstr repr inp (v ': vs) es a ->
    SomeInstr repr inp vs es a ->
    Instr Joinable repr inp vs es a
  RefJoin ::
    LetName v ->
    Instr Joinable repr inp (v ': vs) es a
instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr Joinable repr inp vs es a -> repr inp vs es a
trans = \case
    DefJoin LetName v
n SomeInstr repr inp (v : vs) es a
sub SomeInstr repr 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 :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Joinable repr =>
LetName v
-> repr inp (v : vs) es a -> repr inp vs es a -> repr inp vs es a
defJoin LetName v
n (SomeInstr repr inp (v : vs) es a -> repr inp (v : vs) es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (v : vs) es a
sub) (SomeInstr repr inp vs es a -> repr inp vs es a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp vs es a
k)
    RefJoin LetName v
n -> LetName v -> repr inp (v : vs) es a
forall (repr :: ReprInstr) v inp (vs :: [*]) (es :: Peano) a.
Joinable repr =>
LetName v -> repr inp (v : vs) es a
refJoin LetName v
n
instance Joinable repr => Joinable (SomeInstr repr) where
  defJoin :: forall v inp (vs :: [*]) (es :: Peano) a.
LetName v
-> SomeInstr repr inp (v : vs) es a
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp vs es a
defJoin LetName v
n SomeInstr repr inp (v : vs) es a
sub = Instr Joinable repr inp vs es a -> SomeInstr repr inp vs es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Joinable repr inp vs es a -> SomeInstr repr inp vs es a)
-> (SomeInstr repr inp vs es a -> Instr Joinable repr inp vs es a)
-> SomeInstr repr inp vs es a
-> SomeInstr repr inp vs es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetName v
-> SomeInstr repr inp (v : vs) es a
-> SomeInstr repr inp vs es a
-> Instr Joinable repr inp vs es a
forall es (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
LetName es
-> SomeInstr repr inp (es : vs) es a
-> SomeInstr repr inp vs es a
-> Instr Joinable repr inp vs es a
DefJoin LetName v
n SomeInstr repr inp (v : vs) es a
sub
  refJoin :: forall v inp (vs :: [*]) (es :: Peano) a.
LetName v -> SomeInstr repr inp (v : vs) es a
refJoin = Instr Joinable repr inp (v : vs) es a
-> SomeInstr repr inp (v : vs) es a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr Joinable repr inp (v : vs) es a
 -> SomeInstr repr inp (v : vs) es a)
-> (LetName v -> Instr Joinable repr inp (v : vs) es a)
-> LetName v
-> SomeInstr repr inp (v : vs) es a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetName v -> Instr Joinable repr inp (v : vs) es a
forall es (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
LetName es -> Instr Joinable repr inp (es : vs) es a
RefJoin

-- Readable
data instance Instr (Readable tok) repr inp vs fs a where
  -- | @('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) ->
    SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
    Instr (Readable tok) repr inp vs ('Succ es) a
instance
  ( Readable tok repr, tok ~ InputToken inp ) =>
  Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
  trans :: forall a. Instr (Readable tok) repr inp vs es a -> repr inp vs es a
trans = \case
    Read [ErrorItem (InputToken inp)]
es TermInstr (InputToken inp -> Bool)
p SomeInstr repr inp (InputToken inp : vs) ('Succ es) a
k -> [ErrorItem tok]
-> TermInstr (tok -> Bool)
-> repr inp (tok : vs) ('Succ es) a
-> repr inp vs ('Succ es) a
forall tok (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a.
(Readable tok repr, tok ~ InputToken inp) =>
[ErrorItem tok]
-> TermInstr (tok -> Bool)
-> repr inp (tok : vs) ('Succ es) a
-> repr inp vs ('Succ es) a
read [ErrorItem tok]
[ErrorItem (InputToken inp)]
es TermInstr (tok -> Bool)
TermInstr (InputToken inp -> Bool)
p (SomeInstr repr inp (tok : vs) ('Succ es) a
-> repr inp (tok : vs) ('Succ es) a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans SomeInstr repr inp (tok : vs) ('Succ es) a
SomeInstr repr inp (InputToken inp : vs) ('Succ es) a
k)
instance
  ( Readable tok repr, Typeable tok ) =>
  Readable tok (SomeInstr repr) where
  read :: forall inp (vs :: [*]) (es :: Peano) a.
(tok ~ InputToken inp) =>
[ErrorItem tok]
-> TermInstr (tok -> Bool)
-> SomeInstr repr inp (tok : vs) ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
read [ErrorItem tok]
es TermInstr (tok -> Bool)
p = Instr (Readable tok) repr inp vs ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall (repr :: ReprInstr) inp (vs :: [*]) (es :: Peano) a
       (instr :: ReprInstr -> Constraint).
(Trans (Instr instr repr inp vs es) (repr inp vs es),
 Typeable instr) =>
Instr instr repr inp vs es a -> SomeInstr repr inp vs es a
SomeInstr (Instr (Readable tok) repr inp vs ('Succ es) a
 -> SomeInstr repr inp vs ('Succ es) a)
-> (SomeInstr repr inp (tok : vs) ('Succ es) a
    -> Instr (Readable tok) repr inp vs ('Succ es) a)
-> SomeInstr repr inp (tok : vs) ('Succ es) a
-> SomeInstr repr inp vs ('Succ es) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ErrorItem (InputToken inp)]
-> TermInstr (InputToken inp -> Bool)
-> SomeInstr repr inp (InputToken inp : vs) ('Succ es) a
-> Instr (Readable tok) repr inp vs ('Succ es) a
forall inp (repr :: ReprInstr) (vs :: [*]) (es :: Peano) a tok.
[ErrorItem (InputToken inp)]
-> TermInstr (InputToken inp -> Bool)
-> SomeInstr repr inp (InputToken inp : vs) ('Succ es) a
-> Instr (Readable tok) repr inp vs ('Succ es) a
Read [ErrorItem tok]
[ErrorItem (InputToken inp)]
es TermInstr (tok -> Bool)
TermInstr (InputToken inp -> Bool)
p