{-# LANGUAGE UndecidableInstances #-}

module Symparsec.Parser.Isolate where

import Symparsec.Parser.Common
import GHC.TypeLits hiding ( ErrorMessage(..) )
import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )
import DeFun.Core
import Singleraeh.Either
import Singleraeh.Tuple
import Singleraeh.Equality ( testEqElse )
import Singleraeh.Natural ( (%-) )
import Unsafe.Coerce ( unsafeCoerce )
import Data.Type.Equality

-- | Run the given parser isolated to the next @n@ characters.
--
-- All isolated characters must be consumed.
type Isolate :: Natural -> PParser s r -> PParser (Natural, s) r
type family Isolate n p where
    Isolate n ('PParser pCh pEnd s0) = Isolate' n pCh pEnd s0

-- unwrapped for instances
type Isolate' n pCh pEnd s0 = 'PParser
    (IsolateChSym pCh pEnd)
    (IsolateEndSym pEnd)
    '(n, s0)

type SIsolateS ss = STuple2 SNat ss

sIsolate
    :: SNat n
    -> SParser ss sr p
    -> SParser (SIsolateS ss) sr (Isolate n p)
sIsolate :: forall {s} {r} (n :: Nat) (ss :: s -> Type) (sr :: r -> Type)
       (p :: PParser s r).
SNat n
-> SParser ss sr p -> SParser (SIsolateS ss) sr (Isolate n p)
sIsolate SNat n
n (SParser SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd ss s0
s0) = SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
-> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
-> SIsolateS ss '(n, s0)
-> SParser
     (SIsolateS ss)
     sr
     ('PParser (IsolateChSym pCh pEnd) (IsolateEndSym pEnd) '(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
-> SParserEndSym ss sr pEnd
-> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pCh :: Char ~> (s ~> PResult s r)) (pEnd :: s ~> Either PE r).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
sIsolateChSym SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd)
    (SParserEndSym ss sr pEnd
-> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pEnd :: s ~> Either PE r).
SParserEndSym ss sr pEnd
-> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
sIsolateEndSym SParserEndSym ss sr pEnd
pEnd)
    (SNat n -> ss s0 -> SIsolateS ss '(n, s0)
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 SNat n
n ss s0
s0)

