{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Then.VoidLeft where

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

type SPThenVL ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =
    SParser
        (SEither ssl ssr)
        srr
        (ThenVL' plCh plEnd s0l prCh prEnd s0r)

sThenVL
    :: SParser   ssl srl ('PParser plCh plEnd s0l)
    -> SParser   ssr srr ('PParser prCh prEnd s0r)
    -> SPThenVL  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVL :: forall {l} {rl} {r} {r} (ssl :: l -> Type) (srl :: rl -> Type)
       (plCh :: ParserChSym l rl) (plEnd :: ParserEndSym l rl) (s0l :: l)
       (ssr :: r -> Type) (srr :: r -> Type) (prCh :: ParserChSym r r)
       (prEnd :: ParserEndSym r r) (s0r :: r).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThenVL ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVL (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 ssr) srr (ThenVLChSym plCh prCh s0r)
-> SParserEndSym
     (SEither ssl ssr) srr (ThenVLEndSym plEnd prEnd s0r)
-> SEither ssl ssr ('Left s0l)
-> SParser
     (SEither ssl ssr)
     srr
     ('PParser
        (ThenVLChSym plCh prCh s0r)
        (ThenVLEndSym 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 ssr) srr (ThenVLChSym 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 ssr) srr (ThenVLChSym plCh prCh sr)
sThenVLChSym 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 ssr) srr (ThenVLEndSym 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 ssr) srr (ThenVLEndSym plEnd prEnd s0r)
sThenVLEndSym 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 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
  ( pl ~ 'PParser plCh plEnd s0l
  , pr ~ 'PParser prCh prEnd s0r
  , SingParser pl
  , SingParser pr
  ) => SingParser (ThenVL' plCh plEnd s0l prCh prEnd s0r) where
    type PS (ThenVL' plCh plEnd s0l prCh prEnd s0r) =
        SEither
            (PS ('PParser plCh plEnd s0l))
            (PS ('PParser prCh prEnd s0r))
    type PR (ThenVL' plCh plEnd s0l prCh prEnd s0r) =
        PR ('PParser prCh prEnd s0r)
    singParser' :: SParser
  (PS (ThenVL' plCh plEnd s0l prCh prEnd s0r))
  (PR (ThenVL' plCh plEnd s0l prCh prEnd s0r))
  (ThenVL' 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)
-> SPThenVL
     (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} {rl} {r} {r} (ssl :: l -> Type) (srl :: rl -> Type)
       (plCh :: ParserChSym l rl) (plEnd :: ParserEndSym l rl) (s0l :: l)
       (ssr :: r -> Type) (srr :: r -> Type) (prCh :: ParserChSym r r)
       (prEnd :: ParserEndSym r r) (s0r :: r).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThenVL ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThenVL (forall {s} {r} (p :: PParser s r).
SingParser p =>
SParser (PS p) (PR p) p
forall (p :: PParser sl rl).
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 r). SingParser p => SParser (PS p) (PR p) p
singParser @pr)

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

type ThenVL'
    :: ParserChSym  sl rl
    -> ParserEndSym sl rl
    -> sl
    -> ParserChSym  sr rr
    -> ParserEndSym sr rr
    -> sr
    -> PParser (Either sl sr) rr
type ThenVL' plCh plEnd s0l prCh prEnd s0r =
    'PParser (ThenVLChSym plCh prCh s0r) (ThenVLEndSym plEnd prEnd s0r) (Left s0l)

type ThenVLCh
    :: ParserChSym sl rl
    -> ParserChSym sr rr
    -> sr
    -> PParserCh (Either sl sr) rr
type family ThenVLCh plCh prCh s0r ch s where
    ThenVLCh plCh prCh s0r ch (Left  sl) =
        ThenVLChL prCh s0r ch (plCh @@ ch @@ sl)
    ThenVLCh plCh prCh s0r ch (Right sr) =
        ThenVLChR (prCh @@ ch @@ sr)

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

type EThenVLChL el = EIn "ThenVL(L)" el
eThenVLChL :: SE el -> SE (EThenVLChL el)
eThenVLChL :: forall (el :: PE). SE el -> SE (EThenVLChL el)
eThenVLChL SE el
el = SE el -> (SingE el => SE (EThenVLChL el)) -> SE (EThenVLChL el)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE el
el ((SingE el => SE (EThenVLChL el)) -> SE (EThenVLChL el))
-> (SingE el => SE (EThenVLChL el)) -> SE (EThenVLChL el)
forall a b. (a -> b) -> a -> b
$ SE (EThenVLChL el)
SingE el => SE (EThenVLChL el)
forall (e :: PE). SingE e => SE e
singE

type family ThenVLChR resr where
    ThenVLChR (Cont sr) = Cont (Right sr)
    ThenVLChR (Done rr) = Done rr
    ThenVLChR (Err  er) = Err  (EThenVLChR er)

type EThenVLChR er = EIn "ThenVL(R)" er
eThenVLChR :: SE er -> SE (EThenVLChR er)
eThenVLChR :: forall (er :: PE). SE er -> SE (EThenVLChR er)
eThenVLChR SE er
er = SE er -> (SingE er => SE (EThenVLChR er)) -> SE (EThenVLChR er)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE er
er ((SingE er => SE (EThenVLChR er)) -> SE (EThenVLChR er))
-> (SingE er => SE (EThenVLChR er)) -> SE (EThenVLChR er)
forall a b. (a -> b) -> a -> b
$ SE (EThenVLChR er)
SingE er => SE (EThenVLChR er)
forall (e :: PE). SingE e => SE e
singE

sThenVLChR
    :: SResult ssr srr resr
    -> SResult (SEither ssl ssr) srr (ThenVLChR resr)
sThenVLChR :: forall {b} {r} {l} (ssr :: b -> Type) (srr :: r -> Type)
       (resr :: PResult b r) (ssl :: l -> Type).
SResult ssr srr resr
-> SResult (SEither ssl ssr) srr (ThenVLChR resr)
sThenVLChR = \case
  SCont ssr s1
sr -> SEither ssl ssr ('Right s1)
-> SResult (SEither ssl ssr) srr ('Cont ('Right s1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SEither ssl ssr ('Right s1)
 -> SResult (SEither ssl ssr) srr ('Cont ('Right s1)))
-> SEither ssl ssr ('Right s1)
-> SResult (SEither ssl ssr) srr ('Cont ('Right s1))
forall a b. (a -> b) -> a -> b
$ ssr s1 -> SEither ssl ssr ('Right s1)
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight ssr s1
sr
  SDone srr r1
rr -> srr r1 -> SResult (SEither ssl ssr) srr ('Done r1)
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone srr r1
rr
  SErr  SE e
er -> SE (EThenVLChR e)
-> SResult (SEither ssl ssr) srr ('Err (EThenVLChR e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenVLChR e)
 -> SResult (SEither ssl ssr) srr ('Err (EThenVLChR e)))
-> SE (EThenVLChR e)
-> SResult (SEither ssl ssr) srr ('Err (EThenVLChR e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenVLChR e)
forall (er :: PE). SE er -> SE (EThenVLChR er)
eThenVLChR SE e
er

sThenVLChSym
    :: SParserChSym ssl srl plCh
    -> SParserChSym ssr srr prCh
    -> ssr sr
    -> SParserChSym (SEither ssl ssr) srr
        (ThenVLChSym plCh prCh sr)
sThenVLChSym :: 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 ssr) srr (ThenVLChSym plCh prCh sr)
sThenVLChSym SParserChSym ssl srl plCh
plCh SParserChSym ssr srr prCh
prCh ssr sr
s0r = LamRep2
  SChar
  (SEither ssl ssr)
  (SResult (SEither ssl ssr) srr)
  (ThenVLChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl ssr)
     (SResult (SEither ssl ssr) srr)
     (ThenVLChSym 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 ssr)
   (SResult (SEither ssl ssr) srr)
   (ThenVLChSym plCh prCh sr)
 -> Lam2
      SChar
      (SEither ssl ssr)
      (SResult (SEither ssl ssr) srr)
      (ThenVLChSym plCh prCh sr))
-> LamRep2
     SChar
     (SEither ssl ssr)
     (SResult (SEither ssl ssr) srr)
     (ThenVLChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl ssr)
     (SResult (SEither ssl ssr) srr)
     (ThenVLChSym 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 ssr ('Left s1)
-> SResult (SEither ssl ssr) srr ('Cont ('Left s1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SEither ssl ssr ('Left s1)
 -> SResult (SEither ssl ssr) srr ('Cont ('Left s1)))
-> SEither ssl ssr ('Left s1)
-> SResult (SEither ssl ssr) srr ('Cont ('Left s1))
forall a b. (a -> b) -> a -> b
$ ssl s1 -> SEither ssl 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  -> SResult ssr srr (App (App prCh x) sr)
-> SResult (SEither ssl ssr) srr (ThenVLChR (App (App prCh x) sr))
forall {b} {r} {l} (ssr :: b -> Type) (srr :: r -> Type)
       (resr :: PResult b r) (ssl :: l -> Type).
SResult ssr srr resr
-> SResult (SEither ssl ssr) srr (ThenVLChR resr)
sThenVLChR (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 (EThenVLChL e)
-> SResult (SEither ssl ssr) srr ('Err (EThenVLChL e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenVLChL e)
 -> SResult (SEither ssl ssr) srr ('Err (EThenVLChL e)))
-> SE (EThenVLChL e)
-> SResult (SEither ssl ssr) srr ('Err (EThenVLChL e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenVLChL e)
forall (el :: PE). SE el -> SE (EThenVLChL el)
eThenVLChL SE e
el
  SRight ssr r1
sr -> SResult ssr srr (App (App prCh x) r1)
-> SResult (SEither ssl ssr) srr (ThenVLChR (App (App prCh x) r1))
forall {b} {r} {l} (ssr :: b -> Type) (srr :: r -> Type)
       (resr :: PResult b r) (ssl :: l -> Type).
SResult ssr srr resr
-> SResult (SEither ssl ssr) srr (ThenVLChR resr)
sThenVLChR (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 r1 -> SResult ssr srr (App (App prCh x) r1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr r1
sr)

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

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

type family ThenVLEnd plEnd prEnd s0r s where
    -- | EOT during R: call R end
    ThenVLEnd plEnd prEnd s0r (Right sr) = ThenVLEndR           (prEnd @@ sr)
    -- | EOT during L: call L end, pass R end
    ThenVLEnd plEnd prEnd s0r (Left  sl) = ThenVLEndL prEnd s0r (plEnd @@ sl)

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

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

sThenVLEndR
    :: SResultEnd srr res
    -> SResultEnd srr (ThenVLEndR res)
sThenVLEndR :: forall {b} (srr :: b -> Type) (res :: Either PE b).
SResultEnd srr res -> SResultEnd srr (ThenVLEndR res)
sThenVLEndR = \case
  SRight srr r1
rr -> srr r1 -> SEither SE srr ('Right r1)
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight srr r1
rr
  SLeft  SE l1
er -> SE (EThenVLEndR l1) -> SEither SE srr ('Left (EThenVLEndR l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft  (SE (EThenVLEndR l1) -> SEither SE srr ('Left (EThenVLEndR l1)))
-> SE (EThenVLEndR l1) -> SEither SE srr ('Left (EThenVLEndR l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenVLEndR l1)
forall (er :: PE). SE er -> SE (EThenVLEndR er)
eThenVLEndR SE l1
er

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

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

sThenVLEndSym
    :: SParserEndSym ssl srl plEnd
    -> SParserEndSym ssr srr prEnd
    -> ssr s0r
    -> SParserEndSym (SEither ssl ssr) srr
        (ThenVLEndSym plEnd prEnd s0r)
sThenVLEndSym :: 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 ssr) srr (ThenVLEndSym plEnd prEnd s0r)
sThenVLEndSym SParserEndSym ssl srl plEnd
plEnd SParserEndSym ssr srr prEnd
prEnd ssr s0r
s0r = LamRep
  (SEither ssl ssr) (SResultEnd srr) (ThenVLEndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl ssr) (SResultEnd srr) (ThenVLEndSym 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 ssr) (SResultEnd srr) (ThenVLEndSym plEnd prEnd s0r)
 -> Lam
      (SEither ssl ssr) (SResultEnd srr) (ThenVLEndSym plEnd prEnd s0r))
-> LamRep
     (SEither ssl ssr) (SResultEnd srr) (ThenVLEndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl ssr) (SResultEnd srr) (ThenVLEndSym plEnd prEnd s0r)
forall a b. (a -> b) -> a -> b
$ \case
  SRight ssr r1
sr -> SResultEnd srr (App prEnd r1)
-> SResultEnd srr (ThenVLEndR (App prEnd r1))
forall {b} (srr :: b -> Type) (res :: Either PE b).
SResultEnd srr res -> SResultEnd srr (ThenVLEndR res)
sThenVLEndR (SParserEndSym ssr srr prEnd
prEnd SParserEndSym ssr srr prEnd
-> ssr r1 -> SResultEnd srr (App prEnd r1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ssr r1
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 -> SResultEnd srr (App prEnd s0r)
-> SResultEnd srr (ThenVLEndR (App prEnd s0r))
forall {b} (srr :: b -> Type) (res :: Either PE b).
SResultEnd srr res -> SResultEnd srr (ThenVLEndR res)
sThenVLEndR (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 (EThenVLEndL l1) -> SEither SE srr ('Left (EThenVLEndL l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE (EThenVLEndL l1) -> SEither SE srr ('Left (EThenVLEndL l1)))
-> SE (EThenVLEndL l1) -> SEither SE srr ('Left (EThenVLEndL l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenVLEndL l1)
forall (er :: PE). SE er -> SE (EThenVLEndL er)
eThenVLEndL SE l1
el

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