Refactor Parser.Stream

Parser/Basic.lean

@@ -12,7 +12,7 @@ public import Parser.Stream
 public section
 
 namespace Parser
-variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
+variable {σ τ} [Parser.Stream σ τ] {ε} [Parser.Error ε σ τ] {m} [Monad m]
 
 /-! # Token Functions -/
 
@@ -22,10 +22,11 @@ variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
 This is a low-level parser to customize how the parser stream is used.
 -/
 @[inline]
-def tokenCore (next? : σ → Option (τ × σ)) : ParserT ε σ τ m τ := do
-  match next? (← getStream) with
-  | some (tok, stream) =>
-    let _ ← setStream stream
+def tokenCore (next? : Stream.Position σ → Option (τ × Stream.Position σ)) :
+    ParserT ε σ τ m τ := do
+  match next? (← getPosition) with
+  | some (tok, pos) =>
+    setPosition pos
     return tok
   | none => throwUnexpected
 
@@ -35,7 +36,7 @@ the unexpected token.
 -/
 @[specialize]
 def tokenMap (test : τ → Option α) : ParserT ε σ τ m α := do
-  let tok ← tokenCore Stream.next?
+  let tok ← tokenCore (Stream.next? (← getStream))
   match test tok with
   | some x => return x
   | none => throwUnexpected tok

Parser/Char/Basic.lean

@@ -26,15 +26,18 @@ def chars (tks : String) : ParserT ε σ Char m String :=
     return acc
 
 /-- `string tks` accepts and returns string `tks`, otherwise fails -/
-def string [Parser.Error ε String.Slice Char] (tks : String.Slice) :
-    ParserT ε String.Slice Char m String.Slice :=
-  withErrorMessage s!"expected {repr tks.toString}" do
-    match (← getStream).dropPrefix? tks with
-    | some s =>
-      setStream s
-      return tks
-    | none =>
-      throwUnexpected
+def string [Parser.Error ε String.Slice Char] (tks : String) :
+    ParserT ε String.Slice Char m String :=
+  withErrorMessage s!"expected {repr tks}" do
+    let s ← getStream
+    let pos ← getPosition
+    if h : pos.IsValidForSlice s then
+      match (s.sliceFrom ⟨pos, h⟩).skipPrefix? tks with
+      | some ⟨pos', _⟩ =>
+        setPosition pos'
+        return tks
+      | none => throwUnexpected
+    else throwUnexpected
 
 /-- `captureStr p` parses `p` and returns the output of `p` with the corresponding `String.Slice` -/
 def captureStr {α} [h : Parser.Error ε String.Slice Char] (p : ParserT ε String.Slice Char m α) :
