add user state to parsers

CHANGELOG.md

@@ -1,3 +1,7 @@
+## 2.1.0 (unreleased)
+- Parsers now take user state.
+  Use `Run'`, `RunTest'` to ignore (run with the empty state `'()`).
+
 ## 2.0.0 (2025-10-11)
 Full rewrite.
 

README.md

@@ -24,8 +24,8 @@ 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_etc"
-Run ...
+ghci> :k! Run' PExample "xFF_etc"
+Run' ...
 = Right '( '(255, "etc"), "")
 ```
 

src/Symparsec.hs

@@ -13,7 +13,9 @@ module Symparsec
   (
   -- * Base definitions
     type Run
+  , type Run'
   , type RunTest
+  , type RunTest'
 
   -- * Parsers
   , module Symparsec.Parsers

src/Symparsec/Example/Expr.hs

@@ -48,15 +48,15 @@ data ExprTok
   | TokParenL
   | TokParenR
 
-type PExpr :: PParser (Expr Natural)
+type PExpr :: PParser u (Expr Natural)
 data PExpr s
 type instance App PExpr s = PExprNext s '[] '[] (UnconsState s)
 type PExprNext
-    :: PState
+    :: PState u
     -> [ExprTok]
     -> [Expr Natural]
-    -> (Maybe Char, PState)
-    -> PReply (Expr Natural)
+    -> (Maybe Char, PState u)
+    -> PReply u (Expr Natural)
 type family PExprNext sPrev ops exprs s where
     PExprNext sPrev ops exprs '(Just ch, s) =
         PExprCh sPrev s ops exprs ch
@@ -134,8 +134,8 @@ type family PExprEBOpOpCh ch where
     PExprEBOpOpCh _   = Nothing
 
 type PExprEBOp'
-    :: PState -> PState -> BOp -> Natural -> [Expr Natural] -> [ExprTok]
-    -> PReply (Expr Natural)
+    :: PState u -> PState u -> BOp -> Natural -> [Expr Natural] -> [ExprTok]
+    -> PReply u (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)

src/Symparsec/Example/Printf.hs

@@ -31,7 +31,7 @@ type Number = NatBaseWhile 10 ParseDigitDecSym
 
 -- special parser that I probably don't want (surely can just combine)
 -- backtracks!!
-type NotChar :: Char -> PParser Char
+type NotChar :: Char -> PParser u Char
 data NotChar c s
 type instance App (NotChar c) s = NotChar' c s (UnconsState s)
 type family NotChar' cNo sPrev s where
@@ -71,13 +71,13 @@ data Flags = Flags
   , fAlternate :: Bool
   }
 
-type FlagParser :: PParser Flags
+type FlagParser :: PParser u Flags
 data FlagParser s
 type instance App FlagParser s = PFlags' EmptyFlags s (UnconsState s)
 
 type EmptyFlags = 'Flags Nothing Nothing False
 
-type PFlags' :: Flags -> PState -> (Maybe Char, PState) -> PReply Flags
+type PFlags' :: Flags -> PState u -> (Maybe Char, PState u) -> PReply u Flags
 type family PFlags' flags sPrev s where
   PFlags' ('Flags d i l) sPrev '(Just '-', s) =
     PFlags' ('Flags (Just (UpdateAdjust d LeftAdjust)) i l) s (UnconsState s)
@@ -113,7 +113,10 @@ data FieldFormat = FF
   }
 
 -- copied as-is except for 'Con5'
-type FFParser :: PParser FieldFormat
+-- TODO with user state introduced, adding a standalone kind signature results
+-- in a type error. GHC initialises an inner u0 and doesn't see u ~ u0.
+-- Can be fixed by using type abstraction syntax, I think.
+--type FFParser :: PParser u FieldFormat
 type FFParser = Con5 FF
     <$> FlagParser
     <*> Optional Number

src/Symparsec/Parser.hs

@@ -14,7 +14,7 @@ import Singleraeh.List
 --import Singleraeh.Symbol
 
 -- | Parser state.
-data State str n = State
+data State str n u = State
   -- | Remaining input.
   { remaining :: str
 
@@ -34,23 +34,32 @@ data State str n = State
   --
   -- Overall index. Used for nicer error reporting after parse completion.
   , index :: n
+
+  -- | User state.
+  , user :: u
   } deriving stock Show
 
 -- | Promoted 'State'.
 type PState = State Symbol Natural
 
 -- | Singled 'State'.
-data SState (s :: PState) where
-    SState :: SSymbol rem -> SNat len -> SNat idx -> SState ('State rem len idx)
+data SState (su :: u -> Type) (pu :: PState u) where
+    SState :: SSymbol rem -> SNat len -> SNat idx -> su u -> SState su ('State rem len idx user)
+
+-- | Demoted 'State'.
+type DState = State String Natural
 
 -- | Demote an 'SState'.
-demoteSState :: SState s -> State String Natural
-demoteSState (SState srem slen sidx) =
-    State (fromSSymbol srem) (fromSNat slen) (fromSNat sidx)
+demoteSState
+    :: (forall u. su u -> du)
+    -> SState su pu
+    -> DState du
+demoteSState demoteSU (SState srem slen sidx suser) =
+    State (fromSSymbol srem) (fromSNat slen) (fromSNat sidx) (demoteSU suser)
 
-instance Demotable SState where
-    type Demote SState = State String Natural
-    demote = demoteSState
+instance Demotable su => Demotable (SState su) where
+    type Demote (SState su) = DState (Demote su)
+    demote = demoteSState demote
 
 {-
 data Span n = Span
@@ -82,29 +91,33 @@ instance Demotable SError where
 --
 -- TODO: megaparsec also returns a bool indicating if any input was consumed.
 -- Unsure what it's used for.
-data Reply str n a = Reply
+data Reply str n u a = Reply
   { result :: Result str n a -- ^ Parse result.
-  , state  :: State str n    -- ^ Final parser state.
+  , state  ::  State str n u -- ^ Final parser state.
   } deriving stock Show
 
 -- | Promoted 'Reply'.
 type PReply = Reply Symbol Natural
 
 -- | Singled 'Reply'.
-data SReply (sa :: a -> Type) (rep :: PReply a) where
-    SReply :: SResult sa result -> SState state -> SReply sa ('Reply result state)
+data SReply (su :: u -> Type) (sa :: a -> Type) (rep :: PReply u a) where
+    SReply :: SResult sa result -> SState su state -> SReply su sa ('Reply result state)
+
+-- | Demoted 'Reply'.
+type DReply = Reply String Natural
 
 -- | 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)
+    :: (forall u. su u -> du)
+    -> (forall a. sa a -> da)
+    -> SReply su sa rep
+    -> DReply du da
+demoteSReply demoteSU demoteSA (SReply sresult sstate) =
+    Reply (demoteSResult demoteSA sresult) (demoteSState demoteSU sstate)
 
-instance Demotable sa => Demotable (SReply sa) where
-    type Demote (SReply sa) = Reply String Natural (Demote sa)
-    demote = demoteSReply demote
+instance (Demotable su, Demotable sa) => Demotable (SReply su sa) where
+    type Demote (SReply su sa) = DReply (Demote su) (Demote sa)
+    demote = demoteSReply demote demote
 
 -- | Parse result: a value, or an error.
 data Result str n a = OK a            -- ^ Parser succeeded.
@@ -114,20 +127,19 @@ data Result str n a = OK a            -- ^ Parser succeeded.
 -- | Promoted 'Result'.
 type PResult = Result Symbol Natural
 
---type SState = State 
---type SResult :: _ -> Type
--- TODO ^ how to do explicit kind signature for GADT?
-
 -- | 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)
 
+-- | Demoted 'Result'.
+type DResult = Result String Natural
+
 -- | Demote an 'SResult'.
 demoteSResult
     :: (forall a. sa a -> da)
     -> SResult sa res
-    -> Result String Natural da
+    -> DResult da
 demoteSResult demoteSA = \case
   SOK  sa -> OK  $ demoteSA sa
   SErr se -> Err $ demoteSError se
@@ -137,14 +149,14 @@ instance Demotable sa => Demotable (SResult sa) where
     demote = demoteSResult demote
 
 -- | A parser is a function on parser state.
-type Parser str n a = State str n -> Reply str n a
+type Parser str n u a = State str n u -> Reply str n u a
 
 -- | Promoted 'Parser': a defunctionalization symbol to a function on promoted
 --   parser state.
-type PParser a = PState ~> PReply a
+type PParser u a = PState u ~> PReply u a
 
 -- | Singled 'Parser'.
-type SParser sa p = Lam SState (SReply sa) p
+type SParser su sa p = Lam (SState su) (SReply su sa) p
 --data SParser (sa :: a -> Type) (p :: PParser a) where
  --   SParser :: Lam SState (SReply sa) (PParser a)
 

src/Symparsec/Parser/Alternative.hs

@@ -22,22 +22,22 @@ import qualified Singleraeh.List as List
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
 --
 -- TODO shitty errors
-type (<|>) :: PParser a -> PParser a -> PParser a
+type (<|>) :: PParser u a -> PParser u a -> PParser u 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 Plus :: PParser u a -> PReply u a -> PReply u 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
+type Empty :: PParser u 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 :: PParser u a -> PParser u (Maybe a)
 type Optional p = Con1 Just <$> p <|> Pure Nothing
 
 {- Wow, I guess that works. But also, the manual version:
@@ -52,7 +52,7 @@ type family OptionalEnd rep where
 -- | 'Control.Alternative.many' for parsers.
 --
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
-type Many :: PParser a -> PParser [a]
+type Many :: PParser u a -> PParser u [a]
 data Many p s
 type instance App (Many p) s = Many' p '[] (p @@ s)
 type family Many' p as rep where
@@ -62,21 +62,21 @@ type family Many' p as rep where
 -- | 'Control.Alternative.some' for parsers.
 --
 -- Does not backtrack. Wrap parsers with 'Symparsec.Parser.Try' as needed.
-type Some :: PParser a -> PParser [a]
+type Some :: PParser u a -> PParser u [a]
 type Some p = LiftA2 (Con2 '(:)) p (Many p)
 
 -- | @'SepBy' p sep@ parses zero or more occurrences of @p@, separated by @sep@.
 --   Returns a list of values parsed by @p@.
-type SepBy :: PParser a -> PParser sep -> PParser [a]
+type SepBy :: PParser u a -> PParser u sep -> PParser u [a]
 type SepBy p sep = SepBy1 p sep <|> Pure '[]
 
 -- | @'SepBy1' p sep@ parses one or more occurrences of @p@, separated by @sep@.
 --   Returns a list of values parsed by @p@.
-type SepBy1 :: PParser a -> PParser sep -> PParser [a]
+type SepBy1 :: PParser u a -> PParser u sep -> PParser u [a]
 type SepBy1 p sep = LiftA2 (Con2 '(:)) p (Many (sep *> p))
 
 -- TODO doesn't backtrack, matching megaparsec.
-type Choice :: [PParser a] -> PParser a
+type Choice :: [PParser u a] -> PParser u a
 data Choice pList ps
 type instance App (Choice pList) ps = ChoiceStart pList ps
 

src/Symparsec/Parser/Applicative.hs

@@ -13,33 +13,33 @@ 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
+type (<*>) :: PParser u (a ~> b) -> PParser u a -> PParser u 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 ApL :: PParser u a -> PReply u (a ~> b) -> PReply u 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
+type Pure :: a -> PParser u 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 :: (a ~> b ~> c) -> PParser u a -> PParser u b -> PParser u 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
+type (*>) :: PParser u a -> PParser u b -> PParser u 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
+type (<*) :: PParser u a -> PParser u b -> PParser u a
 infixl 4 <*
 type l <* r = LiftA2 ConstSym l r

src/Symparsec/Parser/Common.hs

@@ -45,17 +45,17 @@ import GHC.TypeError qualified as TE
 --
 -- 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 UnconsState :: PState u -> (Maybe Char, PState u)
 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
+    UnconsState ('State rem 0   idx user) = '(Nothing, 'State rem 0 idx user)
+    UnconsState ('State rem len idx user) = UnconsState' (UnconsSymbol rem) len idx user
 
 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 =
+    :: Maybe (Char, Symbol) -> Natural -> Natural -> u -> (Maybe Char, PState u)
+type family UnconsState' mstr len idx user where
+    UnconsState' (Just '(ch, rem)) len idx user =
+        '(Just ch, 'State rem (len-1) (idx+1) user)
+    UnconsState' Nothing           len idx user =
         -- 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")
 

src/Symparsec/Parser/Count.hs

@@ -8,7 +8,7 @@ import qualified Singleraeh.List as List
 -- TODO Could possibly make more efficient.
 
 -- | @'Count' n p@ parses @n@ occurrences of @p@.
-type Count :: Natural -> PParser a -> PParser [a]
+type Count :: Natural -> PParser u a -> PParser u [a]
 data Count n p s
 type instance App (Count n p) s = CountLoop p '[] n s
 

src/Symparsec/Parser/Ensure.hs

@@ -6,11 +6,11 @@ import Symparsec.Parser.Common
 import Symparsec.Utils ( type IfNatLte )
 
 -- | Assert that there are at least @n@ characters remaining. Non-consuming.
-type Ensure :: Natural -> PParser ()
+type Ensure :: Natural -> PParser u ()
 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) =
+    Ensure' n ('State rem len idx user) =
         IfNatLte n len
-            ('Reply (OK '()) ('State rem len idx))
-            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx))
+            ('Reply (OK '()) ('State rem len idx user))
+            ('Reply (Err (Error1 (EStrInputTooShort n len))) ('State rem len idx user))

src/Symparsec/Parser/Eof.hs

@@ -5,7 +5,7 @@ module Symparsec.Parser.Eof ( type Eof ) where
 import Symparsec.Parser.Common
 
 -- | Assert end of input, or fail.
-type Eof :: PParser ()
+type Eof :: PParser u ()
 data Eof s
 type instance App Eof s = Eof' (UnconsState s)
 type family Eof' ms where