{-# 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