{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Then where

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

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

sThen
    :: SParser ssl srl ('PParser plCh plEnd s0l)
    -> SParser ssr srr ('PParser prCh prEnd s0r)
    -> SPThen  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThen :: forall {l} {a} {b} {b} (ssl :: l -> Type) (srl :: a -> Type)
       (plCh :: ParserChSym l a) (plEnd :: ParserEndSym l a) (s0l :: l)
       (ssr :: b -> Type) (srr :: b -> Type) (prCh :: ParserChSym b b)
       (prEnd :: ParserEndSym b b) (s0r :: b).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThen ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThen (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))
  (STuple2 srl srr)
  (ThenChSym plCh prCh s0r)
-> SParserEndSym
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     (ThenEndSym plEnd prEnd s0r)
-> SEither ssl (STuple2 srl ssr) ('Left s0l)
-> SParser
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('PParser
        (ThenChSym plCh prCh s0r) (ThenEndSym 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))
     (STuple2 srl srr)
     (ThenChSym 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))
     (STuple2 srl srr)
     (ThenChSym plCh prCh sr)
sThenChSym 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))
     (STuple2 srl srr)
     (ThenEndSym 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))
     (STuple2 srl srr)
     (ThenEndSym plEnd prEnd s0r)
sThenEndSym 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 (Then' plCh plEnd s0l prCh prEnd s0r) where
    type PS (Then' 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 (Then' plCh plEnd s0l prCh prEnd s0r) =
        STuple2
            (PR ('PParser plCh plEnd s0l))
            (PR ('PParser prCh prEnd s0r))
    singParser' :: SParser
  (PS (Then' plCh plEnd s0l prCh prEnd s0r))
  (PR (Then' plCh plEnd s0l prCh prEnd s0r))
  (Then' 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)
-> SPThen
     (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} {a} {b} {b} (ssl :: l -> Type) (srl :: a -> Type)
       (plCh :: ParserChSym l a) (plEnd :: ParserEndSym l a) (s0l :: l)
       (ssr :: b -> Type) (srr :: b -> Type) (prCh :: ParserChSym b b)
       (prEnd :: ParserEndSym b b) (s0r :: b).
SParser ssl srl ('PParser plCh plEnd s0l)
-> SParser ssr srr ('PParser prCh prEnd s0r)
-> SPThen ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r
sThen (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 rr).
SingParser p =>
SParser (PS p) (PR p) p
singParser @pr)

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

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

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

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

type EThenChL el = EIn "Then(L)" el
eThenChL :: SE el -> SE (EThenChL el)
eThenChL :: forall (el :: PE). SE el -> SE (EThenChL el)
eThenChL SE el
el = SE el -> (SingE el => SE (EThenChL el)) -> SE (EThenChL el)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE el
el ((SingE el => SE (EThenChL el)) -> SE (EThenChL el))
-> (SingE el => SE (EThenChL el)) -> SE (EThenChL el)
forall a b. (a -> b) -> a -> b
$ SE (EThenChL el)
SingE el => SE (EThenChL el)
forall (e :: PE). SingE e => SE e
singE

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

type EThenChR er = EIn "Then(R)" er
eThenChR :: SE er -> SE (EThenChR er)
eThenChR :: forall (er :: PE). SE er -> SE (EThenChR er)
eThenChR SE er
er = SE er -> (SingE er => SE (EThenChR er)) -> SE (EThenChR er)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE er
er ((SingE er => SE (EThenChR er)) -> SE (EThenChR er))
-> (SingE er => SE (EThenChR er)) -> SE (EThenChR er)
forall a b. (a -> b) -> a -> b
$ SE (EThenChR er)
SingE er => SE (EThenChR er)
forall (e :: PE). SingE e => SE e
singE

sThenChR
    :: srl rl
    -> SResult ssr srr resr
    -> SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
        (ThenChR rl resr)
sThenChR :: forall {k} {k} {k} {l} (srl :: k -> Type) (rl :: k)
       (ssr :: k -> Type) (srr :: k -> Type) (resr :: PResult k k)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult
     (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr) (ThenChR rl resr)
sThenChR srl rl
rl = \case
  SCont ssr s1
sr -> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('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))
      (STuple2 srl srr)
      ('Cont ('Right '(rl, s1))))
-> SEither ssl (STuple2 srl ssr) ('Right '(rl, s1))
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('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 -> STuple2 srl srr '(rl, r1)
-> SResult
     (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr) ('Done '(rl, r1))
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone (STuple2 srl srr '(rl, r1)
 -> SResult
      (SEither ssl (STuple2 srl ssr))
      (STuple2 srl srr)
      ('Done '(rl, r1)))
-> STuple2 srl srr '(rl, r1)
-> SResult
     (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr) ('Done '(rl, r1))
forall a b. (a -> b) -> a -> b
$ srl rl -> srr r1 -> STuple2 srl srr '(rl, r1)
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 srr r1
rr
  SErr  SE e
er -> SE (EThenChR e)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('Err (EThenChR e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenChR e)
 -> SResult
      (SEither ssl (STuple2 srl ssr))
      (STuple2 srl srr)
      ('Err (EThenChR e)))
-> SE (EThenChR e)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('Err (EThenChR e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenChR e)
forall (er :: PE). SE er -> SE (EThenChR er)
eThenChR SE e
er

sThenChSym
    :: SParserChSym ssl srl plCh
    -> SParserChSym ssr srr prCh
    -> ssr sr
    -> SParserChSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
        (ThenChSym plCh prCh sr)
sThenChSym :: 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))
     (STuple2 srl srr)
     (ThenChSym plCh prCh sr)
sThenChSym 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)) (STuple2 srl srr))
  (ThenChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr))
     (ThenChSym 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)) (STuple2 srl srr))
   (ThenChSym plCh prCh sr)
 -> Lam2
      SChar
      (SEither ssl (STuple2 srl ssr))
      (SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr))
      (ThenChSym plCh prCh sr))
-> LamRep2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr))
     (ThenChSym plCh prCh sr)
-> Lam2
     SChar
     (SEither ssl (STuple2 srl ssr))
     (SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr))
     (ThenChSym 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))
     (STuple2 srl 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 (STuple2 srl ssr) ('Left s1)
 -> SResult
      (SEither ssl (STuple2 srl ssr))
      (STuple2 srl srr)
      ('Cont ('Left s1)))
-> SEither ssl (STuple2 srl ssr) ('Left s1)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('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))
     (STuple2 srl srr)
     (ThenChR r1 (App (App prCh x) sr))
forall {k} {k} {k} {l} (srl :: k -> Type) (rl :: k)
       (ssr :: k -> Type) (srr :: k -> Type) (resr :: PResult k k)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult
     (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr) (ThenChR rl resr)
sThenChR 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 (EThenChL e)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('Err (EThenChL e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EThenChL e)
 -> SResult
      (SEither ssl (STuple2 srl ssr))
      (STuple2 srl srr)
      ('Err (EThenChL e)))
-> SE (EThenChL e)
-> SResult
     (SEither ssl (STuple2 srl ssr))
     (STuple2 srl srr)
     ('Err (EThenChL e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EThenChL e)
forall (el :: PE). SE el -> SE (EThenChL el)
eThenChL 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))
     (STuple2 srl srr)
     (ThenChR a1 (App (App prCh x) b1))
forall {k} {k} {k} {l} (srl :: k -> Type) (rl :: k)
       (ssr :: k -> Type) (srr :: k -> Type) (resr :: PResult k k)
       (ssl :: l -> Type).
srl rl
-> SResult ssr srr resr
-> SResult
     (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr) (ThenChR rl resr)
sThenChR 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 ThenChSym
    :: ParserChSym sl rl
    -> ParserChSym sr rr
    -> sr
    -> ParserChSym (Either sl (rl, sr)) (rl, rr)
data ThenChSym plCh prCh s0r f
type instance App (ThenChSym plCh prCh s0r) f = ThenChSym1 plCh prCh s0r f

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

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

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

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

sThenEndR
    :: srl rl
    -> SResultEnd srr res
    -> SResultEnd (STuple2 srl srr) (ThenEndR rl res)
sThenEndR :: forall {k} {k} (srl :: k -> Type) (rl :: k) (srr :: k -> Type)
       (res :: Either PE k).
srl rl
-> SResultEnd srr res
-> SResultEnd (STuple2 srl srr) (ThenEndR rl res)
sThenEndR srl rl
rl = \case
  SRight srr r1
rr -> STuple2 srl srr '(rl, r1)
-> SEither SE (STuple2 srl srr) ('Right '(rl, r1))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (STuple2 srl srr '(rl, r1)
 -> SEither SE (STuple2 srl srr) ('Right '(rl, r1)))
-> STuple2 srl srr '(rl, r1)
-> SEither SE (STuple2 srl srr) ('Right '(rl, r1))
forall a b. (a -> b) -> a -> b
$ srl rl -> srr r1 -> STuple2 srl srr '(rl, r1)
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 srr r1
rr
  SLeft  SE l1
er -> SE (EThenEndR l1)
-> SEither SE (STuple2 srl srr) ('Left (EThenEndR l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft  (SE (EThenEndR l1)
 -> SEither SE (STuple2 srl srr) ('Left (EThenEndR l1)))
-> SE (EThenEndR l1)
-> SEither SE (STuple2 srl srr) ('Left (EThenEndR l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenEndR l1)
forall (er :: PE). SE er -> SE (EThenEndR er)
eThenEndR SE l1
er

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

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

sThenEndSym
    :: SParserEndSym ssl srl plEnd
    -> SParserEndSym ssr srr prEnd
    -> ssr s0r
    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)
        (ThenEndSym plEnd prEnd s0r)
sThenEndSym :: 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))
     (STuple2 srl srr)
     (ThenEndSym plEnd prEnd s0r)
sThenEndSym SParserEndSym ssl srl plEnd
plEnd SParserEndSym ssr srr prEnd
prEnd ssr s0r
s0r = LamRep
  (SEither ssl (STuple2 srl ssr))
  (SResultEnd (STuple2 srl srr))
  (ThenEndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd (STuple2 srl srr))
     (ThenEndSym 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 (STuple2 srl srr))
   (ThenEndSym plEnd prEnd s0r)
 -> Lam
      (SEither ssl (STuple2 srl ssr))
      (SResultEnd (STuple2 srl srr))
      (ThenEndSym plEnd prEnd s0r))
-> LamRep
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd (STuple2 srl srr))
     (ThenEndSym plEnd prEnd s0r)
-> Lam
     (SEither ssl (STuple2 srl ssr))
     (SResultEnd (STuple2 srl srr))
     (ThenEndSym 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 (STuple2 srl srr) (ThenEndR a1 (App prEnd b1))
forall {k} {k} (srl :: k -> Type) (rl :: k) (srr :: k -> Type)
       (res :: Either PE k).
srl rl
-> SResultEnd srr res
-> SResultEnd (STuple2 srl srr) (ThenEndR rl res)
sThenEndR 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 (STuple2 srl srr) (ThenEndR r1 (App prEnd s0r))
forall {k} {k} (srl :: k -> Type) (rl :: k) (srr :: k -> Type)
       (res :: Either PE k).
srl rl
-> SResultEnd srr res
-> SResultEnd (STuple2 srl srr) (ThenEndR rl res)
sThenEndR 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 (EThenEndL l1)
-> SEither SE (STuple2 srl srr) ('Left (EThenEndL l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE (EThenEndL l1)
 -> SEither SE (STuple2 srl srr) ('Left (EThenEndL l1)))
-> SE (EThenEndL l1)
-> SEither SE (STuple2 srl srr) ('Left (EThenEndL l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EThenEndL l1)
forall (er :: PE). SE er -> SE (EThenEndL er)
eThenEndL SE l1
el

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