{-# LANGUAGE UndecidableInstances #-} module Symparsec.Parser.Count where import Symparsec.Parser.Common import GHC.TypeLits hiding ( ErrorMessage(..) ) import Singleraeh.Tuple import Singleraeh.List import Singleraeh.Either import Singleraeh.Natural import DeFun.Core import Data.Type.Equality import Unsafe.Coerce ( unsafeCoerce ) type CountS s r = (Natural, [r], s) type family Count n p where Count n ('PParser pCh pEnd s0) = Count' n pCh pEnd s0 type Count' n pCh pEnd s0 = 'PParser (CountChSym pCh s0) (CountEndSym pEnd s0) '(n, '[], s0) type SCountS ss sr = STuple3 SNat (SList sr) ss sCount :: SNat n -> SParser ss sr ('PParser pCh pEnd s0) -> SParser (SCountS ss sr) (SList sr) (Count' n pCh pEnd s0) sCount :: forall {k} {r} (n :: Nat) (ss :: k -> Type) (sr :: r -> Type) (pCh :: ParserChSym k r) (pEnd :: ParserEndSym k r) (s0 :: k). SNat n -> SParser ss sr ('PParser pCh pEnd s0) -> SParser (SCountS ss sr) (SList sr) (Count' n pCh pEnd s0) sCount SNat n n (SParser SParserChSym ss sr pCh pCh SParserEndSym ss sr pEnd pEnd ss s0 s0) = SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0) -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0) -> SCountS ss sr '(n, '[], s0) -> SParser (SCountS ss sr) (SList sr) ('PParser (CountChSym pCh s0) (CountEndSym pEnd s0) '(n, '[], s0)) 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 ss sr pCh -> ss s0 -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0) forall {s} {r} (ss :: s -> Type) (sr :: r -> Type) (pCh :: Char ~> (s ~> PResult s r)) (s0 :: s). SParserChSym ss sr pCh -> ss s0 -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0) sCountChSym SParserChSym ss sr pCh SParserChSym ss sr pCh pCh ss s0 ss s0 s0) (SParserEndSym ss sr pEnd -> ss s0 -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0) forall {s} {r} (ss :: s -> Type) (sr :: r -> Type) (pEnd :: s ~> Either PE r) (s0 :: s). SParserEndSym ss sr pEnd -> ss s0 -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0) sCountEndSym SParserEndSym ss sr pEnd SParserEndSym ss sr pEnd pEnd ss s0 ss s0 s0) (SNat n -> SList sr '[] -> ss s0 -> SCountS ss sr '(n, '[], s0) forall {a} {b} {c} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type) (b1 :: b) (sc :: c -> Type) (c1 :: c). sa a1 -> sb b1 -> sc c1 -> STuple3 sa sb sc '(a1, b1, c1) STuple3 SNat n n SList sr '[] forall {a} (sa :: a -> Type). SList sa '[] SNil ss s0 ss s0 s0) instance ( p ~ 'PParser pCh pEnd s0, SingParser p, KnownNat n ) => SingParser (Count' n pCh pEnd s0) where type PS (Count' n pCh pEnd s0) = SCountS (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0)) type PR (Count' n pCh pEnd s0) = SList (PR ('PParser pCh pEnd s0)) singParser' :: SParser (PS (Count' n pCh pEnd s0)) (PR (Count' n pCh pEnd s0)) (Count' n pCh pEnd s0) singParser' = SNat n -> SParser (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0)) ('PParser pCh pEnd s0) -> SParser (SCountS (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0))) (SList (PR ('PParser pCh pEnd s0))) (Count' n pCh pEnd s0) forall {k} {r} (n :: Nat) (ss :: k -> Type) (sr :: r -> Type) (pCh :: ParserChSym k r) (pEnd :: ParserEndSym k r) (s0 :: k). SNat n -> SParser ss sr ('PParser pCh pEnd s0) -> SParser (SCountS ss sr) (SList sr) (Count' n pCh pEnd s0) sCount SNat n forall (n :: Nat). KnownNat n => SNat n SNat (forall {s} {r} (p :: PParser s r). SingParser p => SParser (PS p) (PR p) p forall (p :: PParser k r). SingParser p => SParser (PS p) (PR p) p singParser @p) type family CountCh pCh s0 ch s where CountCh pCh s0 ch '(n, rs, s) = CountCh' pCh s0 ch n rs s sCountChSym :: SParserChSym ss sr pCh -> ss s0 -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0) sCountChSym :: forall {s} {r} (ss :: s -> Type) (sr :: r -> Type) (pCh :: Char ~> (s ~> PResult s r)) (s0 :: s). SParserChSym ss sr pCh -> ss s0 -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0) sCountChSym SParserChSym ss sr pCh pCh ss s0 s0 = LamRep2 SChar (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0) -> Lam2 SChar (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0) 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 (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0) -> Lam2 SChar (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0)) -> LamRep2 SChar (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0) -> Lam2 SChar (SCountS ss sr) (SResult (SCountS ss sr) (SList sr)) (CountChSym pCh s0) forall a b. (a -> b) -> a -> b $ \SChar x ch (STuple3 SNat a1 n SList sr b1 rs ss c1 s) -> SParserChSym ss sr pCh -> ss s0 -> SChar x -> SNat a1 -> SList sr b1 -> ss c1 -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 x a1 b1 c1) forall {k} {k} (ss :: k -> Type) (sr :: k -> Type) (pCh :: Char ~> (k ~> PResult k k)) (s0 :: k) (ch :: Char) (n :: Nat) (rs :: [k]) (s :: k). SParserChSym ss sr pCh -> ss s0 -> SChar ch -> SNat n -> SList sr rs -> ss s -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) sCountCh' SParserChSym ss sr pCh pCh ss s0 s0 SChar x ch SNat a1 n SList sr b1 rs ss c1 s type family CountCh' pCh s0 ch n rs s where CountCh' pCh s0 ch 0 rs s = Done (Reverse rs) CountCh' pCh s0 ch n rs s = CountChN pCh ch n rs s0 (pCh @@ ch @@ s) sCountCh' :: SParserChSym ss sr pCh -> ss s0 -> SChar ch -> SNat n -> SList sr rs -> ss s -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) sCountCh' :: forall {k} {k} (ss :: k -> Type) (sr :: k -> Type) (pCh :: Char ~> (k ~> PResult k k)) (s0 :: k) (ch :: Char) (n :: Nat) (rs :: [k]) (s :: k). SParserChSym ss sr pCh -> ss s0 -> SChar ch -> SNat n -> SList sr rs -> ss s -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) sCountCh' SParserChSym ss sr pCh pCh ss s0 s0 SChar ch ch SNat n n SList sr rs rs ss s s = case SNat n -> SNat 0 -> Maybe (n :~: 0) forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality SNat n n (forall (n :: Nat). KnownNat n => SNat n SNat @0) of Just n :~: 0 Refl -> SList sr (Reverse' '[] rs) -> SResult (SCountS ss sr) (SList sr) ('Done (Reverse' '[] rs)) forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type). sr r1 -> SResult ss sr ('Done r1) SDone (SList sr (Reverse' '[] rs) -> SResult (SCountS ss sr) (SList sr) ('Done (Reverse' '[] rs))) -> SList sr (Reverse' '[] rs) -> SResult (SCountS ss sr) (SList sr) ('Done (Reverse' '[] rs)) forall a b. (a -> b) -> a -> b $ SList sr rs -> SList sr (Reverse' '[] rs) forall {k} (sa :: k -> Type) (as :: [k]). SList sa as -> SList sa (Reverse as) sReverse SList sr rs rs Maybe (n :~: 0) Nothing -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 (App (App pCh ch) s)) -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) forall a b. a -> b unsafeCoerce (SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 (App (App pCh ch) s)) -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s)) -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 (App (App pCh ch) s)) -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) forall a b. (a -> b) -> a -> b $ SParserChSym ss sr pCh -> SChar ch -> SNat n -> SList sr rs -> ss s0 -> SResult ss sr (App (App pCh ch) s) -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 (App (App pCh ch) s)) forall {k} {k} (ss :: k -> Type) (sr :: k -> Type) (pCh :: Char ~> (k ~> PResult k k)) (ch :: Char) (n :: Nat) (rs :: [k]) (s0 :: k) (res :: PResult k k). SParserChSym ss sr pCh -> SChar ch -> SNat n -> SList sr rs -> ss s0 -> SResult ss sr res -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 res) sCountChN SParserChSym ss sr pCh pCh SChar ch ch SNat n n SList sr rs rs ss s0 s0 (SParserChSym ss sr pCh pCh SParserChSym ss sr pCh -> SChar ch -> Lam ss (SResult ss sr) (App pCh ch) forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k) (x :: a1). Lam a2 b f -> a2 x -> b (f @@ x) @@ SChar ch ch Lam ss (SResult ss sr) (App pCh ch) -> ss s -> SResult ss sr (App (App pCh ch) s) forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k) (x :: a1). Lam a2 b f -> a2 x -> b (f @@ x) @@ ss s s) type family CountChN pCh ch n rs s0 res where CountChN pCh ch n rs s0 (Cont s) = Cont '(n, rs, s) CountChN pCh ch n rs s0 (Done r) = CountCh' pCh s0 ch (n-1) (r:rs) s0 CountChN pCh ch n rs s0 (Err e) = Err (ECount e) sCountChN :: SParserChSym ss sr pCh -> SChar ch -> SNat n -> SList sr rs -> ss s0 -> SResult ss sr res -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 res) sCountChN :: forall {k} {k} (ss :: k -> Type) (sr :: k -> Type) (pCh :: Char ~> (k ~> PResult k k)) (ch :: Char) (n :: Nat) (rs :: [k]) (s0 :: k) (res :: PResult k k). SParserChSym ss sr pCh -> SChar ch -> SNat n -> SList sr rs -> ss s0 -> SResult ss sr res -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 res) sCountChN SParserChSym ss sr pCh pCh SChar ch ch SNat n n SList sr rs rs ss s0 s0 = \case SCont ss s1 s -> SCountS ss sr '(n, rs, s1) -> SResult (SCountS ss sr) (SList sr) ('Cont '(n, rs, s1)) forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type). ss s1 -> SResult ss sr ('Cont s1) SCont (SCountS ss sr '(n, rs, s1) -> SResult (SCountS ss sr) (SList sr) ('Cont '(n, rs, s1))) -> SCountS ss sr '(n, rs, s1) -> SResult (SCountS ss sr) (SList sr) ('Cont '(n, rs, s1)) forall a b. (a -> b) -> a -> b $ SNat n -> SList sr rs -> ss s1 -> SCountS ss sr '(n, rs, s1) forall {a} {b} {c} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type) (b1 :: b) (sc :: c -> Type) (c1 :: c). sa a1 -> sb b1 -> sc c1 -> STuple3 sa sb sc '(a1, b1, c1) STuple3 SNat n n SList sr rs rs ss s1 s SDone sr r1 r -> SParserChSym ss sr pCh -> ss s0 -> SChar ch -> SNat (n - 1) -> SList sr (r1 : rs) -> ss s0 -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch (n - 1) (r1 : rs) s0) forall {k} {k} (ss :: k -> Type) (sr :: k -> Type) (pCh :: Char ~> (k ~> PResult k k)) (s0 :: k) (ch :: Char) (n :: Nat) (rs :: [k]) (s :: k). SParserChSym ss sr pCh -> ss s0 -> SChar ch -> SNat n -> SList sr rs -> ss s -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s) sCountCh' SParserChSym ss sr pCh pCh ss s0 s0 SChar ch ch (SNat n n SNat n -> SNat 1 -> SNat (n - 1) forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m) %- forall (n :: Nat). KnownNat n => SNat n SNat @1) (sr r1 -> SList sr rs -> SList sr (r1 : rs) forall {a} (sa :: a -> Type) (a1 :: a) (as1 :: [a]). sa a1 -> SList sa as1 -> SList sa (a1 : as1) SCons sr r1 r SList sr rs rs) ss s0 s0 SErr SE e e -> SE (ECount e) -> SResult (SCountS ss sr) (SList sr) ('Err (ECount e)) forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type). SE e -> SResult ss sr ('Err e) SErr (SE (ECount e) -> SResult (SCountS ss sr) (SList sr) ('Err (ECount e))) -> SE (ECount e) -> SResult (SCountS ss sr) (SList sr) ('Err (ECount e)) forall a b. (a -> b) -> a -> b $ SE e -> SE (ECount e) forall (e :: PE). SE e -> SE (ECount e) eCount SE e e type ECount e = EIn "Count" e eCount :: SE e -> SE (ECount e) eCount :: forall (e :: PE). SE e -> SE (ECount e) eCount SE e e = SE e -> (SingE e => SE (ECount e)) -> SE (ECount e) forall (e :: PE) r. SE e -> (SingE e => r) -> r withSingE SE e e ((SingE e => SE (ECount e)) -> SE (ECount e)) -> (SingE e => SE (ECount e)) -> SE (ECount e) forall a b. (a -> b) -> a -> b $ SE (ECount e) SingE e => SE (ECount e) forall (e :: PE). SingE e => SE e singE type CountChSym :: ParserChSym s r -> s -> ParserChSym (CountS s r) [r] data CountChSym pCh s0 f type instance App (CountChSym pCh s0) f = CountChSym1 pCh s0 f type CountChSym1 :: ParserChSym s r -> s -> ParserChSym1 (CountS s r) [r] data CountChSym1 pCh s0 ch s type instance App (CountChSym1 pCh s0 ch) s = CountCh pCh s0 ch s type family CountEnd pEnd s0 s where CountEnd pEnd s0 '(n, rs, s) = CountEnd' pEnd s0 n rs s type family CountEnd' pEnd s0 n rs s where CountEnd' pEnd s0 0 rs s = Right (Reverse rs) CountEnd' pEnd s0 n rs s = CountEndN pEnd s0 n rs (pEnd @@ s) sCountEnd' :: SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> ss s -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) sCountEnd' :: forall {a} {k} (ss :: a -> Type) (sr :: k -> Type) (pEnd :: a ~> Either PE k) (s0 :: a) (n :: Nat) (rs :: [k]) (s :: a). SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> ss s -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) sCountEnd' SParserEndSym ss sr pEnd pEnd ss s0 s0 SNat n n SList sr rs rs ss s s = case SNat n -> SNat 0 -> Maybe (n :~: 0) forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality SNat n n (forall (n :: Nat). KnownNat n => SNat n SNat @0) of Just n :~: 0 Refl -> SList sr (Reverse' '[] rs) -> SEither SE (SList sr) ('Right (Reverse' '[] rs)) forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type). sr r1 -> SEither sl sr ('Right r1) SRight (SList sr (Reverse' '[] rs) -> SEither SE (SList sr) ('Right (Reverse' '[] rs))) -> SList sr (Reverse' '[] rs) -> SEither SE (SList sr) ('Right (Reverse' '[] rs)) forall a b. (a -> b) -> a -> b $ SList sr rs -> SList sr (Reverse' '[] rs) forall {k} (sa :: k -> Type) (as :: [k]). SList sa as -> SList sa (Reverse as) sReverse SList sr rs rs Maybe (n :~: 0) Nothing -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs (App pEnd s)) -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) forall a b. a -> b unsafeCoerce (SResultEnd (SList sr) (CountEndN pEnd s0 n rs (App pEnd s)) -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s)) -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs (App pEnd s)) -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) forall a b. (a -> b) -> a -> b $ SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> SResultEnd sr (App pEnd s) -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs (App pEnd s)) forall {a} {k} (ss :: a -> Type) (sr :: k -> Type) (pEnd :: a ~> Either PE k) (s0 :: a) (n :: Nat) (rs :: [k]) (res :: Either PE k). SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> SResultEnd sr res -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs res) sCountEndN SParserEndSym ss sr pEnd pEnd ss s0 s0 SNat n n SList sr rs rs (SParserEndSym ss sr pEnd pEnd SParserEndSym ss sr pEnd -> ss s -> SResultEnd sr (App pEnd s) forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k) (x :: a1). Lam a2 b f -> a2 x -> b (f @@ x) @@ ss s s) type family CountEndN pEnd s0 n rs res where CountEndN pEnd s0 n rs (Right r) = CountEnd' pEnd s0 (n-1) (r:rs) s0 CountEndN pEnd s0 n rs (Left e) = Left (ECount e) sCountEndN :: SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> SResultEnd sr res -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs res) sCountEndN :: forall {a} {k} (ss :: a -> Type) (sr :: k -> Type) (pEnd :: a ~> Either PE k) (s0 :: a) (n :: Nat) (rs :: [k]) (res :: Either PE k). SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> SResultEnd sr res -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs res) sCountEndN SParserEndSym ss sr pEnd pEnd ss s0 s0 SNat n n SList sr rs rs = \case SRight sr r1 r -> SParserEndSym ss sr pEnd -> ss s0 -> SNat (n - 1) -> SList sr (r1 : rs) -> ss s0 -> SResultEnd (SList sr) (CountEnd' pEnd s0 (n - 1) (r1 : rs) s0) forall {a} {k} (ss :: a -> Type) (sr :: k -> Type) (pEnd :: a ~> Either PE k) (s0 :: a) (n :: Nat) (rs :: [k]) (s :: a). SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> ss s -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) sCountEnd' SParserEndSym ss sr pEnd pEnd ss s0 s0 (SNat n n SNat n -> SNat 1 -> SNat (n - 1) forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m) %- forall (n :: Nat). KnownNat n => SNat n SNat @1) (sr r1 -> SList sr rs -> SList sr (r1 : rs) forall {a} (sa :: a -> Type) (a1 :: a) (as1 :: [a]). sa a1 -> SList sa as1 -> SList sa (a1 : as1) SCons sr r1 r SList sr rs rs) ss s0 s0 SLeft SE l1 e -> SE (ECount l1) -> SEither SE (SList sr) ('Left (ECount l1)) forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type). sl l1 -> SEither sl sr ('Left l1) SLeft (SE (ECount l1) -> SEither SE (SList sr) ('Left (ECount l1))) -> SE (ECount l1) -> SEither SE (SList sr) ('Left (ECount l1)) forall a b. (a -> b) -> a -> b $ SE l1 -> SE (ECount l1) forall (e :: PE). SE e -> SE (ECount e) eCount SE l1 e type CountEndSym :: ParserEndSym s r -> s -> ParserEndSym (CountS s r) [r] data CountEndSym pEnd s0 s type instance App (CountEndSym pEnd s0) s = CountEnd pEnd s0 s sCountEndSym :: SParserEndSym ss sr pEnd -> ss s0 -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0) sCountEndSym :: forall {s} {r} (ss :: s -> Type) (sr :: r -> Type) (pEnd :: s ~> Either PE r) (s0 :: s). SParserEndSym ss sr pEnd -> ss s0 -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0) sCountEndSym SParserEndSym ss sr pEnd pEnd ss s0 s0 = LamRep (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0) -> Lam (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0) forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b). LamRep a1 b1 f -> Lam a1 b1 f Lam (LamRep (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0) -> Lam (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0)) -> LamRep (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0) -> Lam (SCountS ss sr) (SResultEnd (SList sr)) (CountEndSym pEnd s0) forall a b. (a -> b) -> a -> b $ \(STuple3 SNat a1 n SList sr b1 rs ss c1 s) -> SParserEndSym ss sr pEnd -> ss s0 -> SNat a1 -> SList sr b1 -> ss c1 -> SResultEnd (SList sr) (CountEnd' pEnd s0 a1 b1 c1) forall {a} {k} (ss :: a -> Type) (sr :: k -> Type) (pEnd :: a ~> Either PE k) (s0 :: a) (n :: Nat) (rs :: [k]) (s :: a). SParserEndSym ss sr pEnd -> ss s0 -> SNat n -> SList sr rs -> ss s -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s) sCountEnd' SParserEndSym ss sr pEnd pEnd ss s0 s0 SNat a1 n SList sr b1 rs ss c1 s