diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/src/Symparsec.hs b/src/Symparsec.hs --- a/src/Symparsec.hs +++ b/src/Symparsec.hs @@ -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 diff --git a/src/Symparsec/Internal/Digits.hs b/src/Symparsec/Internal/Digits.hs deleted file mode 100644 --- a/src/Symparsec/Internal/Digits.hs +++ /dev/null @@ -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 diff --git a/src/Symparsec/Parser.hs b/src/Symparsec/Parser.hs --- a/src/Symparsec/Parser.hs +++ b/src/Symparsec/Parser.hs @@ -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 diff --git a/src/Symparsec/Parser/Common.hs b/src/Symparsec/Parser/Common.hs --- a/src/Symparsec/Parser/Common.hs +++ b/src/Symparsec/Parser/Common.hs @@ -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 diff --git a/src/Symparsec/Parser/End.hs b/src/Symparsec/Parser/End.hs --- a/src/Symparsec/Parser/End.hs +++ b/src/Symparsec/Parser/End.hs @@ -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 diff --git a/src/Symparsec/Parser/Isolate.hs b/src/Symparsec/Parser/Isolate.hs --- a/src/Symparsec/Parser/Isolate.hs +++ b/src/Symparsec/Parser/Isolate.hs @@ -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 diff --git a/src/Symparsec/Parser/Literal.hs b/src/Symparsec/Parser/Literal.hs --- a/src/Symparsec/Parser/Literal.hs +++ b/src/Symparsec/Parser/Literal.hs @@ -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 diff --git a/src/Symparsec/Parser/Natural.hs b/src/Symparsec/Parser/Natural.hs --- a/src/Symparsec/Parser/Natural.hs +++ b/src/Symparsec/Parser/Natural.hs @@ -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 diff --git a/src/Symparsec/Parser/Natural/Digits.hs b/src/Symparsec/Parser/Natural/Digits.hs new file mode 100644 --- /dev/null +++ b/src/Symparsec/Parser/Natural/Digits.hs @@ -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 diff --git a/src/Symparsec/Parser/Or.hs b/src/Symparsec/Parser/Or.hs deleted file mode 100644 --- a/src/Symparsec/Parser/Or.hs +++ /dev/null @@ -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 diff --git a/src/Symparsec/Parser/Skip.hs b/src/Symparsec/Parser/Skip.hs --- a/src/Symparsec/Parser/Skip.hs +++ b/src/Symparsec/Parser/Skip.hs @@ -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 diff --git a/src/Symparsec/Parser/Take.hs b/src/Symparsec/Parser/Take.hs --- a/src/Symparsec/Parser/Take.hs +++ b/src/Symparsec/Parser/Take.hs @@ -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 diff --git a/src/Symparsec/Parser/Then.hs b/src/Symparsec/Parser/Then.hs --- a/src/Symparsec/Parser/Then.hs +++ b/src/Symparsec/Parser/Then.hs @@ -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 diff --git a/src/Symparsec/Parser/Then/VoidLeft.hs b/src/Symparsec/Parser/Then/VoidLeft.hs --- a/src/Symparsec/Parser/Then/VoidLeft.hs +++ b/src/Symparsec/Parser/Then/VoidLeft.hs @@ -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 diff --git a/src/Symparsec/Parser/Then/VoidRight.hs b/src/Symparsec/Parser/Then/VoidRight.hs --- a/src/Symparsec/Parser/Then/VoidRight.hs +++ b/src/Symparsec/Parser/Then/VoidRight.hs @@ -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 diff --git a/src/Symparsec/Parsers.hs b/src/Symparsec/Parsers.hs --- a/src/Symparsec/Parsers.hs +++ b/src/Symparsec/Parsers.hs @@ -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 diff --git a/src/Symparsec/Run.hs b/src/Symparsec/Run.hs --- a/src/Symparsec/Run.hs +++ b/src/Symparsec/Run.hs @@ -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 diff --git a/symparsec.cabal b/symparsec.cabal --- a/symparsec.cabal +++ b/symparsec.cabal @@ -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