instance
  ( p ~ 'PParser pCh pEnd s0
  , KnownNat n, SingParser p
  ) => SingParser (Isolate' n pCh pEnd s0) where
    type PS (Isolate' n pCh pEnd s0) =
        SIsolateS (PS ('PParser pCh pEnd s0))
    type PR (Isolate' n pCh pEnd s0) =
        PR ('PParser pCh pEnd s0)
    singParser' :: SParser
  (PS (Isolate' n pCh pEnd s0))
  (PR (Isolate' n pCh pEnd s0))
  (Isolate' n pCh pEnd s0)
singParser' = SNat n
-> SParser
     (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0)) p
-> SParser
     (SIsolateS (PS ('PParser pCh pEnd s0)))
     (PR ('PParser pCh pEnd s0))
     (Isolate n p)
forall {s} {r} (n :: Nat) (ss :: s -> Type) (sr :: r -> Type)
       (p :: PParser s r).
SNat n
-> SParser ss sr p -> SParser (SIsolateS ss) sr (Isolate n p)
sIsolate (forall (n :: Nat). KnownNat n => SNat n
natSing @n) (forall {s} {r} (p :: PParser s r).
SingParser p =>
SParser (PS p) (PR p) p
forall (p :: PParser s r). SingParser p => SParser (PS p) (PR p) p
singParser @p)

type IsolateCh
    :: ParserChSym s r
    -> ParserEndSym s r
    -> PParserCh (Natural, s) r
type family IsolateCh pCh pEnd ch s where
    IsolateCh pCh pEnd ch '(0, s) = IsolateInnerEnd (pEnd @@ s)
    IsolateCh pCh pEnd ch '(n, s) = IsolateInner n (pCh @@ ch @@ s)

sIsolateChSym
    :: SParserChSym  ss sr pCh
    -> SParserEndSym ss sr pEnd
    -> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
sIsolateChSym :: forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pCh :: Char ~> (s ~> PResult s r)) (pEnd :: s ~> Either PE r).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)
sIsolateChSym SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd = LamRep2
  SChar
  (SIsolateS ss)
  (SResult (SIsolateS ss) sr)
  (IsolateChSym pCh pEnd)
-> Lam2
     SChar
     (SIsolateS ss)
     (SResult (SIsolateS ss) sr)
     (IsolateChSym pCh pEnd)
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
   (SIsolateS ss)
   (SResult (SIsolateS ss) sr)
   (IsolateChSym pCh pEnd)
 -> Lam2
      SChar
      (SIsolateS ss)
      (SResult (SIsolateS ss) sr)
      (IsolateChSym pCh pEnd))
-> LamRep2
     SChar
     (SIsolateS ss)
     (SResult (SIsolateS ss) sr)
     (IsolateChSym pCh pEnd)
-> Lam2
     SChar
     (SIsolateS ss)
     (SResult (SIsolateS ss) sr)
     (IsolateChSym pCh pEnd)
forall a b. (a -> b) -> a -> b
$ \SChar x
ch (STuple2 SNat a1
n ss b1
s) ->
    case SNat a1 -> SNat 0 -> Maybe (a1 :~: 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 a1
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) of
      Just a1 :~: 0
Refl ->
        case SParserEndSym ss sr pEnd
pEnd SParserEndSym ss sr pEnd -> ss b1 -> SResultEnd sr (pEnd @@ b1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss b1
s of
          SRight sr r1
r -> sr r1 -> SResult (SIsolateS ss) sr ('Done r1)
forall {r} {s} (sr :: r -> Type) (r1 :: r) (ss :: s -> Type).
sr r1 -> SResult ss sr ('Done r1)
SDone sr r1
r
          SLeft  SE l1
e -> SE (EIsolateWrap l1)
-> SResult (SIsolateS ss) sr ('Err (EIsolateWrap l1))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr (SE (EIsolateWrap l1)
 -> SResult (SIsolateS ss) sr ('Err (EIsolateWrap l1)))
-> SE (EIsolateWrap l1)
-> SResult (SIsolateS ss) sr ('Err (EIsolateWrap l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EIsolateWrap l1)
forall (e :: PE). SE e -> SE (EIsolateWrap e)
eIsolateWrap SE l1
e
      Maybe (a1 :~: 0)
Nothing -> SResult (SIsolateS ss) sr (IsolateInner a1 (App (App pCh x) b1))
-> SResult (SIsolateS ss) sr ((IsolateChSym pCh pEnd @@ x) @@ y)
forall a b. a -> b
unsafeCoerce (SResult (SIsolateS ss) sr (IsolateInner a1 (App (App pCh x) b1))
 -> SResult (SIsolateS ss) sr ((IsolateChSym pCh pEnd @@ x) @@ y))
-> SResult (SIsolateS ss) sr (IsolateInner a1 (App (App pCh x) b1))
-> SResult (SIsolateS ss) sr ((IsolateChSym pCh pEnd @@ x) @@ y)
forall a b. (a -> b) -> a -> b
$ SNat a1
-> SResult ss sr (App (App pCh x) b1)
-> SResult (SIsolateS ss) sr (IsolateInner a1 (App (App pCh x) b1))
forall {s} {r} (n :: Nat) (ss :: s -> Type) (sr :: r -> Type)
       (res :: PResult s r).
SNat n
-> SResult ss sr res
-> SResult (SIsolateS ss) sr (IsolateInner n res)
sIsolateInner SNat a1
n (SParserChSym ss sr pCh
pCh SParserChSym ss sr pCh
-> SChar x -> Lam ss (SResult ss sr) (App pCh 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 ss (SResult ss sr) (App pCh x)
-> ss b1 -> SResult ss sr (App (App pCh 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)
@@ ss b1
s)

type IsolateInnerEnd :: Either PE r -> PResult (Natural, s) r
type family IsolateInnerEnd a where
    IsolateInnerEnd (Right r) = Done r
    IsolateInnerEnd (Left  e) = Err  (EIsolateWrap e)

type IsolateInner :: Natural -> PResult s r -> PResult (Natural, s) r
type family IsolateInner n res where
    IsolateInner n (Cont s) = Cont '(n-1, s)
    IsolateInner n (Done _) = Err (EIsolateRemaining n)
    IsolateInner _ (Err  e) = Err (EIsolateWrap e)

sIsolateInner
    :: SNat n
    -> SResult ss sr res
    -> SResult (SIsolateS ss) sr (IsolateInner n res)
sIsolateInner :: forall {s} {r} (n :: Nat) (ss :: s -> Type) (sr :: r -> Type)
       (res :: PResult s r).
SNat n
-> SResult ss sr res
-> SResult (SIsolateS ss) sr (IsolateInner n res)
sIsolateInner SNat n
n = \case
  SCont  ss s1
s -> SIsolateS ss '(n - 1, s1)
-> SResult (SIsolateS ss) sr ('Cont '(n - 1, s1))
forall {s} {r} (ss :: s -> Type) (s1 :: s) (sr :: r -> Type).
ss s1 -> SResult ss sr ('Cont s1)
SCont (SIsolateS ss '(n - 1, s1)
 -> SResult (SIsolateS ss) sr ('Cont '(n - 1, s1)))
-> SIsolateS ss '(n - 1, s1)
-> SResult (SIsolateS ss) sr ('Cont '(n - 1, s1))
forall a b. (a -> b) -> a -> b
$ SNat (n - 1) -> ss s1 -> SIsolateS ss '(n - 1, s1)
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 (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)) ss s1
s
  SDone sr r1
_r -> SE
  ('EBase
     "Isolate"
     (('Text "isolated parser ended without consuming all input ("
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " remaining)"))
-> SResult
     (SIsolateS ss)
     sr
     ('Err
        ('EBase
           "Isolate"
           (('Text "isolated parser ended without consuming all input ("
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
            ':<>: 'Text " remaining)")))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE
   ('EBase
      "Isolate"
      (('Text "isolated parser ended without consuming all input ("
        ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
       ':<>: 'Text " remaining)"))
 -> SResult
      (SIsolateS ss)
      sr
      ('Err
         ('EBase
            "Isolate"
            (('Text "isolated parser ended without consuming all input ("
              ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
             ':<>: 'Text " remaining)"))))
-> SE
     ('EBase
        "Isolate"
        (('Text "isolated parser ended without consuming all input ("
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
         ':<>: 'Text " remaining)"))
-> SResult
     (SIsolateS ss)
     sr
     ('Err
        ('EBase
           "Isolate"
           (('Text "isolated parser ended without consuming all input ("
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
            ':<>: 'Text " remaining)")))
forall a b. (a -> b) -> a -> b
$ SNat n
-> SE
     ('EBase
        "Isolate"
        (('Text "isolated parser ended without consuming all input ("
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
         ':<>: 'Text " remaining)"))
forall (n :: Nat). SNat n -> SE (EIsolateRemaining n)
eIsolateRemaining SNat n
n
  SErr   SE e
e -> SE (EIsolateWrap e)
-> SResult (SIsolateS ss) sr ('Err (EIsolateWrap e))
forall {s} {r} (e :: PE) (ss :: s -> Type) (sr :: r -> Type).
SE e -> SResult ss sr ('Err e)
SErr  (SE (EIsolateWrap e)
 -> SResult (SIsolateS ss) sr ('Err (EIsolateWrap e)))
-> SE (EIsolateWrap e)
-> SResult (SIsolateS ss) sr ('Err (EIsolateWrap e))
forall a b. (a -> b) -> a -> b
$ SE e -> SE (EIsolateWrap e)
forall (e :: PE). SE e -> SE (EIsolateWrap e)
eIsolateWrap SE e
e

type IsolateEnd :: ParserEndSym s r -> PParserEnd (Natural, s) r
type family IsolateEnd pEnd s where
    IsolateEnd pEnd '(0, s) = IsolateEnd' (pEnd @@ s)
    -- ^ will only occur on @Isolate 0@
    IsolateEnd pEnd '(n, s) = Left (EIsolateEndN n)

sIsolateEndSym
    :: SParserEndSym ss sr pEnd
    -> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
sIsolateEndSym :: forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (pEnd :: s ~> Either PE r).
SParserEndSym ss sr pEnd
-> SParserEndSym (SIsolateS ss) sr (IsolateEndSym pEnd)
sIsolateEndSym SParserEndSym ss sr pEnd
pEnd = LamRep (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd)
-> Lam (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd)
forall a b (a1 :: a -> Type) (b1 :: b -> Type) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (LamRep (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd)
 -> Lam (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd))
-> LamRep (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd)
-> Lam (SIsolateS ss) (SResultEnd sr) (IsolateEndSym pEnd)
forall a b. (a -> b) -> a -> b
$ \(STuple2 SNat a1
n ss b1
s) ->
      SNat a1
-> SNat 0
-> ((a1 ~ 0) => SResultEnd sr (IsolateEndSym pEnd @@ x))
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
forall {k} (f :: k -> Type) (a :: k) (b :: k) r.
TestEquality f =>
f a -> f b -> ((a ~ b) => r) -> r -> r
testEqElse SNat a1
n (forall (n :: Nat). KnownNat n => SNat n
SNat @0) (SResultEnd sr (App pEnd b1)
-> SResultEnd sr (IsolateEnd' (App pEnd b1))
forall {r} (sr :: r -> Type) (res :: Either PE r).
SResultEnd sr res -> SResultEnd sr (IsolateEnd' res)
sIsolateEnd' (SParserEndSym ss sr pEnd
pEnd SParserEndSym ss sr pEnd -> ss b1 -> SResultEnd sr (App pEnd b1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss b1
s))
    (SResultEnd sr (IsolateEndSym pEnd @@ x)
 -> SResultEnd sr (IsolateEndSym pEnd @@ x))
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
forall a b. (a -> b) -> a -> b
$ SEither
  SE
  Any
  ('Left
     ('EBase
        "Isolate"
        (('Text "tried to isolate more than present (needed "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " more)")))
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
forall a b. a -> b
unsafeCoerce (SEither
   SE
   Any
   ('Left
      ('EBase
         "Isolate"
         (('Text "tried to isolate more than present (needed "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
          ':<>: 'Text " more)")))
 -> SResultEnd sr (IsolateEndSym pEnd @@ x))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Isolate"
           (('Text "tried to isolate more than present (needed "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " more)")))
-> SResultEnd sr (IsolateEndSym pEnd @@ x)
forall a b. (a -> b) -> a -> b
$ SE
  ('EBase
     "Isolate"
     (('Text "tried to isolate more than present (needed "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
      ':<>: 'Text " more)"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Isolate"
           (('Text "tried to isolate more than present (needed "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " more)")))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE
   ('EBase
      "Isolate"
      (('Text "tried to isolate more than present (needed "
        ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
       ':<>: 'Text " more)"))
 -> SEither
      SE
      Any
      ('Left
         ('EBase
            "Isolate"
            (('Text "tried to isolate more than present (needed "
              ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
             ':<>: 'Text " more)"))))
-> SE
     ('EBase
        "Isolate"
        (('Text "tried to isolate more than present (needed "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " more)"))
-> SEither
     SE
     Any
     ('Left
        ('EBase
           "Isolate"
           (('Text "tried to isolate more than present (needed "
             ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
            ':<>: 'Text " more)")))
forall a b. (a -> b) -> a -> b
$ SNat a1
-> SE
     ('EBase
        "Isolate"
        (('Text "tried to isolate more than present (needed "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym a1))
         ':<>: 'Text " more)"))
forall (n :: Nat). SNat n -> SE (EIsolateEndN n)
eIsolateEndN SNat a1
n

type IsolateEnd' :: Either PE r -> Either PE r
type family IsolateEnd' res where
    IsolateEnd' (Right r) = Right r
    IsolateEnd' (Left  e) = Left (EIsolateWrap e)

sIsolateEnd'
    :: SResultEnd sr res
    -> SResultEnd sr (IsolateEnd' res)
sIsolateEnd' :: forall {r} (sr :: r -> Type) (res :: Either PE r).
SResultEnd sr res -> SResultEnd sr (IsolateEnd' res)
sIsolateEnd' = \case
  SRight sr r1
r -> sr r1 -> SEither SE sr ('Right r1)
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight sr r1
r
  SLeft  SE l1
e -> SE (EIsolateWrap l1) -> SEither SE sr ('Left (EIsolateWrap l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft  (SE (EIsolateWrap l1) -> SEither SE sr ('Left (EIsolateWrap l1)))
-> SE (EIsolateWrap l1) -> SEither SE sr ('Left (EIsolateWrap l1))
forall a b. (a -> b) -> a -> b
$ SE l1 -> SE (EIsolateWrap l1)
forall (e :: PE). SE e -> SE (EIsolateWrap e)
eIsolateWrap SE l1
e

type IsolateEndSym :: ParserEndSym s r -> ParserEndSym (Natural, s) r
data IsolateEndSym pEnd s
type instance App (IsolateEndSym pEnd) s = IsolateEnd pEnd s

type IsolateChSym
    :: ParserChSym s r
    -> ParserEndSym s r
    -> ParserChSym (Natural, s) r
data IsolateChSym pCh pEnd f
type instance App (IsolateChSym pCh pEnd) f = IsolateChSym1 pCh pEnd f

type IsolateChSym1
    :: ParserChSym s r
    -> ParserEndSym s r
    -> Char -> (Natural, s) ~> PResult (Natural, s) r
data IsolateChSym1 pCh pEnd ch s
type instance App (IsolateChSym1 pCh pEnd ch) s = IsolateCh pCh pEnd ch s

type EIsolateWrap e = EIn "Isolate" e

eIsolateWrap :: SE e -> SE (EIsolateWrap e)
eIsolateWrap :: forall (e :: PE). SE e -> SE (EIsolateWrap e)
eIsolateWrap SE e
e = SE e -> (SingE e => SE (EIsolateWrap e)) -> SE (EIsolateWrap e)
forall (e :: PE) r. SE e -> (SingE e => r) -> r
withSingE SE e
e SE (EIsolateWrap e)
SingE e => SE (EIsolateWrap e)
forall (e :: PE). SingE e => SE e
singE

type EIsolateEndN n = EBase "Isolate"
    (      Text "tried to isolate more than present (needed "
      :<>: Text (ShowNatDec n) :<>: Text " more)" )

eIsolateEndN :: SNat n -> SE (EIsolateEndN n)
eIsolateEndN :: forall (n :: Nat). SNat n -> SE (EIsolateEndN n)
eIsolateEndN SNat n
n = SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
-> (KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
    SE
      ('EBase
         "Isolate"
         (('Text "tried to isolate more than present (needed "
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
          ':<>: 'Text " more)")))
-> SE
     ('EBase
        "Isolate"
        (('Text "tried to isolate more than present (needed "
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
         ':<>: 'Text " more)"))
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol (SNat n -> SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatDec SNat n
n) SE
  ('EBase
     "Isolate"
     (('Text "tried to isolate more than present (needed "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " more)"))
KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
SE
  ('EBase
     "Isolate"
     (('Text "tried to isolate more than present (needed "
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " more)"))
forall (e :: PE). SingE e => SE e
singE

type EIsolateRemaining n = EBase "Isolate"
    (      Text "isolated parser ended without consuming all input ("
      :<>: Text (ShowNatDec n) :<>: Text " remaining)" )

eIsolateRemaining :: SNat n -> SE (EIsolateRemaining n)
eIsolateRemaining :: forall (n :: Nat). SNat n -> SE (EIsolateRemaining n)
eIsolateRemaining SNat n
n = SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
-> (KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
    SE
      ('EBase
         "Isolate"
         (('Text "isolated parser ended without consuming all input ("
           ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
          ':<>: 'Text " remaining)")))
-> SE
     ('EBase
        "Isolate"
        (('Text "isolated parser ended without consuming all input ("
          ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
         ':<>: 'Text " remaining)"))
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol (SNat n -> SSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n)
forall (n :: Nat). SNat n -> SSymbol (ShowNatDec n)
sShowNatDec SNat n
n) SE
  ('EBase
     "Isolate"
     (('Text "isolated parser ended without consuming all input ("
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " remaining)"))
KnownSymbol (ShowNatBase 10 ShowNatDigitHexLowerSym n) =>
SE
  ('EBase
     "Isolate"
     (('Text "isolated parser ended without consuming all input ("
       ':<>: 'Text (ShowNatBase 10 ShowNatDigitHexLowerSym n))
      ':<>: 'Text " remaining)"))
forall (e :: PE). SingE e => SE e
singE