{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Then.VoidRight where

import Symparsec.Parser.Common
import Singleraeh.Either ( SEither(..) )
import Singleraeh.Tuple ( STuple2(..) )
import DeFun.Core

type SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
    SParser
        (SEither ssl (STuple2 srl ssr))
        srl
        (ThenVR' plCh plEnd s0l prCh prEnd s0r)

sThenVR
    :: SParser  ssl srl ('PParser plCh plEnd s0l)
    -> SParser  ssr srr ('PParser prCh prEnd s0r)
    -> SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVR :: forall {l} {r} {b} {rr} (ssl :: l -> Type) (srl :: r -> Type)
       (plCh :: ParserChSym l r) (plEnd :: ParserEndSym l r) (s0l :: l)
       (ssr :: b -> Type) (srr :: rr -> Type) (prCh :: ParserChSym b rr)
       (prEnd :: ParserEndSym b rr) (s0r :: b).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVR (SParser SParserChSym ssl srl pCh
plCh SParserEndSym ssl srl pEnd
plEnd ssl s0
s0l) (SParser SParserChSym ssr srr pCh
prCh SParserEndSym ssr srr pEnd
prEnd ssr s0
s0r) =
    SParserChSym
  (SEither ssl (STuple2 srl ssr)) srl (ThenVRChSym plCh prCh s0r)
-> SParserEndSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVREndSym plEnd prEnd s0r)
-> SEither ssl (STuple2 srl ssr) ('Left s0l)
-> SParser
     (SEither ssl (STuple2 srl ssr))
     srl
     ('PParser
        (ThenVRChSym plCh prCh s0r)
        (ThenVREndSym plEnd prEnd s0r)
        ('Left s0l))
forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pCh :: ParserChSym s r) (pEnd :: ParserEndSym s r) (s0 :: s).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> ss s0
-> SParser ss sr ('PParser pCh pEnd s0)
SParser (SParserChSym ssl srl plCh
-> SParserChSym ssr srr prCh
-> ssr s0r
-> SParserChSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVRChSym plCh prCh s0r)
forall {sl} {rl} {sr} {rr} (ssl :: sl -> Type) (srl :: rl -> Type)
       (plCh :: Char ~> (sl ~> PResult sl rl)) (ssr :: sr -> Type)
       (srr :: rr -> Type) (prCh :: Char ~> (sr ~> PResult sr rr))
       (sr :: sr).
SParserChSym ssl srl plCh
-> SParserChSym ssr srr prCh
-> ssr sr
-> SParserChSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVRChSym plCh prCh sr)
sThenVRChSym SParserChSym ssl srl plCh
SParserChSym ssl srl pCh
plCh SParserChSym ssr srr prCh
SParserChSym ssr srr pCh
prCh ssr s0r
ssr s0
s0r) (SParserEndSym ssl srl plEnd
-> SParserEndSym ssr srr prEnd
-> ssr s0r
-> SParserEndSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVREndSym plEnd prEnd s0r)
forall {sl} {rl} {sr} {rr} (ssl :: sl -> Type) (srl :: rl -> Type)
       (plEnd :: sl ~> Either PE rl) (ssr :: sr -> Type)
       (srr :: rr -> Type) (prEnd :: sr ~> Either PE rr) (s0r :: sr).
SParserEndSym ssl srl plEnd
-> SParserEndSym ssr srr prEnd
-> ssr s0r
-> SParserEndSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVREndSym plEnd prEnd s0r)
sThenVREndSym SParserEndSym ssl srl plEnd
SParserEndSym ssl srl pEnd
plEnd SParserEndSym ssr srr prEnd
SParserEndSym ssr srr pEnd
prEnd ssr s0r
ssr s0
s0r) (ssl s0l -> SEither ssl (STuple2 srl ssr) ('Left s0l)
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft ssl s0l
ssl s0
s0l)

instance
  -- Shame I can't use pl, pr in associated type synonyms! :(
  ( pl ~ 'PParser plCh plEnd s0l
  , pr ~ 'PParser prCh prEnd s0r
  , SingParser pl
  , SingParser pr
  ) => SingParser (ThenVR' plCh plEnd s0l prCh prEnd s0r) where
    type PS (ThenVR' plCh plEnd s0l prCh prEnd s0r) =
        SEither
            (PS ('PParser plCh plEnd s0l))
            (STuple2
                (PR ('PParser plCh plEnd s0l))
                (PS ('PParser prCh prEnd s0r)))
    type PR (ThenVR' plCh plEnd s0l prCh prEnd s0r) =
        PR ('PParser plCh plEnd s0l)
    singParser' :: SParser
  (PS (ThenVR' plCh plEnd s0l prCh prEnd s0r))
  (PR (ThenVR' plCh plEnd s0l prCh prEnd s0r))
  (ThenVR' plCh plEnd s0l prCh prEnd s0r)
singParser' = SParser
  (PS ('PParser plCh plEnd s0l))
  (PR ('PParser plCh plEnd s0l))
  ('PParser plCh plEnd s0l)
-> SParser
     (PS ('PParser prCh prEnd s0r))
     (PR ('PParser prCh prEnd s0r))
     ('PParser prCh prEnd s0r)
-> SPThenVR
     (PS ('PParser plCh plEnd s0l))
     (PR ('PParser plCh plEnd s0l))
     (PS ('PParser prCh prEnd s0r))
     (PR ('PParser prCh prEnd s0r))
     plCh
     plEnd
     s0l
     prCh
     prEnd
     s0r
forall {l} {r} {b} {rr} (ssl :: l -> Type) (srl :: r -> Type)
       (plCh :: ParserChSym l r) (plEnd :: ParserEndSym l r) (s0l :: l)
       (ssr :: b -> Type) (srr :: rr -> Type) (prCh :: ParserChSym b rr)
       (prEnd :: ParserEndSym b rr) (s0r :: b).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVR (forall {s} {r} (p :: PParser s r).
SingParser p =>
SParser (PS p) (PR p) p
forall (p :: PParser sl r). SingParser p => SParser (PS p) (PR p) p
singParser @pl) (forall {s} {r} (p :: PParser s r).
SingParser p =>
SParser (PS p) (PR p) p
forall (p :: PParser sr rr).
SingParser p =>
SParser (PS p) (PR p) p
singParser @pr)

-- | Sequence two parsers, running left then right, and discard the return value
--   of the right parser.
infixl 4 :<*:
type (:<*:)
    :: PParser sl rl
    -> PParser sr rr
    -> PParser (Either sl (rl, sr)) rl
type family pl :<*: pr where
    'PParser plCh plEnd s0l :<*: 'PParser prCh prEnd s0r =
        ThenVR' plCh plEnd s0l prCh prEnd s0r

type ThenVR'
    :: ParserChSym  sl rl
    -> ParserEndSym sl rl
    -> sl
    -> ParserChSym  sr rr
    -> ParserEndSym sr rr
    -> sr
    -> PParser (Either sl (rl, sr)) rl
type ThenVR' plCh plEnd s0l prCh prEnd s0r =
    'PParser (ThenVRChSym plCh prCh s0r) (ThenVREndSym plEnd prEnd s0r) (Left s0l)

type ThenVRCh
    :: ParserChSym sl rl
    -> ParserChSym sr rr
    -> sr
    -> PParserCh (Either sl (rl, sr)) rl
type family ThenVRCh plCh prCh s0r ch s where
    ThenVRCh plCh prCh s0r ch (Left  sl) =
        ThenVRChL prCh s0r ch (plCh @@ ch @@ sl)
    ThenVRCh plCh prCh s0r ch (Right '(rl, sr)) =
        ThenVRChR rl (prCh @@ ch @@ sr)

type family ThenVRChL prCh s0r ch resl where
    ThenVRChL prCh s0r ch (Cont sl) = Cont (Left  sl)
    ThenVRChL prCh s0r ch (Done rl) =
        -- 'Done' doesn't consume, so re-parse with the R parser.
        ThenVRChR rl (prCh @@ ch @@ s0r)
    ThenVRChL prCh s0r ch (Err  el) = Err  (EThenVRChL el)

type EThenVRChL el = EIn "ThenVR(L)" el
eThenVRChL :: SE el -> SE (EThenVRChL el)
eThenVRChL :: forall (el :: PE). SE el -> SE (EThenVRChL el)
eThenVRChL SE el
el = SE el -> (SingE el => SE (EThenVRChL el)) -> SE (EThenVRChL el)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE el
el ((SingE el => SE (EThenVRChL el)) -> SE (EThenVRChL el))
-> (SingE el => SE (EThenVRChL el)) -> SE (EThenVRChL el)
forall a b. (a -> b) -> a -> b
$ SE (EThenVRChL el)
SingE el => SE (EThenVRChL el)
forall (e :: PE). SingE e => SE e
singE

type family ThenVRChR rl resr where
    ThenVRChR rl (Cont sr) = Cont (Right '(rl, sr))
    ThenVRChR rl (Done rr) = Done rl
    ThenVRChR rl (Err  er) = Err  (EThenVRChR er)

type EThenVRChR er = EIn "ThenVR(R)" er
eThenVRChR :: SE er -> SE (EThenVRChR er)
eThenVRChR :: forall (er :: PE). SE er -> SE (EThenVRChR er)
eThenVRChR SE er
er = SE er -> (SingE er => SE (EThenVRChR er)) -> SE (EThenVRChR er)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE er
er ((SingE er => SE (EThenVRChR er)) -> SE (EThenVRChR er))
-> (SingE er => SE (EThenVRChR er)) -> SE (EThenVRChR er)
forall a b. (a -> b) -> a -> b
$ SE (EThenVRChR er)
SingE er => SE (EThenVRChR er)
forall (e :: PE). SingE e => SE e
singE

sThenVRChR
    :: srl rl
    -> SResult ssr srr resr
    -> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)
sThenVRChR :: forall {r} {k} {r} {l} (srl :: r -> Type) (rl :: r)
       (ssr :: k -> Type) (srr :: r -> Type) (resr :: PResult k r)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)
sThenVRChR srl rl
rl = \case
  SCont  ssr s1
sr -> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Right '(rl, s1)))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
 -> SResult
      (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Right '(rl, s1))))
-> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Right '(rl, s1)))
forall a b. (a -> b) -> a -> b
$ STuple2 srl ssr '(rl, s1)
-> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (STuple2 srl ssr '(rl, s1)
 -> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1)))
-> STuple2 srl ssr '(rl, s1)
-> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
forall a b. (a -> b) -> a -> b
$ srl rl -> ssr s1 -> STuple2 srl ssr '(rl, s1)
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 srl rl
rl ssr s1
sr
  SDone srr r1
_rr -> srl rl -> SResult (SEither ssl (STuple2 srl ssr)) srl ('Done rl)
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone srl rl
rl
  SErr   SE e
er -> SE (EThenVRChR e)
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChR e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenVRChR e)
 -> SResult
      (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChR e)))
-> SE (EThenVRChR e)
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChR e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenVRChR e)
forall (er :: PE). SE er -> SE (EThenVRChR er)
eThenVRChR SE e
er

sThenVRChSym
    :: SParserChSym ssl srl plCh
    -> SParserChSym ssr srr prCh
    -> ssr sr
    -> SParserChSym (SEither ssl (STuple2 srl ssr)) srl
        (ThenVRChSym plCh prCh sr)
sThenVRChSym :: forall {sl} {rl} {sr} {rr} (ssl :: sl -> Type) (srl :: rl -> Type)
       (plCh :: Char ~> (sl ~> PResult sl rl)) (ssr :: sr -> Type)
       (srr :: rr -> Type) (prCh :: Char ~> (sr ~> PResult sr rr))
       (sr :: sr).
SParserChSym ssl srl plCh
-> SParserChSym ssr srr prCh
-> ssr sr
-> SParserChSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVRChSym plCh prCh sr)
sThenVRChSym SParserChSym ssl srl plCh
plCh SParserChSym ssr srr prCh
prCh ssr sr
s0r = LamRep2
  SChar
  (SEither ssl (STuple2 srl ssr))
  (SResult (SEither ssl (STuple2 srl ssr)) srl)
  (ThenVRChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) srl)
     (ThenVRChSym plCh prCh sr)
forall {a1} {a2} {b1} (a3 :: a1 -> Type) (b2 :: a2 -> Type)
       (c :: b1 -> Type) (fun :: a1 ~> (a2 ~> b1)).
LamRep2 a3 b2 c fun -> Lam2 a3 b2 c fun
Lam2 (LamRep2
   SChar
   (SEither ssl (STuple2 srl ssr))
   (SResult (SEither ssl (STuple2 srl ssr)) srl)
   (ThenVRChSym plCh prCh sr)
 -> Lam2
      SChar
      (SEither ssl (STuple2 srl ssr))
      (SResult (SEither ssl (STuple2 srl ssr)) srl)
      (ThenVRChSym plCh prCh sr))
-> LamRep2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) srl)
     (ThenVRChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) srl)
     (ThenVRChSym plCh prCh sr)
forall a b. (a -> b) -> a -> b
$ \SChar x
ch -> \case
  SLeft ssl l1
sl ->
    case SParserChSym ssl srl plCh
plCh SParserChSym ssl srl plCh
-> SChar x -> Lam ssl (SResult ssl srl) (App plCh x)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar x
ch Lam ssl (SResult ssl srl) (App plCh x)
-> ssl l1 -> SResult ssl srl (App plCh x @@ l1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssl l1
sl of
      SCont ssl s1
sl' -> SEither ssl (STuple2 srl ssr) ('Left s1)
-> SResult (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Left s1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SEither ssl (STuple2 srl ssr) ('Left s1)
 -> SResult (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Left s1)))
-> SEither ssl (STuple2 srl ssr) ('Left s1)
-> SResult (SEither ssl (STuple2 srl ssr)) srl ('Cont ('Left s1))
forall a b. (a -> b) -> a -> b
$ ssl s1 -> SEither ssl (STuple2 srl ssr) ('Left s1)
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft ssl s1
sl'
      SDone srl r1
rl  -> srl r1
-> SResult ssr srr (App (App prCh x) sr)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     srl
     (ThenVRChR r1 (App (App prCh x) sr))
forall {r} {k} {r} {l} (srl :: r -> Type) (rl :: r)
       (ssr :: k -> Type) (srr :: r -> Type) (resr :: PResult k r)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)
sThenVRChR srl r1
rl (SParserChSym ssr srr prCh
prCh SParserChSym ssr srr prCh
-> SChar x -> Lam ssr (SResult ssr srr) (App prCh x)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar x
ch Lam ssr (SResult ssr srr) (App prCh x)
-> ssr sr -> SResult ssr srr (App (App prCh x) sr)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr sr
s0r)
      SErr  SE e
el  -> SE (EThenVRChL e)
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChL e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenVRChL e)
 -> SResult
      (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChL e)))
-> SE (EThenVRChL e)
-> SResult
     (SEither ssl (STuple2 srl ssr)) srl ('Err (EThenVRChL e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenVRChL e)
forall (el :: PE). SE el -> SE (EThenVRChL el)
eThenVRChL SE e
el
  SRight (STuple2 srl a1
rl ssr b1
sr) -> srl a1
-> SResult ssr srr (App (App prCh x) b1)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     srl
     (ThenVRChR a1 (App (App prCh x) b1))
forall {r} {k} {r} {l} (srl :: r -> Type) (rl :: r)
       (ssr :: k -> Type) (srr :: r -> Type) (resr :: PResult k r)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)
sThenVRChR srl a1
rl (SParserChSym ssr srr prCh
prCh SParserChSym ssr srr prCh
-> SChar x -> Lam ssr (SResult ssr srr) (App prCh x)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar x
ch Lam ssr (SResult ssr srr) (App prCh x)
-> ssr b1 -> SResult ssr srr (App (App prCh x) b1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr b1
sr)

type ThenVRChSym
    :: ParserChSym sl rl
    -> ParserChSym sr rr
    -> sr
    -> ParserChSym (Either sl (rl, sr)) rl
data ThenVRChSym plCh prCh s0r f
type instance App (ThenVRChSym plCh prCh s0r) f = ThenVRChSym1 plCh prCh s0r f

type ThenVRChSym1
    :: ParserChSym sl rl
    -> ParserChSym sr rr
    -> sr
    -> ParserChSym1 (Either sl (rl, sr)) rl
data ThenVRChSym1 plCh prCh s0r ch s
type instance App (ThenVRChSym1 plCh prCh s0r ch) s = ThenVRCh plCh prCh s0r ch s

type family ThenVREnd plEnd prEnd s0r s where
    -- | EOT during R: call R end
    ThenVREnd plEnd prEnd s0r (Right '(rl, sr)) = ThenVREndR rl    (prEnd @@ sr)
    -- | EOT during L: call L end, pass R end
    ThenVREnd plEnd prEnd s0r (Left sl)         = ThenVREndL prEnd s0r (plEnd @@ sl)

type family ThenVREndR rl res where
    -- | EOT during R, R end succeeds: success
    ThenVREndR rl (Right rr) = Right rl
    -- | EOT during R, R end fails: error
    ThenVREndR rl (Left  er) = Left  (EThenVREndR er)

type EThenVREndR er = EIn "ThenVR(R) end" er
eThenVREndR :: SE er -> SE (EThenVREndR er)
eThenVREndR :: forall (er :: PE). SE er -> SE (EThenVREndR er)
eThenVREndR SE er
er = SE er -> (SingE er => SE (EThenVREndR er)) -> SE (EThenVREndR er)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE er
er ((SingE er => SE (EThenVREndR er)) -> SE (EThenVREndR er))
-> (SingE er => SE (EThenVREndR er)) -> SE (EThenVREndR er)
forall a b. (a -> b) -> a -> b
$ SE (EThenVREndR er)
SingE er => SE (EThenVREndR er)
forall (e :: PE). SingE e => SE e
singE

sThenVREndR
    :: srl rl
    -> SResultEnd srr res
    -> SResultEnd srl (ThenVREndR rl res)
sThenVREndR :: forall {b} {b} (srl :: b -> Type) (rl :: b) (srr :: b -> Type)
       (res :: Either PE b).
srl rl -> SResultEnd srr res -> SResultEnd srl (ThenVREndR rl res)
sThenVREndR srl rl
rl = \case
  SRight srr r1
_rr -> srl rl -> SEither SE srl ('Right rl)
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight srl rl
rl
  SLeft   SE l1
er -> SE (EThenVREndR l1) -> SEither SE srl ('Left (EThenVREndR l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft  (SE (EThenVREndR l1) -> SEither SE srl ('Left (EThenVREndR l1)))
-> SE (EThenVREndR l1) -> SEither SE srl ('Left (EThenVREndR l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenVREndR l1)
forall (er :: PE). SE er -> SE (EThenVREndR er)
eThenVREndR SE l1
er

type family ThenVREndL prEnd s0r res where
    -- | EOT during L, L end succeeds: call R end on initial R state
    ThenVREndL prEnd s0r (Right rl) = ThenVREndR rl (prEnd @@ s0r)
    -- | EOT during L, L end fails: error
    ThenVREndL prEnd s0r (Left  el) = Left (EThenVREndL el)

type EThenVREndL er = EIn "ThenVR(L) end" er
eThenVREndL :: SE er -> SE (EThenVREndL er)
eThenVREndL :: forall (er :: PE). SE er -> SE (EThenVREndL er)
eThenVREndL SE er
er = SE er -> (SingE er => SE (EThenVREndL er)) -> SE (EThenVREndL er)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE er
er ((SingE er => SE (EThenVREndL er)) -> SE (EThenVREndL er))
-> (SingE er => SE (EThenVREndL er)) -> SE (EThenVREndL er)
forall a b. (a -> b) -> a -> b
$ SE (EThenVREndL er)
SingE er => SE (EThenVREndL er)
forall (e :: PE). SingE e => SE e
singE

sThenVREndSym
    :: SParserEndSym ssl srl plEnd
    -> SParserEndSym ssr srr prEnd
    -> ssr s0r
    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) srl
        (ThenVREndSym plEnd prEnd s0r)
sThenVREndSym :: forall {sl} {rl} {sr} {rr} (ssl :: sl -> Type) (srl :: rl -> Type)
       (plEnd :: sl ~> Either PE rl) (ssr :: sr -> Type)
       (srr :: rr -> Type) (prEnd :: sr ~> Either PE rr) (s0r :: sr).
SParserEndSym ssl srl plEnd
-> SParserEndSym ssr srr prEnd
-> ssr s0r
-> SParserEndSym
     (SEither ssl (STuple2 srl ssr)) srl (ThenVREndSym plEnd prEnd s0r)
sThenVREndSym SParserEndSym ssl srl plEnd
plEnd SParserEndSym ssr srr prEnd
prEnd ssr s0r
s0r = LamRep
  (SEither ssl (STuple2 srl ssr))
  (SResultEnd srl)
  (ThenVREndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd srl)
     (ThenVREndSym plEnd prEnd s0r)
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep
   (SEither ssl (STuple2 srl ssr))
   (SResultEnd srl)
   (ThenVREndSym plEnd prEnd s0r)
 -> Lam
      (SEither ssl (STuple2 srl ssr))
      (SResultEnd srl)
      (ThenVREndSym plEnd prEnd s0r))
-> LamRep
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd srl)
     (ThenVREndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd srl)
     (ThenVREndSym plEnd prEnd s0r)
forall a b. (a -> b) -> a -> b
$ \case
  SRight (STuple2 srl a1
rl ssr b1
sr) -> srl a1
-> SResultEnd srr (App prEnd b1)
-> SResultEnd srl (ThenVREndR a1 (App prEnd b1))
forall {b} {b} (srl :: b -> Type) (rl :: b) (srr :: b -> Type)
       (res :: Either PE b).
srl rl -> SResultEnd srr res -> SResultEnd srl (ThenVREndR rl res)
sThenVREndR srl a1
rl (SParserEndSym ssr srr prEnd
prEnd SParserEndSym ssr srr prEnd
-> ssr b1 -> SResultEnd srr (App prEnd b1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr b1
sr)
  SLeft  ssl l1
sl ->
    case SParserEndSym ssl srl plEnd
plEnd SParserEndSym ssl srl plEnd
-> ssl l1 -> SResultEnd srl (plEnd @@ l1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssl l1
sl of
      SRight srl r1
rl -> srl r1
-> SResultEnd srr (App prEnd s0r)
-> SResultEnd srl (ThenVREndR r1 (App prEnd s0r))
forall {b} {b} (srl :: b -> Type) (rl :: b) (srr :: b -> Type)
       (res :: Either PE b).
srl rl -> SResultEnd srr res -> SResultEnd srl (ThenVREndR rl res)
sThenVREndR srl r1
rl (SParserEndSym ssr srr prEnd
prEnd SParserEndSym ssr srr prEnd
-> ssr s0r -> SResultEnd srr (App prEnd s0r)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr s0r
s0r)
      SLeft  SE l1
el -> SE (EThenVREndL l1) -> SEither SE srl ('Left (EThenVREndL l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE (EThenVREndL l1) -> SEither SE srl ('Left (EThenVREndL l1)))
-> SE (EThenVREndL l1) -> SEither SE srl ('Left (EThenVREndL l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenVREndL l1)
forall (er :: PE). SE er -> SE (EThenVREndL er)
eThenVREndL SE l1
el

type ThenVREndSym
    :: ParserEndSym sl rl
    -> ParserEndSym sr rr
    -> sr
    -> ParserEndSym (Either sl (rl, sr)) rl
data ThenVREndSym plEnd prEnd s0r s
type instance App (ThenVREndSym plEnd prEnd s0r) s = ThenVREnd plEnd prEnd s0r s