packages feed

symparsec 0.4.0 → 1.0.0

raw patch · 20 files changed

+1383/−691 lines, 20 filesdep +singleraehdep +type-level-showdep ~base

Dependencies added: singleraeh, type-level-show

Dependency ranges changed: base

Files

CHANGELOG.md view
@@ -1,3 +1,8 @@+## 1.0.0 (2024-05-25)+* small rewrite, changing how `Done` works (now non-consuming)+* single all parsers+  * ...except `:<|>:`, which is disabled for now due to complexity+ ## 0.4.0 (2024-05-12) * rebrand from symbol-parser to Symparsec * rename `Drop` -> `Skip` (more commonly used for monadic parsers)
README.md view
@@ -1,15 +1,19 @@ # Symparsec-Type level string (`Symbol`) parser combinators.+Type level string (`Symbol`) parser combinators. Reify to runtime parsers with+guaranteed identical behaviour. -It's a Parsec for `Symbol`s; thus, Symparsec.+It's a Parsec-like for `Symbol`s; thus, Symparsec.  Previously named symbol-parser. +Requires GHC 9.6 for singling parsers.+ ## Features * Define parsers compositionally, largely as you would on the term level. * Pretty parse errors. * Hopefully decent performance.-* No runtime cost (you shall find no term level code here).+* Reify parsers to term level with guaranteed identical behaviour via a+  healthy dose of singletons.  ## Examples ```haskell@@ -26,81 +30,34 @@ level instead. Catch bugs earlier, get faster runtime.  ## Design-### Parser basics-[hackage-defun-core]: https://hackage.haskell.org/package/defun-core-[hackage-symbols]: https://hackage.haskell.org/package/symbols--_(Note that I may omit "type-level" when referring to type-level operations.)_--Until GHC 9.2, `Symbol`s were largely opaque. You could get them, but you-couldn't _decompose_ them like you could `String`s with `uncons :: [a] -> Maybe-(a, [a])`. Some Haskellers took this as a challenge (see-[symbols][hackage-symbols]). But realistically, we needed a bit more compiler-support.--As of GHC 9.2, `Symbol`s may be decomposed via `UnconsSymbol :: Symbol -> Maybe-(Char, Symbol)`. We thus design a `Char`-based parser:--```haskell-type ParserCh s r = Char -> s -> Result s r-data Result   s r = Cont s | Done r | Err E-```--A parser is a function which takes a `Char`, the current state `s`, and returns-some result:--* `Cont s`: keep going, here's the next state `s`-* `Done r`: parse successful with value `r`-* `Err  E`: parse error, details in the `E` (a structured error)--`Run` handles calling the parser `Char` by `Char`, threading the state through,-and does some bookkeeping for nice errors.--This is a good first step, but we have some outstanding issues:--* What do we do when we reach the end of the string?-* How do we initialize parser state?-* How do we pass parsers around? (As of 2024-04-20, GHC HEAD does not support-  unsaturated type families.)--As always, types are our salvation.--```haskell-type ParserEnd s r = s -> Either E r-type Parser s r = (ParserChSym s r, ParserEndSym s r, s)--type ParserChSym s r = Char ~> s ~> Result s r-type ParserEndSym s r = s ~> Either E r-```--We define a parser as a tuple of a character parser, an end handler, and an-initial state. The types ending in `Sym` are _defunctionalization symbols_,-which enable us to pass our parsers around as type-level functions. The plumbing-is provided Oleg's fantastic library [defun-core][hackage-defun-core].--### Example: `NatDec`-Let's write a parser that parses a natural decimal.+### The parser+A parser is a 4-tuple of: -```haskell-type NatDec = '(NatDecChSym, NatDecEndSym, 0)+* a consuming character parser; given a character and a state, returns+  * `Cont s`: keep going, here's the next state `s`+  * `Done r`: parse successful with value `r`+  * `Err  E`: parse error, details in the `E` (a structured error)+* an end handler, which takes only a state, and can only return `Done` or `Err`+* an initial "raw" state+* a state initializer, which turns the initial "raw" state into the first state+  value (the indirection here assists singling) -type NatDecCh ch acc = NatDecCh' acc (ParseDecimalDigitSym @@ ch)-type family NatDecCh' acc mDigit where-    NatDecCh' acc (Just digit) = Cont (acc * 10 + digit)-    NatDecCh' acc Nothing      = Err -- ...+Running a parser is simple: -type NatDecEnd acc = Right acc+* initialize state+* parse character by character until end of input, or `Done`/`Err` --- boring defunctionalization symbol definitions-```+Parsers may not communicate with the runner any other way. This means no+backtracking, chunking etc. This is a conscious decision, made for simplicity. -At each `Char`, we attempt to parse as a digit. If it's valid, we multiply the-current accumulator by 10 (a left shift) and add the digit value. At the end of-the string, we simply emit the current accumulator.+Note that due to character parsers being consuming, we often need to do a bit of+"internal lookahead", where we check if we expect to consume any more+characters, and if not then emit a `Done`. It also means that non-consuming+parsers such as `Take 0` are invalid for non-empty strings. The state+initializer should be used to catch such cases. -It can be that easy to define a parser with Symparsec! But it isn't always.-Combinators get weird thanks to state handling. Take a look at `Isolate`, then-`Then`.+This is a rough overview of parser design. See the code and/or Haddock+documentation for precise details.  ### Pitfall: Character parsers always consume There is no backtracking or lookahead, that you do not implement yourself. This@@ -115,6 +72,9 @@   (s, [Char]) r` are not definable. _Parsers may not backtrack._   * Combinators such as `<|>` can emulate backtracking, but they are complex and     hard to reason about (they may have bugs!).++### Feature: Parsers may be reified to use at runtime, with guaranteed same behaviour+TODO  ## Contributing I would gladly accept further combinators or other suggestions. Please add an
src/Symparsec.hs view
@@ -1,13 +1,11 @@ module Symparsec   (   -- * Base definitions-    Parser-  , Run+    Run, run'    -- * Parsers   , module Symparsec.Parsers   ) where  import Symparsec.Run-import Symparsec.Parser import Symparsec.Parsers
− src/Symparsec/Internal/Digits.hs
@@ -1,68 +0,0 @@-{- | Parse digits from type-level 'Char's.--A 'Nothing' indicates the given 'Char' was not a valid digit for the given base.--}--module Symparsec.Internal.Digits where--import GHC.TypeLits---- | Parse a binary digit (0 or 1).-type family ParseBinaryDigit (ch :: Char) :: Maybe Natural where-    ParseBinaryDigit '0' = Just 0-    ParseBinaryDigit '1' = Just 1-    ParseBinaryDigit _   = Nothing---- | Parse an octal digit (0-7).-type family ParseOctalDigit (ch :: Char) :: Maybe Natural where-    ParseOctalDigit '0' = Just 0-    ParseOctalDigit '1' = Just 1-    ParseOctalDigit '2' = Just 2-    ParseOctalDigit '3' = Just 3-    ParseOctalDigit '4' = Just 4-    ParseOctalDigit '5' = Just 5-    ParseOctalDigit '6' = Just 6-    ParseOctalDigit '7' = Just 7-    ParseOctalDigit _   = Nothing---- | Parse a decimal digit (0-9).-type family ParseDecimalDigit (ch :: Char) :: Maybe Natural where-    ParseDecimalDigit '0' = Just 0-    ParseDecimalDigit '1' = Just 1-    ParseDecimalDigit '2' = Just 2-    ParseDecimalDigit '3' = Just 3-    ParseDecimalDigit '4' = Just 4-    ParseDecimalDigit '5' = Just 5-    ParseDecimalDigit '6' = Just 6-    ParseDecimalDigit '7' = Just 7-    ParseDecimalDigit '8' = Just 8-    ParseDecimalDigit '9' = Just 9-    ParseDecimalDigit _   = Nothing---- | Parse a hexadecimal digit (0-9A-Fa-f).------ Both upper and lower case are permitted.-type family ParseHexDigit (ch :: Char) :: Maybe Natural where-    ParseHexDigit '0' = Just 0-    ParseHexDigit '1' = Just 1-    ParseHexDigit '2' = Just 2-    ParseHexDigit '3' = Just 3-    ParseHexDigit '4' = Just 4-    ParseHexDigit '5' = Just 5-    ParseHexDigit '6' = Just 6-    ParseHexDigit '7' = Just 7-    ParseHexDigit '8' = Just 8-    ParseHexDigit '9' = Just 9-    ParseHexDigit 'a' = Just 10-    ParseHexDigit 'A' = Just 10-    ParseHexDigit 'b' = Just 11-    ParseHexDigit 'B' = Just 11-    ParseHexDigit 'c' = Just 12-    ParseHexDigit 'C' = Just 12-    ParseHexDigit 'd' = Just 13-    ParseHexDigit 'D' = Just 13-    ParseHexDigit 'e' = Just 14-    ParseHexDigit 'E' = Just 14-    ParseHexDigit 'f' = Just 15-    ParseHexDigit 'F' = Just 15-    ParseHexDigit _   = Nothing
src/Symparsec/Parser.hs view
@@ -1,59 +1,197 @@--- | Base definitions for type-level symbol parsers.+{-# LANGUAGE AllowAmbiguousTypes #-} -- for singling +{- | Base definitions for Symparsec parsers.++Some types are useable both on term-level, and promoted on type-level e.g.+'Result'. For ease of use, you can access the promoted version via type synonyms+like 'PResult' (for promoted X). (This pattern is copied from @singletons@.)++Some definitions I use:++  * "defun symbol": Short for "defunctionalization symbol". A method of passing+    type-level functions (type families) around, without applying them. We use+    phadej's @defun@ library for the basic functionality.+  * "consuming [parser]": A parser which must consume its input. Symparsec+    parsers are always consuming, as it helps keep parser running simple. This+    is problematic, as you can define non-consuming parsers e.g. @Take 0@. We+    handle this by preprocessing initial parser state, to check for such cases.+-}+ module Symparsec.Parser   (-  -- * Parsers-    ParserCh-  , Result(..)-  , ParserEnd-  , E(..)+  -- * Parser+    Parser(..), PParser(..), SParser(..)+  , ParserCh, PParserCh, ParserChSym, ParserChSym1, SParserChSym, SParserChSym1+  , ParserEnd, PParserEnd, ParserEndSym, SParserEndSym+  , ParserSInit, ParserSInitSym, SParserSInitSym+  , Result(..), PResult, SResult(..)+  , PResultEnd, SResultEnd+  , PResultSInit, SResultSInit -  -- * Defun symbols-  , Parser-  , ParserChSym-  , ParserEndSym+  -- * Error+  , E(..), PE, SE(..), demoteSE, SingE(singE), withSingE++  -- * Singling+  , SingParser(..)+  , singParser   ) where  import GHC.TypeLits-import DeFun.Core ( type (~>) )+import DeFun.Core+import GHC.Exts ( withDict )+import TypeLevelShow.Doc+import Singleraeh.Either ( SEither )+import Singleraeh.Demote+import Singleraeh.Tuple ( STuple2 )+import Data.Kind ( Type ) +data Parser str s r = Parser+  { parserCh  :: ParserCh  str s r+  , parserEnd :: ParserEnd str s r+  , parserS0  :: s+  }++-- | A type-level parser, containing defunctionalization symbols.+--+-- Only intended for promoted use. For singled term-level parsers, use+-- 'SParser'. (Symparsec doesn't provide "regular" term-level parsers.)+--+-- I would make this demotable, but the defun symbols get in the way.+data PParser s r = PParser+  { pparserCh  :: ParserChSym s r+  , pparserEnd :: ParserEndSym s r+  , pparserS0  :: s+  }++-- | A singled parser.+--+-- TODO consider swapping for STuple3...? this is much easier though+type SParser+    :: (s -> Type) -> (r -> Type) -> PParser s r+    -> Type+data SParser ss sr p where+    SParser+        :: SParserChSym  ss sr pCh+        -> SParserEndSym ss sr pEnd+        -> ss s0+        -> SParser ss sr ('PParser pCh pEnd s0)+ -- | Parse a 'Char' with the given state. -- -- The action is always consuming. For this reason, you may need to look ahead -- for the final case, so as to not consume an extra 'Char'. This prevents many -- zero-length parsers. It's a bit weird. See -- 'Data.Type.Symbol.Parser.Parser.Drop' for an example.-type ParserCh  s r = Char -> s -> Result s r+type  ParserCh str s r = Char -> s -> Result str s r+type PParserCh     s r = ParserCh Symbol s r --- | The result of a single step of a parser.-data Result s r-  = Cont s -- ^ OK, continue with the given state-  | Done r -- ^ OK, parse successful with result @r@-  | Err  E -- ^ parse error+-- | A defunctionalization symbol for a 'ParserCh'.+type ParserChSym s r = Char ~> s ~> PResult s r +-- | A partially-applied defunctionalization symbol for a 'ParserCh'.+type ParserChSym1 s r = Char -> s ~> PResult s r++type SParserChSym ss sr pCh = Lam2 SChar ss (SResult ss sr) pCh+type SParserChSym1 ch ss sr pCh = SChar ch -> Lam ss (SResult ss sr) (pCh ch)+ -- | What a parser should do at the end of a 'Symbol'.-type ParserEnd s r = s -> Either E r+type  ParserEnd str s r = s -> ResultEnd str r+type PParserEnd     s r = ParserEnd Symbol s r +-- | A defunctionalization symbol for a 'ParserEnd'.+type ParserEndSym s r = s ~> PResultEnd r++type SParserEndSym ss sr pEnd = Lam ss (SResultEnd sr) pEnd++type ParserSInit s0 s = s0 -> PResultSInit s+type ParserSInitSym s0 s = s0 ~> PResultSInit s+type SParserSInitSym ss0 ss sInit = Lam ss0 (SResultSInit ss) sInit++-- | The result of a single step of a parser.+--+-- Promotable. Instantiate with 'String' for term-level, 'Symbol' for+-- type-level.+--+-- Note that a 'Done' indicates the parser has not consumed the character. In+-- the original design, it did consume it, and parsers did their own "lookahead"+-- to handle this. The non-consuming behaviour simplifies permitting+-- non-consuming parsers such as @Take 0@.+data Result str s r+  = Cont s       -- ^ OK,     consumed, continue with state @s@+  | Done r       -- ^ OK, not consumed, parse succeeded with result @r@+  | Err  (E str) -- ^ parse error++-- | Promoted 'Result'.+type PResult = Result Symbol++data SResult (ss :: s -> Type) (sr :: r -> Type) (res :: PResult s r) where+    SCont :: ss s -> SResult ss sr (Cont s)+    SDone :: sr r -> SResult ss sr (Done r)+    SErr  :: SE e -> SResult ss sr (Err e)++type  ResultEnd str =  Either (E str)+type PResultEnd     =  Either PE+type SResultEnd     = SEither SE++type PResultSInit s = Either (PE, s) s+type SResultSInit ss = SEither (STuple2 SE ss) ss+ -- | Parser error.-data E+--+-- Promotable. Instantiate with 'String' for term-level, 'Symbol' for+-- type-level.+data E str   -- | Base parser error.   = EBase-        Symbol       -- ^ parser name-        ErrorMessage -- ^ error message+        str       -- ^ parser name+        (Doc str) -- ^ error message    -- | Inner parser error inside combinator.   | EIn-        Symbol -- ^ combinator name-        E      -- ^ inner error+        str     -- ^ combinator name+        (E str) -- ^ inner error+    deriving stock Show --- | A parser you can pass (heh) around.------ Parsers are defined by the product of a 'ParserCh' character parser,--- 'ParserEnd' end handler, and 's' starting state.-type Parser s r = (ParserChSym s r, ParserEndSym s r, s)+-- | Promoted 'E'.+type PE = E Symbol --- | A defunctionalization symbol for a 'ParserCh'.-type ParserChSym s r = Char ~> s ~> Result s r+data SE (e :: PE) where+    SEBase :: SSymbol name -> SDoc doc -> SE (EBase name doc)+    SEIn   :: SSymbol name -> SE   e   -> SE (EIn name e) --- | A defunctionalization symbol for a 'ParserEnd'.-type ParserEndSym s r = s ~> Either E r+demoteSE :: SE e -> E String+demoteSE = \case+  SEBase sname sdoc -> EBase (fromSSymbol sname) (demoteDoc sdoc)+  SEIn   sname se   -> EIn   (fromSSymbol sname) (demoteSE  se)++instance Demotable SE where+    type Demote SE = E String+    demote = demoteSE++class SingE (e :: PE) where singE :: SE e+instance (KnownSymbol name, SingDoc doc) => SingE (EBase name doc) where+    singE = SEBase (SSymbol @name) (singDoc @doc)+instance (KnownSymbol name, SingE e) => SingE (EIn name e) where+    singE = SEIn   (SSymbol @name) (singE   @e)++withSingE :: forall e r. SE e -> (SingE e => r) -> r+withSingE = withDict @(SingE e)++-- | Promoted parsers with singled implementations.+class SingParser (p :: PParser s r) where+    -- | A singleton for the parser state.+    type PS  p :: s -> Type++    -- | A singleton for the parser return type.+    type PR  p :: r -> Type++    -- | The singled parser.+    singParser' :: SParser (PS p) (PR p) p++-- | Get the singled version of the requested parser.+--+-- 'singParser'' with better type application ergonomics.+singParser+    :: forall {s} {r} (p :: PParser s r). SingParser p+    => SParser (PS p) (PR p) p+singParser = singParser' @_ @_ @p
src/Symparsec/Parser/Common.hs view
@@ -1,36 +1,47 @@ -- | Common definitions for parsers.  module Symparsec.Parser.Common-  ( FailChSym-  , FailEndSym-  , EmitEndSym+  (+  -- * Re-exports+    module Symparsec.Parser+  , Doc(..)+  , type (~>), type (@@), type App++  -- * Common definitions+  , FailChSym,  failChSym+  , FailEndSym, failEndSym   , ErrParserLimitation   ) where  import Symparsec.Parser-import GHC.TypeLits-import DeFun.Core ( type App, type (~>) )+import GHC.TypeLits hiding ( ErrorMessage(..) )+import DeFun.Core+import TypeLevelShow.Doc+import Singleraeh.Either  -- | Fail with the given message when given any character to parse.-type FailChSym :: Symbol -> ErrorMessage -> ParserChSym s r+type FailChSym :: Symbol -> PDoc -> ParserChSym s r data FailChSym name e f type instance App (FailChSym name e) f = FailChSym1 name e f -type FailChSym1 :: Symbol -> ErrorMessage -> Char -> s ~> Result s r+type FailChSym1 :: Symbol -> PDoc -> ParserChSym1 s r data FailChSym1 name e ch s type instance App (FailChSym1 name e ch) s = Err (EBase name e) +failChSym+    :: SSymbol name -> SDoc e -> SParserChSym ss sr (FailChSym name e)+failChSym name e = Lam2 $ \_ch _s -> SErr $ SEBase name e+ -- | Fail with the given message if we're at the end of the symbol.-type FailEndSym :: Symbol -> ErrorMessage -> ParserEndSym s r+type FailEndSym :: Symbol -> PDoc -> ParserEndSym s r data FailEndSym name e s type instance App (FailEndSym name e) s = Left (EBase name e) --- | At the end of the symbol, emit parser state.-type EmitEndSym :: ParserEndSym r r-data EmitEndSym r-type instance App EmitEndSym r = Right r+failEndSym+    :: SSymbol name -> SDoc e -> SParserEndSym ss sr (FailEndSym name e)+failEndSym name e = Lam $ \_s -> SLeft $ SEBase name e  -- | Helper for writing error messages to do with parser limitations (e.g. if --   you tried to use a non-consuming parser like @Skip 0@).-type ErrParserLimitation :: Symbol -> ErrorMessage+type ErrParserLimitation :: Symbol -> PDoc type ErrParserLimitation msg = Text "parser limitation: " :<>: Text msg
src/Symparsec/Parser/End.hs view
@@ -1,9 +1,24 @@-module Symparsec.Parser.End ( End ) where+module Symparsec.Parser.End where -import Symparsec.Parser ( Parser )-import Symparsec.Parser.Common ( FailChSym, EmitEndSym )-import GHC.TypeLits ( ErrorMessage(Text) )+import Symparsec.Parser.Common+import DeFun.Core ( Con1, con1 )+import Singleraeh.Tuple ( SUnit(..) )+import Singleraeh.Either ( SEither(..) )+import GHC.TypeLits ( symbolSing )+import TypeLevelShow.Doc ( singDoc )  -- | Assert end of symbol, or fail.-type End :: Parser () ()-type End = '(FailChSym "End" (Text "expected end of symbol"), EmitEndSym, '())+type End :: PParser () ()+type End = 'PParser+    (FailChSym "End" (Text "expected end of string"))+    (Con1 Right)+    '()++sEnd :: SParser SUnit SUnit End+sEnd = SParser (failChSym symbolSing singDoc) (con1 SRight) SUnit++-- TODO orphan instance. if I need to, make some dumb type family idk.+instance SingParser End where+    type PS  End = SUnit+    type PR  End = SUnit+    singParser' = sEnd
src/Symparsec/Parser/Isolate.hs view
@@ -1,58 +1,121 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Isolate ( Isolate ) where+module Symparsec.Parser.Isolate where -import Symparsec.Parser import Symparsec.Parser.Common-import GHC.TypeLits-import DeFun.Core ( type (~>), type (@@), type App )+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 -> Parser s r -> Parser (Natural, s) r+type Isolate :: Natural -> PParser s r -> PParser (Natural, s) r type family Isolate n p where-    Isolate 0 '(pCh, pEnd, s) =-        '( FailChSym "Isolate" (ErrParserLimitation "cannot isolate 0")-         , IsolateEndSym, '(0, s))-    Isolate n '(pCh, pEnd, s) = '(IsolateChSym pCh pEnd, IsolateEndSym, '(n-1, s))+    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 n (SParser pCh pEnd s0) = SParser+    (sIsolateChSym pCh pEnd)+    (sIsolateEndSym pEnd)+    (STuple2 n 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' = sIsolate (natSing @n) (singParser @p)+ type IsolateCh     :: ParserChSym s r     -> ParserEndSym s r-    -> ParserCh (Natural, s) r+    -> PParserCh (Natural, s) r type family IsolateCh pCh pEnd ch s where-    IsolateCh pCh pEnd ch '(0, s) = IsolateInnerEnd' pEnd (pCh @@ ch @@ s)+    IsolateCh pCh pEnd ch '(0, s) = IsolateInnerEnd (pEnd @@ s)     IsolateCh pCh pEnd ch '(n, s) = IsolateInner n (pCh @@ ch @@ s) --- TODO clean up names here----type IsolateInnerEnd' :: Either ErrorMessage r -> Result (Natural, s) r-type family IsolateInnerEnd' pEnd res where-    IsolateInnerEnd' pEnd (Err  e) = Err  (EIn "Isolate" e)-    IsolateInnerEnd' pEnd (Done r) = Done r-    IsolateInnerEnd' pEnd (Cont s) = IsolateInnerEnd (pEnd @@ s)+sIsolateChSym+    :: SParserChSym  ss sr pCh+    -> SParserEndSym ss sr pEnd+    -> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)+sIsolateChSym pCh pEnd = Lam2 $ \ch (STuple2 n s) ->+    case testEquality n (SNat @0) of+      Just Refl ->+        case pEnd @@ s of+          SRight r -> SDone r+          SLeft  e -> SErr $ eIsolateWrap e+      Nothing -> unsafeCoerce $ sIsolateInner n (pCh @@ ch @@ s) -type IsolateInnerEnd :: Either E r -> Result (Natural, s) r+type IsolateInnerEnd :: Either PE r -> PResult (Natural, s) r type family IsolateInnerEnd a where-    IsolateInnerEnd (Left  e) = Err  (EIn "Isolate" e)     IsolateInnerEnd (Right r) = Done r+    IsolateInnerEnd (Left  e) = Err  (EIsolateWrap e) -type IsolateInner :: Natural -> Result s r -> Result (Natural, s) r-type family IsolateInner n a where+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 _ (Err  e) = Err  e-    IsolateInner n (Done _) = Err (EBase "Isolate"-        (      Text "isolated parser ended without consuming all input ("-          :<>: ShowType n :<>: Text " remaining)" ))+    IsolateInner n (Done _) = Err (EIsolateRemaining n)+    IsolateInner _ (Err  e) = Err (EIsolateWrap e) -type IsolateEnd :: ParserEnd (Natural, s) r-type family IsolateEnd s where-    IsolateEnd '(0, s) = Right '(0, s)-    IsolateEnd '(n, s) = Left (EBase "Isolate"-        (      Text "tried to isolate more than present (needed "-          :<>: ShowType n :<>: Text " more)" ))+sIsolateInner+    :: SNat n+    -> SResult ss sr res+    -> SResult (SIsolateS ss) sr (IsolateInner n res)+sIsolateInner n = \case+  SCont  s -> SCont $ STuple2 (n %- (SNat @1)) s+  SDone _r -> SErr  $ eIsolateRemaining n+  SErr   e -> SErr  $ eIsolateWrap 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 pEnd = Lam $ \(STuple2 n s) ->+      testEqElse n (SNat @0) (sIsolateEnd' (pEnd @@ s))+    $ unsafeCoerce $ SLeft $ eIsolateEndN 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' = \case+  SRight r -> SRight r+  SLeft  e -> SLeft  $ eIsolateWrap 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@@ -63,10 +126,25 @@ type IsolateChSym1     :: ParserChSym s r     -> ParserEndSym s r-    -> Char -> (Natural, s) ~> Result (Natural, 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 IsolateEndSym :: ParserEndSym (Natural, s) r-data IsolateEndSym s-type instance App IsolateEndSym s = IsolateEnd s+type EIsolateWrap e = EIn "Isolate" e++eIsolateWrap :: SE e -> SE (EIsolateWrap e)+eIsolateWrap e = withSingE 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 n = withKnownSymbol (sShowNatDec n) 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 n = withKnownSymbol (sShowNatDec n) singE
src/Symparsec/Parser/Literal.hs view
@@ -1,53 +1,80 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Literal ( Literal ) where+module Symparsec.Parser.Literal where -import Symparsec.Parser import Symparsec.Parser.Common-import GHC.TypeLits-import DeFun.Core ( type (~>), type App )+import GHC.TypeLits hiding ( ErrorMessage(..) )+import TypeLevelShow.Utils ( ShowChar, sShowChar )+import Data.Type.Equality+import DeFun.Core+import Singleraeh.Tuple+import Singleraeh.Either+import Singleraeh.Maybe+import Singleraeh.Symbol+import Unsafe.Coerce+import TypeLevelShow.Doc  -- | Parse the given 'Symbol'.-type Literal :: Symbol -> Parser (Char, Maybe (Char, Symbol)) ()-type Literal sym = Literal' (UnconsSymbol sym)+type Literal :: Symbol -> PParser Symbol ()+type Literal str = 'PParser LiteralChSym LiteralEndSym str -type EEmptyLit = ErrParserLimitation "cannot parse empty literal"+sLiteral :: SSymbol str -> SParser SSymbol SUnit (Literal str)+sLiteral str = SParser sLiteralChSym sLiteralEndSym str -type family Literal' msym where-    Literal' Nothing           =-        '( FailChSym "Literal" EEmptyLit-         , FailEndSym "Literal" EEmptyLit, '( '\0', Nothing))-    Literal' (Just '(ch, sym)) =-        '(LiteralChSym, LiteralEndSym, '(ch, UnconsSymbol sym))+instance KnownSymbol str => SingParser (Literal str) where+    type PS (Literal str) = SSymbol+    type PR (Literal str) = SUnit+    singParser' = sLiteral SSymbol -type family LiteralCh ch s where-    LiteralCh ch0 '(ch0, Just '(ch1, sym)) = Cont '(ch1, UnconsSymbol sym)-    LiteralCh ch0 '(ch0, Nothing)          = Done '()-    LiteralCh ch  '(ch0, msym)             = Err (EBase "Literal"-        (      Text "expected " :<>: ShowType ch0-          :<>: Text ", got " :<>: ShowType ch))+type LiteralCh ch str = LiteralCh' ch (UnconsSymbol str)+type family LiteralCh' ch str where+    LiteralCh' ch (Just '(ch, str))     = Cont str+    LiteralCh' ch (Just '(chNext, str)) = Err (EWrongChar chNext ch)+    LiteralCh' ch Nothing               = Done '() -type LiteralEnd :: ParserEnd (Char, Maybe (Char, Symbol)) ()-type family LiteralEnd s where-    LiteralEnd '(ch0, msym) = Left (EBase "Literal"-      (      Text "still parsing literal: "-        :<>: Text (ConsSymbol ch0 (ReconsSymbol msym))))+type EWrongChar chNext ch = EBase "Literal"+    (      Text "expected " :<>: Text (ShowChar chNext)+      :<>: Text    ", got " :<>: Text (ShowChar ch)) -type family ReconsSymbol msym where-    ReconsSymbol Nothing           = ""-    ReconsSymbol (Just '(ch, sym)) = ConsSymbol ch sym+eWrongChar :: SChar chNext -> SChar ch -> SE (EWrongChar chNext ch)+eWrongChar chNext ch = SEBase symbolSing $+          SText symbolSing :$<>: SText (sShowChar chNext)+    :$<>: SText symbolSing :$<>: SText (sShowChar ch) -type LiteralChSym :: ParserChSym (Char, Maybe (Char, Symbol)) ()+type LiteralChSym :: ParserChSym Symbol () data LiteralChSym f type instance App LiteralChSym f = LiteralChSym1 f -type LiteralChSym1-    :: Char-    -> (Char, Maybe (Char, Symbol))-    ~> Result (Char, Maybe (Char, Symbol)) ()+type LiteralChSym1 :: ParserChSym1 Symbol () data LiteralChSym1 ch s type instance App (LiteralChSym1 ch) s = LiteralCh ch s -type LiteralEndSym :: ParserEndSym (Char, Maybe (Char, Symbol)) ()+sLiteralChSym :: SParserChSym SSymbol SUnit LiteralChSym+sLiteralChSym = Lam2 $ \ch str ->+    case sUnconsSymbol str of+      SJust (STuple2 chNext str') ->+        case testEquality ch chNext of+          Just Refl -> SCont str'+          Nothing   -> unsafeCoerce $ SErr $ eWrongChar chNext ch+      SNothing -> SDone SUnit++type LiteralEnd :: PParserEnd Symbol ()+type family LiteralEnd str where+    LiteralEnd ""  = Right '()+    LiteralEnd str = Left (EStillParsing str)++type EStillParsing str =+    EBase "Literal" (Text "still parsing literal: " :<>: Text str)++eStillParsing :: SSymbol str -> SE (EStillParsing str)+eStillParsing str = withKnownSymbol str singE++type LiteralEndSym :: ParserEndSym Symbol () data LiteralEndSym s type instance App LiteralEndSym s = LiteralEnd s++sLiteralEndSym :: SParserEndSym SSymbol SUnit LiteralEndSym+sLiteralEndSym = Lam $ \str ->+    case testEquality str (SSymbol @"") of+      Just Refl -> SRight SUnit+      Nothing   -> unsafeCoerce $ SLeft $ eStillParsing str
src/Symparsec/Parser/Natural.hs view
@@ -1,49 +1,67 @@-{-# LANGUAGE UndecidableInstances #-} -- for natural multiplication etc.+{-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Natural-  ( NatBin, NatOct, NatDec, NatHex-  , NatBase-  ) where+module Symparsec.Parser.Natural where -import Symparsec.Parser-import Symparsec.Parser.Common ( EmitEndSym )-import GHC.TypeLits-import DeFun.Core ( type (~>), type App, type (@@) )-import Symparsec.Internal.Digits+import Symparsec.Parser.Common+import Symparsec.Parser.Natural.Digits+import DeFun.Core+import GHC.TypeLits hiding ( ErrorMessage(..) )+import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )+import Singleraeh.Maybe+import Singleraeh.Either+import Singleraeh.Natural  -- | Parse a binary (base 2) natural.-type NatBin = NatBase  2 ParseBinaryDigitSym+type NatBin = NatBase  2 ParseDigitBinSym  -- | Parse an octal (base 8) natural.-type NatOct = NatBase  8 ParseOctalDigitSym+type NatOct = NatBase  8 ParseDigitOctSym  -- | Parse a decimal (base 10) natural.-type NatDec = NatBase 10 ParseDecimalDigitSym+type NatDec = NatBase 10 ParseDigitDecSym  -- | Parse a hexadecimal (base 16) natural. Permits mixed-case (@0-9A-Fa-f@).-type NatHex = NatBase 16 ParseHexDigitSym+type NatHex = NatBase 16 ParseDigitHexSym  -- | Parse a natural in the given base, using the given digit parser. type NatBase-    :: Natural -> (Char ~> Maybe Natural) -> Parser Natural Natural+    :: Natural -> (Char ~> Maybe Natural) -> PParser (Maybe Natural) Natural type NatBase base parseDigit =-    '(NatBaseChSym base parseDigit, EmitEndSym, 0)+    'PParser (NatBaseChSym base parseDigit) NatBaseEndSym Nothing +sNatBase+    :: SNat base+    -> SParseDigit parseDigit+    -> SParser (SMaybe SNat) SNat (NatBase base parseDigit)+sNatBase base parseDigit =+    SParser (sNatBaseChSym base parseDigit) sNatBaseEndSym SNothing++instance (KnownNat base, SingParseDigit parseDigit)+  => SingParser (NatBase base parseDigit) where+    type PS (NatBase base parseDigit) = SMaybe SNat+    type PR (NatBase base parseDigit) = SNat+    singParser' = sNatBase natSing singParseDigit+ type NatBaseCh     :: Natural     -> (Char ~> Maybe Natural)-    -> ParserCh Natural Natural-type NatBaseCh base parseDigit ch n = NatBaseCh' base n (parseDigit @@ ch)+    -> PParserCh (Maybe Natural) Natural+type NatBaseCh base parseDigit ch mn = NatBaseCh' base mn (parseDigit @@ ch) -type family NatBaseCh' base n mDigit where-    NatBaseCh' base n (Just digit) = Cont (n * base + digit)-    NatBaseCh' base n Nothing      = Err (EBase "NatBase"-        (Text "not a base " :<>: ShowType base :<>: Text " digit"))+type family NatBaseCh' base mn mDigit where+    NatBaseCh' base (Just n) (Just digit) = Cont (Just (n * base + digit))+    NatBaseCh' base Nothing  (Just digit) = Cont (Just digit)+    NatBaseCh' base mn       Nothing      = Err (EInvalidDigit base) +type EInvalidDigit base = EBase "NatBase"+    (Text "not a base " :<>: Text (ShowNatDec base) :<>: Text " digit")+eInvalidDigit :: SNat base -> SE (EInvalidDigit base)+eInvalidDigit base = withKnownSymbol (sShowNatDec base) singE+ type NatBaseChSym     :: Natural     -> (Char ~> Maybe Natural)-    -> ParserChSym Natural Natural+    -> ParserChSym (Maybe Natural) Natural data NatBaseChSym base parseDigit f type instance App (NatBaseChSym base parseDigit) f =     NatBaseChSym1 base parseDigit f@@ -51,24 +69,36 @@ type NatBaseChSym1     :: Natural     -> (Char ~> Maybe Natural)-    -> Char -> Natural-    ~> Result Natural Natural-data NatBaseChSym1 base parseDigit ch n-type instance App (NatBaseChSym1 base parseDigit ch) n =-    NatBaseCh base parseDigit ch n+    -> ParserChSym1 (Maybe Natural) Natural+data NatBaseChSym1 base parseDigit ch mn+type instance App (NatBaseChSym1 base parseDigit ch) mn =+    NatBaseCh base parseDigit ch mn -type ParseBinaryDigitSym :: Char ~> Maybe Natural-data ParseBinaryDigitSym a-type instance App ParseBinaryDigitSym a = ParseBinaryDigit a+sNatBaseChSym+    :: SNat base+    -> SParseDigit parseDigit+    -> SParserChSym (SMaybe SNat) SNat (NatBaseChSym base parseDigit)+sNatBaseChSym base parseDigit = Lam2 $ \ch mn ->+    case parseDigit @@ ch of+      SJust digit ->+        case mn of+          SJust n  -> SCont $ SJust $ n %* base %+ digit+          SNothing -> SCont $ SJust digit+      SNothing -> SErr $ eInvalidDigit base -type ParseOctalDigitSym :: Char ~> Maybe Natural-data ParseOctalDigitSym a-type instance App ParseOctalDigitSym a = ParseOctalDigit a+type family NatBaseEnd mn where+    NatBaseEnd (Just n) = Right n+    NatBaseEnd Nothing  = Left EEmpty -type ParseDecimalDigitSym :: Char ~> Maybe Natural-data ParseDecimalDigitSym a-type instance App ParseDecimalDigitSym a = ParseDecimalDigit a+type EEmpty = EBase "NatBase" (Text "no digits parsed")+eEmpty :: SE EEmpty+eEmpty = singE -type ParseHexDigitSym :: Char ~> Maybe Natural-data ParseHexDigitSym a-type instance App ParseHexDigitSym a = ParseHexDigit a+type NatBaseEndSym :: ParserEndSym (Maybe Natural) Natural+data NatBaseEndSym mn+type instance App NatBaseEndSym mn = NatBaseEnd mn++sNatBaseEndSym :: SParserEndSym (SMaybe SNat) SNat NatBaseEndSym+sNatBaseEndSym = Lam $ \case+  SJust n  -> SRight n+  SNothing -> SLeft eEmpty
+ src/Symparsec/Parser/Natural/Digits.hs view
@@ -0,0 +1,163 @@+{- | Parse digits from type-level 'Char's.++A 'Nothing' indicates the given 'Char' was not a valid digit for the given base.+-}++module Symparsec.Parser.Natural.Digits where++import GHC.TypeLits+import DeFun.Core+import Singleraeh.Equality ( testEqElse )+import Singleraeh.Maybe+import Unsafe.Coerce ( unsafeCoerce )++type SParseDigit parseDigit = Lam SChar (SMaybe SNat) parseDigit++class SingParseDigit parseDigit where+    singParseDigit :: SParseDigit parseDigit++-- | Parse a binary digit (0 or 1).+type family ParseDigitBin (ch :: Char) :: Maybe Natural where+    ParseDigitBin '0' = Just 0+    ParseDigitBin '1' = Just 1+    ParseDigitBin _   = Nothing++type ParseDigitBinSym :: Char ~> Maybe Natural+data ParseDigitBinSym ch+type instance App ParseDigitBinSym ch = ParseDigitBin ch++sParseDigitBinSym :: SParseDigit ParseDigitBinSym+sParseDigitBinSym = Lam $ \ch ->+      testEqElse ch (SChar @'0') (SJust (SNat @0))+    $ testEqElse ch (SChar @'1') (SJust (SNat @1))+    $ unsafeCoerce SNothing++instance SingParseDigit ParseDigitBinSym where+    singParseDigit = sParseDigitBinSym++-- | Parse an octal digit (0-7).+type family ParseDigitOct (ch :: Char) :: Maybe Natural where+    ParseDigitOct '0' = Just 0+    ParseDigitOct '1' = Just 1+    ParseDigitOct '2' = Just 2+    ParseDigitOct '3' = Just 3+    ParseDigitOct '4' = Just 4+    ParseDigitOct '5' = Just 5+    ParseDigitOct '6' = Just 6+    ParseDigitOct '7' = Just 7+    ParseDigitOct _   = Nothing++type ParseDigitOctSym :: Char ~> Maybe Natural+data ParseDigitOctSym ch+type instance App ParseDigitOctSym ch = ParseDigitOct ch++sParseDigitOctSym :: SParseDigit ParseDigitOctSym+sParseDigitOctSym = Lam $ \ch ->+      testEqElse ch (SChar @'0') (SJust (SNat @0))+    $ testEqElse ch (SChar @'1') (SJust (SNat @1))+    $ testEqElse ch (SChar @'2') (SJust (SNat @2))+    $ testEqElse ch (SChar @'3') (SJust (SNat @3))+    $ testEqElse ch (SChar @'4') (SJust (SNat @4))+    $ testEqElse ch (SChar @'5') (SJust (SNat @5))+    $ testEqElse ch (SChar @'6') (SJust (SNat @6))+    $ testEqElse ch (SChar @'7') (SJust (SNat @7))+    $ unsafeCoerce SNothing++instance SingParseDigit ParseDigitOctSym where+    singParseDigit = sParseDigitOctSym++-- | Parse a decimal digit (0-9).+type family ParseDigitDec (ch :: Char) :: Maybe Natural where+    ParseDigitDec '0' = Just 0+    ParseDigitDec '1' = Just 1+    ParseDigitDec '2' = Just 2+    ParseDigitDec '3' = Just 3+    ParseDigitDec '4' = Just 4+    ParseDigitDec '5' = Just 5+    ParseDigitDec '6' = Just 6+    ParseDigitDec '7' = Just 7+    ParseDigitDec '8' = Just 8+    ParseDigitDec '9' = Just 9+    ParseDigitDec _   = Nothing++type ParseDigitDecSym :: Char ~> Maybe Natural+data ParseDigitDecSym ch+type instance App ParseDigitDecSym ch = ParseDigitDec ch++sParseDigitDecSym :: SParseDigit ParseDigitDecSym+sParseDigitDecSym = Lam $ \ch ->+      testEqElse ch (SChar @'0') (SJust (SNat @0))+    $ testEqElse ch (SChar @'1') (SJust (SNat @1))+    $ testEqElse ch (SChar @'2') (SJust (SNat @2))+    $ testEqElse ch (SChar @'3') (SJust (SNat @3))+    $ testEqElse ch (SChar @'4') (SJust (SNat @4))+    $ testEqElse ch (SChar @'5') (SJust (SNat @5))+    $ testEqElse ch (SChar @'6') (SJust (SNat @6))+    $ testEqElse ch (SChar @'7') (SJust (SNat @7))+    $ testEqElse ch (SChar @'8') (SJust (SNat @8))+    $ testEqElse ch (SChar @'9') (SJust (SNat @9))+    $ unsafeCoerce SNothing++instance SingParseDigit ParseDigitDecSym where+    singParseDigit = sParseDigitDecSym++-- | Parse a hexadecimal digit (0-9A-Fa-f).+--+-- Both upper and lower case are permitted.+type family ParseDigitHex (ch :: Char) :: Maybe Natural where+    ParseDigitHex '0' = Just  0+    ParseDigitHex '1' = Just  1+    ParseDigitHex '2' = Just  2+    ParseDigitHex '3' = Just  3+    ParseDigitHex '4' = Just  4+    ParseDigitHex '5' = Just  5+    ParseDigitHex '6' = Just  6+    ParseDigitHex '7' = Just  7+    ParseDigitHex '8' = Just  8+    ParseDigitHex '9' = Just  9+    ParseDigitHex 'a' = Just 10+    ParseDigitHex 'A' = Just 10+    ParseDigitHex 'b' = Just 11+    ParseDigitHex 'B' = Just 11+    ParseDigitHex 'c' = Just 12+    ParseDigitHex 'C' = Just 12+    ParseDigitHex 'd' = Just 13+    ParseDigitHex 'D' = Just 13+    ParseDigitHex 'e' = Just 14+    ParseDigitHex 'E' = Just 14+    ParseDigitHex 'f' = Just 15+    ParseDigitHex 'F' = Just 15+    ParseDigitHex _   = Nothing++type ParseDigitHexSym :: Char ~> Maybe Natural+data ParseDigitHexSym ch+type instance App ParseDigitHexSym ch = ParseDigitHex ch++sParseDigitHexSym :: SParseDigit ParseDigitHexSym+sParseDigitHexSym = Lam $ \ch ->+      testEqElse ch (SChar @'0') (SJust (SNat  @0))+    $ testEqElse ch (SChar @'1') (SJust (SNat  @1))+    $ testEqElse ch (SChar @'2') (SJust (SNat  @2))+    $ testEqElse ch (SChar @'3') (SJust (SNat  @3))+    $ testEqElse ch (SChar @'4') (SJust (SNat  @4))+    $ testEqElse ch (SChar @'5') (SJust (SNat  @5))+    $ testEqElse ch (SChar @'6') (SJust (SNat  @6))+    $ testEqElse ch (SChar @'7') (SJust (SNat  @7))+    $ testEqElse ch (SChar @'8') (SJust (SNat  @8))+    $ testEqElse ch (SChar @'9') (SJust (SNat  @9))+    $ testEqElse ch (SChar @'a') (SJust (SNat @10))+    $ testEqElse ch (SChar @'A') (SJust (SNat @10))+    $ testEqElse ch (SChar @'b') (SJust (SNat @11))+    $ testEqElse ch (SChar @'B') (SJust (SNat @11))+    $ testEqElse ch (SChar @'c') (SJust (SNat @12))+    $ testEqElse ch (SChar @'C') (SJust (SNat @12))+    $ testEqElse ch (SChar @'d') (SJust (SNat @13))+    $ testEqElse ch (SChar @'D') (SJust (SNat @13))+    $ testEqElse ch (SChar @'e') (SJust (SNat @14))+    $ testEqElse ch (SChar @'E') (SJust (SNat @14))+    $ testEqElse ch (SChar @'f') (SJust (SNat @15))+    $ testEqElse ch (SChar @'F') (SJust (SNat @15))+    $ unsafeCoerce SNothing++instance SingParseDigit ParseDigitHexSym where+    singParseDigit = sParseDigitHexSym
− src/Symparsec/Parser/Or.hs
@@ -1,175 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--{- | Choice operator. Try left; if it fails, try right.--This is a problematic combinator:--  * Implementation is clumsy due to internal parser state being untouchable.-    We must record seen characters, in order to replay them on the right parser-    in case the left parser fails.-  * Errors degrade due to left parser errors being discarded. Perhaps your-    string was one character off a successful left parse; but if it fails, you-    won't see that error.-  * It's hard to reason about. It might break in certain situations.--}---module Symparsec.Parser.Or ( (:<|>:) ) where--import Symparsec.Parser-import Symparsec.Internal.List ( Reverse )-import DeFun.Core ( type (@@), type App )---- | Parser choice. Try left; if it fails, backtrack and try right.------ Be warned that this parser is experimental, and likely brittle. If possible,--- consider designing your schema to permit non-backtracking parsing. Or if not,--- have both sides always parse the same length, in which case this parser--- should probably work fine.-infixl 3 :<|>:-type (:<|>:)-    :: Parser sl rl-    -> Parser sr rr-    -> Parser (Either (sl, [Char]) sr) (Either rl rr)-type family pl :<|>: pr where-    '(plCh, plEnd, sl) :<|>: '(prCh, prEnd, sr) =-        '(OrChSym plCh prCh sr, OrEndSym plEnd prCh prEnd sr, Left '(sl, '[]))--type OrCh-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> ParserCh (Either (sl, [Char]) sr) (Either rl rr)-type family OrCh plCh prCh sr ch s where-    -- | Parsing left-    OrCh plCh prCh sr ch (Left  '(sl, chs)) =-        OrChL prCh sr (ch : chs) (plCh @@ ch @@ sl)--    -- | Parsing right (left failed and was successfully replayed)-    OrCh plCh prCh _  ch (Right sr) =-        OrChR (prCh @@ ch @@ sr)---- TODO [Char] is actually nonempty, but it's awkward because we need to reverse--- it and place the known char at the end. we _can_ fix this, but it's just--- annoying lol-type OrChL-    :: ParserChSym sr rr-    -> sr-    -> [Char]-    -> Result sl rl-    -> Result (Either (sl, [Char]) sr) (Either rl rr)-type family OrChL prCh sr chs resl where-    -- | Left parser OK, continue-    OrChL _    _  chs (Cont sl) = Cont (Left  '(sl, chs))--    -- | Left parser OK, done-    OrChL _    _  chs (Done rl) = Done (Left  rl)--    -- | Left parser failed: ignore, replay consumed characters on right parser-    OrChL prCh sr chs (Err  _ ) =-        OrChLReplay prCh (Reverse chs) (Cont sr)---- TODO [Char] is nonempty, see 'OrChL'. also if we fix that, we can get better--- equation ordering!-type OrChLReplay-    :: ParserChSym sr rr-    -> [Char]-    -> Result sr rr-    -> Result (Either (sl, [Char]) sr) (Either rl rr)-type family OrChLReplay prCh chs resr where-    -- | Right parser OK, last char-    OrChLReplay prCh (ch : '[]) (Cont sr) = OrChR (prCh @@ ch @@ sr)--    -- | Right parser OK, keep replaying-    OrChLReplay prCh (ch : chs) (Cont sr) =-        OrChLReplay prCh chs (prCh @@ ch @@ sr)--    -- | Right parser fail: wrap error-    ---    -- TODO error behaviour here?-    OrChLReplay prCh chs        (Err  er) = Err (EIn "Or(R)" er)--    -- | Right parser done: early success-    ---    -- If this matches before we finish replaying, any remaining replay-    -- characters are lost. This _should_ break certain parses. Or, maybe it-    -- only breaks return symbol..? In which case, we can fix by returning-    -- the extra replayed chars in our return type???? TODO-    OrChLReplay prCh chs        (Done rr) = Done (Right rr)-        -- (EBase "Or" (ErrParserLimitation "cannot parse less on right of Or"))--type family OrChR resr where-    OrChR (Cont sr) = Cont (Right sr)-    OrChR (Done rr) = Done (Right rr)-    OrChR (Err  er) = Err (EIn "Or(R)" er)--type OrEnd-    :: ParserEndSym sl rl-    -> ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> sr-    -> ParserEnd (Either (sl, [Char]) sr) (Either rl rr)-type family OrEnd plEnd prCh prEnd sr res where-    -- | Input ended on L.-    OrEnd plEnd prCh prEnd sr (Left  '(sl, chs)) =-        OrEndL prCh prEnd sr chs (plEnd @@ sl)--    -- | Input ended on R.-    OrEnd plEnd prCh prEnd _  (Right sr)         = OrEndR (prEnd @@ sr)--type OrEndR-    :: Either E rr-    -> Either E (Either rl rr)-type family OrEndR s where-    OrEndR (Left  er) = Left (EIn "Or(R)" er)-    OrEndR (Right rr) = Right (Right rr)--type OrEndL-    :: ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> sr-    -> [Char]-    -> Either E rl-    -> Either E (Either rl rr)-type family OrEndL prCh prEnd sr chs res where-    OrEndL prCh prEnd sr chs (Right rl) = Right (Left rl)-    OrEndL prCh prEnd sr chs (Left  el) =-        OrChLReplay' prCh prEnd (Reverse chs) (Cont sr)--type OrChLReplay'-    :: ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> [Char]-    -> Result sr rr-    -> Either E (Either rl rr)-type family OrChLReplay' prCh prEnd chs resr where-    OrChLReplay' prCh prEnd (ch : '[]) (Cont sr) =-        OrEndR' prEnd (prCh @@ ch @@ sr)-    OrChLReplay' prCh prEnd (ch : chs) (Cont sr) =-        OrChLReplay' prCh prEnd chs (prCh @@ ch @@ sr)-    OrChLReplay' prCh prEnd chs        (Err  er) = Left (EIn "Or(R)" er)--    -- TODO Here, we successfully ended while replaying left-consumed chars.-    -- This may not work if it's wrapped in further combinators, I'm unsure.-    OrChLReplay' prCh prEnd chs        (Done rr) = Right (Right rr)-        -- (EBase "Or" (ErrParserLimitation "cannot parse less on right of Or"))--type family OrEndR' prEnd s where-    OrEndR' prEnd (Err  er) = Left (EIn "Or(R)" er)-    OrEndR' prEnd (Done rr) = Right (Right rr)-    OrEndR' prEnd (Cont sr) = OrEndR (prEnd @@ sr)--data OrChSym plCh prCh sr f-type instance App (OrChSym plCh prCh sr) f = OrChSym1 plCh prCh sr f--data OrChSym1 plCh prCh sr ch s-type instance App (OrChSym1 plCh prCh sr ch) s = OrCh plCh prCh sr ch s--type OrEndSym-    :: ParserEndSym sl rl-    -> ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> sr-    -> ParserEndSym (Either (sl, [Char]) sr) (Either rl rr)-data OrEndSym plEnd prCh prEnd sr s-type instance App (OrEndSym plEnd prCh prEnd sr) s = OrEnd plEnd prCh prEnd sr s
src/Symparsec/Parser/Skip.hs view
@@ -1,44 +1,66 @@-{-# LANGUAGE UndecidableInstances #-} -- for natural subtraction+{-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Skip ( Skip, Skip' ) where+module Symparsec.Parser.Skip where -import Symparsec.Parser import Symparsec.Parser.Common-import GHC.TypeLits-import DeFun.Core ( type (~>), type App )+import GHC.TypeLits hiding ( ErrorMessage(..) )+import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )+import Data.Type.Equality+import Singleraeh.Tuple+import Singleraeh.Either+import Singleraeh.Natural+import DeFun.Core+import Unsafe.Coerce ( unsafeCoerce )  -- | Skip forward @n@ characters. Fails if fewer than @n@ characters are---   available.-type Skip :: Natural -> Parser Natural ()-type family Skip n where-    Skip 0 =-        '(FailChSym "Skip" (ErrParserLimitation "can't drop 0"), SkipEndSym, 0)-    Skip n = Skip' n+--   available'.+type Skip :: Natural -> PParser Natural ()+type Skip n = 'PParser SkipChSym SkipEndSym n --- | Unsafe 'Skip' which doesn't check for @n=0@. May get stuck.-type Skip' :: Natural -> Parser Natural ()-type Skip' n = '(SkipChSym, SkipEndSym, n)+sSkip :: SNat n -> SParser SNat SUnit (Skip n)+sSkip n = SParser sSkipChSym sSkipEndSym n -type SkipCh :: ParserCh Natural ()+instance KnownNat n => SingParser (Skip n) where+    type PS (Skip n) = SNat+    type PR (Skip n) = SUnit+    singParser' = sSkip SNat++type SkipCh :: PParserCh Natural () type family SkipCh ch n where-    SkipCh _ 1 = Done '()+    SkipCh _ 0 = Done '()     SkipCh _ n = Cont (n-1) -type SkipEnd :: ParserEnd Natural ()-type family SkipEnd n where-    SkipEnd 0 = Right '()-    SkipEnd n = Left (EBase "Skip"-      ( Text "tried to drop "-        :<>: ShowType n :<>: Text " chars from empty symbol"))- type SkipChSym :: ParserChSym Natural () data SkipChSym f type instance App SkipChSym f = SkipChSym1 f -type SkipChSym1 :: Char -> Natural ~> Result Natural ()+type SkipChSym1 :: ParserChSym1 Natural () data SkipChSym1 ch n type instance App (SkipChSym1 ch) n = SkipCh ch n +sSkipChSym :: SParserChSym SNat SUnit SkipChSym+sSkipChSym = Lam2 $ \_ n ->+    case testEquality n (SNat @0) of+      Just Refl -> SDone SUnit+      Nothing   -> unsafeCoerce $ SCont $ n %- (SNat @1)++type SkipEnd :: PParserEnd Natural ()+type family SkipEnd n where+    SkipEnd 0 = Right '()+    SkipEnd n = Left (ESkipPastEnd n)++type ESkipPastEnd n = EBase "Skip"+    (      Text "tried to drop "+      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")+eSkipPastEnd :: SNat n -> SE (ESkipPastEnd n)+eSkipPastEnd n = withKnownSymbol (sShowNatDec n) singE+ type SkipEndSym :: ParserEndSym Natural () data SkipEndSym n type instance App SkipEndSym n = SkipEnd n++sSkipEndSym :: SParserEndSym SNat SUnit SkipEndSym+sSkipEndSym = Lam $ \n ->+    case testEquality n (SNat @0) of+      Just Refl -> SRight SUnit+      Nothing   -> unsafeCoerce $ SLeft $ eSkipPastEnd n
src/Symparsec/Parser/Take.hs view
@@ -1,45 +1,71 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Take ( Take ) where+module Symparsec.Parser.Take where -import Symparsec.Parser import Symparsec.Parser.Common-import GHC.TypeLits-import DeFun.Core ( type (~>), type App )+import Singleraeh.Symbol ( RevCharsToSymbol, revCharsToSymbol )+import Singleraeh.List ( SList(..) )+import Singleraeh.Tuple ( STuple2(..) )+import Data.Type.Equality+import Singleraeh.Natural ( (%-) )+import Singleraeh.Either ( SEither(..) )+import TypeLevelShow.Natural+import GHC.TypeLits hiding ( ErrorMessage(..) )+import Unsafe.Coerce ( unsafeCoerce )+import DeFun.Core  -- | Return the next @n@ characters.-type Take :: Natural -> Parser (Natural, [Char]) Symbol-type family Take n where-    Take 0 =-        '( FailChSym "Take" (ErrParserLimitation "can't take 0")-         , TakeEndSym, '(0, '[]))-    Take n = '(TakeChSym, TakeEndSym, '(n, '[]))+type Take n = 'PParser TakeChSym TakeEndSym '(n, '[]) -type TakeCh :: ParserCh (Natural, [Char]) Symbol-type family TakeCh ch s where-    TakeCh ch '(1, chs) = Done (RevCharsToSymbol (ch : chs))-    TakeCh ch '(n, chs) = Cont '(n-1, ch : chs)+type STakeS = STuple2 SNat (SList SChar)+type  TakeS = (Natural, [Char]) -type TakeEnd :: ParserEnd (Natural, [Char]) Symbol-type family TakeEnd s where-    TakeEnd '(0, chs) = Right (RevCharsToSymbol chs)-    TakeEnd '(n, _)   = Left (EBase "Take"-      ( Text "tried to take "-        :<>: ShowType n :<>: Text " chars from empty symbol"))+sTake :: SNat n -> SParser STakeS SSymbol (Take n)+sTake n = SParser takeChSym takeEndSym (STuple2 n SNil) -type RevCharsToSymbol chs = RevCharsToSymbol' "" chs-type family RevCharsToSymbol' sym chs where-    RevCharsToSymbol' sym '[]        = sym-    RevCharsToSymbol' sym (ch : chs) = RevCharsToSymbol' (ConsSymbol ch sym) chs+instance KnownNat n => SingParser (Take n) where+    type PS (Take n) = STakeS+    type PR (Take n) = SSymbol+    singParser' = sTake SNat -type TakeChSym :: ParserChSym (Natural, [Char]) Symbol+type TakeCh :: PParserCh TakeS Symbol+type family TakeCh ch s where+    TakeCh ch '(0, chs) = Done (RevCharsToSymbol chs)+    TakeCh ch '(n, chs) = Cont '(n-1, ch : chs)++type TakeChSym :: ParserChSym TakeS Symbol data TakeChSym f type instance App TakeChSym f = TakeChSym1 f -type TakeChSym1 :: Char -> (Natural, [Char]) ~> Result (Natural, [Char]) Symbol+takeChSym :: SParserChSym STakeS SSymbol TakeChSym+takeChSym = Lam2 $ \ch (STuple2 n chs) ->+    case testEquality n (SNat @0) of+      Just Refl -> SDone $ revCharsToSymbol chs+      Nothing   ->+        unsafeCoerce $ SCont $ STuple2 (n %- (SNat @1)) (SCons ch chs)++type TakeChSym1 :: ParserChSym1 TakeS Symbol data TakeChSym1 ch s type instance App (TakeChSym1 ch) s = TakeCh ch s -type TakeEndSym :: ParserEndSym (Natural, [Char]) Symbol+type TakeEnd :: PParserEnd TakeS Symbol+type family TakeEnd s where+    TakeEnd '(0, chs) = Right (RevCharsToSymbol chs)+    TakeEnd '(n, _)   = Left (ETakeEnd n)++type ETakeEnd n = EBase "Take"+    (      Text "tried to take "+      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")++eTakeEnd :: SNat n -> SE (ETakeEnd n)+eTakeEnd sn = withKnownSymbol (sShowNatDec sn) singE++type TakeEndSym :: ParserEndSym TakeS Symbol data TakeEndSym s type instance App TakeEndSym s = TakeEnd s++takeEndSym :: SParserEndSym STakeS SSymbol TakeEndSym+takeEndSym = Lam $ \(STuple2 n chs) ->+    case testEquality n (SNat @0) of+      Just Refl -> SRight $ revCharsToSymbol chs+      Nothing   -> unsafeCoerce $ SLeft $ eTakeEnd n
src/Symparsec/Parser/Then.hs view
@@ -1,69 +1,187 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Then ( (:<*>:) ) where+module Symparsec.Parser.Then where -import Symparsec.Parser-import GHC.TypeLits-import DeFun.Core ( type (~>), type (@@), type App )+import Symparsec.Parser.Common+import Singleraeh.Either ( SEither(..) )+import Singleraeh.Tuple ( STuple2(..) )+import DeFun.Core +type SPThen ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =+    SParser+        (SEither ssl (STuple2 srl ssr))+        (STuple2 srl srr)+        (Then' plCh plEnd s0l prCh prEnd s0r)++sThen+    :: SParser ssl srl ('PParser plCh plEnd s0l)+    -> SParser ssr srr ('PParser prCh prEnd s0r)+    -> SPThen  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r+sThen (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =+    SParser (sThenChSym plCh prCh s0r) (sThenEndSym plEnd prEnd s0r) (SLeft s0l)++instance+  -- Shame I can't use pl, pr in associated type synonyms! :(+  ( pl ~ 'PParser plCh plEnd s0l+  , pr ~ 'PParser prCh prEnd s0r+  , SingParser pl+  , SingParser pr+  ) => SingParser (Then' plCh plEnd s0l prCh prEnd s0r) where+    type PS (Then' plCh plEnd s0l prCh prEnd s0r) =+        SEither+            (PS ('PParser plCh plEnd s0l))+            (STuple2+                (PR ('PParser plCh plEnd s0l))+                (PS ('PParser prCh prEnd s0r)))+    type PR (Then' plCh plEnd s0l prCh prEnd s0r) =+        STuple2+            (PR ('PParser plCh plEnd s0l))+            (PR ('PParser prCh prEnd s0r))+    singParser' = sThen (singParser @pl) (singParser @pr)+ -- | Sequence two parsers, running left then right, and return both results. infixl 4 :<*>: type (:<*>:)-    :: Parser sl rl-    -> Parser sr rr-    -> Parser (Either sl (rl, sr)) (rl, rr)+    :: PParser sl rl+    -> PParser sr rr+    -> PParser (Either sl (rl, sr)) (rl, rr) type family pl :<*>: pr where-    '(plCh, plEnd, sl) :<*>: '(prCh, prEnd, sr) =-        '(ThenChSym plCh prCh sr, ThenEndSym prEnd, Left sl)+    'PParser plCh plEnd s0l :<*>: 'PParser prCh prEnd s0r =+        Then' plCh plEnd s0l prCh prEnd s0r +type Then'+    :: ParserChSym  sl rl+    -> ParserEndSym sl rl+    -> sl+    -> ParserChSym  sr rr+    -> ParserEndSym sr rr+    -> sr+    -> PParser (Either sl (rl, sr)) (rl, rr)+type Then' plCh plEnd s0l prCh prEnd s0r =+    'PParser (ThenChSym plCh prCh s0r) (ThenEndSym plEnd prEnd s0r) (Left s0l)+ type ThenCh     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> ParserCh (Either sl (rl, sr)) (rl, rr)-type family ThenCh plCh prCh sr ch s where-    ThenCh plCh prCh sr ch (Left  sl) =-        ThenL sr (plCh @@ ch @@ sl)-    ThenCh plCh prCh _  ch (Right '(rl, sr)) =-        ThenR rl (prCh @@ ch @@ sr)+    -> PParserCh (Either sl (rl, sr)) (rl, rr)+type family ThenCh plCh prCh s0r ch s where+    ThenCh plCh prCh s0r ch (Left  sl) =+        ThenChL prCh s0r ch (plCh @@ ch @@ sl)+    ThenCh plCh prCh s0r ch (Right '(rl, sr)) =+        ThenChR rl (prCh @@ ch @@ sr) -type family ThenL sr resl where-    ThenL sr (Err  el) = Err  (EIn "Then(L)" el)-    ThenL sr (Cont sl) = Cont (Left  sl)-    ThenL sr (Done rl) = Cont (Right '(rl, sr))+type family ThenChL prCh s0r ch resl where+    ThenChL prCh s0r ch (Cont sl) = Cont (Left  sl)+    ThenChL prCh s0r ch (Done rl) =+        -- 'Done' doesn't consume, so re-parse with the R parser.+        ThenChR rl (prCh @@ ch @@ s0r)+    ThenChL prCh s0r ch (Err  el) = Err  (EThenChL el) -type family ThenR rl resr where-    ThenR rl (Err  er) = Err  (EIn "Then(R)" er)-    ThenR rl (Cont sr) = Cont (Right '(rl, sr))-    ThenR rl (Done rr) = Done '(rl, rr)+type EThenChL el = EIn "Then(L)" el+eThenChL :: SE el -> SE (EThenChL el)+eThenChL el = withSingE el $ singE -type family ThenEnd prEnd s where-    ThenEnd prEnd (Left sl) = Left (EBase "Then" (Text "ended during left"))-    ThenEnd prEnd (Right '(rl, sr)) =-        ThenEnd' rl (prEnd @@ sr)+type family ThenChR rl resr where+    ThenChR rl (Cont sr) = Cont (Right '(rl, sr))+    ThenChR rl (Done rr) = Done '(rl, rr)+    ThenChR rl (Err  er) = Err  (EThenChR er) -type family ThenEnd' rl s where-    ThenEnd' rl (Left  er) = Left  (EIn "Then(R)" er)-    ThenEnd' rl (Right rr) = Right '(rl, rr)+type EThenChR er = EIn "Then(R)" er+eThenChR :: SE er -> SE (EThenChR er)+eThenChR er = withSingE er $ singE +sThenChR+    :: srl rl+    -> SResult ssr srr resr+    -> SResult (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)+        (ThenChR rl resr)+sThenChR rl = \case+  SCont sr -> SCont $ SRight $ STuple2 rl sr+  SDone rr -> SDone $ STuple2 rl rr+  SErr  er -> SErr  $ eThenChR er++sThenChSym+    :: SParserChSym ssl srl plCh+    -> SParserChSym ssr srr prCh+    -> ssr sr+    -> SParserChSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)+        (ThenChSym plCh prCh sr)+sThenChSym plCh prCh s0r = Lam2 $ \ch -> \case+  SLeft sl ->+    case plCh @@ ch @@ sl of+      SCont sl' -> SCont $ SLeft sl'+      SDone rl  -> sThenChR rl (prCh @@ ch @@ s0r)+      SErr  el  -> SErr  $ eThenChL el+  SRight (STuple2 rl sr) -> sThenChR rl (prCh @@ ch @@ sr)+ type ThenChSym     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr     -> ParserChSym (Either sl (rl, sr)) (rl, rr)-data ThenChSym plCh prCh sr f-type instance App (ThenChSym plCh prCh sr) f = ThenChSym1 plCh prCh sr f+data ThenChSym plCh prCh s0r f+type instance App (ThenChSym plCh prCh s0r) f = ThenChSym1 plCh prCh s0r f  type ThenChSym1     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> Char -> Either sl (rl, sr) ~> Result (Either sl (rl, sr)) (rl, rr)-data ThenChSym1 plCh prCh sr ch s-type instance App (ThenChSym1 plCh prCh sr ch) s = ThenCh plCh prCh sr ch s+    -> ParserChSym1 (Either sl (rl, sr)) (rl, rr)+data ThenChSym1 plCh prCh s0r ch s+type instance App (ThenChSym1 plCh prCh s0r ch) s = ThenCh plCh prCh s0r ch s +type family ThenEnd plEnd prEnd s0r s where+    -- | EOT during R: call R end+    ThenEnd plEnd prEnd s0r (Right '(rl, sr)) = ThenEndR rl    (prEnd @@ sr)+    -- | EOT during L: call L end, pass R end+    ThenEnd plEnd prEnd s0r (Left sl)         = ThenEndL prEnd s0r (plEnd @@ sl)++type family ThenEndR rl res where+    -- | EOT during R, R end succeeds: success+    ThenEndR rl (Right rr) = Right '(rl, rr)+    -- | EOT during R, R end fails: error+    ThenEndR rl (Left  er) = Left  (EThenEndR er)++type EThenEndR er = EIn "Then(R) end" er+eThenEndR :: SE er -> SE (EThenEndR er)+eThenEndR er = withSingE er $ singE++sThenEndR+    :: srl rl+    -> SResultEnd srr res+    -> SResultEnd (STuple2 srl srr) (ThenEndR rl res)+sThenEndR rl = \case+  SRight rr -> SRight $ STuple2 rl rr+  SLeft  er -> SLeft  $ eThenEndR er++type family ThenEndL prEnd s0r res where+    -- | EOT during L, L end succeeds: call R end on initial R state+    ThenEndL prEnd s0r (Right rl) = ThenEndR rl (prEnd @@ s0r)+    -- | EOT during L, L end fails: error+    ThenEndL prEnd s0r (Left  el) = Left (EThenEndL el)++type EThenEndL er = EIn "Then(L) end" er+eThenEndL :: SE er -> SE (EThenEndL er)+eThenEndL er = withSingE er $ singE++sThenEndSym+    :: SParserEndSym ssl srl plEnd+    -> SParserEndSym ssr srr prEnd+    -> ssr s0r+    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) (STuple2 srl srr)+        (ThenEndSym plEnd prEnd s0r)+sThenEndSym plEnd prEnd s0r = Lam $ \case+  SRight (STuple2 rl sr) -> sThenEndR rl (prEnd @@ sr)+  SLeft  sl ->+    case plEnd @@ sl of+      SRight rl -> sThenEndR rl (prEnd @@ s0r)+      SLeft  el -> SLeft $ eThenEndL el+ type ThenEndSym-    :: ParserEndSym sr rr+    :: ParserEndSym sl rl+    -> ParserEndSym sr rr+    -> sr     -> ParserEndSym (Either sl (rl, sr)) (rl, rr)-data ThenEndSym prEnd s-type instance App (ThenEndSym prEnd) s = ThenEnd prEnd s+data ThenEndSym plEnd prEnd s0r s+type instance App (ThenEndSym plEnd prEnd s0r) s = ThenEnd plEnd prEnd s0r s
src/Symparsec/Parser/Then/VoidLeft.hs view
@@ -1,70 +1,179 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Then.VoidLeft ( (:*>:) ) where+module Symparsec.Parser.Then.VoidLeft where -import Symparsec.Parser-import GHC.TypeLits-import DeFun.Core ( type (~>), type (@@), type App )+import Symparsec.Parser.Common+import Singleraeh.Either ( SEither(..) )+import DeFun.Core +type SPThenVL ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =+    SParser+        (SEither ssl ssr)+        srr+        (ThenVL' plCh plEnd s0l prCh prEnd s0r)++sThenVL+    :: SParser   ssl srl ('PParser plCh plEnd s0l)+    -> SParser   ssr srr ('PParser prCh prEnd s0r)+    -> SPThenVL  ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r+sThenVL (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =+    SParser (sThenVLChSym plCh prCh s0r) (sThenVLEndSym plEnd prEnd s0r) (SLeft s0l)++instance+  ( pl ~ 'PParser plCh plEnd s0l+  , pr ~ 'PParser prCh prEnd s0r+  , SingParser pl+  , SingParser pr+  ) => SingParser (ThenVL' plCh plEnd s0l prCh prEnd s0r) where+    type PS (ThenVL' plCh plEnd s0l prCh prEnd s0r) =+        SEither+            (PS ('PParser plCh plEnd s0l))+            (PS ('PParser prCh prEnd s0r))+    type PR (ThenVL' plCh plEnd s0l prCh prEnd s0r) =+        PR ('PParser prCh prEnd s0r)+    singParser' = sThenVL (singParser @pl) (singParser @pr)+ -- | Sequence two parsers, running left then right, and discard the return value --   of the left parser. infixl 4 :*>: type (:*>:)-    :: Parser sl rl-    -> Parser sr rr-    -> Parser (Either sl sr) rr+    :: PParser sl rl+    -> PParser sr rr+    -> PParser (Either sl sr) rr type family pl :*>: pr where-    '(plCh, plEnd, sl) :*>: '(prCh, prEnd, sr) =-        '(ThenVLChSym plCh prCh sr, ThenVLEndSym prEnd, Left sl)+    'PParser plCh plEnd s0l :*>: 'PParser prCh prEnd s0r =+        ThenVL' plCh plEnd s0l prCh prEnd s0r +type ThenVL'+    :: ParserChSym  sl rl+    -> ParserEndSym sl rl+    -> sl+    -> ParserChSym  sr rr+    -> ParserEndSym sr rr+    -> sr+    -> PParser (Either sl sr) rr+type ThenVL' plCh plEnd s0l prCh prEnd s0r =+    'PParser (ThenVLChSym plCh prCh s0r) (ThenVLEndSym plEnd prEnd s0r) (Left s0l)+ type ThenVLCh     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> ParserCh (Either sl sr) rr-type family ThenVLCh plCh prCh sr ch s where-    ThenVLCh plCh prCh sr ch (Left  sl) =-        ThenVLL sr (plCh @@ ch @@ sl)-    ThenVLCh plCh prCh _  ch (Right sr) =-        ThenVLR (prCh @@ ch @@ sr)+    -> PParserCh (Either sl sr) rr+type family ThenVLCh plCh prCh s0r ch s where+    ThenVLCh plCh prCh s0r ch (Left  sl) =+        ThenVLChL prCh s0r ch (plCh @@ ch @@ sl)+    ThenVLCh plCh prCh s0r ch (Right sr) =+        ThenVLChR (prCh @@ ch @@ sr) -type family ThenVLL sr resl where-    ThenVLL sr (Err  el) = Err  (EIn "ThenVL(L)" el)-    ThenVLL sr (Cont sl) = Cont (Left  sl)-    ThenVLL sr (Done rl) = Cont (Right sr)+type family ThenVLChL prCh s0r ch resl where+    ThenVLChL prCh s0r ch (Cont sl) = Cont (Left  sl)+    ThenVLChL prCh s0r ch (Done rl) =+        -- 'Done' doesn't consume, so re-parse with the R parser.+        ThenVLChR (prCh @@ ch @@ s0r)+    ThenVLChL prCh s0r ch (Err  el) = Err  (EThenVLChL el) -type family ThenVLR resr where-    ThenVLR (Err  er) = Err  (EIn "ThenVL(R)" er)-    ThenVLR (Cont sr) = Cont (Right sr)-    ThenVLR (Done rr) = Done rr+type EThenVLChL el = EIn "ThenVL(L)" el+eThenVLChL :: SE el -> SE (EThenVLChL el)+eThenVLChL el = withSingE el $ singE -type family ThenVLEnd prEnd s where-    ThenVLEnd prEnd (Left  sl) =-        Left (EBase "ThenVL" (Text "ended during left"))-    ThenVLEnd prEnd (Right sr) = ThenVLEnd' (prEnd @@ sr)+type family ThenVLChR resr where+    ThenVLChR (Cont sr) = Cont (Right sr)+    ThenVLChR (Done rr) = Done rr+    ThenVLChR (Err  er) = Err  (EThenVLChR er) -type family ThenVLEnd' s where-    ThenVLEnd' (Left  er) = Left  (EIn "ThenVL(R)" er)-    ThenVLEnd' (Right rr) = Right rr+type EThenVLChR er = EIn "ThenVL(R)" er+eThenVLChR :: SE er -> SE (EThenVLChR er)+eThenVLChR er = withSingE er $ singE +sThenVLChR+    :: SResult ssr srr resr+    -> SResult (SEither ssl ssr) srr (ThenVLChR resr)+sThenVLChR = \case+  SCont sr -> SCont $ SRight sr+  SDone rr -> SDone rr+  SErr  er -> SErr  $ eThenVLChR er++sThenVLChSym+    :: SParserChSym ssl srl plCh+    -> SParserChSym ssr srr prCh+    -> ssr sr+    -> SParserChSym (SEither ssl ssr) srr+        (ThenVLChSym plCh prCh sr)+sThenVLChSym plCh prCh s0r = Lam2 $ \ch -> \case+  SLeft  sl ->+    case plCh @@ ch @@ sl of+      SCont  sl' -> SCont $ SLeft sl'+      SDone _rl  -> sThenVLChR (prCh @@ ch @@ s0r)+      SErr   el  -> SErr  $ eThenVLChL el+  SRight sr -> sThenVLChR (prCh @@ ch @@ sr)+ type ThenVLChSym     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr     -> ParserChSym (Either sl sr) rr data ThenVLChSym plCh prCh sr f-type instance App (ThenVLChSym plCh prCh sr) f = ThenVLChSym1 plCh prCh sr f+type instance App (ThenVLChSym plCh prCh s0r) f = ThenVLChSym1 plCh prCh s0r f  type ThenVLChSym1     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> Char -> Either sl sr ~> Result (Either sl sr) rr-data ThenVLChSym1 plCh prCh sr ch s-type instance App (ThenVLChSym1 plCh prCh sr ch) s = ThenVLCh plCh prCh sr ch s+    -> ParserChSym1 (Either sl sr) rr+data ThenVLChSym1 plCh prCh s0r ch s+type instance App (ThenVLChSym1 plCh prCh s0r ch) s = ThenVLCh plCh prCh s0r ch s +type family ThenVLEnd plEnd prEnd s0r s where+    -- | EOT during R: call R end+    ThenVLEnd plEnd prEnd s0r (Right sr) = ThenVLEndR           (prEnd @@ sr)+    -- | EOT during L: call L end, pass R end+    ThenVLEnd plEnd prEnd s0r (Left  sl) = ThenVLEndL prEnd s0r (plEnd @@ sl)++type family ThenVLEndR res where+    -- | EOT during R, R end succeeds: success+    ThenVLEndR (Right rr) = Right rr+    -- | EOT during R, R end fails: error+    ThenVLEndR (Left  er) = Left  (EThenVLEndR er)++type EThenVLEndR er = EIn "ThenVL(R) end" er+eThenVLEndR :: SE er -> SE (EThenVLEndR er)+eThenVLEndR er = withSingE er $ singE++sThenVLEndR+    :: SResultEnd srr res+    -> SResultEnd srr (ThenVLEndR res)+sThenVLEndR = \case+  SRight rr -> SRight rr+  SLeft  er -> SLeft  $ eThenVLEndR er++type family ThenVLEndL prEnd s0r res where+    -- | EOT during L, L end succeeds: call R end on initial R state+    ThenVLEndL prEnd s0r (Right rl) = ThenVLEndR (prEnd @@ s0r)+    -- | EOT during L, L end fails: error+    ThenVLEndL prEnd s0r (Left  el) = Left (EThenVLEndL el)++type EThenVLEndL er = EIn "ThenVL(L) end" er+eThenVLEndL :: SE er -> SE (EThenVLEndL er)+eThenVLEndL er = withSingE er $ singE++sThenVLEndSym+    :: SParserEndSym ssl srl plEnd+    -> SParserEndSym ssr srr prEnd+    -> ssr s0r+    -> SParserEndSym (SEither ssl ssr) srr+        (ThenVLEndSym plEnd prEnd s0r)+sThenVLEndSym plEnd prEnd s0r = Lam $ \case+  SRight sr -> sThenVLEndR (prEnd @@ sr)+  SLeft  sl ->+    case plEnd @@ sl of+      SRight _rl -> sThenVLEndR (prEnd @@ s0r)+      SLeft   el -> SLeft $ eThenVLEndL el+ type ThenVLEndSym-    :: ParserEndSym sr rr+    :: ParserEndSym sl rl+    -> ParserEndSym sr rr+    -> sr     -> ParserEndSym (Either sl sr) rr-data ThenVLEndSym prEnd s-type instance App (ThenVLEndSym prEnd) s = ThenVLEnd prEnd s+data ThenVLEndSym plEnd prEnd s0r s+type instance App (ThenVLEndSym plEnd prEnd s0r) s = ThenVLEnd plEnd prEnd s0r s
src/Symparsec/Parser/Then/VoidRight.hs view
@@ -1,74 +1,185 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Then.VoidRight ( (:<*:) ) where+module Symparsec.Parser.Then.VoidRight where -import Symparsec.Parser-import GHC.TypeLits-import DeFun.Core ( type (~>), type (@@), type App )+import Symparsec.Parser.Common+import Singleraeh.Either ( SEither(..) )+import Singleraeh.Tuple ( STuple2(..) )+import DeFun.Core +type SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =+    SParser+        (SEither ssl (STuple2 srl ssr))+        srl+        (ThenVR' plCh plEnd s0l prCh prEnd s0r)++sThenVR+    :: SParser  ssl srl ('PParser plCh plEnd s0l)+    -> SParser  ssr srr ('PParser prCh prEnd s0r)+    -> SPThenVR ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r+sThenVR (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) =+    SParser (sThenVRChSym plCh prCh s0r) (sThenVREndSym plEnd prEnd s0r) (SLeft s0l)++instance+  -- Shame I can't use pl, pr in associated type synonyms! :(+  ( pl ~ 'PParser plCh plEnd s0l+  , pr ~ 'PParser prCh prEnd s0r+  , SingParser pl+  , SingParser pr+  ) => SingParser (ThenVR' plCh plEnd s0l prCh prEnd s0r) where+    type PS (ThenVR' plCh plEnd s0l prCh prEnd s0r) =+        SEither+            (PS ('PParser plCh plEnd s0l))+            (STuple2+                (PR ('PParser plCh plEnd s0l))+                (PS ('PParser prCh prEnd s0r)))+    type PR (ThenVR' plCh plEnd s0l prCh prEnd s0r) =+        PR ('PParser plCh plEnd s0l)+    singParser' = sThenVR (singParser @pl) (singParser @pr)+ -- | Sequence two parsers, running left then right, and discard the return value --   of the right parser.------ Consider using 'Data.Type.Symbol.Parser.Parser.Then.VoidLeft.:*>:' instead,--- which is simpler and potentially faster since we parse left-to-right. infixl 4 :<*: type (:<*:)-    :: Parser sl rl-    -> Parser sr rr-    -> Parser (Either sl (rl, sr)) rl+    :: PParser sl rl+    -> PParser sr rr+    -> PParser (Either sl (rl, sr)) rl type family pl :<*: pr where-    '(plCh, plEnd, sl) :<*: '(prCh, prEnd, sr) =-        '(ThenVRChSym plCh prCh sr, ThenVREndSym prEnd, Left sl)+    'PParser plCh plEnd s0l :<*: 'PParser prCh prEnd s0r =+        ThenVR' plCh plEnd s0l prCh prEnd s0r +type ThenVR'+    :: ParserChSym  sl rl+    -> ParserEndSym sl rl+    -> sl+    -> ParserChSym  sr rr+    -> ParserEndSym sr rr+    -> sr+    -> PParser (Either sl (rl, sr)) rl+type ThenVR' plCh plEnd s0l prCh prEnd s0r =+    'PParser (ThenVRChSym plCh prCh s0r) (ThenVREndSym plEnd prEnd s0r) (Left s0l)+ type ThenVRCh     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> ParserCh (Either sl (rl, sr)) rl-type family ThenVRCh plCh prCh sr ch s where-    ThenVRCh plCh prCh sr ch (Left  sl) =-        ThenVRL sr (plCh @@ ch @@ sl)-    ThenVRCh plCh prCh _  ch (Right '(rl, sr)) =-        ThenVRR rl (prCh @@ ch @@ sr)+    -> PParserCh (Either sl (rl, sr)) rl+type family ThenVRCh plCh prCh s0r ch s where+    ThenVRCh plCh prCh s0r ch (Left  sl) =+        ThenVRChL prCh s0r ch (plCh @@ ch @@ sl)+    ThenVRCh plCh prCh s0r ch (Right '(rl, sr)) =+        ThenVRChR rl (prCh @@ ch @@ sr) -type family ThenVRL sr resl where-    ThenVRL sr (Err  el) = Err  (EIn "ThenVR(L)" el)-    ThenVRL sr (Cont sl) = Cont (Left  sl)-    ThenVRL sr (Done rl) = Cont (Right '(rl, sr))+type family ThenVRChL prCh s0r ch resl where+    ThenVRChL prCh s0r ch (Cont sl) = Cont (Left  sl)+    ThenVRChL prCh s0r ch (Done rl) =+        -- 'Done' doesn't consume, so re-parse with the R parser.+        ThenVRChR rl (prCh @@ ch @@ s0r)+    ThenVRChL prCh s0r ch (Err  el) = Err  (EThenVRChL el) -type family ThenVRR rl resr where-    ThenVRR rl (Err  er) = Err  (EIn "ThenVR(R)" er)-    ThenVRR rl (Cont sr) = Cont (Right '(rl, sr))-    ThenVRR rl (Done rr) = Done rl+type EThenVRChL el = EIn "ThenVR(L)" el+eThenVRChL :: SE el -> SE (EThenVRChL el)+eThenVRChL el = withSingE el $ singE -type family ThenVREnd prEnd s where-    ThenVREnd prEnd (Left  sl) =-        Left (EBase "ThenVR" (Text "ended during left"))-    ThenVREnd prEnd (Right '(rl, sr)) =-        ThenVREnd' rl (prEnd @@ sr)+type family ThenVRChR rl resr where+    ThenVRChR rl (Cont sr) = Cont (Right '(rl, sr))+    ThenVRChR rl (Done rr) = Done rl+    ThenVRChR rl (Err  er) = Err  (EThenVRChR er) -type family ThenVREnd' rl s where-    ThenVREnd' rl (Left  er) = Left  (EIn "ThenVR(R)" er)-    ThenVREnd' rl (Right rr) = Right rl+type EThenVRChR er = EIn "ThenVR(R)" er+eThenVRChR :: SE er -> SE (EThenVRChR er)+eThenVRChR er = withSingE er $ singE +sThenVRChR+    :: srl rl+    -> SResult ssr srr resr+    -> SResult (SEither ssl (STuple2 srl ssr)) srl (ThenVRChR rl resr)+sThenVRChR rl = \case+  SCont  sr -> SCont $ SRight $ STuple2 rl sr+  SDone _rr -> SDone rl+  SErr   er -> SErr  $ eThenVRChR er++sThenVRChSym+    :: SParserChSym ssl srl plCh+    -> SParserChSym ssr srr prCh+    -> ssr sr+    -> SParserChSym (SEither ssl (STuple2 srl ssr)) srl+        (ThenVRChSym plCh prCh sr)+sThenVRChSym plCh prCh s0r = Lam2 $ \ch -> \case+  SLeft sl ->+    case plCh @@ ch @@ sl of+      SCont sl' -> SCont $ SLeft sl'+      SDone rl  -> sThenVRChR rl (prCh @@ ch @@ s0r)+      SErr  el  -> SErr  $ eThenVRChL el+  SRight (STuple2 rl sr) -> sThenVRChR rl (prCh @@ ch @@ sr)+ type ThenVRChSym     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr     -> ParserChSym (Either sl (rl, sr)) rl-data ThenVRChSym plCh prCh sr f-type instance App (ThenVRChSym plCh prCh sr) f = ThenVRChSym1 plCh prCh sr f+data ThenVRChSym plCh prCh s0r f+type instance App (ThenVRChSym plCh prCh s0r) f = ThenVRChSym1 plCh prCh s0r f  type ThenVRChSym1     :: ParserChSym sl rl     -> ParserChSym sr rr     -> sr-    -> Char -> Either sl (rl, sr) ~> Result (Either sl (rl, sr)) rl-data ThenVRChSym1 plCh prCh sr ch s-type instance App (ThenVRChSym1 plCh prCh sr ch) s = ThenVRCh plCh prCh sr ch s+    -> ParserChSym1 (Either sl (rl, sr)) rl+data ThenVRChSym1 plCh prCh s0r ch s+type instance App (ThenVRChSym1 plCh prCh s0r ch) s = ThenVRCh plCh prCh s0r ch s +type family ThenVREnd plEnd prEnd s0r s where+    -- | EOT during R: call R end+    ThenVREnd plEnd prEnd s0r (Right '(rl, sr)) = ThenVREndR rl    (prEnd @@ sr)+    -- | EOT during L: call L end, pass R end+    ThenVREnd plEnd prEnd s0r (Left sl)         = ThenVREndL prEnd s0r (plEnd @@ sl)++type family ThenVREndR rl res where+    -- | EOT during R, R end succeeds: success+    ThenVREndR rl (Right rr) = Right rl+    -- | EOT during R, R end fails: error+    ThenVREndR rl (Left  er) = Left  (EThenVREndR er)++type EThenVREndR er = EIn "ThenVR(R) end" er+eThenVREndR :: SE er -> SE (EThenVREndR er)+eThenVREndR er = withSingE er $ singE++sThenVREndR+    :: srl rl+    -> SResultEnd srr res+    -> SResultEnd srl (ThenVREndR rl res)+sThenVREndR rl = \case+  SRight _rr -> SRight rl+  SLeft   er -> SLeft  $ eThenVREndR er++type family ThenVREndL prEnd s0r res where+    -- | EOT during L, L end succeeds: call R end on initial R state+    ThenVREndL prEnd s0r (Right rl) = ThenVREndR rl (prEnd @@ s0r)+    -- | EOT during L, L end fails: error+    ThenVREndL prEnd s0r (Left  el) = Left (EThenVREndL el)++type EThenVREndL er = EIn "ThenVR(L) end" er+eThenVREndL :: SE er -> SE (EThenVREndL er)+eThenVREndL er = withSingE er $ singE++sThenVREndSym+    :: SParserEndSym ssl srl plEnd+    -> SParserEndSym ssr srr prEnd+    -> ssr s0r+    -> SParserEndSym (SEither ssl (STuple2 srl ssr)) srl+        (ThenVREndSym plEnd prEnd s0r)+sThenVREndSym plEnd prEnd s0r = Lam $ \case+  SRight (STuple2 rl sr) -> sThenVREndR rl (prEnd @@ sr)+  SLeft  sl ->+    case plEnd @@ sl of+      SRight rl -> sThenVREndR rl (prEnd @@ s0r)+      SLeft  el -> SLeft $ eThenVREndL el+ type ThenVREndSym-    :: ParserEndSym sr rr+    :: ParserEndSym sl rl+    -> ParserEndSym sr rr+    -> sr     -> ParserEndSym (Either sl (rl, sr)) rl-data ThenVREndSym prEnd s-type instance App (ThenVREndSym prEnd) s = ThenVREnd prEnd s+data ThenVREndSym plEnd prEnd s0r s+type instance App (ThenVREndSym plEnd prEnd s0r) s = ThenVREnd plEnd prEnd s0r s
src/Symparsec/Parsers.hs view
@@ -1,4 +1,4 @@--- | Re-exported type-level symbol parsers.+-- | Type-level string parsers. -- -- You may ignore the equations that Haddock displays: they are internal and -- irrelevant to library usage.@@ -10,7 +10,7 @@     (:<*>:)   ,  (:*>:)   , (:<*:)-  , (:<|>:)+  -- , (:<|>:)    -- * Positional   -- $positional@@ -40,7 +40,7 @@ import Symparsec.Parser.Literal import Symparsec.Parser.End import Symparsec.Parser.Take-import Symparsec.Parser.Or+--import Symparsec.Parser.Or  -- $binary-combinators -- Parsers that combine two parsers. Any parsers that have term-level parallels
src/Symparsec/Run.hs view
@@ -1,31 +1,107 @@ {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying/singled parsers -module Symparsec.Run ( Run ) where+module Symparsec.Run where -- ( Run, ERun(..) ) where  import Symparsec.Parser-import GHC.TypeLits-import DeFun.Core ( type (@@) )+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'.-type Run :: Parser s r -> Symbol -> Either ErrorMessage (r, Symbol)-type family Run p sym where-    Run '(pCh, pEnd, s) sym =-        MapLeftPrettyERun (RunStart pCh pEnd s (UnconsSymbol sym))+-- | 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 family RunStart pCh pEnd s msym where-    -- | Parsing non-empty string: call main loop-    RunStart pCh pEnd s (Just '(ch, sym)) =-        RunCh pCh pEnd 0 ch (UnconsSymbol sym) (pCh @@ ch @@ s)+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)) -    -- | Parsing empty string: call special early exit-    RunStart pCh pEnd s Nothing           = RunEnd0 (pEnd @@ s)+-- | 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 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' demotePR str = withSomeSSymbol str $ \sstr ->+    case sRun' (singParser @p) sstr of+      SRight (STuple2 pr sstr') -> Right (demotePR pr, fromSSymbol sstr')+      SLeft  e                  -> Left $ demoteSERun 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 str =+    case run' @p demote str of+      Right r -> r+      Left  e -> error $ show e++sRun'+    :: SParser ss sr p+    -> SSymbol str+    -> SEither SERun (STuple2 sr SSymbol) (Run' p str)+sRun' (SParser pCh pEnd s0) str =+    sRunStart pCh pEnd s0 (sUnconsSymbol 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 pCh pEnd s0 = \case+  SJust (STuple2 ch str) ->+    sRunCh pCh pEnd (SNat @0) ch (sUnconsSymbol str) (pCh @@ ch @@ s0)+  SNothing -> sRunEnd0 (pEnd @@ 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' msym res where+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)@@ -35,49 +111,96 @@         RunEnd idx ch' (pEnd @@ s)      -- | OK, and we're finished early: return value and remaining string-    RunCh pCh pEnd idx ch' msym              (Done r) =-        Right '(r, ReconsSymbol msym)+    RunCh pCh pEnd idx ch' mstr              (Done r) =+        Right '(r, ConsSymbol ch' (ReconsSymbol mstr))      -- | Parse error: return error-    RunCh pCh pEnd idx ch' msym              (Err  e) =+    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 pCh pEnd idx chPrev mstr = \case+  SCont s ->+    case mstr of+      SJust (STuple2 ch str) ->+        sRunCh pCh pEnd (idx %+ (SNat @1)) ch (sUnconsSymbol str)+            (pCh @@ ch @@ s)+      SNothing ->+        sRunEnd idx chPrev (pEnd @@ s)+  SDone r -> SRight (STuple2 r (sConsSymbol chPrev (sReconsSymbol mstr)))+  SErr  e -> SLeft (SERun idx chPrev e)+ -- | Inspect end parser result.-type RunEnd :: Natural -> Char -> Either E r -> Either ERun (r, Symbol)+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 idx ch = \case+  SRight r -> SRight (STuple2 r (SSymbol @""))+  SLeft  e -> SLeft (SERun idx ch 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) -type PrettyERun :: ERun -> ErrorMessage+sRunEnd0+    :: SEither SE sr res+    -> SEither SERun (STuple2 sr SSymbol) (RunEnd0 res)+sRunEnd0 = \case+  SRight r -> SRight (STuple2 r (SSymbol @""))+  SLeft  e -> SLeft (SERun0 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 " :<>: ShowType idx-        :<>: Text ", char " :<>: ShowType ch :$$: PrettyE 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--type family MapLeftPrettyERun eea where-    MapLeftPrettyERun (Left  e) = Left (PrettyERun e)-    MapLeftPrettyERun (Right a) = Right a---- | Re-construct the output from 'UnconsSymbol'.-type family ReconsSymbol msym where-    ReconsSymbol Nothing           = ""-    ReconsSymbol (Just '(ch, sym)) = ConsSymbol ch sym+    PrettyE (EIn   name e)     = Text name :<>: Text ": " :<>: PrettyE e  -- | Error while running parser.-data ERun+data ERun s   -- | Parser error at index X, character C.-  = ERun Natural Char E+  = ERun Natural Char (E s)    -- | Parser error on the empty string.-  | ERun0 E+  | ERun0 (E s)+    deriving stock 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 = \case+  SERun  idx ch e -> ERun  (fromSNat idx) (fromSChar ch) (demoteSE e)+  SERun0        e -> ERun0                               (demoteSE e)++instance Demotable SERun where+    type Demote SERun = ERun String+    demote = demoteSERun
symparsec.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           symparsec-version:        0.4.0+version:        1.0.0 synopsis:       Type level string parser combinators description:    Please see README.md. category:       Types, Data@@ -19,8 +19,6 @@ tested-with:     GHC==9.8   , GHC==9.6-  , GHC==9.4-  , GHC==9.2 extra-source-files:     README.md     CHANGELOG.md@@ -32,7 +30,6 @@ library   exposed-modules:       Symparsec-      Symparsec.Internal.Digits       Symparsec.Internal.List       Symparsec.Parser       Symparsec.Parser.Common@@ -40,7 +37,7 @@       Symparsec.Parser.Isolate       Symparsec.Parser.Literal       Symparsec.Parser.Natural-      Symparsec.Parser.Or+      Symparsec.Parser.Natural.Digits       Symparsec.Parser.Skip       Symparsec.Parser.Take       Symparsec.Parser.Then@@ -65,8 +62,10 @@       MagicHash   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.16 && <5+      base >=4.18 && <5     , defun-core ==0.1.*+    , singleraeh >=0.2.0 && <0.3+    , type-level-show >=0.2.1 && <0.3   default-language: GHC2021  test-suite spec@@ -89,8 +88,10 @@       MagicHash   ghc-options: -Wall -Wno-unticked-promoted-constructors   build-depends:-      base >=4.16 && <5+      base >=4.18 && <5     , defun-core ==0.1.*+    , singleraeh >=0.2.0 && <0.3     , symparsec+    , type-level-show >=0.2.1 && <0.3     , type-spec >=0.4.0.0 && <0.5   default-language: GHC2021