packages feed

symparsec 1.1.1 → 2.0.0

raw patch · 37 files changed

+1154/−2239 lines, 37 files

Files

CHANGELOG.md view
@@ -1,3 +1,14 @@+## 2.0.0 (2025-10-11)+Full rewrite.++* parsers are now much more general: mutually-recursive parsers are game+  * added an example parser for a simple expression AST+* added parsers matching `Functor`, `Applicative`, `Monad` type class methods+* temporarily removed singling (will be lots of work)++Simple parsers written with the provided combinators should still function the+same, or with minimal changes.+ ## 1.1.1 (2024-06-15) * add `Apply` combinator (effectively `fmap`) * add some more runners and utils (handy for generic-data-functions)
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2024 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>+Copyright (c) 2024-2025 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the
README.md view
@@ -1,15 +1,14 @@ # Symparsec [hackage-parsec]: https://hackage.haskell.org/package/parsec -Type level string (`Symbol`) parser combinators. A [Parsec][hackage-parsec]-like-for `Symbol`s; thus, Symparsec! With many of the features you'd expect:+Type level string parser combinators. A [Parsec][hackage-parsec]-like for+`Symbol`s; thus, Symparsec! With many of the features you'd expect:  * define parsers compositionally, largely as you would on the term level+* define complex parsers, including mutually recursive ones (e.g. expression+  parsers!) * pretty, detailed parse errors-* decent performance (for simple parsers)--Parsers may also be reified and used at runtime with _guaranteed identical-behaviour_ via a healthy dose of singletons.+* good performance (probably? please help me benchmark!)  Requires GHC >= 9.6. @@ -18,24 +17,19 @@  ```haskell import Symparsec-type PExample = Skip 1 :*>: Isolate 2 NatHex :<*>: (Literal "_" :*>: TakeRest)+import DeFun.Core+type PExample = Skip 1 *> Tuple (Isolate 2 NatHex) (Literal "_" *> TakeRest) ```  Use it to parse a type-level string (in a GHCi session):  ```haskell-ghci> :k! Run PExample "xFF_"+ghci> :k! Run PExample "xFF_etc" Run ... = Right '( '(255, "etc"), "") ``` -Use it to parse a different, term-level string:--```haskell-ghci> import Singleraeh.Demote ( demote )-ghci> run' @PExample demote "abc_123"-Right ((188,"123"),"")-```+See the `Symparsec.Example` namespace for further examples.  ## Why? Via `GHC.Generics`, we may inspect Haskell data types on the type level.@@ -45,28 +39,22 @@  Also type-level Haskell authors deserve fun libraries too!! -## Design-### The parser-A parser is a 3-tuple of:--* a 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`, _do not consume character_-  * `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 state--Running such a parser is very simple:+## Limitations+Symparsec defines a lot of low-level parsers you would expect on the term level,+even monadic (bind) and applicative (ap) parser combinators. The key limitation+Symparsec grapples with is Haskell having _no type-level binders_. This means: -* initialize state-* parse character by character until end of input, or `Done`/`Err`+* no `let`s, no `where`s+* no `do` notation -Parsers may not communicate with the runner any other way. This means no-backtracking, chunking etc. This is a conscious decision, made for simplicity.-We're still able to implement a good handful of parser combinators regardless,-including a limited form of backtracking.+The workaround is writing extra functions, and writing uglier functions.+Otherwise, I believe an average term-level Parsec-like parser should look+comparable to a type-level `Symparsec` one. -This is a rough overview. See the code & Haddocks for precise details.+Writing complex type-level Haskell programs in 2025 is unintuitive. I intend to+provide guides on writing Symparsec parsers that walk through type-level+programming design patterns and solutions. Please ping me on the issues tab if+you read this, and can't find any such guides!  ## Contributing I would gladly accept further combinators or other suggestions. Please add an
+ src/Data/Type/Symbol.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE UndecidableInstances #-}++-- TODO move this to singleraeh!++-- | Type families on 'Symbol's.+module Data.Type.Symbol+  ( type Length+  , type Take, type TakeNoTailRec+  , type Drop+  , type Replicate+  ) where++import GHC.TypeLits ( type Symbol, type UnconsSymbol, type ConsSymbol )+import GHC.TypeNats ( type Natural, type (+), type (-) )+import Singleraeh.Symbol ( type RevCharsToSymbol )++-- | Calculate the length of a 'Symbol'.+type Length  ::            Symbol               -> Natural+type Length' :: Natural -> Maybe (Char, Symbol) -> Natural+type Length str = Length' 0 (UnconsSymbol str)+type family Length' len mstr where+    Length' len Nothing            = len+    Length' len (Just '(_ch, str)) = Length' (len+1) (UnconsSymbol str)++-- | Take the prefix of the given 'Symbol' of the given length.+--+-- Returns less than requested if the 'Symbol' is too short.+type Take :: Natural -> Symbol -> Symbol+type Take n str = TakeLoop '[] n (UnconsSymbol str)+type family TakeLoop chs n mstr where+    TakeLoop chs 0 _                 = RevCharsToSymbol chs+    TakeLoop chs n (Just '(ch, str)) = TakeLoop (ch:chs) (n-1) (UnconsSymbol str)+    TakeLoop chs n Nothing           = RevCharsToSymbol chs++-- | Take the prefix of the given 'Symbol' of the given length.+--+-- Returns less than requested if the 'Symbol' is too short.+--+-- Does not do tail-call recursion, but avoids doing extra work.+-- Unsure which is better.+type TakeNoTailRec :: Natural -> Symbol -> Symbol+type TakeNoTailRec n str = TakeNoTailRec' n (UnconsSymbol str)+type family TakeNoTailRec' n mstr where+  TakeNoTailRec' 0 _                 = ""+  TakeNoTailRec' n (Just '(ch, str)) = ConsSymbol ch (TakeNoTailRec' (n-1) (UnconsSymbol str))+  TakeNoTailRec' _ Nothing           = ""++-- | Drop the prefix of the given 'Symbol' of the given length.+type Drop :: Natural -> Symbol -> Symbol+type Drop n str = Drop' n (UnconsSymbol str)+type family Drop' n mstr where+    Drop' 0 (Just '(ch, str)) = ConsSymbol ch str+    Drop' n (Just '(ch, str)) = Drop' (n-1) (UnconsSymbol str)+    Drop' _ Nothing           = ""++type Replicate :: Natural -> Char -> Symbol+type Replicate n ch = ReplicateLoop ch '[] n+type family ReplicateLoop ch chs n where+    ReplicateLoop ch chs 0 = RevCharsToSymbol chs+    ReplicateLoop ch chs n = ReplicateLoop ch (ch:chs) (n-1)
src/Symparsec.hs view
@@ -1,7 +1,19 @@+{- | Top-level Symparsec module, exporting builtin parsers and runners.++I suggest importing this module qualified. Or, consider the following imports:++@+import "Symparsec.Run" qualified as Symparsec+import "Symparsec.Parsers" qualified as P+-- > :k! Symparsec.Run (P.Take 1) "hello"+@+-}+ module Symparsec   (   -- * Base definitions-    Run, run'+    type Run+  , type RunTest    -- * Parsers   , module Symparsec.Parsers
src/Symparsec/Example/Expr.hs view
@@ -1,50 +1,188 @@-{-# LANGUAGE UndecidableInstances#-}+{-# LANGUAGE UndecidableInstances #-} -{- | Experiments.+-- | An example Symparsec parser for a basic expression tree. -Turns out we can't write recursive parsers. But 'P.Apply' can help us write-handier parsers.+module Symparsec.Example.Expr where++import Symparsec.Parser.Common+import Symparsec.Utils ( type IfNatLte )+import Symparsec.Parser.Natural+import Symparsec.Parser.Natural.Digits+import Symparsec.Parser.While ( type While )+import Symparsec.Parser.While.Predicates ( type IsDecDigitSym )+import GHC.TypeNats qualified as TypeNats++{- TODO+* empty paren pairs are permitted in many cases e.g. @()1() -> ELit 1@+  * probably I should assert that >=1 thing gets parsed inside parens+  * well, I solved it. but I think in the wrong way. surely I should not be+    parsing parens in certain places. like I can't parse parens immediately+    after a number. or if I do, I need to implicitly parse a Mult. -} -module Symparsec.Example.Expr where+-- | A basic expression tree, polymorphic over a single literal type.+data Expr a+  = EBOp BOp (Expr a) (Expr a)+  | ELit a -import Numeric.Natural-import Symparsec.Parsers qualified as P-import Symparsec.Parser.While.Predicates qualified as P-import Symparsec.Parser.Apply qualified as P-import DeFun.Core-import DeFun.Function+-- | A binary operator.+data BOp = Add | Sub | Mul | Div -data Expr-  = ELit Lit-  | EBOp Expr BOp Expr+-- | Evaluate an 'Expr' of 'Natural's on the type level.+--+-- Naive, doesn't attempt to tail-call recurse.+type Eval :: Expr Natural -> Natural+type family Eval expr where+    Eval (EBOp bop l r) = EvalBOp bop (Eval l) (Eval r)+    Eval (ELit n) = n -data BOp = Plus+type EvalBOp :: BOp -> Natural -> Natural -> Natural+type family EvalBOp bop l r where+    EvalBOp Add l r = l + r+    EvalBOp Sub l r = l - r+    EvalBOp Mul l r = l * r+    EvalBOp Div l r = l `TypeNats.Div` r -data Lit-  = LNat Natural+data ExprTok+  = TokBOp BOp+  | TokParenL+  | TokParenR -type PLit  = PLNat-type PLNat = Con1 LNat P.:<$>: P.While P.IsHexDigitSym P.NatHex-type PELit = Con1 ELit P.:<$>: PLit-type PEBOp = Curry3Sym (Con3 EBOp) P.:<$>: (PExpr P.:<*>: PBOp P.:<*>: PExpr)-type PExpr = PELit---type PExpr :: PParser (P.OrS (Maybe Natural) (Maybe Natural)) Expr---type PExpr = FromEitherSym P.:<$>: (PELit P.:<|>: PEBOp)-type PBOp  = ConstSym1 Plus P.:<$>: P.Literal "+"+type PExpr :: PParser (Expr Natural)+data PExpr s+type instance App PExpr s = PExprNext s '[] '[] (UnconsState s)+type PExprNext+    :: PState+    -> [ExprTok]+    -> [Expr Natural]+    -> (Maybe Char, PState)+    -> PReply (Expr Natural)+type family PExprNext sPrev ops exprs s where+    PExprNext sPrev ops exprs '(Just ch, s) =+        PExprCh sPrev s ops exprs ch+    PExprNext sPrev ops exprs '(Nothing, s) = PExprEnd sPrev s ops exprs -type Curry3Sym-    :: (a ~> b ~> c ~> r)-    -> ((a, b), c)-    ~> r-data Curry3Sym f abc-type instance App (Curry3Sym f) '( '(a, b), c) = f @@ a @@ b @@ c+type family PExprEnd sPrev s ops exprs where+    PExprEnd sPrev s (TokBOp op:ops) exprs      = PExprEndPopOp sPrev s ops exprs op+    -- TODO what about parens+    PExprEnd sPrev s '[]      (expr:'[]) = 'Reply (OK expr) s+    PExprEnd sPrev s '[]      _          =+        'Reply (Err (Error1 "badly formed expression")) sPrev -type FromEither :: Either a a -> a-type family FromEither eaa where-    FromEither (Right a) = a-    FromEither (Left  a) = a+type family PExprEndPopOp sPrev s ops exprs op where+    PExprEndPopOp sPrev s ops (r:l:exprs) bop =+        PExprEnd sPrev s ops (EBOp bop l r : exprs)+    PExprEndPopOp sPrev s ops exprs bop =+        'Reply (Err (Error1 "badly formed expression")) sPrev -type FromEitherSym :: Either a a ~> a-data FromEitherSym eaa-type instance App FromEitherSym eaa = FromEither eaa+type family PExprCh sPrev s ops exprs ch where+    PExprCh sPrev s ops exprs ' ' = PExprNext s ops exprs (UnconsState s)+    PExprCh sPrev s ops exprs ch  = PExprELit sPrev s ops exprs ch (ParseDigitDecSym @@ ch)++type family PExprELit sPrev s ops exprs ch mDigit where+    PExprELit sPrev s ops exprs _ch (Just digit) =+        PExprELitEnd ops exprs+            (While IsDecDigitSym (NatBase1 10 ParseDigitDecSym digit) @@ s)+    PExprELit sPrev s ops exprs  ch Nothing      =+        PExprEBOp sPrev s ops exprs ch (PExprEBOpOpCh ch)++type family PExprELitEnd ops exprs res where+    PExprELitEnd ops exprs ('Reply (OK  n) s) =+        PExprNext s ops (ELit n : exprs) (UnconsState s)+    PExprELitEnd ops exprs ('Reply (Err e) s) =+        -- The digit parser we're wrapping shouldn't ever fail, due to how+        -- 'While' works, and that we've already handled the 0-length case.+        Impossible++type family PExprEBOp sPrev s ops exprs ch mbop where+    PExprEBOp sPrev s ops exprs ch (Just (TokBOp bop)) =+        PExprEBOp' sPrev s bop (BOpPrec bop) exprs ops+    PExprEBOp sPrev s ops exprs ch (Just TokParenL) =+        PExprNext sPrev (TokParenL:ops) exprs (UnconsState s)+    PExprEBOp sPrev s ops exprs ch (Just TokParenR) =+        PExprParenRStart sPrev s exprs ops+    PExprEBOp sPrev s ops exprs ch Nothing =+        'Reply (Err (Error1 "bad expression, expected digit or operator")) sPrev++type family PExprParenRStart sPrev s exprs ops where+    PExprParenRStart sPrev s exprs (TokParenL : ops) =+        'Reply (Err (Error1 "invalid bracket syntax (empty brackets, or otherwise bad)")) sPrev+    PExprParenRStart sPrev s exprs ops =+        PExprParenR sPrev s exprs ops++type family PExprParenR sPrev s exprs ops where+    PExprParenR sPrev s exprs (TokBOp bop : ops) =+        PExprParenRPopBOp sPrev s bop ops exprs+    PExprParenR sPrev s exprs (TokParenL : ops) =+        PExprNext sPrev ops exprs (UnconsState s)+    PExprParenR sPrev s exprs ops =+        'Reply (Err (Error1 "badly formed expression")) sPrev++type family PExprParenRPopBOp sPrev s bop ops exprs where+    PExprParenRPopBOp sPrev s bop ops (r:l:exprs) =+        PExprParenR sPrev s (EBOp bop l r : exprs) ops+    PExprParenRPopBOp sPrev s bop ops      exprs  =+        'Reply (Err (Error1 "badly formed expression")) sPrev++type family PExprEBOpOpCh ch where+    PExprEBOpOpCh '+' = Just (TokBOp Add)+    PExprEBOpOpCh '-' = Just (TokBOp Sub)+    PExprEBOpOpCh '*' = Just (TokBOp Mul)+    PExprEBOpOpCh '/' = Just (TokBOp Div)+    PExprEBOpOpCh '(' = Just TokParenL+    PExprEBOpOpCh ')' = Just TokParenR+    PExprEBOpOpCh _   = Nothing++type PExprEBOp'+    :: PState -> PState -> BOp -> Natural -> [Expr Natural] -> [ExprTok]+    -> PReply (Expr Natural)+type family PExprEBOp' sPrev s op prec exprs ops where+    PExprEBOp' sPrev s op prec exprs (TokBOp opPrev : ops) =+        IfNatLte prec (BOpPrec opPrev)+            (PExprEBOpPop sPrev s op prec opPrev ops exprs)+            (PExprNext sPrev (TokBOp op : TokBOp opPrev : ops) exprs (UnconsState s))+    PExprEBOp' sPrev s op prec exprs '[]          =+        PExprNext s '[TokBOp op] exprs (UnconsState s)++    -- both parens treated same as LTE prec+    -- (how could I better design this?)+    PExprEBOp' sPrev s op prec exprs (TokParenL : ops) =+        PExprNext sPrev (TokBOp op : TokParenL : ops) exprs (UnconsState s)+    PExprEBOp' sPrev s op prec exprs (TokParenR : ops) =+        PExprNext sPrev (TokBOp op : TokParenR : ops) exprs (UnconsState s)++type family PExprEBOpPop sPrev s op prec opPrev ops exprs where+    PExprEBOpPop sPrev s op prec opPrev ops (r:l:exprs) =+        PExprEBOp' sPrev s op prec (EBOp opPrev l r : exprs) ops+    PExprEBOpPop sPrev s op prec opPrev ops exprs =+        'Reply (Err (Error1 "badly formed expression")) sPrev++type BOpPrec :: BOp -> Natural+type family BOpPrec bop where+    BOpPrec Add = 2+    BOpPrec Sub = 2+    BOpPrec Mul = 3+    BOpPrec Div = 3++{-+import GHC.TypeError qualified as TE++-- | Build an 'Expr' from a postfix stack (RPN style).+--+-- The stack must be a valid 'Expr'. It will type error if not.+type FromRpn:: [ExprTok a] -> Expr a+type FromRpn toks = FromRpnEnd (FromRpn' '[] toks)++type FromRpn' :: [Expr a] -> [ExprTok a] -> [Expr a]+type family FromRpn' es toks where+    FromRpn' es       (TokLit a   : toks) =+        FromRpn' (ELit a       : es) toks+    FromRpn' (r:l:es) (TokBOp bop : toks) =+        FromRpn' (EBOp bop l r : es) toks+    FromRpn' es       '[]                 = es++type family FromRpnEnd res where+    FromRpnEnd    '[]  = TE.TypeError (TE.Text "bad RPN: empty")+    FromRpnEnd (e:'[]) = e+    FromRpnEnd _       = TE.TypeError (TE.Text "bad RPN: unused operands")+-}
src/Symparsec/Parser.hs view
@@ -1,195 +1,152 @@-{-# 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-  (-  -- * Parser-    Parser(..), PParser(..), ResultOf, SParser(..)-  , ParserCh, PParserCh, ParserChSym, ParserChSym1, SParserChSym, SParserChSym1-  , ParserEnd, PParserEnd, ParserEndSym, SParserEndSym-  , ParserSInit, ParserSInitSym, SParserSInitSym-  , Result(..), PResult, SResult(..)-  , PResultEnd, SResultEnd-  , PResultSInit, SResultSInit--  -- * Error-  , E(..), PE, SE(..), demoteSE, SingE(singE), withSingE+{-# LANGUAGE UndecidableInstances #-} -  -- * Singling-  , SingParser(..)-  , singParser-  ) where+module Symparsec.Parser where -import GHC.TypeLits import DeFun.Core-import GHC.Exts ( withDict )-import TypeLevelShow.Doc-import Singleraeh.Either ( SEither )+import GHC.TypeLits ( type Symbol )+import GHC.TypeNats ( type Natural )+ import Singleraeh.Demote-import Singleraeh.Tuple ( STuple2 )-import Data.Kind ( Type )+import Data.Kind ( type Type )+import GHC.TypeLits ( type SSymbol, fromSSymbol )+import GHC.TypeNats ( type SNat, fromSNat )+import Singleraeh.List+--import Singleraeh.Symbol -data Parser str s r = Parser-  { parserCh  :: ParserCh  str s r-  , parserEnd :: ParserEnd str s r-  , parserS0  :: s-  }+-- | Parser state.+data State str n = State+  -- | Remaining input.+  { remaining :: str --- | 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-  }+  -- | Remaining permitted length.+  --+  -- Must be less than or equal to the actual length of the remaining input.+  -- Parsers must use this field when reading from input:+  --+  -- * if ==0, treat as end of input.+  -- * if  >0 but remaining input is empty, unrecoverable parser error+  --+  -- This extra bookkeeping permits much simpler parser design, specifically for+  -- parsers that act on a substring of the input.+  , length :: n --- | The result type of a type-level parser. (Sometimes handy.)-type ResultOf (p :: PParser s r) = r+  -- | Index in the input string.+  --+  -- Overall index. Used for nicer error reporting after parse completion.+  , index :: n+  } deriving stock Show --- | 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)+-- | Promoted 'State'.+type PState = State Symbol Natural --- | Parse a 'Char' with the given state.-type  ParserCh str s r = Char -> s -> Result str s r-type PParserCh     s r = ParserCh Symbol s r+-- | Singled 'State'.+data SState (s :: PState) where+    SState :: SSymbol rem -> SNat len -> SNat idx -> SState ('State rem len idx) --- | A defunctionalization symbol for a 'ParserCh'.-type ParserChSym s r = Char ~> s ~> PResult s r+-- | Demote an 'SState'.+demoteSState :: SState s -> State String Natural+demoteSState (SState srem slen sidx) =+    State (fromSSymbol srem) (fromSNat slen) (fromSNat sidx) --- | A partially-applied defunctionalization symbol for a 'ParserCh'.-type ParserChSym1 s r = Char -> s ~> PResult s r+instance Demotable SState where+    type Demote SState = State String Natural+    demote = demoteSState -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)+{-+data Span n = Span+  { start :: n+  , end   :: n+  } deriving stock Show+-} --- | What a parser should do at the end of a 'Symbol'.-type  ParserEnd str s r = s -> ResultEnd str r-type PParserEnd     s r = ParserEnd Symbol s r+data Error str = Error+  { detail :: [str]+  } deriving stock Show --- | A defunctionalization symbol for a 'ParserEnd'.-type ParserEndSym s r = s ~> PResultEnd r+-- | Promoted 'Error'.+type PError = Error Symbol -type SParserEndSym ss sr pEnd = Lam ss (SResultEnd sr) pEnd+-- | Singled 'Error'.+data SError (e :: PError) where+    SError :: SList SSymbol detail -> SError ('Error detail) -type ParserSInit s0 s = s0 -> PResultSInit s-type ParserSInitSym s0 s = s0 ~> PResultSInit s-type SParserSInitSym ss0 ss sInit = Lam ss0 (SResultSInit ss) sInit+-- | Demote an 'SError'.+demoteSError :: SError e -> Error String+demoteSError (SError sdetail) = Error $ demoteSList fromSSymbol sdetail --- | 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+instance Demotable SError where+    type Demote SError = Error String+    demote = demoteSError --- | Promoted 'Result'.-type PResult = Result Symbol+-- | Parser completion: result, and final state.+--+-- TODO: megaparsec also returns a bool indicating if any input was consumed.+-- Unsure what it's used for.+data Reply str n a = Reply+  { result :: Result str n a -- ^ Parse result.+  , state  :: State str n    -- ^ Final parser state.+  } deriving stock Show -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)+-- | Promoted 'Reply'.+type PReply = Reply Symbol Natural -type  ResultEnd str =  Either (E str)-type PResultEnd     =  Either PE-type SResultEnd     = SEither SE+-- | Singled 'Reply'.+data SReply (sa :: a -> Type) (rep :: PReply a) where+    SReply :: SResult sa result -> SState state -> SReply sa ('Reply result state) -type PResultSInit s = Either (PE, s) s-type SResultSInit ss = SEither (STuple2 SE ss) ss+-- | Demote an 'SReply.+demoteSReply+    :: (forall a. sa a -> da)+    -> SReply sa rep+    -> Reply String Natural da+demoteSReply demoteSA (SReply sresult sstate) =+    Reply (demoteSResult demoteSA sresult) (demoteSState sstate) --- | Parser error.------ Promotable. Instantiate with 'String' for term-level, 'Symbol' for--- type-level.-data E str-  -- | Base parser error.-  = EBase-        str       -- ^ parser name-        (Doc str) -- ^ error message+instance Demotable sa => Demotable (SReply sa) where+    type Demote (SReply sa) = Reply String Natural (Demote sa)+    demote = demoteSReply demote -  -- | Inner parser error inside combinator.-  | EIn-        str     -- ^ combinator name-        (E str) -- ^ inner error+-- | Parse result: a value, or an error.+data Result str n a = OK a            -- ^ Parser succeeded.+                    | Err (Error str) -- ^ Parser failed.     deriving stock Show --- | Promoted 'E'.-type PE = E Symbol--data SE (e :: PE) where-    SEBase :: SSymbol name -> SDoc doc -> SE (EBase name doc)-    SEIn   :: SSymbol name -> SE   e   -> SE (EIn name e)+-- | Promoted 'Result'.+type PResult = Result Symbol Natural -demoteSE :: SE e -> E String-demoteSE = \case-  SEBase sname sdoc -> EBase (fromSSymbol sname) (demoteDoc sdoc)-  SEIn   sname se   -> EIn   (fromSSymbol sname) (demoteSE  se)+--type SState = State +--type SResult :: _ -> Type+-- TODO ^ how to do explicit kind signature for GADT? -instance Demotable SE where-    type Demote SE = E String-    demote = demoteSE+-- | Singled 'Result'.+data SResult (sa :: a -> Type) (res :: PResult a) where+    SOK  :: sa a     -> SResult sa (OK a)+    SErr :: SError e -> SResult sa (Err e) -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)+-- | Demote an 'SResult'.+demoteSResult+    :: (forall a. sa a -> da)+    -> SResult sa res+    -> Result String Natural da+demoteSResult demoteSA = \case+  SOK  sa -> OK  $ demoteSA sa+  SErr se -> Err $ demoteSError se -withSingE :: forall e r. SE e -> (SingE e => r) -> r-withSingE = withDict @(SingE e)+instance Demotable sa => Demotable (SResult sa) where+    type Demote (SResult sa) = Result String Natural (Demote sa)+    demote = demoteSResult demote --- | Promoted parsers with singled implementations.-class SingParser (p :: PParser s r) where-    -- | A singleton for the parser state.-    type PS  p :: s -> Type+-- | A parser is a function on parser state.+type Parser str n a = State str n -> Reply str n a -    -- | A singleton for the parser return type.-    type PR  p :: r -> Type+-- | Promoted 'Parser': a defunctionalization symbol to a function on promoted+--   parser state.+type PParser a = PState ~> PReply a -    -- | The singled parser.-    singParser' :: SParser (PS p) (PR p) p+-- | Singled 'Parser'.+type SParser sa p = Lam SState (SReply sa) p+--data SParser (sa :: a -> Type) (p :: PParser a) where+ --   SParser :: Lam SState (SReply sa) (PParser a) --- | 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+--class SingParser (p :: PParser a) where+--    singParser :: SParser sa p
+ src/Symparsec/Parser/Alternative.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Type-level string parsers shaped like 'Alternative' functions.++module Symparsec.Parser.Alternative+  ( type (<|>), type Empty+  , type Optional+  ) where++import Symparsec.Parser.Functor+import Symparsec.Parser.Applicative+import Symparsec.Parser.Common+import DeFun.Core++-- | 'Control.Alternative.<|>' for parsers. Try the left parser; if it succeeds, return the result,+-- else try the right parser with the left parser's output state.+--+-- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.+--+-- TODO shitty errors+type (<|>) :: PParser a -> PParser a -> PParser a+infixl 3 <|>+data (<|>) l r s+type instance App (l <|> r) s = Plus r (l @@ s)+type Plus :: PParser a -> PReply a -> PReply a+type family Plus r rep where+    Plus r ('Reply (OK   a) s) = 'Reply (OK a) s+    Plus r ('Reply (Err _e) s) = r @@ s++-- | 'Control.Alternative.empty' for parsers. Immediately fail with no consumption.+type Empty :: PParser a+data Empty s+type instance App Empty s = 'Reply (Err (Error1 "called empty parser")) s++-- | 'Control.Alternative.optional' for parsers.+type Optional :: PParser a -> PParser (Maybe a)+type Optional p = Con1 Just <$> p <|> Pure Nothing++{- Wow, I guess that works. But also, the manual version:+data Optional p s+type instance App (Optional p) s = OptionalEnd (p @@ s)++type family OptionalEnd rep where+    OptionalEnd ('Reply (OK   a) s) = 'Reply (OK (Just a)) s+    OptionalEnd ('Reply (Err _e) s) = 'Reply (OK Nothing)  s+-}
+ src/Symparsec/Parser/Applicative.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Type-level string parsers shaped like 'Applicative' functions.++module Symparsec.Parser.Applicative+  ( type (<*>), type Pure+  , type LiftA2+  , type (*>), type (<*)+  ) where++import Symparsec.Parser.Common+import Symparsec.Parser.Functor+import DeFun.Function ( type IdSym, type ConstSym )++-- | '<*>' for parsers. Sequence two parsers, left to right.+type (<*>) :: PParser (a ~> b) -> PParser a -> PParser b+infixl 4 <*>+data (<*>) l r s+type instance App (l <*> r) s = ApL r (l @@ s)+type ApL :: PParser a -> PReply (a ~> b) -> PReply b+type family ApL r rep where+    ApL r ('Reply (OK  fa) s) = (fa <$> r) @@ s+    ApL r ('Reply (Err e)  s) = 'Reply (Err e) s++-- | 'pure' for parsers. Non-consuming parser that just returns the given value.+type Pure :: a -> PParser a+data Pure a s+type instance App (Pure a) s = 'Reply (OK a) s++-- | 'liftA2' for parsers. Sequence two parsers, and combine their results with+-- a binary type function.+type LiftA2 :: (a ~> b ~> c) -> PParser a -> PParser b -> PParser c+type LiftA2 f l r = (f <$> l) <*> r++-- | '*>' for parsers. Sequence two parsers left to right, discarding the value+-- of the left parser.+type (*>) :: PParser a -> PParser b -> PParser b+infixl 4 *>+type l *> r = (IdSym <$ l) <*> r++-- | '<*' for parsers. Sequence two parsers left to right, discarding the value+-- of the right parser.+type (<*) :: PParser a -> PParser b -> PParser a+infixl 4 <*+type l <* r = LiftA2 ConstSym l r
− src/Symparsec/Parser/Apply.hs 
@@ -1,61 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Symparsec.Parser.Apply where--import Symparsec.Parser.Common---- | Apply the given type function to the result.------ Effectively 'fmap' for parsers.-type (:<$>:) :: (r ~> r') -> PParser s r -> PParser s r'-type family f :<$>: p where-    f :<$>: 'PParser pCh pEnd s0 = Apply' f pCh pEnd s0---- unwrapped for instances-type Apply' f pCh pEnd s0 = 'PParser (ApplyChSym f pCh) (ApplyEndSym f pEnd) s0---- TODO: Singling is a pain, similar to While. Let's ignore it for now.--type ApplyCh-    :: (r ~> r')-    -> ParserChSym s r-    -> PParserCh s r'-type family ApplyCh f pCh ch s where-    ApplyCh f pCh ch s = ApplyCh' f (pCh @@ ch @@ s)--type family ApplyCh' f res where-    ApplyCh' f (Cont s) = Cont s-    ApplyCh' f (Done r) = Done (f @@ r)-    ApplyCh' f (Err  e) = Err e--type ApplyChSym-    :: (r ~> r')-    -> ParserChSym s r-    -> ParserChSym s r'-data ApplyChSym f pCh x-type instance App (ApplyChSym f pCh) x = ApplyChSym1 f pCh x--type ApplyChSym1-    :: (r ~> r')-    -> ParserChSym  s r-    -> ParserChSym1 s r'-data ApplyChSym1 f pCh ch s-type instance App (ApplyChSym1 f pCh ch) s = ApplyCh f pCh ch s--type ApplyEnd-    :: (r ~> r')-    -> ParserEndSym s r-    -> PParserEnd s r'-type family ApplyEnd f pEnd s where-    ApplyEnd f pEnd s = ApplyEnd' f (pEnd @@ s)--type family ApplyEnd' f res where-    ApplyEnd' f (Right r) = Right (f @@ r)-    ApplyEnd' f (Left  e) = Left  e--type ApplyEndSym-    :: (r ~> r')-    -> ParserEndSym s r-    -> ParserEndSym s r'-data ApplyEndSym f pEnd s-type instance App (ApplyEndSym f pEnd) s = ApplyEnd f pEnd s
src/Symparsec/Parser/Common.hs view
@@ -1,49 +1,82 @@--- | Common definitions for parsers.+{-# LANGUAGE UndecidableInstances #-} +-- | Common definitions used by parsers.+ module Symparsec.Parser.Common   (+  -- * Common definitions+    type UnconsState+  , type Error1+  --, type Err1+  , type EStrInputTooShort, type EStrWrongChar+  --, type Err, type Done+  , type Impossible+   -- * Re-exports-    module Symparsec.Parser-  , Doc(..)-  , type (~>), type (@@), type App+  , module Symparsec.Parser+  , Doc(..), type (++)+  , type App -  -- * Common definitions-  , FailChSym,  failChSym-  , FailEndSym, failEndSym-  , ErrParserLimitation+  -- ** Common imports+  -- $common-imports+  , type Symbol, type UnconsSymbol, ConsSymbol+  , type Natural, type (+), type (-), type (*)+  , type ShowNatDec, type ShowChar+  , type (@@), type (~>)   ) where  import Symparsec.Parser-import GHC.TypeLits hiding ( ErrorMessage(..) ) import DeFun.Core+import GHC.TypeLits ( type Symbol, type UnconsSymbol, type ConsSymbol )+import GHC.TypeNats ( type Natural, type (+), type (-), type (*) ) import TypeLevelShow.Doc-import Singleraeh.Either+import TypeLevelShow.Natural ( type ShowNatDec )+import TypeLevelShow.Utils ( type ShowChar, type (++) )+-- TODO clean up (++) stuff, probably just export my own one+import GHC.TypeError qualified as TE --- | Fail with the given message when given any character to parse.-type FailCh name e = Err (EBase name e)+-- $common-imports+-- Not used by all parsers, but common enough that we'll export them here. -type FailChSym :: Symbol -> PDoc -> ParserChSym s r-data FailChSym name e f-type instance App (FailChSym name e) f = FailChSym1 name e f+-- TODO this is pre-spans+--type EBase parserName = 'Error '[(Text parserName) ('Span 0 0) '[] -type FailChSym1 :: Symbol -> PDoc -> ParserChSym1 s r-data FailChSym1 name e ch s-type instance App (FailChSym1 name e ch) s = FailCh name e+-- | Get the next character in the string and update the parser state.+--+-- If at end of the string, the state is returned untouched, and @len@ is+-- guaranteed to be 0.+type UnconsState :: PState -> (Maybe Char, PState)+type family UnconsState s where+    UnconsState ('State rem 0   idx) = '(Nothing, 'State rem 0 idx)+    UnconsState ('State rem len idx) = UnconsState' (UnconsSymbol rem) len idx -failChSym-    :: SSymbol name -> SDoc e -> SParserChSym ss sr (FailChSym name e)-failChSym name e = Lam2 $ \_ch _s -> SErr $ SEBase name e+type UnconsState'+    :: Maybe (Char, Symbol) -> Natural -> Natural -> (Maybe Char, PState)+type family UnconsState' mstr len idx where+    UnconsState' (Just '(ch, rem)) len idx =+        '(Just ch, 'State rem (len-1) (idx+1))+    UnconsState' Nothing           len idx =+        -- TODO could I change this to a regular parser error? should I?+        TE.TypeError (TE.Text "unrecoverable parser error: got to end of input string before len=0") --- | Fail with the given message if we're at the end of the symbol.-type FailEndSym :: Symbol -> PDoc -> ParserEndSym s r-data FailEndSym name e s-type instance App (FailEndSym name e) s = Left (EBase name e)+-- TODO: add type synonym for @(Maybe Char, PState) -> PResult res@ -failEndSym-    :: SSymbol name -> SDoc e -> SParserEndSym ss sr (FailEndSym name e)-failEndSym name e = Lam $ \_s -> SLeft $ SEBase name e+-- TODO+type Error1 str = 'Error '[str]+--type Err1 str = Err (Error1 str)+--type OK' a s = 'Reply (OK a) s --- | 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 -> PDoc-type ErrParserLimitation msg = Text "parser limitation: " :<>: Text msg+type EStrInputTooShort :: Natural -> Natural -> Symbol+type EStrInputTooShort nNeed nGot =+         "needed " ++ ShowNatDec nNeed+      ++ " chars, but only " ++ ShowNatDec nGot ++ " remain"++type EStrWrongChar :: Char -> Char -> Symbol+type EStrWrongChar chExpect chGot =+         "expected '" ++ ShowChar chExpect+      ++  "', got '"  ++ ShowChar chGot ++ "'"++-- | Impossible parser state.+--+-- Use when you can prove that an equation is impossible.+type Impossible = TE.TypeError (TE.Text "impossible parser state")
src/Symparsec/Parser/Count.hs view
@@ -1,147 +1,24 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Count where+module Symparsec.Parser.Count ( type Count ) where  import Symparsec.Parser.Common-import GHC.TypeLits hiding ( ErrorMessage(..) )-import Singleraeh.Tuple-import Singleraeh.List-import Singleraeh.Either-import Singleraeh.Natural-import DeFun.Core-import Data.Type.Equality-import Unsafe.Coerce ( unsafeCoerce )--type CountS s r = (Natural, [r], s)--type family Count n p where-    Count n ('PParser pCh pEnd s0) = Count' n pCh pEnd s0-type Count' n pCh pEnd s0 =-    'PParser (CountChSym pCh s0) (CountEndSym pEnd s0) '(n, '[], s0)--type SCountS ss sr = STuple3 SNat (SList sr) ss--sCount-    :: SNat n-    -> SParser ss sr ('PParser pCh pEnd s0)-    -> SParser (SCountS ss sr) (SList sr) (Count' n pCh pEnd s0)-sCount n (SParser pCh pEnd s0) =-    SParser (sCountChSym pCh s0) (sCountEndSym pEnd s0) (STuple3 n SNil s0)--instance-  ( p ~ 'PParser pCh pEnd s0, SingParser p, KnownNat n-  ) => SingParser (Count' n pCh pEnd s0) where-    type PS (Count' n pCh pEnd s0) =-          SCountS (PS ('PParser pCh pEnd s0)) (PR ('PParser pCh pEnd s0))-    type PR (Count' n pCh pEnd s0) = SList (PR ('PParser pCh pEnd s0))-    singParser' = sCount SNat (singParser @p)--type family CountCh pCh s0 ch s where-    CountCh pCh s0 ch '(n, rs, s) = CountCh' pCh s0 ch n rs s--sCountChSym-    :: SParserChSym  ss sr pCh-    -> ss s0-    -> SParserChSym (SCountS ss sr) (SList sr) (CountChSym pCh s0)-sCountChSym pCh s0 = Lam2 $ \ch (STuple3 n rs s) ->-    sCountCh' pCh s0 ch n rs s--type family CountCh' pCh s0 ch n rs s where-    CountCh' pCh s0 ch 0 rs s = Done (Reverse rs)-    CountCh' pCh s0 ch n rs s = CountChN pCh ch n rs s0 (pCh @@ ch @@ s)--sCountCh'-    :: SParserChSym ss sr pCh-    -> ss s0-    -> SChar ch-    -> SNat n-    -> SList sr rs-    -> ss s-    -> SResult (SCountS ss sr) (SList sr) (CountCh' pCh s0 ch n rs s)-sCountCh' pCh s0 ch n rs s =-    case testEquality n (SNat @0) of-      Just Refl -> SDone $ sReverse rs-      Nothing   -> unsafeCoerce $ sCountChN pCh ch n rs s0 (pCh @@ ch @@ s)--type family CountChN pCh ch n rs s0 res where-    CountChN pCh ch n rs s0 (Cont s) = Cont '(n, rs, s)-    CountChN pCh ch n rs s0 (Done r) = CountCh' pCh s0 ch (n-1) (r:rs) s0-    CountChN pCh ch n rs s0 (Err  e) = Err (ECount e)--sCountChN-    :: SParserChSym ss sr pCh-    -> SChar ch-    -> SNat n-    -> SList sr rs-    -> ss s0-    -> SResult ss sr res-    -> SResult (SCountS ss sr) (SList sr) (CountChN pCh ch n rs s0 res)-sCountChN pCh ch n rs s0 = \case-  SCont s -> SCont $ STuple3 n rs s-  SDone r -> sCountCh' pCh s0 ch (n %- SNat @1) (SCons r rs) s0-  SErr  e -> SErr  $ eCount e--type ECount e = EIn "Count" e-eCount :: SE e -> SE (ECount e)-eCount e = withSingE e $ singE--type CountChSym-    :: ParserChSym  s r-    -> s-    -> ParserChSym  (CountS s r) [r]-data CountChSym pCh s0 f-type instance App (CountChSym pCh s0) f = CountChSym1 pCh s0 f--type CountChSym1-    :: ParserChSym  s r-    -> s-    -> ParserChSym1 (CountS s r) [r]-data CountChSym1 pCh s0 ch s-type instance App (CountChSym1 pCh s0 ch) s = CountCh pCh s0 ch s--type family CountEnd pEnd s0 s where-    CountEnd pEnd s0 '(n, rs, s) = CountEnd' pEnd s0 n rs s--type family CountEnd' pEnd s0 n rs s where-    CountEnd' pEnd s0 0 rs s = Right (Reverse rs)-    CountEnd' pEnd s0 n rs s = CountEndN pEnd s0 n rs (pEnd @@ s)--sCountEnd'-    :: SParserEndSym ss sr pEnd-    -> ss s0-    -> SNat n-    -> SList sr rs-    -> ss s-    -> SResultEnd (SList sr) (CountEnd' pEnd s0 n rs s)-sCountEnd' pEnd s0 n rs s =-    case testEquality n (SNat @0) of-      Just Refl -> SRight $ sReverse rs-      Nothing   -> unsafeCoerce $ sCountEndN pEnd s0 n rs (pEnd @@ s)+import qualified Singleraeh.List as List -type family CountEndN pEnd s0 n rs res where-    CountEndN pEnd s0 n rs (Right r) = CountEnd' pEnd s0 (n-1) (r:rs) s0-    CountEndN pEnd s0 n rs (Left  e) = Left (ECount e)+-- TODO Could possibly make more efficient. -sCountEndN-    :: SParserEndSym ss sr pEnd-    -> ss s0-    -> SNat n-    -> SList sr rs-    -> SResultEnd sr res-    -> SResultEnd (SList sr) (CountEndN pEnd s0 n rs res)-sCountEndN pEnd s0 n rs = \case-  SRight r -> sCountEnd' pEnd s0 (n %- SNat @1) (SCons r rs) s0-  SLeft  e -> SLeft $ eCount e+-- | @'Count' n p@ parses @n@ occurrences of @p@.+type Count :: Natural -> PParser a -> PParser [a]+data Count n p s+type instance App (Count n p) s = CountLoop p '[] n s -type CountEndSym-    :: ParserEndSym s r-    -> s-    -> ParserEndSym (CountS s r) [r]-data CountEndSym pEnd s0 s-type instance App (CountEndSym pEnd s0) s = CountEnd pEnd s0 s+type family CountLoop p as n s where+    CountLoop p as 0 s = 'Reply (OK (List.Reverse as)) s+    CountLoop p as n s = CountLoopWrap p as n (p @@ s) -sCountEndSym-    :: SParserEndSym ss              sr         pEnd-    -> ss s0-    -> SParserEndSym (SCountS ss sr) (SList sr) (CountEndSym pEnd s0)-sCountEndSym pEnd s0 = Lam $ \(STuple3 n rs s) -> sCountEnd' pEnd s0 n rs s+type family CountLoopWrap p as n rep where+    CountLoopWrap p as n ('Reply (OK  a) s) =+        CountLoop p (a:as) (n-1) s+    CountLoopWrap p as n ('Reply (Err e) s) =+        -- TODO am I passing the wrong state back here?+        'Reply (Err e) s
− src/Symparsec/Parser/End.hs 
@@ -1,32 +0,0 @@-module Symparsec.Parser.End where--import Symparsec.Parser.Common-import DeFun.Core-import Singleraeh.Tuple ( SUnit(..) )-import Singleraeh.Either ( SEither(..) )---- | Assert end of symbol, or fail.-type End :: PParser () ()-type End = 'PParser EndChSym (Con1 Right) '()--sEnd :: SParser SUnit SUnit End-sEnd = SParser sEndChSym (con1 SRight) SUnit--instance SingParser End where-    type PS  End = SUnit-    type PR  End = SUnit-    singParser' = sEnd---- it'd be nice to just reuse FailChSym here but we get told off for writing an--- orphan instance. fair enough, write this instead-type EndChSym :: ParserChSym s r-data EndChSym f-type instance App EndChSym f = EndChSym1 f--type EndChSym1 :: ParserChSym1 s r-data EndChSym1 ch s-type instance App (EndChSym1 ch) s =-    Err (EBase "End" (Text "expected end of string"))--sEndChSym :: SParserChSym ss rr EndChSym-sEndChSym = Lam2 $ \_ch _s -> SErr singE
+ src/Symparsec/Parser/Ensure.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE UndecidableInstances #-}++module Symparsec.Parser.Ensure ( type Ensure ) where++import Symparsec.Parser.Common+import Symparsec.Utils ( type IfNatLte )++-- | Assert that there are at least @n@ characters remaining. Non-consuming.+type Ensure :: Natural -> PParser ()+data Ensure n s+type instance App (Ensure n) s = Ensure' n s+type family Ensure' n s where+    Ensure' n ('State rem len idx) =+        IfNatLte n len+            ('Reply (OK '()) ('State rem len idx))+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx))
+ src/Symparsec/Parser/Eof.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE UndecidableInstances #-}++module Symparsec.Parser.Eof ( type Eof ) where++import Symparsec.Parser.Common++-- | Assert end of input, or fail.+type Eof :: PParser ()+data Eof s+type instance App Eof s = Eof' (UnconsState s)+type family Eof' ms where+    Eof' '(Nothing,  s) = 'Reply (OK '()) s+    Eof' '(Just _ch, s) = 'Reply (Err EEof) s++type EEof = Error1 "expected end of string"
+ src/Symparsec/Parser/Functor.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Type-level string parsers shaped like 'Functor' functions.++module Symparsec.Parser.Functor+  ( type (<$>), type (<$), type ($>)+  ) where++import Symparsec.Parser.Common+import DeFun.Function ( type ConstSym1 )++-- | '<$>' for parsers. Apply the given type function to the result.+type (<$>) :: (a ~> b) -> PParser a -> PParser b+infixl 4 <$>+data (<$>) f p s+type instance App (f <$> p) s = FmapEnd f (p @@ s)++type family FmapEnd f rep where+    FmapEnd f ('Reply (OK  a) s) = 'Reply (OK  (f @@ a)) s+    FmapEnd f ('Reply (Err e) s) = 'Reply (Err e)        s++-- | '<$' for parsers. Replace the parser result with the given value.+type (<$) :: a -> PParser b -> PParser a+infixl 4 <$+type a <$ p = ConstSym1 a <$> p++-- | 'Data.Functor.$>' for parsers. Flipped t'Symparsec.Parser.Functor.<$'.+type ($>) :: PParser a -> b -> PParser b+infixl 4 $>+type p $> a = ConstSym1 a <$> p
src/Symparsec/Parser/Isolate.hs view
@@ -1,150 +1,44 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Isolate where+module Symparsec.Parser.Isolate ( type Isolate, type IsolateSym ) where  import Symparsec.Parser.Common-import GHC.TypeLits hiding ( ErrorMessage(..) )-import TypeLevelShow.Natural ( ShowNatDec, sShowNatDec )-import DeFun.Core-import Singleraeh.Either-import Singleraeh.Tuple-import Singleraeh.Equality ( testEqElse )-import Singleraeh.Natural ( (%-) )-import Unsafe.Coerce ( unsafeCoerce )-import Data.Type.Equality---- | Run the given parser isolated to the next @n@ characters.------ All isolated characters must be consumed.-type Isolate :: Natural -> PParser s r -> PParser (Natural, s) r-type family Isolate n p where-    Isolate n ('PParser pCh pEnd s0) = Isolate' n pCh pEnd s0---- unwrapped for instances-type Isolate' n pCh pEnd s0 = 'PParser-    (IsolateChSym pCh pEnd)-    (IsolateEndSym pEnd)-    '(n, s0)--type SIsolateS ss = STuple2 SNat ss--sIsolate-    :: SNat n-    -> SParser ss sr p-    -> SParser (SIsolateS ss) sr (Isolate n p)-sIsolate 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-    -> PParserCh (Natural, s) r-type family IsolateCh pCh pEnd ch s where-    IsolateCh pCh pEnd ch '(0, s) = IsolateInnerEnd (pEnd @@ s)-    IsolateCh pCh pEnd ch '(n, s) = IsolateInner n (pCh @@ ch @@ s)--sIsolateChSym-    :: SParserChSym  ss sr pCh-    -> SParserEndSym ss sr pEnd-    -> SParserChSym (SIsolateS ss) sr (IsolateChSym pCh pEnd)-sIsolateChSym 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 PE r -> PResult (Natural, s) r-type family IsolateInnerEnd a where-    IsolateInnerEnd (Right r) = Done r-    IsolateInnerEnd (Left  e) = Err  (EIsolateWrap e)--type IsolateInner :: Natural -> PResult s r -> PResult (Natural, s) r-type family IsolateInner n res where-    IsolateInner n (Cont s) = Cont '(n-1, s)-    IsolateInner n (Done _) = Err (EIsolateRemaining n)-    IsolateInner _ (Err  e) = Err (EIsolateWrap e)--sIsolateInner-    :: SNat n-    -> SResult ss sr res-    -> SResult (SIsolateS ss) sr (IsolateInner n res)-sIsolateInner 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-    -> ParserChSym (Natural, s) r-data IsolateChSym pCh pEnd f-type instance App (IsolateChSym pCh pEnd) f = IsolateChSym1 pCh pEnd f--type IsolateChSym1-    :: ParserChSym s r-    -> ParserEndSym s r-    -> Char -> (Natural, s) ~> PResult (Natural, s) r-data IsolateChSym1 pCh pEnd ch s-type instance App (IsolateChSym1 pCh pEnd ch) s = IsolateCh pCh pEnd ch s+import Symparsec.Utils ( type IfNatLte ) -type EIsolateWrap e = EIn "Isolate" e+-- TODO can use 'Ensure' to help define this+type Isolate :: Natural -> PParser a -> PParser a+data Isolate n p s+type instance App (Isolate n p) s = Isolate' n p s+type family Isolate' n p s where+    Isolate' n p ('State rem len idx) =+        -- Could perhaps improve this, since 'OrdCond' probably does similar+        -- work to @len-n@.+        IfNatLte n len+            (IsolateEnd len n (p @@ ('State rem n idx)))+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx)) -eIsolateWrap :: SE e -> SE (EIsolateWrap e)-eIsolateWrap e = withSingE e singE+--type IsolateEnd :: Natural -> ? -> ?+-- TODO are lenRem/lenConsumed actually good names?+type family IsolateEnd lenOrig n rep where+    -- isolated parser succeeded and consumed all input:+    -- return success with state updated to have actual remaining length+    IsolateEnd lenOrig n ('Reply (OK  a) ('State rem 0   idx)) =+        'Reply (OK  a) ('State rem (lenOrig-n)     idx) -type EIsolateEndN n = EBase "Isolate"-    (      Text "tried to isolate more than present (needed "-      :<>: Text (ShowNatDec n) :<>: Text " more)" )+    -- isolated parser failed+    IsolateEnd lenOrig n ('Reply (Err e) ('State rem len idx)) =+        -- TODO add some isolate meta+        'Reply (Err e) ('State rem (lenOrig-n+len) idx) -eIsolateEndN :: SNat n -> SE (EIsolateEndN n)-eIsolateEndN n = withKnownSymbol (sShowNatDec n) singE+    -- isolated parser succeeded but didn't consume all input+    IsolateEnd lenOrig n ('Reply (OK _a) ('State rem len idx)) =+        'Reply (Err (EIsolateIncomplete len)) ('State rem (lenOrig-n+len) idx) -type EIsolateRemaining n = EBase "Isolate"-    (      Text "isolated parser ended without consuming all input ("-      :<>: Text (ShowNatDec n) :<>: Text " remaining)" )+type EIsolateIncomplete n = Error1+    (    "isolated parser completed without consuming all input ("+      ++ ShowNatDec n ++ " remaining)" ) -eIsolateRemaining :: SNat n -> SE (EIsolateRemaining n)-eIsolateRemaining n = withKnownSymbol (sShowNatDec n) singE+-- TODO testing. args flipped because you're more likely to defun the len+type IsolateSym :: PParser a -> Natural ~> PParser a+data IsolateSym p x+type instance App (IsolateSym p) n = Isolate n p
src/Symparsec/Parser/Literal.hs view
@@ -1,80 +1,52 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Literal where+module Symparsec.Parser.Literal ( type Literal ) where  import Symparsec.Parser.Common-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 -> PParser Symbol ()-type Literal str = 'PParser LiteralChSym LiteralEndSym str--sLiteral :: SSymbol str -> SParser SSymbol SUnit (Literal str)-sLiteral str = SParser sLiteralChSym sLiteralEndSym str--instance KnownSymbol str => SingParser (Literal str) where-    type PS (Literal str) = SSymbol-    type PR (Literal str) = SUnit-    singParser' = sLiteral SSymbol--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 EWrongChar chNext ch = EBase "Literal"-    (      Text "expected " :<>: Text (ShowChar chNext)-      :<>: Text    ", got " :<>: Text (ShowChar ch))--eWrongChar :: SChar chNext -> SChar ch -> SE (EWrongChar chNext ch)-eWrongChar chNext ch = SEBase symbolSing $-          SText symbolSing :$<>: SText (sShowChar chNext)-    :$<>: SText symbolSing :$<>: SText (sShowChar ch)+import Symparsec.Utils ( type IfNatLte )+import Data.Type.Symbol qualified as Symbol -type LiteralChSym :: ParserChSym Symbol ()-data LiteralChSym f-type instance App LiteralChSym f = LiteralChSym1 f+-- TODO megaparsec auto-backtracks its similar primitive.+-- confusingly they write it on the type class method Haddock, even though it+-- doesn't seem enforced (the backtracking is done internally).+-- idk why. but should we also?+-- (similarly to megaparsec, it doesn't really change performance.) -type LiteralChSym1 :: ParserChSym1 Symbol ()-data LiteralChSym1 ch s-type instance App (LiteralChSym1 ch) s = LiteralCh ch s+type EDuringLit :: Symbol -> Symbol -> PError+type EDuringLit lit detail = 'Error+    [ "while parsing literal '" ++ lit ++ "':"+    , detail ] -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 ETooShort lit nNeed nGot =+    EDuringLit lit (EStrInputTooShort nNeed nGot) -type LiteralEnd :: PParserEnd Symbol ()-type family LiteralEnd str where-    LiteralEnd ""  = Right '()-    LiteralEnd str = Left (EStillParsing str)+type EWrongChar lit chExpect chGot =+    EDuringLit lit (EStrWrongChar chExpect chGot) -type EStillParsing str =-    EBase "Literal" (Text "still parsing literal: " :<>: Text str)+type EEof lit = EDuringLit lit "EOF while still parsing literal" -eStillParsing :: SSymbol str -> SE (EStillParsing str)-eStillParsing str = withKnownSymbol str singE+type Literal :: Symbol -> PParser ()+data Literal lit s+type instance App (Literal lit) s = LiteralCheckLen lit s (Symbol.Length lit) -type LiteralEndSym :: ParserEndSym Symbol ()-data LiteralEndSym s-type instance App LiteralEndSym s = LiteralEnd s+-- now, I could use 'Ensure' here. but we add context to errors here, which I+-- quite like. perhaps I should provide an @Ensure'@ that lets you add e detail?+type family LiteralCheckLen lit s n where+    LiteralCheckLen lit ('State rem len idx) litLen =+        IfNatLte litLen len+            (LiteralStep lit ('State rem len idx))+            ('Reply (Err (ETooShort lit litLen len)) ('State rem len idx)) -sLiteralEndSym :: SParserEndSym SSymbol SUnit LiteralEndSym-sLiteralEndSym = Lam $ \str ->-    case testEquality str (SSymbol @"") of-      Just Refl -> SRight SUnit-      Nothing   -> unsafeCoerce $ SLeft $ eStillParsing str+type LiteralStep lit s = Literal' lit s (UnconsSymbol lit) (UnconsState s)+type family Literal' lit sPrev ch ms where+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Just litCh,  s) =+        Literal' lit s (UnconsSymbol litStr) (UnconsState s)+    Literal' _lit sPrev Nothing                 _                 =+        'Reply (OK '()) sPrev+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Just    ch, _s) =+        -- TODO which state to pass back here?+        'Reply (Err (EWrongChar lit litCh ch)) sPrev+    Literal'  lit sPrev (Just '(litCh, litStr)) '(Nothing,    _s) =+        -- note that this equation is impossible providing length is checked+        -- both states are guaranteed the same here, but prev is morally better+        'Reply (Err (EEof lit)) sPrev
+ src/Symparsec/Parser/Monad.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Type-level string parsers shaped like 'Monad' functions.++module Symparsec.Parser.Monad ( type (>>=) ) where++import Symparsec.Parser.Common++-- | '>>=' for parsers. Sequentially compose two parsers, passing the value from+-- the left parser as an argument to the second.+type (>>=) :: PParser a -> (a ~> PParser b) -> PParser b+infixl 1 >>=+data (>>=) l r s+type instance App (l >>= r) s = BindL r (l @@ s)+type BindL :: (a ~> PParser b) -> PReply a -> PReply b+type family BindL r rep where+    BindL r ('Reply (OK  a) s) = r @@ a @@ s+    BindL r ('Reply (Err e) s) = 'Reply (Err e) s
src/Symparsec/Parser/Natural.hs view
@@ -1,104 +1,136 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Natural where+module Symparsec.Parser.Natural+  ( type NatBase, type NatBase1+  , type NatDec+  , type NatHex+  , type NatBin+  , type NatOct +  , type NatBaseWhile+  ) where+ 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.+-- TODO decide which version to export primarily, isolate or while++{-+The main loops here consume greedily to hopefully speed up evaluation.+It adds to the complexity, and means we have to backtrack on failure.+It'd be nice to assert that it /does/ help in some way.+-}++-- | Parse a binary (base 2) 'Natural'. type NatBin = NatBase  2 ParseDigitBinSym --- | Parse an octal (base 8) natural.+-- | Parse an octal (base 8) 'Natural'. type NatOct = NatBase  8 ParseDigitOctSym --- | Parse a decimal (base 10) natural.+-- | Parse a decimal (base 10) 'Natural'. type NatDec = NatBase 10 ParseDigitDecSym --- | Parse a hexadecimal (base 16) natural. Permits mixed-case (@0-9A-Fa-f@).+-- | Parse a hexadecimal (base 16) 'Natural'. Permits mixed-case (@0-9A-Fa-f@). type NatHex = NatBase 16 ParseDigitHexSym --- | Parse a natural in the given base, using the given digit parser.-type NatBase-    :: Natural -> (Char ~> Maybe Natural) -> PParser (Maybe Natural) Natural-type NatBase base parseDigit =-    'PParser (NatBaseChSym base parseDigit) NatBaseEndSym Nothing+-- | Parse a non-empty 'Natural' using the given base and digit parser.+--+-- Only permits parsing numbers with digits exactly one 'Char' long.+--+-- Returns an error if it parses zero digits, or if any character fails to+-- parse.+type NatBase :: Natural -> (Char ~> Maybe Natural) -> PParser Natural+data NatBase base parseDigit s+type instance App (NatBase base parseDigit) s =+    NatBaseStart base parseDigit s (UnconsState s)+type family NatBaseStart base parseDigit sCh s where+    NatBaseStart base parseDigit sCh '(Just ch, s) =+        NatBaseLoop base parseDigit sCh s 0 ch (parseDigit @@ ch) (UnconsState s)+    NatBaseStart base parseDigit sCh '(Nothing, s) = 'Reply (Err EEmpty) sCh -sNatBase-    :: SNat base-    -> SParseDigit parseDigit-    -> SParser (SMaybe SNat) SNat (NatBase base parseDigit)-sNatBase base parseDigit =-    SParser (sNatBaseChSym base parseDigit) sNatBaseEndSym SNothing+-- | Parse a 'Natural' with the given starting value.+--+-- Skips some extra work. May be handy for hand-written parsers.+type NatBase1 :: Natural -> (Char ~> Maybe Natural) -> Natural -> PParser Natural+data NatBase1 base parseDigit digit s+type instance App (NatBase1 base parseDigit digit) s =+    NatBase1' base parseDigit s digit (UnconsState s)+type family NatBase1' base parseDigit sCh digit s where+    NatBase1' base parseDigit sCh digit '(Just ch, s) =+        NatBaseLoop base parseDigit sCh s digit ch (parseDigit @@ ch) (UnconsState s)+    NatBase1' base parseDigit sCh digit '(Nothing, s) =+        'Reply (OK digit) s -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 EEmpty = Error1 "no digits parsed" -- TODO not great eh+type EInvalidDigit ch base =+    Error1 ( "not a base " ++ ShowNatDec base ++ " digit: " ++ ShowChar ch) -type NatBaseCh+type NatBaseLoop     :: Natural     -> (Char ~> Maybe Natural)-    -> PParserCh (Maybe Natural) Natural-type NatBaseCh base parseDigit ch mn = NatBaseCh' base mn (parseDigit @@ ch)+    -> PState+    -> PState+    -> Natural+    -> Char+    -> Maybe Natural+    -> (Maybe Char, PState)+    -> PReply Natural+type family NatBaseLoop base parseDigit sCh s n chCur mDigit ms where+    -- parsed digit and have next char+    NatBaseLoop base parseDigit sCh s n chCur (Just digit) '(Just ch, sNext) =+        NatBaseLoop base parseDigit s sNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState sNext)+    NatBaseLoop base parseDigit sCh s n chCur (Just digit) '(Nothing, sNext) =+        'Reply (OK (n * base + digit)) sNext+    NatBaseLoop base parseDigit sCh s n chCur Nothing      '(_, sNext) =+        -- we've consumed the next character, but digit parse failed:+        -- backtrack and return error+        'Reply (Err (EInvalidDigit chCur base)) sCh -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)+-- | Parse a non-empty 'Natural' using the given base and digit parser.+--+-- Only permits parsing numbers with digits exactly one 'Char' long.+--+-- Returns an error if it parses zero digits, or if the first digit fails to+-- parse. Returns success on parsing up to EOF, or just before the first failed+-- character parse. (Should match the behaviour of Megaparsec's number parsers.)+type NatBaseWhile :: Natural -> (Char ~> Maybe Natural) -> PParser Natural+data NatBaseWhile base parseDigit s+type instance App (NatBaseWhile base parseDigit) s =+    NatBaseWhileStart base parseDigit s (UnconsState s)+type family NatBaseWhileStart base parseDigit sCh s where+    NatBaseWhileStart base parseDigit sCh '(Just ch, s) =+        NatBaseWhileStart2 base parseDigit sCh s ch (parseDigit @@ ch) (UnconsState s)+    NatBaseWhileStart base parseDigit sCh '(Nothing, s) = 'Reply (Err EEmpty) sCh -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+-- TODO While1 -type NatBaseChSym-    :: Natural-    -> (Char ~> Maybe Natural)-    -> ParserChSym (Maybe Natural) Natural-data NatBaseChSym base parseDigit f-type instance App (NatBaseChSym base parseDigit) f =-    NatBaseChSym1 base parseDigit f+type family NatBaseWhileStart2 base parseDigit sCh s chChur mDigit ms where+    NatBaseWhileStart2 base parseDigit sCh s chCur (Just digit) '(Just ch, sNext) =+        NatBaseWhileLoop base parseDigit s sNext digit ch (parseDigit @@ ch) (UnconsState sNext)+    NatBaseWhileStart2 base parseDigit sCh s chCur (Just digit) '(Nothing, sNext) =+        -- parsed first digit, no more input: done+        'Reply (OK digit) sNext+    NatBaseWhileStart2 base parseDigit sCh s chCur Nothing      _ =+        -- failed to parse first digit: backtrack and error+        'Reply (Err (EInvalidDigit chCur base)) sCh -type NatBaseChSym1+-- Note that this parser never fails.+type NatBaseWhileLoop     :: Natural     -> (Char ~> Maybe Natural)-    -> ParserChSym1 (Maybe Natural) Natural-data NatBaseChSym1 base parseDigit ch mn-type instance App (NatBaseChSym1 base parseDigit ch) mn =-    NatBaseCh base parseDigit ch mn--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 family NatBaseEnd mn where-    NatBaseEnd (Just n) = Right n-    NatBaseEnd Nothing  = Left EEmpty--type EEmpty = EBase "NatBase" (Text "no digits parsed")-eEmpty :: SE EEmpty-eEmpty = singE--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+    -> PState+    -> PState+    -> Natural+    -> Char+    -> Maybe Natural+    -> (Maybe Char, PState)+    -> PReply Natural+type family NatBaseWhileLoop base parseDigit sCh s n chCur mDigit ms where+    -- parsed digit and have next char+    NatBaseWhileLoop base parseDigit sCh s n chCur (Just digit) '(Just ch, sNext) =+        NatBaseWhileLoop base parseDigit s sNext (n * base + digit) ch (parseDigit @@ ch) (UnconsState sNext)+    NatBaseWhileLoop base parseDigit sCh s n chCur (Just digit) '(Nothing, sNext) =+        'Reply (OK (n * base + digit)) sNext+    NatBaseWhileLoop base parseDigit sCh s n chCur Nothing      _ =+        -- failed to parse next digit: backtrack and finish+        'Reply (OK n) sCh
src/Symparsec/Parser/Natural/Digits.hs view
@@ -1,6 +1,8 @@ {- | Parse digits from type-level 'Char's.  A 'Nothing' indicates the given 'Char' was not a valid digit for the given base.++raehik copied this directly from his own Symparsec library. -}  module Symparsec.Parser.Natural.Digits where
− src/Symparsec/Parser/Or.hs 
@@ -1,330 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Symparsec.Parser.Or where--import Symparsec.Parser-import TypeLevelShow.Doc-import GHC.TypeLits hiding ( ErrorMessage(..) )-import DeFun.Core-import Singleraeh.Tuple-import Singleraeh.Either-import Singleraeh.List--{- | Limited parser choice. Try left; if it fails, backtrack and try right.-     However, _the right choice must consume at least as much as the left-     choice._ If it doesn't, then even if the right parser succeeds, it-     will emit an error.--This behaviour is due to the parser runner not supporting backtracking. We can-emulate it by storing a record of the characters parsed so far, and "replaying"-these on the right parser if the left parser fails. If the right parser ends-before we finish replaying, we will have consumed extra characters that we can't-ask the runner to revert.--For example, @Literal "abcd" :<|>: Literal "ab"@ is bad. An input of @abcX@ will-trigger the consumption error.--I can't think of another way to implement this with the current parser design. I-think it's the best we have. A more complex parser design may permit changing-internal running state, so we could save and load state (this would permit a-@Try p@ parser). But that's scary. And you're better off designing your-type-level string schemas to permit non-backtracking parsing anyway...--Also problematic is that we never emit a left parser error, so errors can-degrade. Perhaps your string was one character off a successful left parse; but-if it fails, you won't see that error.--}-infixl 3 :<|>:-type (:<|>:)-    :: PParser sl rl-    -> PParser sr rr-    -> PParser (OrS sl sr) (Either rl rr)-type family pl :<|>: pr where-    'PParser plCh plEnd s0l :<|>: 'PParser prCh prEnd s0r =-        Or' plCh plEnd s0l prCh prEnd s0r--type Or' plCh plEnd s0l prCh prEnd s0r = 'PParser-    (OrChSym plCh prCh s0r)-    (OrEndSym plEnd prCh prEnd s0r)-    (Left '(s0l, '[]))--type SOrS ssl ssr = SEither (STuple2 ssl (SList SChar)) ssr-type OrS  sl  sr  = Either (sl, [Char]) sr-type SPOr ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r =-    SParser (SOrS ssl ssr) (SEither srl srr) (Or' plCh plEnd s0l prCh prEnd s0r)--sOr-    :: SParser ssl srl ('PParser plCh plEnd s0l)-    -> SParser ssr srr ('PParser prCh prEnd s0r)-    -> SPOr    ssl srl ssr srr plCh plEnd s0l prCh prEnd s0r-sOr (SParser plCh plEnd s0l) (SParser prCh prEnd s0r) = SParser-    (sOrChSym plCh prCh s0r)-    (sOrEndSym plEnd prCh prEnd s0r)-    (SLeft (STuple2 s0l SNil))--instance-  ( pl ~ 'PParser plCh plEnd s0l-  , pr ~ 'PParser prCh prEnd s0r-  , SingParser pl-  , SingParser pr-  ) => SingParser (Or' plCh plEnd s0l prCh prEnd s0r) where-    type PS (Or' plCh plEnd s0l prCh prEnd s0r) = SOrS-        (PS ('PParser plCh plEnd s0l))-        (PS ('PParser prCh prEnd s0r))-    type PR (Or' plCh plEnd s0l prCh prEnd s0r) = SEither-        (PR ('PParser plCh plEnd s0l))-        (PR ('PParser prCh prEnd s0r))-    singParser' = sOr (singParser @pl) (singParser @pr)--type OrCh-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> PParserCh (OrS sl sr) (Either rl rr)-type family OrCh plCh prCh sr ch s where-    -- | parsing left-    OrCh plCh prCh s0r ch (Left  '(sl, chs)) =-        OrChL prCh s0r ch chs (plCh @@ ch @@ sl)--    -- | parsing right (after left failed and was successfully replayed)-    OrCh plCh prCh _  ch (Right sr) =-        OrChR (prCh @@ ch @@ sr)--type OrChL-    :: ParserChSym sr rr-    -> sr-    -> Char-    -> [Char]-    -> PResult sl rl-    -> PResult (Either (sl, [Char]) sr) (Either rl rr)-type family OrChL prCh s0r chLast chs resl where-    -- | left parser OK, continue-    OrChL _    _   chLast chs (Cont sl) = Cont (Left  '(sl, chLast : chs))--    -- | left parser OK, done-    OrChL _    _   _      _   (Done rl) = Done (Left  rl)--    -- | left parser failed: ignore, replay consumed characters on right parser-    OrChL prCh s0r chLast chs (Err  _ ) =-        OrChLReplay prCh chLast (Reverse chs) (Cont s0r)--type OrChLReplay-    :: ParserChSym sr rr-    -> Char-    -> [Char]-    -> PResult sr rr-    -> PResult (Either (sl, [Char]) sr) (Either rl rr)-type family OrChLReplay prCh chLast chs resr where-    -- | right parser OK, keep replaying-    OrChLReplay prCh chLast (ch : chs) (Cont sr) =-        OrChLReplay prCh chLast chs (prCh @@ ch @@ sr)-    ---    -- | right parser OK, final replay char-    OrChLReplay prCh chLast '[]        (Cont sr) = OrChR (prCh @@ chLast @@ sr)--    -- | right parser fail: wrap error-    OrChLReplay prCh chLast chs        (Err  er) = Err (EOrR er)--    -- | right parser done but still replaying! no choice but to error out-    OrChLReplay prCh chLast chs        (Done rr) = Err EOrStillReplaying-        -- Done (Right rr) -- TODO--sOrChLReplay-    :: SParserChSym ssr srr prCh-    -> SChar chLast-    -> SList SChar chs-    -> SResult ssr srr resr-    -> SResult (SOrS ssl ssr) (SEither srl srr)-        (OrChLReplay prCh chLast chs resr)-sOrChLReplay prCh chLast chs resr =-    case chs of-      SCons ch chs' ->-        case resr of-          SCont  sr ->-            sOrChLReplay prCh chLast chs' (prCh @@ ch @@ sr)-          SDone _rr -> SErr eOrStillReplaying-          SErr   er -> SErr $ eOrR er-      SNil ->-        case resr of-          SCont  sr -> sOrChR (prCh @@ chLast @@ sr)-          SDone _rr -> SErr eOrStillReplaying-          SErr   er -> SErr $ eOrR er--type EOrR er = EIn "Or(R)" er-eOrR :: SE er -> SE (EOrR er)-eOrR er = SEIn symbolSing er--type EOrStillReplaying = EBase "Or"-    (Text "right parser much consume at least as much as the failed left parser")-eOrStillReplaying :: SE EOrStillReplaying-eOrStillReplaying = singE--type family OrChR resr where-    OrChR (Cont sr) = Cont (Right sr)-    OrChR (Done rr) = Done (Right rr)-    OrChR (Err  er) = Err (EOrR er)--sOrChR-    :: SResult ssr srr resr-    -> SResult (SOrS ssl ssr) (SEither srl srr) (OrChR resr)-sOrChR = \case-  SCont sr -> SCont $ SRight sr-  SDone rr -> SDone $ SRight rr-  SErr  er -> SErr  $ eOrR er--type OrEnd-    :: ParserEndSym sl rl-    -> ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> sr-    -> PParserEnd (Either (sl, [Char]) sr) (Either rl rr)-type family OrEnd plEnd prCh prEnd sr res where-    -- | input ended during left parser-    OrEnd plEnd prCh prEnd s0r (Left  '(sl, chs)) =-        OrEndL prCh prEnd s0r chs (plEnd @@ sl)--    -- | input ended during right parser: call right end-    OrEnd plEnd prCh prEnd _   (Right sr)         = OrEndR (prEnd @@ sr)--type OrEndR :: PResultEnd rr -> PResultEnd (Either rl rr)-type family OrEndR resr where-    OrEndR (Right rr) = Right (Right rr)-    OrEndR (Left  er) = Left  (EOrR er)--sOrEndR-    :: SResultEnd srr resr-    -> SResultEnd (SEither srl srr) (OrEndR resr)-sOrEndR = \case-  SRight rr -> SRight $ SRight rr-  SLeft  er -> SLeft  $ eOrR er--type OrEndL-    :: ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> sr-    -> [Char]-    -> Either PE rl-    -> Either PE (Either rl rr)-type family OrEndL prCh prEnd s0r chs resl where-    -- | input ended during left parser and left end succeeeded: phew-    OrEndL prCh prEnd s0r chs (Right rl) = Right (Left rl)--    -- | input ended during left parser and left end failed. replay on right,-    --   then eventually call right end-    OrEndL prCh prEnd s0r chs (Left  el) =-        OrEndLReplay prCh prEnd (Reverse chs) (Cont s0r)--sOrEndL-    :: SParserChSym  ssr srr prCh-    -> SParserEndSym ssr srr prEnd-    -> ssr s0r-    -> SList SChar chs-    -> SResultEnd srl resl-    -> SResultEnd (SEither srl srr) (OrEndL prCh prEnd s0r chs resl)-sOrEndL prCh prEnd s0r chs = \case-  SRight  rl -> SRight $ SLeft rl-  SLeft  _el -> sOrEndLReplay prCh prEnd (sReverse chs) (SCont s0r)--type OrEndLReplay-    :: ParserChSym  sr rr-    -> ParserEndSym sr rr-    -> [Char]-    -> PResult sr rr-    -> Either PE (Either rl rr)-type family OrEndLReplay prCh prEnd chs resr where-    -- | right parser OK, keep replaying-    OrEndLReplay prCh prEnd (ch : chs) (Cont sr) =-        OrEndLReplay prCh prEnd chs (prCh @@ ch @@ sr)--    -- | replay complete-    OrEndLReplay prCh prEnd '[]        resr      = OrEndLReplay' prEnd resr--    -- | right parser fail: wrap error-    OrEndLReplay prCh prEnd chs        (Err  er) = Left (EOrR er)--    -- | right parser done but still replaying! no choice but to error out-    OrEndLReplay prCh prEnd chs        (Done rr) = Left EOrStillReplaying-        -- Right (Right rr) TODO--sOrEndLReplay-    :: SParserChSym  ssr srr prCh-    -> SParserEndSym ssr srr prEnd-    -> SList SChar chs-    -> SResult ssr srr resr-    -> SResultEnd (SEither srl srr) (OrEndLReplay prCh prEnd chs resr)-sOrEndLReplay prCh prEnd chs resr =-    case chs of-      SCons ch chs' ->-        case resr of-          SCont  sr ->-            sOrEndLReplay prCh prEnd chs' (prCh @@ ch @@ sr)-          SErr   er -> SLeft $ eOrR er-          SDone _rr -> SLeft eOrStillReplaying-      SNil ->-        case resr of-          SCont sr -> sOrEndR $ prEnd @@ sr-          SDone rr -> SRight  $ SRight rr-          SErr  er -> SLeft   $ eOrR er--type family OrEndLReplay' prEnd resr where-    OrEndLReplay' prEnd (Cont sr) = OrEndR (prEnd @@ sr)-    OrEndLReplay' prEnd (Done rr) = Right  (Right rr)-    OrEndLReplay' prEnd (Err  er) = Left   (EOrR er)--type OrChSym-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> ParserChSym (OrS sl sr) (Either rl rr)-data OrChSym plCh prCh s0r f-type instance App (OrChSym plCh prCh s0r) f = OrChSym1 plCh prCh s0r f--type OrChSym1-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> ParserChSym1 (OrS sl sr) (Either rl rr)-data OrChSym1 plCh prCh sr ch s-type instance App (OrChSym1 plCh prCh sr ch) s = OrCh plCh prCh sr ch s--sOrChSym-    :: SParserChSym ssl srl plCh-    -> SParserChSym ssr srr prCh-    -> ssr s0r-    -> SParserChSym (SOrS ssl ssr) (SEither srl srr) (OrChSym plCh prCh s0r)-sOrChSym plCh prCh s0r = Lam2 $ \ch -> \case-  SLeft  (STuple2 sl chs) -> sOrChL prCh s0r ch chs (plCh @@ ch @@ sl)-  SRight sr -> sOrChR (prCh @@ ch @@ sr)--sOrChL-    :: SParserChSym ssr srr prCh-    -> ssr s0r-    -> SChar chLast-    -> SList SChar chs-    -> SResult ssl srl resl-    -> SResult (SOrS ssl ssr) (SEither srl srr) (OrChL prCh s0r chLast chs resl)-sOrChL prCh s0r chLast chs = \case-  SCont  sl -> SCont $ SLeft $ STuple2 sl $ SCons chLast chs-  SDone  rl -> SDone $ SLeft rl-  SErr  _el -> sOrChLReplay prCh chLast (sReverse chs) (SCont s0r)--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 s0r s-type instance App (OrEndSym plEnd prCh prEnd s0r) s =-    OrEnd plEnd prCh prEnd s0r s--sOrEndSym-    :: SParserEndSym ssl srl plEnd-    -> SParserChSym  ssr srr prCh-    -> SParserEndSym ssr srr prEnd-    -> ssr s0r-    -> SParserEndSym (SOrS ssl ssr) (SEither srl srr)-        (OrEndSym plEnd prCh prEnd s0r)-sOrEndSym plEnd prCh prEnd s0r = Lam $ \case-  SLeft (STuple2 sl chs) -> sOrEndL prCh prEnd s0r chs (plEnd @@ sl)-  SRight sr -> sOrEndR $ prEnd @@ sr
src/Symparsec/Parser/Skip.hs view
@@ -1,66 +1,21 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Skip where+module Symparsec.Parser.Skip ( type Skip, type SkipUnsafe ) where  import Symparsec.Parser.Common-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 -> PParser Natural ()-type Skip n = 'PParser SkipChSym SkipEndSym n--sSkip :: SNat n -> SParser SNat SUnit (Skip n)-sSkip n = SParser sSkipChSym sSkipEndSym n--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 _ 0 = Done '()-    SkipCh _ n = Cont (n-1)--type SkipChSym :: ParserChSym Natural ()-data SkipChSym f-type instance App SkipChSym f = SkipChSym1 f--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 skip "-      :<>: Text (ShowNatDec n) :<>: Text " chars from empty string")-eSkipPastEnd :: SNat n -> SE (ESkipPastEnd n)-eSkipPastEnd n = withKnownSymbol (sShowNatDec n) singE+import Symparsec.Parser.Ensure+import Symparsec.Parser.Applicative+import Data.Type.Symbol qualified as Symbol -type SkipEndSym :: ParserEndSym Natural ()-data SkipEndSym n-type instance App SkipEndSym n = SkipEnd n+-- | Skip forward @n@ characters. Fails if fewer than @n@ characters remain.+type Skip :: Natural -> PParser ()+type Skip n = Ensure n *> SkipUnsafe n -sSkipEndSym :: SParserEndSym SNat SUnit SkipEndSym-sSkipEndSym = Lam $ \n ->-    case testEquality n (SNat @0) of-      Just Refl -> SRight SUnit-      Nothing   -> unsafeCoerce $ SLeft $ eSkipPastEnd n+-- | Skip forward @n@ characters. @n@ must be less than or equal to the number+--   of remaining characters. (Fairly unhelpful; use 'Skip' instead.)+type SkipUnsafe :: Natural -> PParser ()+data SkipUnsafe n s+type instance App (SkipUnsafe n) s = SkipUnsafe' n s+type family SkipUnsafe' n s where+    SkipUnsafe' n ('State rem len idx) =+        'Reply (OK '()) ('State (Symbol.Drop n rem) (len-n) (idx+n))
src/Symparsec/Parser/Take.hs view
@@ -1,71 +1,24 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.Take where+module Symparsec.Parser.Take ( type Take, type TakeSym ) where  import Symparsec.Parser.Common-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+import Singleraeh.Symbol ( type RevCharsToSymbol )  -- | Return the next @n@ characters.-type Take n = 'PParser TakeChSym TakeEndSym '(n, '[])--type STakeS = STuple2 SNat (SList SChar)-type  TakeS = (Natural, [Char])--sTake :: SNat n -> SParser STakeS SSymbol (Take n)-sTake n = SParser sTakeChSym sTakeEndSym (STuple2 n SNil)--instance KnownNat n => SingParser (Take n) where-    type PS (Take n) = STakeS-    type PR (Take n) = SSymbol-    singParser' = sTake SNat--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--sTakeChSym :: SParserChSym STakeS SSymbol TakeChSym-sTakeChSym = 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 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 Take :: Natural -> PParser Symbol+data Take n s+type instance App (Take n) s = Take' '[] n s (UnconsState s)+type family Take' chs n sPrev s where+    Take' chs 0 sPrev _             = 'Reply (OK (RevCharsToSymbol chs)) sPrev+    Take' chs n sPrev '(Just ch, s) = Take' (ch:chs) (n-1) s (UnconsState s)+    Take' chs n sPrev '(Nothing, s) = 'Reply (Err (ETakeEnd n)) sPrev -type TakeEndSym :: ParserEndSym TakeS Symbol-data TakeEndSym s-type instance App TakeEndSym s = TakeEnd s+type ETakeEnd :: Natural -> PError+type ETakeEnd n = Error1+    ( "tried to take " ++ ShowNatDec n ++ " chars from empty string" ) -sTakeEndSym :: SParserEndSym STakeS SSymbol TakeEndSym-sTakeEndSym = Lam $ \(STuple2 n chs) ->-    case testEquality n (SNat @0) of-      Just Refl -> SRight $ revCharsToSymbol chs-      Nothing   -> unsafeCoerce $ SLeft $ eTakeEnd n+-- | 'Take' defunctionalization symbol.+type TakeSym :: Natural ~> PParser Symbol+data TakeSym n+type instance App TakeSym n = Take n
src/Symparsec/Parser/TakeRest.hs view
@@ -1,39 +1,25 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.TakeRest where+module Symparsec.Parser.TakeRest ( type TakeRest ) where  import Symparsec.Parser.Common-import Singleraeh.Symbol ( RevCharsToSymbol, revCharsToSymbol )-import Singleraeh.List ( SList(..) )-import Singleraeh.Either ( SEither(..) )-import GHC.TypeLits hiding ( ErrorMessage(..) )-import DeFun.Core---- | Return the remaining input string.-type TakeRest = 'PParser TakeRestChSym TakeRestEndSym '[]--sTakeRest :: SParser (SList SChar) SSymbol TakeRest-sTakeRest = SParser sTakeRestChSym sTakeRestEndSym SNil--instance SingParser TakeRest where-    type PS TakeRest = SList SChar-    type PR TakeRest = SSymbol-    singParser' = sTakeRest--type TakeRestChSym :: ParserChSym [Char] Symbol-data TakeRestChSym f-type instance App TakeRestChSym f = TakeRestChSym1 f--type TakeRestChSym1 :: ParserChSym1 [Char] Symbol-data TakeRestChSym1 ch chs-type instance App (TakeRestChSym1 ch) chs = Cont (ch : chs)+import qualified Data.Type.Symbol as Symbol -sTakeRestChSym :: SParserChSym (SList SChar) SSymbol TakeRestChSym-sTakeRestChSym = Lam2 $ \ch chs -> SCont $ SCons ch chs+-- | Consume and return the rest of the input string.+--+-- Never fails. May return the empty string.+type TakeRest :: PParser Symbol+data TakeRest s+type instance App TakeRest s = TakeRest' s+type family TakeRest' s where+    TakeRest' ('State rem len idx) =+        'Reply (OK (Symbol.Take len rem)) ('State (Symbol.Drop len rem) 0 (idx+len)) -type TakeRestEndSym :: ParserEndSym [Char] Symbol-data TakeRestEndSym chs-type instance App TakeRestEndSym chs = Right (RevCharsToSymbol chs)+{-+import GHC.TypeLits+import DeFun.Core -sTakeRestEndSym :: SParserEndSym (SList SChar) SSymbol TakeRestEndSym-sTakeRestEndSym = Lam $ \chs -> SRight $ revCharsToSymbol chs+sTakeRest :: SParser SSymbol TakeRest+sTakeRest = Lam $ \(SState srem slen sidx) ->+        SReply (SOK _) (SState _ (SNat @0) _)+-}
+ src/Symparsec/Parser/TakeWhile.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE UndecidableInstances #-}++module Symparsec.Parser.TakeWhile ( type TakeWhile ) where++import Symparsec.Parser.Common+import Singleraeh.Symbol ( type RevCharsToSymbol )++-- | Take zero or more 'Char's for which the supplied predicate holds.+--+-- May also be defined via+-- @'Symparsec.Parser.While.While' chPred 'Symparsec.Parser.TakeRest.TakeRest'@,+-- but a custom implementation is more efficient.+type TakeWhile :: (Char ~> Bool) -> PParser Symbol+data TakeWhile chPred s+type instance App (TakeWhile chPred) s = TakeWhileStart chPred s (UnconsState s)++type family TakeWhileStart chPred sPrev ms where+    TakeWhileStart chPred sPrev '(Just ch, s) =+        TakeWhileLoop chPred sPrev s ch '[] (chPred @@ ch) (UnconsState s)+    TakeWhileStart chPred sPrev '(Nothing, s) =+        'Reply (OK "") sPrev++type family TakeWhileLoop chPred sPrev sCh ch taken res ms where+    -- next char succeeded and not EOF+    TakeWhileLoop chPred sPrev sCh ch taken True '(Just chNext, s) =+        TakeWhileLoop chPred sCh s chNext (ch:taken) (chPred @@ chNext) (UnconsState s)++    -- next char succeeded and EOF: end+    TakeWhileLoop chPred sPrev sCh ch taken True '(Nothing, s) =+        'Reply (OK (RevCharsToSymbol (ch:taken))) sCh -- @sCh == s@ should hold++    -- next char failed: backtrack and end+    TakeWhileLoop chPred sPrev sCh ch taken False _ =+        'Reply (OK (RevCharsToSymbol taken)) sPrev
− src/Symparsec/Parser/Then.hs 
@@ -1,187 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Symparsec.Parser.Then where--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 (:<*>:)-    :: PParser sl rl-    -> PParser sr rr-    -> PParser (Either sl (rl, sr)) (rl, rr)-type family pl :<*>: pr where-    '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-    -> 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 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 EThenChL el = EIn "Then(L)" el-eThenChL :: SE el -> SE (EThenChL el)-eThenChL el = withSingE el $ singE--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 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 s0r f-type instance App (ThenChSym plCh prCh s0r) f = ThenChSym1 plCh prCh s0r f--type ThenChSym1-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> 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 sl rl-    -> ParserEndSym sr rr-    -> sr-    -> ParserEndSym (Either sl (rl, sr)) (rl, rr)-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 
@@ -1,179 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Symparsec.Parser.Then.VoidLeft where--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 (:*>:)-    :: PParser sl rl-    -> PParser sr rr-    -> PParser (Either sl sr) rr-type family pl :*>: pr where-    '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-    -> 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 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 EThenVLChL el = EIn "ThenVL(L)" el-eThenVLChL :: SE el -> SE (EThenVLChL el)-eThenVLChL el = withSingE el $ singE--type family ThenVLChR resr where-    ThenVLChR (Cont sr) = Cont (Right sr)-    ThenVLChR (Done rr) = Done rr-    ThenVLChR (Err  er) = Err  (EThenVLChR er)--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 s0r) f = ThenVLChSym1 plCh prCh s0r f--type ThenVLChSym1-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> 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 sl rl-    -> ParserEndSym sr rr-    -> sr-    -> ParserEndSym (Either sl sr) rr-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 
@@ -1,185 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Symparsec.Parser.Then.VoidRight where--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.-infixl 4 :<*:-type (:<*:)-    :: PParser sl rl-    -> PParser sr rr-    -> PParser (Either sl (rl, sr)) rl-type family pl :<*: pr where-    '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-    -> 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 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 EThenVRChL el = EIn "ThenVR(L)" el-eThenVRChL :: SE el -> SE (EThenVRChL el)-eThenVRChL el = withSingE el $ singE--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 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 s0r f-type instance App (ThenVRChSym plCh prCh s0r) f = ThenVRChSym1 plCh prCh s0r f--type ThenVRChSym1-    :: ParserChSym sl rl-    -> ParserChSym sr rr-    -> sr-    -> 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 sl rl-    -> ParserEndSym sr rr-    -> sr-    -> ParserEndSym (Either sl (rl, sr)) rl-data ThenVREndSym plEnd prEnd s0r s-type instance App (ThenVREndSym plEnd prEnd s0r) s = ThenVREnd plEnd prEnd s0r s
+ src/Symparsec/Parser/Try.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE UndecidableInstances #-}++module Symparsec.Parser.Try ( type Try ) where++import Symparsec.Parser.Common++-- | Run the given parser, backtracking on error.+type Try :: PParser a -> PParser a+data Try p s+type instance App (Try p) s = Try' s (p @@ s)+type Try' :: PState -> PReply a -> PReply a+type family Try' sPrev rep where+    Try' sPrev ('Reply (OK  a) s) = 'Reply (OK  a) s+    Try' sPrev ('Reply (Err e) s) = 'Reply (Err e) sPrev
src/Symparsec/Parser/While.hs view
@@ -1,72 +1,39 @@ {-# LANGUAGE UndecidableInstances #-} -module Symparsec.Parser.While where+module Symparsec.Parser.While ( type While ) where  import Symparsec.Parser.Common-import DeFun.Core-import GHC.TypeLits-import Singleraeh.Bool-import Singleraeh.Either-import Symparsec.Parser.While.Predicates  -- | Run the given parser while the given character predicate succeeds.-type family While chPred p where-    While chPred ('PParser pCh pEnd s0) = While' chPred pCh pEnd s0-type While' chPred pCh pEnd s0 = 'PParser (WhileChSym chPred pCh pEnd) pEnd s0--sWhile-    :: Lam SChar SBool chPred-    -> SParser ss sr ('PParser pCh pEnd s0)-    -> SParser ss sr (While' chPred pCh pEnd s0)-sWhile chPred (SParser pCh pEnd s0) =-    SParser (sWhileChSym chPred pCh pEnd) pEnd s0--instance-  ( p ~ 'PParser pCh pEnd s0, SingParser p-  , SingChPred chPred-  ) => SingParser (While' chPred pCh pEnd s0) where-    type PS (While' chPred pCh pEnd s0) = PS ('PParser pCh pEnd s0)-    type PR (While' chPred pCh pEnd s0) = PR ('PParser pCh pEnd s0)-    singParser' = sWhile (singChPred @chPred) (singParser @p)--type WhileCh chPred pCh pEnd ch s = WhileCh' pCh pEnd ch s (chPred @@ ch)-type family WhileCh' pCh pEnd ch s res where-    WhileCh' pCh pEnd ch s True  = pCh @@ ch @@ s-    WhileCh' pCh pEnd ch s False = WhileCh'' (pEnd @@ s)--type family WhileCh'' res where-    WhileCh'' (Right r) = Done r-    WhileCh'' (Left  e) = Err (EWhile e)+type While :: (Char ~> Bool) -> PParser a -> PParser a+data While chPred p s+type instance App (While chPred p) s = While' chPred p s -type EWhile e = EIn "While" e-eWhile :: SE e -> SE (EWhile e)-eWhile e = withSingE e $ singE+type family While' chPred p s where+    While' chPred p ('State rem len idx) =+        WhileCountStart len rem idx chPred p (UnconsSymbol rem) -type WhileChSym-    :: (Char ~> Bool)-    -> ParserChSym  s r-    -> ParserEndSym s r-    -> ParserChSym  s r-data WhileChSym chPred pCh pEnd f-type instance App (WhileChSym chPred pCh pEnd) f = WhileChSym1 chPred pCh pEnd f+type family WhileCountStart len rem idx chPred p mstr where+    WhileCountStart len rem idx chPred p (Just '(ch, str)) =+        WhileCount len rem idx chPred p 0 (UnconsSymbol str) (chPred @@ ch)+    WhileCountStart len rem idx chPred p Nothing           = p @@ ('State rem 0 idx) -type WhileChSym1-    :: (Char ~> Bool)-    -> ParserChSym  s r-    -> ParserEndSym s r-    -> ParserChSym1 s r-data WhileChSym1 chPred pCh pEnd ch s-type instance App (WhileChSym1 chPred pCh pEnd ch) s = WhileCh chPred pCh pEnd ch s+type family WhileCount len rem idx chPred p n mstr res where+    WhileCount len rem idx chPred p n (Just '(ch, str)) True  =+        WhileCount len rem idx chPred p (n+1) (UnconsSymbol str) (chPred @@ ch)+    WhileCount len rem idx chPred p n (Just '(ch, str)) False =+        WhileEnd (len-n)     (p @@ ('State rem n     idx))+    WhileCount len rem idx chPred p n Nothing           True  =+        WhileEnd (len-(n+1)) (p @@ ('State rem (n+1) idx))+    WhileCount len rem idx chPred p n Nothing           False =+        WhileEnd (len-n)     (p @@ ('State rem n     idx)) -sWhileChSym-    :: Lam SChar SBool chPred-    -> SParserChSym  ss sr pCh-    -> SParserEndSym ss sr pEnd-    -> SParserChSym  ss sr (WhileChSym chPred pCh pEnd)-sWhileChSym chPred pCh pEnd = Lam2 $ \ch s ->-    case chPred @@ ch of-      STrue  -> pCh @@ ch @@ s-      SFalse ->-        case pEnd @@ s of-          SRight r -> SDone r-          SLeft  e -> SErr $ eWhile e+type family WhileEnd lenRest rep where+    -- TODO note that we don't require that the inner parser fully consumes.+    -- that's because we "lie" about how this parser works. you probably want a+    -- sort of char-by-char parser, but we measure a chunk and pass that.+    -- but by not requiring full consumption, we recover char-by-char behaviour!+    -- and we can still get full consumption by combining with Isolate.+    -- the inner parser should generally fully consume though, as a design point+    WhileEnd lenRest ('Reply res ('State rem len idx)) =+        'Reply res ('State rem (lenRest+len) idx)
src/Symparsec/Parser/While/Predicates.hs view
@@ -1,19 +1,11 @@ -- | Character predicates.---- TODO for singling, I could cheat by inspecting the char value. should be--- faster and better. but would need a bit more checking so cba for now.+--+-- raehik copied his module from Symparsec.  module Symparsec.Parser.While.Predicates where  import DeFun.Core-import GHC.TypeLits-import Singleraeh.Bool-import Singleraeh.Equality ( testEqElse )-import Unsafe.Coerce ( unsafeCoerce ) -class SingChPred chPred where-    singChPred :: Lam SChar SBool chPred- -- | @A-Za-z@ type IsAlpha :: Char -> Bool type family IsAlpha ch where@@ -75,64 +67,6 @@ data IsAlphaSym ch type instance App IsAlphaSym ch = IsAlpha ch -sIsAlphaSym :: Lam SChar SBool IsAlphaSym-sIsAlphaSym = Lam $ \ch ->-      testEqElse ch (SChar @'a') STrue-    $ testEqElse ch (SChar @'A') STrue-    $ testEqElse ch (SChar @'b') STrue-    $ testEqElse ch (SChar @'B') STrue-    $ testEqElse ch (SChar @'c') STrue-    $ testEqElse ch (SChar @'C') STrue-    $ testEqElse ch (SChar @'d') STrue-    $ testEqElse ch (SChar @'D') STrue-    $ testEqElse ch (SChar @'e') STrue-    $ testEqElse ch (SChar @'E') STrue-    $ testEqElse ch (SChar @'f') STrue-    $ testEqElse ch (SChar @'F') STrue-    $ testEqElse ch (SChar @'g') STrue-    $ testEqElse ch (SChar @'G') STrue-    $ testEqElse ch (SChar @'h') STrue-    $ testEqElse ch (SChar @'H') STrue-    $ testEqElse ch (SChar @'i') STrue-    $ testEqElse ch (SChar @'I') STrue-    $ testEqElse ch (SChar @'j') STrue-    $ testEqElse ch (SChar @'J') STrue-    $ testEqElse ch (SChar @'k') STrue-    $ testEqElse ch (SChar @'K') STrue-    $ testEqElse ch (SChar @'l') STrue-    $ testEqElse ch (SChar @'L') STrue-    $ testEqElse ch (SChar @'m') STrue-    $ testEqElse ch (SChar @'M') STrue-    $ testEqElse ch (SChar @'n') STrue-    $ testEqElse ch (SChar @'N') STrue-    $ testEqElse ch (SChar @'o') STrue-    $ testEqElse ch (SChar @'O') STrue-    $ testEqElse ch (SChar @'p') STrue-    $ testEqElse ch (SChar @'P') STrue-    $ testEqElse ch (SChar @'q') STrue-    $ testEqElse ch (SChar @'Q') STrue-    $ testEqElse ch (SChar @'r') STrue-    $ testEqElse ch (SChar @'R') STrue-    $ testEqElse ch (SChar @'s') STrue-    $ testEqElse ch (SChar @'S') STrue-    $ testEqElse ch (SChar @'t') STrue-    $ testEqElse ch (SChar @'T') STrue-    $ testEqElse ch (SChar @'u') STrue-    $ testEqElse ch (SChar @'U') STrue-    $ testEqElse ch (SChar @'v') STrue-    $ testEqElse ch (SChar @'V') STrue-    $ testEqElse ch (SChar @'w') STrue-    $ testEqElse ch (SChar @'W') STrue-    $ testEqElse ch (SChar @'x') STrue-    $ testEqElse ch (SChar @'X') STrue-    $ testEqElse ch (SChar @'y') STrue-    $ testEqElse ch (SChar @'Y') STrue-    $ testEqElse ch (SChar @'z') STrue-    $ testEqElse ch (SChar @'Z') STrue-    $ unsafeCoerce SFalse--instance SingChPred IsAlphaSym where singChPred = sIsAlphaSym- -- | @0-9A-Fa-f@ type IsHexDigit :: Char -> Bool type family IsHexDigit ch where@@ -164,30 +98,21 @@ data IsHexDigitSym ch type instance App IsHexDigitSym ch = IsHexDigit ch -sIsHexDigitSym :: Lam SChar SBool IsHexDigitSym-sIsHexDigitSym = Lam $ \ch ->-      testEqElse ch (SChar @'0') STrue-    $ testEqElse ch (SChar @'1') STrue-    $ testEqElse ch (SChar @'2') STrue-    $ testEqElse ch (SChar @'3') STrue-    $ testEqElse ch (SChar @'4') STrue-    $ testEqElse ch (SChar @'5') STrue-    $ testEqElse ch (SChar @'6') STrue-    $ testEqElse ch (SChar @'7') STrue-    $ testEqElse ch (SChar @'8') STrue-    $ testEqElse ch (SChar @'9') STrue-    $ testEqElse ch (SChar @'a') STrue-    $ testEqElse ch (SChar @'A') STrue-    $ testEqElse ch (SChar @'b') STrue-    $ testEqElse ch (SChar @'B') STrue-    $ testEqElse ch (SChar @'c') STrue-    $ testEqElse ch (SChar @'C') STrue-    $ testEqElse ch (SChar @'d') STrue-    $ testEqElse ch (SChar @'D') STrue-    $ testEqElse ch (SChar @'e') STrue-    $ testEqElse ch (SChar @'E') STrue-    $ testEqElse ch (SChar @'f') STrue-    $ testEqElse ch (SChar @'F') STrue-    $ unsafeCoerce SFalse+-- | @0-9@+type IsDecDigit :: Char -> Bool+type family IsDecDigit ch where+    IsDecDigit '0' = True+    IsDecDigit '1' = True+    IsDecDigit '2' = True+    IsDecDigit '3' = True+    IsDecDigit '4' = True+    IsDecDigit '5' = True+    IsDecDigit '6' = True+    IsDecDigit '7' = True+    IsDecDigit '8' = True+    IsDecDigit '9' = True+    IsDecDigit _   = False -instance SingChPred IsHexDigitSym where singChPred = sIsHexDigitSym+type IsDecDigitSym :: Char ~> Bool+data IsDecDigitSym ch+type instance App IsDecDigitSym ch = IsDecDigit ch
src/Symparsec/Parsers.hs view
@@ -1,70 +1,106 @@--- | Type-level string parsers.+-- | Common type-level string parsers. ----- You may ignore the equations that Haddock displays: they are internal and--- irrelevant to library usage.+-- Many parsers reuse term-level names, which can cause ambiguity issues.+-- Consider importing qualified.  module Symparsec.Parsers   (-  -- * Binary combinators-  -- $binary-combinators-    (:<*>:)-  ,  (:*>:)-  , (:<*:)-  , (:<|>:)+  -- * Type class-esque+  -- $type-classes+    type (<$>)+  , type (<*>), type Pure, type LiftA2, type (*>), type (<*)+  , type (>>=)+  , type (<|>), type Empty, type Optional    -- * Positional   -- $positional-  , Take-  , TakeRest-  , Skip-  , End-  , Isolate--  -- * Predicated-  -- $predicated-  , While, TakeWhile+  , type Ensure+  , type Isolate+  , type Take+  , type TakeRest+  , type Skip+  , type Eof -  -- * TODO unsorted-  , Count+  -- * Other combinators+  -- $comb-etc+  , type Try+  , type While+  , type TakeWhile+  , type Count -  -- * Basic-  -- $basic-  , Literal+  -- * Common non-combinator+  -- $noncomb-common+  , type Literal    -- ** Naturals-  , NatDec-  , NatHex-  , NatBin-  , NatOct-  , NatBase+  , type NatBase+  , type NatDec+  , type NatHex+  , type NatBin+  , type NatOct++  -- * Derived+  -- $derived+  , type Tuple++  -- * Missing parsers+  -- $missing   ) where +import Symparsec.Parser.Alternative+import Symparsec.Parser.Applicative+import Symparsec.Parser.Count+import Symparsec.Parser.Ensure+import Symparsec.Parser.Eof+import Symparsec.Parser.Functor import Symparsec.Parser.Isolate-import Symparsec.Parser.Skip-import Symparsec.Parser.Natural-import Symparsec.Parser.Then-import Symparsec.Parser.Then.VoidLeft-import Symparsec.Parser.Then.VoidRight import Symparsec.Parser.Literal-import Symparsec.Parser.End+import Symparsec.Parser.Monad+import Symparsec.Parser.Natural+import Symparsec.Parser.Skip import Symparsec.Parser.Take import Symparsec.Parser.TakeRest-import Symparsec.Parser.Or+import Symparsec.Parser.TakeWhile+import Symparsec.Parser.Try import Symparsec.Parser.While-import Symparsec.Parser.Count+import DeFun.Core --- $binary-combinators--- Parsers that combine two parsers. Any parsers that have term-level parallels--- will use the same fixity e.g. ':<*>:' is @infixl 4@, same as '<*>'.+{- $type-classes+Parsers which mirror functions from type classes (specifically 'Functor',+'Applicative', 'Monad' and 'Control.Alternative.Alternative'. These primitive+combinators are powerful, but can be tough to use without type-level binders or+do-notation, and force interacting with defunctionalization.+-} --- $positional--- Parsers that relate to symbol position e.g. length, end of symbol.+{- $positional+Parsers that relate to input position e.g. length, end of input.+-} --- $predicated--- Parsers that include character predicates.+{- $comb-etc+Assorted parser combinators (that wrap other parsers).+-} --- $basic--- Simple non-combinator parsers. Probably fundamental in some way e.g. very--- general or common.+{- $noncomb-common+Simple non-combinator parser. Probably fundamental in some way e.g. very general+or common.+-} -type TakeWhile chPred = While chPred TakeRest+{- $missing+Certain term-level parsers you may be used to you will /not/ see in Symparsec:++* Parsers that rely on underlying instances e.g. no @'Semigroup' a => Semigroup+  (parser a)@ because we'd have to pass @Semigroup a@ manually, which defeats+  the purpose+-}++{- $derived+Derived parsers. Should be type synonyms.+-}++{- | Parse left, then right, and return their results in a tuple.++Classic parser combinators often don't define this because it's trivial, and do+notation is often cleaner anyway. But it's very syntactically busy on the type+level, and we don't have do notation. So here's a convenience definition.+-}+type Tuple l r = LiftA2 (Con2 '(,)) l r
src/Symparsec/Run.hs view
@@ -1,39 +1,34 @@ {-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE AllowAmbiguousTypes #-} -- for reifying/singled parsers -module Symparsec.Run where -- ( Run, ERun(..) ) where+-- | Running Symparsec parsers. +module Symparsec.Run ( type Run, type RunTest ) where+ import Symparsec.Parser-import GHC.TypeLits hiding ( ErrorMessage(..), fromSNat )-import GHC.TypeNats ( fromSNat )-import GHC.TypeLits qualified as TE+import Data.Type.Symbol qualified as Symbol import DeFun.Core+import GHC.TypeLits ( type Symbol )+import GHC.TypeNats ( type Natural, type (+) )+import GHC.TypeError qualified as TE import TypeLevelShow.Doc-import TypeLevelShow.Utils ( ShowChar )-import TypeLevelShow.Natural ( ShowNatDec )-import Singleraeh.Tuple ( STuple2(..) )-import Singleraeh.Maybe ( SMaybe(..) )-import Singleraeh.Either ( SEither(..) )-import Singleraeh.Symbol-    ( sConsSymbol, sUnconsSymbol, ReconsSymbol, sReconsSymbol )-import Singleraeh.Natural ( (%+) )-import Singleraeh.Demote---- | Run the given parser on the given 'Symbol', returning an 'TE.ErrorMessage'---   on failure.-type Run :: PParser s r -> Symbol -> Either TE.ErrorMessage (r, Symbol)-type Run p sym = MapLeftRender (Run' p sym)+import TypeLevelShow.Natural ( type ShowNatDec ) -type MapLeftRender :: Either PERun r -> Either TE.ErrorMessage r-type family MapLeftRender eer where-    MapLeftRender (Right a) = Right a-    MapLeftRender (Left  e) = Left (RenderPDoc (PrettyERun e))+-- | Run the given parser on the given 'Symbol'.+--+-- * On success, returns a tuple of @(result :: a, remaining :: 'Symbol')@.+-- * On failure, returns an 'TE.ErrorMessage'.+type Run :: PParser a -> Symbol -> Either TE.ErrorMessage (a, Symbol)+type Run p str = RunEnd str (p @@ StateInit str) --- | 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)+type RunEnd :: Symbol -> PReply a -> Either TE.ErrorMessage (a, Symbol)+type family RunEnd str rep where+    RunEnd str ('Reply (OK  a) ('State  rem _len _idx)) =+        -- TODO I could return only @len@ of the remaining input @rem@, but+        -- that's more work than just returning @rem@, and I don't see a way+        -- this would matter for correct parsers.+        Right '(a, rem)+    RunEnd str ('Reply (Err e) ('State _rem _len  idx)) =+        Left (RenderPDoc (PrettyErrorTop idx str e))  -- | Run the given parser on the given 'Symbol', emitting a type error on --   failure.@@ -41,176 +36,47 @@ -- 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)+type RunTest :: PParser a -> Symbol -> (a, Symbol)+type RunTest p str = FromRightTypeError (Run p str) --- | Run the given parser on the given 'Symbol', returning a 'PERun' on failure,---   and ignoring any remaining non-consumed characters.-type Run'_ :: PParser s r -> Symbol -> Either TE.ErrorMessage r-type Run'_ p str = Run'_Inner (Run' p str)+type FromRightTypeError :: Either TE.ErrorMessage a -> a+type family FromRightTypeError eea where+    FromRightTypeError (Right a) = a+    FromRightTypeError (Left  e) = TE.TypeError e -type Run'_Inner :: Either PERun (a, b) -> Either TE.ErrorMessage a-type family Run'_Inner eeab where-    Run'_Inner (Right '(a, b)) = Right a-    Run'_Inner (Left  e)       = Left (RenderPDoc (PrettyERun e))+-- | Initial parser state for the given 'Symbol'.+type StateInit :: Symbol -> PState+type StateInit str = 'State str (Symbol.Length str) 0 --- | Run the singled version of type-level parser on the given 'String',---   returning an 'ERun' on failure.+-- | Pretty print a top-level parser error. ----- 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+-- Tries to look a bit like Megaparsec and modern compiler parser errors,+-- except we don't actually track much for now (e.g. no line numbers, spans).+type PrettyErrorTop :: Natural -> Symbol -> PError -> PDoc+type PrettyErrorTop idx str e =+             -- idx+1 because we're emitting char position here, not index+             Text "Symparsec parse error:"+        :$$: Text "1:" :<>: Text (ShowNatDec (idx+1))+        :$$: PrettyErrorPosition idx str+        :$$: PrettyError e --- | Inspect character parser result.+-- | Print a 'Symbol' and some ASCII art highlighting a character index in it. ----- This is purposely written so that the main case is at the top, and a single--- equation (we parse, prepare next character and inspect character parser--- result at the same time). My hope is that this keeps GHC fast.-type family RunCh pCh pEnd idx ch' mstr res where-    -- | OK, and more to come: parse next character-    RunCh pCh pEnd idx ch' (Just '(ch, sym)) (Cont s) =-        RunCh pCh pEnd (idx+1) ch (UnconsSymbol sym) (pCh @@ ch @@ s)--    -- | OK, and we're at the end of the string: run end parser-    RunCh pCh pEnd idx ch' Nothing           (Cont s) =-        RunEnd idx ch' (pEnd @@ s)--    -- | OK, and we're finished early: return value and remaining string-    RunCh pCh pEnd idx ch' mstr              (Done r) =-        Right '(r, ConsSymbol ch' (ReconsSymbol mstr))--    -- | Parse error: return error-    RunCh pCh pEnd idx ch' mstr              (Err  e) =-        Left ('ERun idx ch' e)--sRunCh-    :: SParserChSym  ss sr pCh-    -> SParserEndSym ss sr pEnd-    -> SNat idx-    -> SChar chPrev-    -> SMaybe (STuple2 SChar SSymbol) mstr-    -> SResult ss sr res-    -> SEither SERun (STuple2 sr SSymbol) (RunCh pCh pEnd idx chPrev mstr res)-sRunCh 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 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)--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 " :<>: Text (ShowNatDec idx)-        :<>: Text ", char '" :<>: Text (ShowChar ch) :<>: Text "'"-        :$$: PrettyE e--type PrettyE :: PE -> PDoc-type family PrettyE e where-    PrettyE (EBase name emsg)  = Text name :<>: Text ": " :<>: emsg-    PrettyE (EIn   name e)     = Text name :<>: Text ": " :<>: PrettyE e---- | Error while running parser.-data ERun s-  -- | Parser error at index X, character C.-  = ERun Natural Char (E s)--  -- | Parser error on the empty string.-  | ERun0 (E s)-    deriving stock 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)+-- Looks like Megaparsec and other modern compiler parser errors.+type PrettyErrorPosition :: Natural -> Symbol -> PDoc+type PrettyErrorPosition idx str =+             Text "  |"+        :$$: Text "1 | " :<>: Text str+        :$$: Text "  | " :<>: Text (Symbol.Replicate idx ' ') :<>: Text "^" -demoteSERun :: SERun erun -> ERun String-demoteSERun = \case-  SERun  idx ch e -> ERun  (fromSNat idx) (fromSChar ch) (demoteSE e)-  SERun0        e -> ERun0                               (demoteSE e)+-- | Pretty print a parser error.+type PrettyError :: PError -> PDoc+type family PrettyError e where+    PrettyError ('Error (str:strs)) = ConcatSymbol (Text str) strs+    PrettyError ('Error '[])        = Text "<no detail>" -instance Demotable SERun where-    type Demote SERun = ERun String-    demote = demoteSERun+type ConcatSymbol :: PDoc -> [Symbol] -> PDoc+type family ConcatSymbol doc strs where+    -- TODO get ordering right+    ConcatSymbol doc (str:strs) = ConcatSymbol (doc :$$: Text str) strs+    ConcatSymbol doc '[]        = doc
+ src/Symparsec/Utils.hs view
@@ -0,0 +1,6 @@+module Symparsec.Utils where++import GHC.TypeNats ( type CmpNat )+import Data.Type.Ord ( type OrdCond )++type IfNatLte n m fThen fElse = OrdCond (CmpNat n m) fThen fThen fElse
symparsec.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.38.2. -- -- see: https://github.com/sol/hpack  name:           symparsec-version:        1.1.1+version:        2.0.0 synopsis:       Type level string parser combinators description:    Please see README.md. category:       Types, Data@@ -17,8 +17,7 @@ license-file:   LICENSE build-type:     Simple tested-with:-    GHC==9.8-  , GHC==9.6+    GHC==9.12 extra-source-files:     README.md     CHANGELOG.md@@ -29,28 +28,32 @@  library   exposed-modules:+      Data.Type.Symbol       Symparsec       Symparsec.Example.Expr       Symparsec.Parser-      Symparsec.Parser.Apply+      Symparsec.Parser.Alternative+      Symparsec.Parser.Applicative       Symparsec.Parser.Common       Symparsec.Parser.Count-      Symparsec.Parser.End+      Symparsec.Parser.Ensure+      Symparsec.Parser.Eof+      Symparsec.Parser.Functor       Symparsec.Parser.Isolate       Symparsec.Parser.Literal+      Symparsec.Parser.Monad       Symparsec.Parser.Natural       Symparsec.Parser.Natural.Digits-      Symparsec.Parser.Or       Symparsec.Parser.Skip       Symparsec.Parser.Take       Symparsec.Parser.TakeRest-      Symparsec.Parser.Then-      Symparsec.Parser.Then.VoidLeft-      Symparsec.Parser.Then.VoidRight+      Symparsec.Parser.TakeWhile+      Symparsec.Parser.Try       Symparsec.Parser.While       Symparsec.Parser.While.Predicates       Symparsec.Parsers       Symparsec.Run+      Symparsec.Utils   other-modules:       Paths_symparsec   hs-source-dirs:@@ -66,7 +69,7 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall -Wno-unticked-promoted-constructors+  ghc-options: -fhide-source-paths -Wall   build-depends:       base >=4.18 && <5     , defun-core ==0.1.*@@ -92,7 +95,7 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall -Wno-unticked-promoted-constructors+  ghc-options: -fhide-source-paths -Wall   build-depends:       base >=4.18 && <5     , defun-core ==0.1.*
test/Main.hs view
@@ -2,22 +2,20 @@  import Test.TypeSpec import Symparsec+import DeFun.Core ( type Con2 )  main :: IO () main = print spec --- The type errors for failures are HILARIOUS if you're into that sort of thing.--- Try messing with a test or two and see mad GHC gets!--type CstrX_Y =-          (Literal "Cstr" :*>: Isolate 2 NatDec)-    :<*>: (Literal "_"    :*>: Isolate 2 NatHex)+type CstrX_Y = LiftA2 (Con2 '(,))+    (Literal "Cstr" *> Isolate 2 NatDec)+    (Literal "_"    *> Isolate 2 NatHex)  spec :: Expect     '[ Run (Literal "raehik") "raehik" `Is` Right '( '(), "")      , Run (Literal "raeh") "raehraeh" `Is` Right '( '(), "raeh")-     , Run (Skip 3 :*>: Literal "HI") "...HI" `Is` Right '( '(), "")-     , Run (Literal "0x" :*>: NatHex) "0xfF" `Is` Right '( 255, "")+     , Run (Skip 3 *> Literal "HI") "...HI" `Is` Right '( '(), "")+     , Run (Literal "0x" *> NatHex) "0xfF" `Is` Right '( 255, "")      , Run CstrX_Y "Cstr12_AB" `Is` Right '( '(12, 0xAB), "")      ] spec = Valid