{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying/singled parsers

module Symparsec.Run where -- ( Run, ERun(..) ) where

import Symparsec.Parser
import GHC.TypeLits hiding ( ErrorMessage(..), fromSNat )
import GHC.TypeNats ( fromSNat )
import GHC.TypeLits qualified as TE
import DeFun.Core
import TypeLevelShow.Doc
import TypeLevelShow.Utils ( ShowChar )
import TypeLevelShow.Natural ( ShowNatDec )
import Singleraeh.Tuple ( STuple2(..) )
import Singleraeh.Maybe ( SMaybe(..) )
import Singleraeh.Either ( SEither(..) )
import Singleraeh.Symbol
    ( sConsSymbol, sUnconsSymbol, ReconsSymbol, sReconsSymbol )
import Singleraeh.Natural ( (%+) )
import Singleraeh.Demote

-- | Run the given parser on the given 'Symbol', returning an 'TE.ErrorMessage'
--   on failure.
type Run :: PParser s r -> Symbol -> Either TE.ErrorMessage (r, Symbol)
type Run p sym = MapLeftRender (Run' p sym)

type MapLeftRender :: Either PERun r -> Either TE.ErrorMessage r
type family MapLeftRender eer where
    MapLeftRender (Right a) = Right a
    MapLeftRender (Left  e) = Left (RenderPDoc (PrettyERun e))

-- | Run the given parser on the given 'Symbol', returning a 'PERun' on failure.
type Run' :: PParser s r -> Symbol -> Either PERun (r, Symbol)
type family Run' p str where
    Run' ('PParser pCh pEnd s0) str =
        RunStart pCh pEnd s0 (UnconsSymbol str)

-- | Run the given parser on the given 'Symbol', emitting a type error on
--   failure.
--
-- This /would/ be useful for @:k!@ runs, but it doesn't work properly with
-- 'TE.TypeError's, printing @= (TypeError ...)@ instead of the error message.
-- Alas! Instead, do something like @> Proxy \@(RunTest ...)@.
type RunTest :: PParser s r -> Symbol -> (r, Symbol)
type RunTest p sym = MapLeftTypeError (Run p sym)

-- | Run the given parser on the given 'Symbol', returning a 'PERun' on failure,
--   and ignoring any remaining non-consumed characters.
type Run'_ :: PParser s r -> Symbol -> Either TE.ErrorMessage r
type Run'_ p str = Run'_Inner (Run' p str)

type Run'_Inner :: Either PERun (a, b) -> Either TE.ErrorMessage a
type family Run'_Inner eeab where
    Run'_Inner (Right '(a, b)) = Right a
    Run'_Inner (Left  e)       = Left (RenderPDoc (PrettyERun e))

-- | Run the singled version of type-level parser on the given 'String',
--   returning an 'ERun' on failure.
--
-- You must provide a function for demoting the singled return type.
-- ('Singleraeh.Demote.demote' can do this for you automatically.)
run'
    :: forall {s} {r} (p :: PParser s r) r'. SingParser p
    => (forall a. PR p a -> r') -> String -> Either (ERun String) (r', String)
run' :: forall {s} {r} (p :: PParser s r) r'.
SingParser p =>
(forall (a :: r). PR p a -> r')
-> String -> Either (ERun String) (r', String)
run' forall (a :: r). PR p a -> r'
demotePR String
str = String
-> (forall {s :: Symbol}.
    SSymbol s -> Either (ERun String) (r', String))
-> Either (ERun String) (r', String)
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
withSomeSSymbol String
str ((forall {s :: Symbol}.
  SSymbol s -> Either (ERun String) (r', String))
 -> Either (ERun String) (r', String))
-> (forall {s :: Symbol}.
    SSymbol s -> Either (ERun String) (r', String))
-> Either (ERun String) (r', String)
forall a b. (a -> b) -> a -> b
$ \SSymbol s
sstr ->
    case SParser (PS p) (PR p) p
-> SSymbol s -> SEither SERun (STuple2 (PR p) SSymbol) (Run' p s)
forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (p :: PParser s r) (str :: Symbol).
SParser ss sr p
-> SSymbol str -> SEither SERun (STuple2 sr SSymbol) (Run' p str)
sRun' (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) SSymbol s
sstr of
      SRight (STuple2 PR p a1
pr SSymbol b1
sstr') -> (r', String) -> Either (ERun String) (r', String)
forall a b. b -> Either a b
Right (PR p a1 -> r'
forall (a :: r). PR p a -> r'
demotePR PR p a1
pr, SSymbol b1 -> String
forall (s :: Symbol). SSymbol s -> String
fromSSymbol SSymbol b1
sstr')
      SLeft  SERun l1
e                  -> ERun String -> Either (ERun String) (r', String)
forall a b. a -> Either a b
Left (ERun String -> Either (ERun String) (r', String))
-> ERun String -> Either (ERun String) (r', String)
forall a b. (a -> b) -> a -> b
$ SERun l1 -> ERun String
forall (erun :: PERun). SERun erun -> ERun String
demoteSERun SERun l1
e

-- TODO prettify error. actually run' needs an error demoter :| such a pain
runTest
    :: forall {s} {r} (p :: PParser s r). (SingParser p, Demotable (PR p))
    => String -> (Demote (PR p), String)
runTest :: forall {s} {r} (p :: PParser s r).
(SingParser p, Demotable (PR p)) =>
String -> (Demote (PR p), String)
runTest String
str =
    case forall {s} {r} (p :: PParser s r) r'.
SingParser p =>
(forall (a :: r). PR p a -> r')
-> String -> Either (ERun String) (r', String)
forall (p :: PParser s r) r'.
SingParser p =>
(forall (a :: r). PR p a -> r')
-> String -> Either (ERun String) (r', String)
run' @p PR p a -> Demote (PR p)
forall (a :: r). PR p a -> Demote (PR p)
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote String
str of
      Right (Demote (PR p), String)
r -> (Demote (PR p), String)
r
      Left  ERun String
e -> String -> (Demote (PR p), String)
forall a. HasCallStack => String -> a
error (String -> (Demote (PR p), String))
-> String -> (Demote (PR p), String)
forall a b. (a -> b) -> a -> b
$ ERun String -> String
forall a. Show a => a -> String
show ERun String
e

sRun'
    :: SParser ss sr p
    -> SSymbol str
    -> SEither SERun (STuple2 sr SSymbol) (Run' p str)
sRun' :: forall {s} {r} (ss :: s -> Type) (sr :: r -> Type)
       (p :: PParser s r) (str :: Symbol).
SParser ss sr p
-> SSymbol str -> SEither SERun (STuple2 sr SSymbol) (Run' p str)
sRun' (SParser SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd ss s0
s0) SSymbol str
str =
    SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> ss s0
-> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)
-> SEither
     SERun
     (STuple2 sr SSymbol)
     (RunStart pCh pEnd s0 (UnconsSymbol str))
forall {a} {k} (ss :: a -> Type) (sr :: k -> Type)
       (pCh :: Char ~> (a ~> PResult a k)) (pEnd :: a ~> Either PE k)
       (s0 :: a) (mstr :: Maybe (Char, Symbol)).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> ss s0
-> SMaybe (STuple2 SChar SSymbol) mstr
-> SEither SERun (STuple2 sr SSymbol) (RunStart pCh pEnd s0 mstr)
sRunStart SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd ss s0
s0 (SSymbol str -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)
forall (str :: Symbol).
SSymbol str -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)
sUnconsSymbol SSymbol str
str)

type family RunStart pCh pEnd s0 mstr where
    RunStart pCh pEnd s0 (Just '(ch, str)) =
        RunCh pCh pEnd 0 ch (UnconsSymbol str) (pCh @@ ch @@ s0)

    RunStart pCh pEnd s0 Nothing =
        RunEnd0 (pEnd @@ s0)

sRunStart
    :: SParserChSym  ss sr pCh
    -> SParserEndSym ss sr pEnd
    -> ss s0
    -> SMaybe (STuple2 SChar SSymbol) mstr
    -> SEither SERun (STuple2 sr SSymbol) (RunStart pCh pEnd s0 mstr)
sRunStart :: forall {a} {k} (ss :: a -> Type) (sr :: k -> Type)
       (pCh :: Char ~> (a ~> PResult a k)) (pEnd :: a ~> Either PE k)
       (s0 :: a) (mstr :: Maybe (Char, Symbol)).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> ss s0
-> SMaybe (STuple2 SChar SSymbol) mstr
-> SEither SERun (STuple2 sr SSymbol) (RunStart pCh pEnd s0 mstr)
sRunStart SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd ss s0
s0 = \case
  SJust (STuple2 SChar a1
ch SSymbol b1
str) ->
    SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SNat 0
-> SChar a1
-> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol b1)
-> SResult ss sr (App (App pCh a1) s0)
-> SEither
     SERun
     (STuple2 sr SSymbol)
     (RunCh pCh pEnd 0 a1 (UnconsSymbol b1) (App (App pCh a1) s0))
forall {a} {r} (ss :: a -> Type) (sr :: r -> Type)
       (pCh :: Char ~> (a ~> PResult a r)) (pEnd :: a ~> Either PE r)
       (idx :: Nat) (chPrev :: Char) (mstr :: Maybe (Char, Symbol))
       (res :: PResult a r).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SNat idx
-> SChar chPrev
-> SMaybe (STuple2 SChar SSymbol) mstr
-> SResult ss sr res
-> SEither
     SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)
sRunCh SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd (forall (n :: Nat). KnownNat n => SNat n
SNat @0) SChar a1
ch (SSymbol b1 -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol b1)
forall (str :: Symbol).
SSymbol str -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)
sUnconsSymbol SSymbol b1
str) (SParserChSym ss sr pCh
pCh SParserChSym ss sr pCh
-> SChar a1 -> Lam ss (SResult ss sr) (App pCh a1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar a1
ch Lam ss (SResult ss sr) (App pCh a1)
-> ss s0 -> SResult ss sr (App (App pCh a1) s0)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss s0
s0)
  SMaybe (STuple2 SChar SSymbol) mstr
SNothing -> SEither SE sr (App pEnd s0)
-> SEither SERun (STuple2 sr SSymbol) (RunEnd0 (App pEnd s0))
forall {k} (sr :: k -> Type) (res :: Either PE k).
SEither SE sr res
-> SEither SERun (STuple2 sr SSymbol) (RunEnd0 res)
sRunEnd0 (SParserEndSym ss sr pEnd
pEnd SParserEndSym ss sr pEnd -> ss s0 -> SEither SE sr (App pEnd s0)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss s0
s0)

type MapLeftTypeError :: Either TE.ErrorMessage a -> a
type family MapLeftTypeError eea where
    MapLeftTypeError (Right a) = a
    MapLeftTypeError (Left  e) = TE.TypeError e

-- | Inspect character parser result.
--
-- This is purposely written so that the main case is at the top, and a single
-- equation (we parse, prepare next character and inspect character parser
-- result at the same time). My hope is that this keeps GHC fast.
type family RunCh pCh pEnd idx ch' mstr res where
    -- | OK, and more to come: parse next character
    RunCh pCh pEnd idx ch' (Just '(ch, sym)) (Cont s) =
        RunCh pCh pEnd (idx+1) ch (UnconsSymbol sym) (pCh @@ ch @@ s)

    -- | OK, and we're at the end of the string: run end parser
    RunCh pCh pEnd idx ch' Nothing           (Cont s) =
        RunEnd idx ch' (pEnd @@ s)

    -- | OK, and we're finished early: return value and remaining string
    RunCh pCh pEnd idx ch' mstr              (Done r) =
        Right '(r, ConsSymbol ch' (ReconsSymbol mstr))

    -- | Parse error: return error
    RunCh pCh pEnd idx ch' mstr              (Err  e) =
        Left ('ERun idx ch' e)

sRunCh
    :: SParserChSym  ss sr pCh
    -> SParserEndSym ss sr pEnd
    -> SNat idx
    -> SChar chPrev
    -> SMaybe (STuple2 SChar SSymbol) mstr
    -> SResult ss sr res
    -> SEither SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)
sRunCh :: forall {a} {r} (ss :: a -> Type) (sr :: r -> Type)
       (pCh :: Char ~> (a ~> PResult a r)) (pEnd :: a ~> Either PE r)
       (idx :: Nat) (chPrev :: Char) (mstr :: Maybe (Char, Symbol))
       (res :: PResult a r).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SNat idx
-> SChar chPrev
-> SMaybe (STuple2 SChar SSymbol) mstr
-> SResult ss sr res
-> SEither
     SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)
sRunCh SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd SNat idx
idx SChar chPrev
chPrev SMaybe (STuple2 SChar SSymbol) mstr
mstr = \case
  SCont ss s1
s ->
    case SMaybe (STuple2 SChar SSymbol) mstr
mstr of
      SJust (STuple2 SChar a1
ch SSymbol b1
str) ->
        SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SNat (idx + 1)
-> SChar a1
-> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol b1)
-> SResult ss sr (App (App pCh a1) s1)
-> SEither
     SERun
     (STuple2 sr SSymbol)
     (RunCh
        pCh pEnd (idx + 1) a1 (UnconsSymbol b1) (App (App pCh a1) s1))
forall {a} {r} (ss :: a -> Type) (sr :: r -> Type)
       (pCh :: Char ~> (a ~> PResult a r)) (pEnd :: a ~> Either PE r)
       (idx :: Nat) (chPrev :: Char) (mstr :: Maybe (Char, Symbol))
       (res :: PResult a r).
SParserChSym ss sr pCh
-> SParserEndSym ss sr pEnd
-> SNat idx
-> SChar chPrev
-> SMaybe (STuple2 SChar SSymbol) mstr
-> SResult ss sr res
-> SEither
     SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)
sRunCh SParserChSym ss sr pCh
pCh SParserEndSym ss sr pEnd
pEnd (SNat idx
idx SNat idx -> SNat 1 -> SNat (idx + 1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ (forall (n :: Nat). KnownNat n => SNat n
SNat @1)) SChar a1
ch (SSymbol b1 -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol b1)
forall (str :: Symbol).
SSymbol str -> SMaybe (STuple2 SChar SSymbol) (UnconsSymbol str)
sUnconsSymbol SSymbol b1
str)
            (SParserChSym ss sr pCh
pCh SParserChSym ss sr pCh
-> SChar a1 -> Lam ss (SResult ss sr) (App pCh a1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ SChar a1
ch Lam ss (SResult ss sr) (App pCh a1)
-> ss s1 -> SResult ss sr (App (App pCh a1) s1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss s1
s)
      SMaybe (STuple2 SChar SSymbol) mstr
SNothing ->
        SNat idx
-> SChar chPrev
-> SEither SE sr (App pEnd s1)
-> SEither
     SERun (STuple2 sr SSymbol) (RunEnd idx chPrev (App pEnd s1))
forall {r} (idx :: Nat) (ch :: Char) (sr :: r -> Type)
       (res :: Either PE r).
SNat idx
-> SChar ch
-> SEither SE sr res
-> SEither SERun (STuple2 sr SSymbol) (RunEnd idx ch res)
sRunEnd SNat idx
idx SChar chPrev
chPrev (SParserEndSym ss sr pEnd
pEnd SParserEndSym ss sr pEnd -> ss s1 -> SEither SE sr (App pEnd s1)
forall {a1} {k} (a2 :: a1 -> Type) (b :: k -> Type) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ ss s1
s)
  SDone sr r1
r -> STuple2 sr SSymbol '(r1, ConsSymbol chPrev (ReconsSymbol mstr))
-> SEither
     SERun
     (STuple2 sr SSymbol)
     ('Right '(r1, ConsSymbol chPrev (ReconsSymbol mstr)))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (sr r1
-> SSymbol (ConsSymbol chPrev (ReconsSymbol mstr))
-> STuple2 sr SSymbol '(r1, ConsSymbol chPrev (ReconsSymbol mstr))
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 sr r1
r (SChar chPrev
-> SSymbol (ReconsSymbol mstr)
-> SSymbol (ConsSymbol chPrev (ReconsSymbol mstr))
forall (ch :: Char) (str :: Symbol).
SChar ch -> SSymbol str -> SSymbol (ConsSymbol ch str)
sConsSymbol SChar chPrev
chPrev (SMaybe (STuple2 SChar SSymbol) mstr -> SSymbol (ReconsSymbol mstr)
forall (msym :: Maybe (Char, Symbol)).
SMaybe (STuple2 SChar SSymbol) msym -> SSymbol (ReconsSymbol msym)
sReconsSymbol SMaybe (STuple2 SChar SSymbol) mstr
mstr)))
  SErr  SE e
e -> SERun ('ERun idx chPrev e)
-> SEither SERun (STuple2 sr SSymbol) ('Left ('ERun idx chPrev e))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SNat idx -> SChar chPrev -> SE e -> SERun ('ERun idx chPrev e)
forall (e :: Nat) (ch :: Char) (e :: PE).
SNat e -> SChar ch -> SE e -> SERun ('ERun e ch e)
SERun SNat idx
idx SChar chPrev
chPrev SE e
e)

-- | Inspect end parser result.
type RunEnd
    :: Natural -> Char
    -> Either PE r
    -> Either PERun (r, Symbol)
type family RunEnd idx ch res where
    RunEnd idx ch (Right r) = Right '(r, "")
    RunEnd idx ch (Left  e) = Left ('ERun idx ch e)

sRunEnd
    :: SNat idx -> SChar ch
    -> SEither SE sr res
    -> SEither SERun (STuple2 sr SSymbol) (RunEnd idx ch res)
sRunEnd :: forall {r} (idx :: Nat) (ch :: Char) (sr :: r -> Type)
       (res :: Either PE r).
SNat idx
-> SChar ch
-> SEither SE sr res
-> SEither SERun (STuple2 sr SSymbol) (RunEnd idx ch res)
sRunEnd SNat idx
idx SChar ch
ch = \case
  SRight sr r1
r -> STuple2 sr SSymbol '(r1, "")
-> SEither SERun (STuple2 sr SSymbol) ('Right '(r1, ""))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (sr r1 -> SSymbol "" -> STuple2 sr SSymbol '(r1, "")
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 sr r1
r (forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol @""))
  SLeft  SE l1
e -> SERun ('ERun idx ch l1)
-> SEither SERun (STuple2 sr SSymbol) ('Left ('ERun idx ch l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SNat idx -> SChar ch -> SE l1 -> SERun ('ERun idx ch l1)
forall (e :: Nat) (ch :: Char) (e :: PE).
SNat e -> SChar ch -> SE e -> SERun ('ERun e ch e)
SERun SNat idx
idx SChar ch
ch SE l1
e)

-- | Inspect end parser result for the empty string, where we have no previous
--   character or (meaningful) index.
type family RunEnd0 res where
    RunEnd0 (Right r) = Right '(r, "")
    RunEnd0 (Left  e) = Left (ERun0 e)

sRunEnd0
    :: SEither SE sr res
    -> SEither SERun (STuple2 sr SSymbol) (RunEnd0 res)
sRunEnd0 :: forall {k} (sr :: k -> Type) (res :: Either PE k).
SEither SE sr res
-> SEither SERun (STuple2 sr SSymbol) (RunEnd0 res)
sRunEnd0 = \case
  SRight sr r1
r -> STuple2 sr SSymbol '(r1, "")
-> SEither SERun (STuple2 sr SSymbol) ('Right '(r1, ""))
forall {r} {l} (sr :: r -> Type) (r1 :: r) (sl :: l -> Type).
sr r1 -> SEither sl sr ('Right r1)
SRight (sr r1 -> SSymbol "" -> STuple2 sr SSymbol '(r1, "")
forall {a} {b} (sa :: a -> Type) (a1 :: a) (sb :: b -> Type)
       (b1 :: b).
sa a1 -> sb b1 -> STuple2 sa sb '(a1, b1)
STuple2 sr r1
r (forall (s :: Symbol). KnownSymbol s => SSymbol s
SSymbol @""))
  SLeft  SE l1
e -> SERun ('ERun0 l1)
-> SEither SERun (STuple2 sr SSymbol) ('Left ('ERun0 l1))
forall {l} {r} (sl :: l -> Type) (l1 :: l) (sr :: r -> Type).
sl l1 -> SEither sl sr ('Left l1)
SLeft (SE l1 -> SERun ('ERun0 l1)
forall (e :: PE). SE e -> SERun ('ERun0 e)
SERun0 SE l1
e)

type PrettyERun :: PERun -> PDoc
type family PrettyERun e where
    PrettyERun (ERun0 e) = Text "parse error on empty string" :$$: PrettyE e
    PrettyERun ('ERun idx ch e) =
             Text "parse error at index " :<>: Text (ShowNatDec idx)
        :<>: Text ", char '" :<>: Text (ShowChar ch) :<>: Text "'"
        :$$: PrettyE e

type PrettyE :: PE -> PDoc
type family PrettyE e where
    PrettyE (EBase name emsg)  = Text name :<>: Text ": " :<>: emsg
    PrettyE (EIn   name e)     = Text name :<>: Text ": " :<>: PrettyE e

-- | Error while running parser.
data ERun s
  -- | Parser error at index X, character C.
  = ERun Natural Char (E s)

  -- | Parser error on the empty string.
  | ERun0 (E s)
    deriving stock Int -> ERun s -> ShowS
[ERun s] -> ShowS
ERun s -> String
(Int -> ERun s -> ShowS)
-> (ERun s -> String) -> ([ERun s] -> ShowS) -> Show (ERun s)
forall s. Show s => Int -> ERun s -> ShowS
forall s. Show s => [ERun s] -> ShowS
forall s. Show s => ERun s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall s. Show s => Int -> ERun s -> ShowS
showsPrec :: Int -> ERun s -> ShowS
$cshow :: forall s. Show s => ERun s -> String
show :: ERun s -> String
$cshowList :: forall s. Show s => [ERun s] -> ShowS
showList :: [ERun s] -> ShowS
Show

-- | Promoted 'ERun'.
type PERun = ERun Symbol

data SERun (erun :: PERun) where
    SERun  :: SNat idx -> SChar ch -> SE e -> SERun ('ERun idx ch e)
    SERun0 ::                         SE e -> SERun (ERun0 e)

demoteSERun :: SERun erun -> ERun String
demoteSERun :: forall (erun :: PERun). SERun erun -> ERun String
demoteSERun = \case
  SERun  SNat idx
idx SChar ch
ch SE e
e -> Nat -> Char -> E String -> ERun String
forall s. Nat -> Char -> E s -> ERun s
ERun  (SNat idx -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat idx
idx) (SChar ch -> Char
forall (c :: Char). SChar c -> Char
fromSChar SChar ch
ch) (SE e -> E String
forall (e :: PE). SE e -> E String
demoteSE SE e
e)
  SERun0        SE e
e -> E String -> ERun String
forall s. E s -> ERun s
ERun0                               (SE e -> E String
forall (e :: PE). SE e -> E String
demoteSE SE e
e)

instance Demotable SERun where
    type Demote SERun = ERun String
    demote :: forall (k1 :: PERun). SERun k1 -> Demote SERun
demote = SERun k1 -> Demote SERun
SERun k1 -> ERun String
forall (erun :: PERun). SERun erun -> ERun String
demoteSERun