@@ -46,7 +49,7 @@ def captureStr {α} [h : Parser.Error ε String.Slice Char] (p : ParserT ε Stri
     return (x, ⟨s.str, ⟨start, h'.1⟩ , ⟨stop, h'.2.1⟩, String.Pos.le_iff.1 h'.2.2⟩)
   else
     have : Inhabited (ParserT ε String.Slice Char m (α × String.Slice)) :=
-      ⟨fun s => return .error s (h.unexpected 0 none)⟩
+      ⟨fun s pos => return .error s pos (h.unexpected 0 none)⟩
     unreachable!
 
 /--

Parser/Error.lean

@@ -63,13 +63,13 @@ This error type records the position and, optionally, the offending token where
 occurred; any additional information is discarded. This is useful for parsers where the cause of
 parsing errors is predictable and only the position of the error is needed for processing.
 -/
-abbrev Basic (σ τ) [Parser.Stream σ τ] := Parser.Stream.Position σ × Option τ
+abbrev Basic (σ τ) [Parser.Stream σ τ] := Stream.Position σ × Option τ
 
 instance (σ τ) [Parser.Stream σ τ] : Parser.Error (Basic σ τ) σ τ where
   unexpected p t := (p, t)
   addMessage e _ _ := e
 
-instance (σ τ) [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
+instance (σ τ) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] :
   ToString (Basic σ τ) where
   toString
     | (pos, some tok) => s!"unexpected input {repr tok} at {repr pos}"
@@ -87,8 +87,8 @@ inductive Simple (σ τ) [Parser.Stream σ τ]
   | addMessage : Simple σ τ → Stream.Position σ → String → Simple σ τ
 
 -- The derive handler for `Repr` fails, this is a workaround.
-protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
-  Simple σ τ → Nat → Std.Format
+protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ]
+    [Repr (Stream.Position σ)] : Simple σ τ → Nat → Std.Format
   | unexpected pos a, prec =>
     Repr.addAppParen
       (Std.Format.group

Parser/Parser.lean

@@ -11,69 +11,68 @@ public import Parser.Stream
 public section
 
 /-- Parser result type. -/
-protected inductive Parser.Result (ε σ α : Type _) : Type u
+protected inductive Parser.Result {τ} (ε σ α : Type u) [Parser.Stream σ τ] : Type u
   /-- Result: success! -/
-  | ok : σ → α → Parser.Result ε σ α
+  | ok : σ → Parser.Stream.Position σ → α → Parser.Result ε σ α
   /-- Result: error! -/
-  | error : σ → ε → Parser.Result ε σ α
-  deriving Inhabited, Repr
+  | error : σ → Parser.Stream.Position σ → ε → Parser.Result ε σ α
+deriving Inhabited -- TODO : manually implement Repr
 
 /--
 `ParserT ε σ τ` is a monad transformer to parse tokens of type `τ` from the stream type `σ` with
 error type `ε`.
 -/
 @[expose]
 def ParserT (ε σ τ : Type _) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type _ → Type _)
-  (α : Type _) : Type _ := σ → m (Parser.Result ε σ α)
+  (α : Type _) : Type _ := σ → Parser.Stream.Position σ → m (Parser.Result ε σ α)
 
 /-- Run the monadic parser `p` on input stream `s`. -/
 @[inline]
-def ParserT.run [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : ParserT ε σ τ m α) (s : σ) :
-  m (Parser.Result ε σ α) := p s
+def ParserT.run [stream : Parser.Stream σ τ] [Parser.Error ε σ τ]
+    (p : ParserT ε σ τ m α) (s : σ) (pos : optParam stream.Position (stream.start s)):
+  m (Parser.Result ε σ α) := p s pos
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   Monad (ParserT ε σ τ m) where
-  pure x s := return .ok s x
-  bind x f s := x s >>= fun
-    | .ok s a => f a s
-    | .error s e => return .error s e
-  map f x s := x s >>= fun
-    | .ok s a => return .ok s (f a)
-    | .error s e => return .error s e
-  seq f x s := f s >>= fun
-    | .ok s f => x () s >>= fun
-      | .ok s x => return .ok s (f x)
-      | .error s e => return .error s e
-    | .error s e => return .error s e
-  seqLeft x y s := x s >>= fun
-    | .ok s x => y () s >>= fun
-      | .ok s _ => return .ok s x
-      | .error s e => return .error s e
-    | .error s e => return .error s e
-  seqRight x y s := x s >>= fun
-    | .ok s _ => y () s >>= fun
-      | .ok s y => return .ok s y
-      | .error s e => return .error s e
-    | .error s e => return .error s e
+  pure x s pos := return .ok s pos x
+  bind x f s pos := x s pos >>= fun
+    | .ok s pos a => f a s pos
+    | .error s pos e => return .error s pos e
+  map f x s pos := x s pos >>= fun
+    | .ok s pos a => return .ok s pos (f a)
+    | .error s pos e => return .error s pos e
+  seq f x s pos := f s pos >>= fun
+    | .ok s pos f => x () s pos >>= fun
+      | .ok s pos x => return .ok s pos (f x)
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
+  seqLeft x y s pos := x s pos >>= fun
+    | .ok s pos x => y () s pos >>= fun
+      | .ok s pos _ => return .ok s pos x
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
+  seqRight x y s pos := x s pos >>= fun
+    | .ok s pos _ => y () s pos >>= fun
+      | .ok s pos y => return .ok s pos y
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   MonadExceptOf ε (ParserT ε σ τ m) where
-  throw e s := return .error s e
-  tryCatch p c s := p s >>= fun
-    | .ok s v => return .ok s v
-    | .error s e => (c e).run s
+  throw e s pos := return .error s pos e
+  tryCatch p c s pos := p s pos >>= fun
+    | .ok s pos v => return .ok s pos v
+    | .error s pos e => (c e).run s pos
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   OrElse (ParserT ε σ τ m α) where
-  orElse p q s :=
-    let savePos := Parser.Stream.getPosition s
-    p s >>= fun
-    | .ok s v => return .ok s v
-    | .error s _ => q () (Parser.Stream.setPosition s savePos)
-
+  orElse p q s pos :=
+    p s pos >>= fun
+    | .ok s pos v => return .ok s pos v
+    | .error s _ _ => q () s pos
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   MonadLift m (ParserT ε σ τ m) where
-  monadLift x s := (.ok s ·) <$> x
+  monadLift x s pos := (.ok s pos ·) <$> x
 
 /--
 `Parser ε σ τ` monad to parse tokens of type `τ` from the stream type `σ` with error type `ε`.
@@ -83,7 +82,7 @@ abbrev Parser (ε σ τ) [Parser.Stream σ τ] [Parser.Error ε σ τ] := Parser
 /-- Run parser `p` on input stream `s`. -/
 @[inline]
 protected def Parser.run {ε σ τ α} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : Parser ε σ τ α)
