{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Symparsec.Run 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
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))
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)
type RunTest :: PParser s r -> Symbol -> (r, Symbol)
type RunTest p sym = MapLeftTypeError (Run p sym)
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'
:: 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
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
type family RunCh pCh pEnd idx ch' mstr res where
RunCh pCh pEnd idx ch' (Just '(ch, sym)) (Cont s) =
RunCh pCh pEnd (idx+1) ch (UnconsSymbol sym) (pCh @@ ch @@ s)
RunCh pCh pEnd idx ch' Nothing (Cont s) =
RunEnd idx ch' (pEnd @@ s)
RunCh pCh pEnd idx ch' mstr (Done r) =
Right '(r, ConsSymbol ch' (ReconsSymbol mstr))
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)
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)
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
data ERun s
= ERun Natural Char (E s)
| 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
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