{-# 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
( 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)
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) =
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
ThenVREnd plEnd prEnd s0r (Right '(rl, sr)) = ThenVREndR rl (prEnd @@ sr)
ThenVREnd plEnd prEnd s0r (Left sl) = ThenVREndL prEnd s0r (plEnd @@ sl)
type family ThenVREndR rl res where
ThenVREndR rl (Right rr) = Right rl
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
ThenVREndL prEnd s0r (Right rl) = ThenVREndR rl (prEnd @@ s0r)
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