diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 1d3fbe0f6d..c3903ecd19 100644 --- a/library/init/lean/parser/basic.lean +++ b/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) diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index 3431b96fc6..a73aff38fd 100644 --- a/library/init/lean/parser/module.lean +++ b/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 := diff --git a/library/init/lean/parser/pratt.lean b/library/init/lean/parser/pratt.lean index c61d25a1e4..086886cf94 100644 --- a/library/init/lean/parser/pratt.lean +++ b/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 diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 29d5161925..2d9da3fe43 100644 --- a/library/init/lean/parser/token.lean +++ b/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) := diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 7fd5b94a47..d555d1c197 100644 --- a/tests/lean/parser1.lean +++ b/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 ⟨""⟩ 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 := "