perf(library/init/lean/parser): move backtrackable state from parser_core_t to module_parser_m

library/init/lean/parser/basic.lean

@@ -64,7 +64,7 @@ structure parser_config :=
 
 @[derive monad alternative monad_state monad_parsec monad_except]
 def parser_core_t (m : Type → Type) [monad m] :=
-state_t parser_state $ parsec_t syntax $ state_t parser_cache $ m
+parsec_t syntax $ state_t parser_cache $ m
 
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except]
 def parser_t (ρ : Type) (m : Type → Type) [monad m] := reader_t ρ $ parser_core_t m
@@ -120,9 +120,9 @@ def message_of_parsec_message {μ : Type} (cfg : parser_config) (msg : parsec.me
 {filename := cfg.filename, pos := ⟨0, 0⟩, text := to_string msg}
 
 /-- Run parser stack, returning a partial syntax tree in case of a fatal error -/
-protected def run {m : Type → Type} {α ρ : Type} [monad m] [has_coe_t ρ parser_config] (cfg : ρ) (s : string) (r : parser_t ρ m α) :
+protected def run {m : Type → Type} {α ρ : Type} [monad m] [has_coe_t ρ parser_config] (cfg : ρ) (s : string) (r : state_t parser_state (parser_t ρ m) α) :
 m (sum α syntax × message_log) :=
-do (r, _) ← (((r.run cfg).run {messages:=message_log.empty}).parse s).run {},
+do (r, _) ← (((r.run {messages:=message_log.empty}).run cfg).parse s).run {},
 pure $ match r with
 | except.ok (a, st) := (sum.inl a, st.messages)
 | except.error msg  := (sum.inr msg.custom.get, message_log.empty.add (message_of_parsec_message cfg msg))

library/init/lean/parser/module.lean

@@ -36,7 +36,7 @@ local attribute [reducible] parser_core_t
 /- NOTE: missing the `reader_t` from `parser_t` because the `coroutine` already provides
    `monad_reader module_parser_config`. -/
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_coroutine]
-def module_parser_m := parser_core_t $ coroutine module_parser_config module_parser_output
+def module_parser_m := state_t parser_state $ parser_core_t $ coroutine module_parser_config module_parser_output
 abbreviation module_parser := module_parser_m syntax
 end
 
@@ -44,7 +44,7 @@ instance module_parser_m.lift_parser_t (ρ : Type) [has_lift_t module_parser_con
   has_monad_lift (parser_t ρ id) module_parser_m :=
 { monad_lift := λ α x st it nb_st, do
     cfg ← read,
-    pure ((((x.run ↑cfg).run st) it).run nb_st) }
+    pure (((((λ a, (a, st)) <$> x).run ↑cfg) it).run nb_st) }
 
 section
 local attribute [reducible] basic_parser_m

library/init/lean/parser/token.lean

@@ -192,8 +192,7 @@ do it ← left_over,
    )
 
 def peek_token : basic_parser_m (except (parsec.message syntax) syntax) :=
-do st ← get,
-   observing (try (lookahead token)) <* put st
+observing (try (lookahead token))
 
 variable [monad_basic_parser m]
 

tests/lean/parser1.lean

@@ -42,7 +42,7 @@ do t ← parser.mk_token_trie $
 def parse_module (s : string) : except string (list module_parser_output) :=
 do cfg ← mk_config,
    (outputs, sum.inl (), ⟨[]⟩) ← pure $ coroutine.finish (λ_, cfg)
-     (parser.run cfg s (λ _, module.parser)) cfg
+     (parser.run cfg s (λ st _, module.parser.run st)) cfg
      | except.error "final parser output should be empty!",
    pure outputs
 
@@ -89,7 +89,7 @@ universes u v
 
 def run_frontend (input : string) : except_t string io unit := do
   parser_cfg ← monad_except.lift_except $ mk_config,
-  let parser_k := parser.run parser_cfg input (λ _, module.parser),
+  let parser_k := parser.run parser_cfg input (λ st _, module.parser st),
   let elab_k := elaborator.run {filename := "foo", initial_parser_cfg := parser_cfg},
   outs ← io.prim.iterate_eio (parser_k, elab_k, parser_cfg, ([] : list module_parser_output)) $ λ ⟨parser_k, elab_k, parser_cfg, outs⟩, match parser_k.resume parser_cfg with
     | coroutine_result_core.done p := do {