-  (s : σ) : Parser.Result ε σ α := p s
+  (s : σ) : Parser.Result ε σ α := p s (Stream.start s)
 
 /--
 `TrivialParserT σ τ` monad transformer to parse tokens of type `τ` from the stream `σ` with trivial
@@ -127,22 +126,17 @@ variable {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [M
 /-- Get parser stream. -/
 @[inline]
 def getStream : ParserT ε σ τ m σ :=
-  fun s => return .ok s s
-
-/-- Set parser stream. -/
-@[inline]
-def setStream (s : σ) : ParserT ε σ τ m PUnit :=
-  fun _ => return .ok s PUnit.unit
+  fun s pos => return .ok s pos s
 
 /-- Get stream position from parser. -/
 @[inline]
 def getPosition : ParserT ε σ τ m (Stream.Position σ) :=
-  Stream.getPosition <$> getStream
+  fun s pos => return .ok s pos pos
 
 /-- Set stream position from parser. -/
 @[inline]
 def setPosition (pos : Stream.Position σ) : ParserT ε σ τ m PUnit := do
-  setStream <| Stream.setPosition (← getStream) pos
+  fun s _ => return .ok s pos PUnit.unit
 
 /-- `withBacktracking p` parses `p` but does not consume any input on error. -/
 @[inline]
@@ -191,14 +185,13 @@ def withErrorMessage (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ
 
 @[specialize]
 private partial def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
-  (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ) :
-  m (Parser.Result ε σ (β × ε × Bool)) :=
-  let savePos := Stream.getPosition s
-  p s >>= fun
-    | .ok s x => f y x s >>= fun
-      | .ok s y => efoldlPAux f p y s
-      | .error s e => return .ok (Stream.setPosition s savePos) (y, e, true)
-    | .error s e => return .ok (Stream.setPosition s savePos) (y, e, false)
+    (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ)
+    (pos : Stream.Position σ ) : m (Parser.Result ε σ (β × ε × Bool)) :=
+  p s pos >>= fun
+    | .ok s pos' x => f y x s pos' >>= fun
+      | .ok s pos' y => efoldlPAux f p y s pos'
+      | .error s _ e => return .ok s pos (y, e, true)
+    | .error s _ e => return .ok s pos (y, e, false)
 
 /--
 `foldlP f init p` folds the parser function `f` from left to right using `init` as an intitial
@@ -216,7 +209,7 @@ def efoldlP (f : β → α → ParserT ε σ τ m β) (init : β) (p : ParserT 
   fun s =>
     have : Inhabited β := ⟨init⟩
     have : Inhabited σ := ⟨s⟩
-    have : Inhabited ε := ⟨Error.unexpected (Stream.getPosition s) none⟩
+    have : Inhabited ε := ⟨Error.unexpected (Stream.start s) none⟩
     efoldlPAux f p init s
 
 /--
@@ -276,11 +269,10 @@ This parser never fails.
 -/
 @[specialize]
 def eoption (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Sum α ε) :=
-  fun s =>
-    let savePos := Stream.getPosition s
-    p s >>= fun
-    | .ok s x => return .ok s (.inl x)
-    | .error s e => return .ok (Stream.setPosition s savePos) (.inr e)
+  fun s pos =>
+    p s pos >>= fun
+    | .ok s pos x => return .ok s pos (.inl x)
+    | .error s _ e => return .ok s pos (.inr e)
 
 /--
 `optionM p` tries to parse `p` (with backtracking) and returns `x` if `p` returns `x`, returns the
@@ -357,11 +349,9 @@ def first (ps : List (ParserT ε σ τ m α)) (combine : ε → ε → ε := fun
   go ps (Error.unexpected (← getPosition) none)
 where
   go : List (ParserT ε σ τ m α) → ε → ParserT ε σ τ m α
-    | [], e, s => return .error s e
-    | p :: ps, e, s =>
-      let savePos := Stream.getPosition s
-      p s >>= fun
-      | .ok s v => return .ok s v
-      | .error s f => go ps (combine e f) (Stream.setPosition s savePos)
-
+    | [], e, s, pos => return .error s pos e
+    | p :: ps, e, s, pos =>
+      p s pos >>= fun
+      | .ok s pos v => return .ok s pos v
+      | .error s _ f => go ps (combine e f) s pos
 end Parser

Parser/RegEx/Compile.lean

@@ -171,8 +171,8 @@ end
 /-- Compiles a regex from a string, returns `none` on faiure -/
 protected def compile? (s : String) : Option (RegEx Char) :=
   match Parser.run (re0 <* endOfInput) s with
-  | .ok _ r => some r
-  | .error _ _ => none
+  | .ok _ _ r => some r
+  | .error _ _ _ => none
 
 /-- Compiles a regex from a string, panics on faiure -/
 protected def compile! (s : String) : RegEx Char :=