refactor(library/init/lean/parser): minimize parser_state, have the module coroutine take and return parser_config

library/init/lean/parser/basic.lean

@@ -38,10 +38,10 @@ structure token_config :=
 (suffix_parser : option (parsec' (source_info → syntax)) := none)
 
 structure parser_state :=
-(tokens : trie token_config)
 (messages : message_log)
 
 structure parser_config :=
+(tokens : trie token_config)
 (filename : string)
 
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except]
@@ -112,7 +112,7 @@ def log_message {μ : Type} [monad m] [monad_reader parser_config m] [monad_stat
 do cfg ← read,
    modify (λ st, {st with messages := st.messages.add (message_of_parsec_message cfg msg)})
 
-def mk_parser_state (tokens : list token_config) : except string parser_state :=
+def mk_token_trie (tokens : list token_config) : except string (trie token_config) :=
 do -- the only hardcoded tokens, because they are never directly mentioned by a `parser`
    let builtin_tokens : list token_config := [{«prefix» := "/-"}, {«prefix» := "--"}],
    t ← (builtin_tokens ++ tokens).mfoldl (λ (t : trie token_config) tk,
@@ -125,7 +125,7 @@ do -- the only hardcoded tokens, because they are never directly mentioned by a
          to_string l ++ " and " ++ to_string l')
      | none := pure $ t.insert tk.prefix tk)
      trie.mk,
-   pure ⟨t, message_log.empty⟩
+   pure t
 
 structure parse.view_ty :=
 (root : syntax)

library/init/lean/parser/module.lean

@@ -11,6 +11,7 @@ import init.control.coroutine
 
 namespace lean
 namespace parser
+
 open combinators monad_parsec coroutine
 open parser.has_tokens parser.has_view
 
@@ -21,22 +22,24 @@ local postfix +:10000 := combinators.many1
 structure module_parser_output :=
 (cmd : syntax)
 (messages : message_log)
+(cfg : parser_config)
 
-section
-local attribute [reducible] parser_t
+-- NOTE: missing the `reader_t` from `parser_t` because the `coroutine` already provides `monad_reader parser_config`
 @[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_coroutine]
-def module_parser_m := parser_t (coroutine unit module_parser_output)
-end
+def module_parser_m := state_t parser_state $ parsec_t syntax $ coroutine parser_config module_parser_output
 abbreviation module_parser := module_parser_m syntax
 
 instance module_parser_m.lift_basic_parser_m : monad_basic_read module_parser_m :=
-{ monad_lift := λ α x r st it, pure (((x.run r).run st) it) }
+{ monad_lift := λ α x st it, do
+    cfg ← read,
+    pure (((x.run cfg).run st) it) }
 
 namespace module
 def yield_command (cmd : syntax) : module_parser_m unit :=
 do st ← get,
-   yield {cmd := cmd, messages := st.messages},
-   modify $ λ st, {st with messages := message_log.empty}
+   cfg ← read,
+   yield {cmd := cmd, messages := st.messages, cfg := cfg},
+   put {st with messages := message_log.empty}
 
 @[derive parser.has_view parser.has_tokens]
 def prelude.parser : basic_parser :=

library/init/lean/parser/pratt.lean

@@ -12,18 +12,19 @@ namespace lean.parser
 open monad_parsec combinators
 
 variables {base_m : Type → Type}
-variables [monad base_m] [monad_basic_read base_m] [monad_state parser_state base_m] [monad_parsec syntax base_m]
+variables [monad base_m] [monad_basic_read base_m] [monad_state parser_state base_m] [monad_parsec syntax base_m] [monad_reader parser_config base_m]
 
 local notation `m` := rec_t nat syntax base_m
 local notation `parser` := m syntax
 
 def curr_lbp : m nat :=
 do st ← get,
+   -- suppress error messages
    except.ok tk ← (monad_lift $ observing $ lookahead token) <* put st | pure 0 <* put st,
    match tk with
    | syntax.atom ⟨_, sym⟩ := do
-     st ← get,
-     some ⟨_, tk_cfg⟩ ← pure (st.tokens.match_prefix sym.mk_iterator) | error "curr_lbp: unreachable",
+     cfg ← read,
+     some ⟨_, tk_cfg⟩ ← pure (cfg.tokens.match_prefix sym.mk_iterator) | error "curr_lbp: unreachable",
      pure tk_cfg.lbp
    | syntax.node ⟨@number, _⟩ := pure max_prec
    | syntax.node ⟨@ident, _⟩ := pure max_prec

library/init/lean/parser/token.lean

@@ -20,9 +20,9 @@ namespace parser
 open monad_parsec combinators string has_view
 
 def match_token : basic_parser_m (option token_config) :=
-do st ← get,
+do cfg ← read,
    it ← left_over,
-   pure $ prod.snd <$> st.tokens.match_prefix it
+   pure $ prod.snd <$> cfg.tokens.match_prefix it
 
 private def finish_comment_block_aux : nat → nat → basic_parser_m unit
 | nesting (n+1) :=

tests/lean/parser1.lean

@@ -25,8 +25,9 @@ match msgs with
   io.println (to_string stx)
 
 def parse_module (s : string) : except string (list module_parser_output) :=
-do st ← parser.mk_parser_state (parser.tokens module.parser),
-   (outputs, sum.inl (), ⟨[]⟩) ← pure $ coroutine.finish (λ cmd, ()) (parser.run ⟨"<unknown>"⟩ st s module.parser) ()
+do t ← parser.mk_token_trie (parser.tokens module.parser),
+   (outputs, except.ok ((), ⟨⟨[]⟩⟩)) ← pure $ coroutine.finish (λ out : module_parser_output, out.cfg)
+     ((module.parser.run ⟨message_log.empty⟩).parse s) {filename := "<unknown", tokens := t}
      | except.error "final parser output should be empty!",
    pure outputs
 
@@ -75,9 +76,10 @@ universes u v
 #eval (do {
   s ← io.fs.read_file "../../library/init/core.lean",
   let s := (s.mk_iterator.nextn 6500).prev_to_string,
-  st ← monad_except.lift_except $ parser.mk_parser_state (tokens module.parser),
-  let k := parser.run ⟨"init/core.lean"⟩ st s module.parser,
-  outs ← io.prim.iterate_eio (k, ([] : list module_parser_output)) $ λ ⟨k, outs⟩, match k.resume () with
+  t ← monad_except.lift_except $ parser.mk_token_trie (tokens module.parser),
+  let k := (module.parser.run ⟨message_log.empty⟩).parse s,
+  let cfg : parser_config := {filename := "init/core.lean", tokens := t},
+  outs ← io.prim.iterate_eio (k, cfg, ([] : list module_parser_output)) $ λ ⟨k, cfg, outs⟩, match k.resume cfg with
     | coroutine_result_core.done p := pure (sum.inr outs.reverse)
     | coroutine_result_core.yielded out k := do {
       match out.messages.to_list with
@@ -90,7 +92,7 @@ universes u v
         io.println (to_string out.cmd)-/
       },
       match (expand out.cmd).run {filename := "init/core.lean"} with
-      | except.ok cmd' := pure (sum.inl (k, out :: outs))
+      | except.ok cmd' := pure (sum.inl (k, out.cfg, out :: outs))
       | except.error e := throw e.text
     },
   check_reprint outs s,