From 07901fcfcb64e31c5eae0bfb0ddc86e262437b62 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 26 Sep 2018 13:17:10 -0700 Subject: [PATCH] refactor(library/init/lean/parser/module): put prelude and imports into non-optional `header` parser to make the life of the elaborator and other consumers a bit easier --- library/init/lean/parser/module.lean | 22 +++++++------ tests/lean/parser1.lean | 2 +- tests/lean/parser1.lean.expected.out | 49 ++++++++++++++++++---------- 3 files changed, 45 insertions(+), 28 deletions(-) diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index bce27b375e..3431b96fc6 100644 --- a/library/init/lean/parser/module.lean +++ b/library/init/lean/parser/module.lean @@ -32,26 +32,31 @@ 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) } +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} @[derive parser.has_view parser.has_tokens] -def prelude.parser : module_parser := +def prelude.parser : basic_parser := node! «prelude» ["prelude"] @[derive parser.has_view parser.has_tokens] -def import_path.parser : module_parser := +def import_path.parser : basic_parser := -- use `raw` to ignore registered tokens like ".." node! import_path [ dirups: (raw $ ch '.')*, module: ident.parser] @[derive parser.has_view parser.has_tokens] -def import.parser : module_parser := +def import.parser : basic_parser := node! «import» ["import", imports: import_path.parser+] +@[derive parser.has_view parser.has_tokens] +def header.parser : basic_parser := +node! «header» [«prelude»: prelude.parser?, imports: import.parser*] + /-- Read commands, recovering from errors inside commands (attach partial syntax tree) as well as unknown commands (skip input). -/ private def commands_aux : bool → nat → module_parser_m unit @@ -89,21 +94,18 @@ instance commands.parser.has_view : has_view commands.parser (list syntax) := {..many.view command.parser} def eoi : syntax_node_kind := ⟨`lean.parser.eoi⟩ +end module +open module def module.parser : module_parser_m unit := do catch (do -- `token` assumes that there is no leading whitespace monad_lift whitespace, - pre ← _root_.optional prelude.parser, - match pre with - | some pre := yield_command pre - | none := pure (), - imports ← monad_parsec.many import.parser, - imports.mmap yield_command, + monad_lift header.parser >>= yield_command, commands.parser, monad_parsec.eoi ) $ λ msg, do { - -- fatal error (should only come from import.parser or eoi), yield partial syntax tree and stop + -- fatal error (should only come from header.parser or eoi), yield partial syntax tree and stop log_message msg, yield_command msg.custom }, diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 512c87a100..7fd5b94a47 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -67,7 +67,7 @@ universes u v #eval show_parse "#check Type max u v" #eval do - [nota, eoi] ← parse_module "infixl `+`:65 := nat.add" | throw "huh", + [header, nota, eoi] ← parse_module "infixl `+`:65 := nat.add" | throw "huh", except.ok cmd' ← pure $ (expand nota.cmd).run {filename := "init/core.lean"} | throw "heh", pure cmd'.reprint diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index 6edf326577..e3d5a01890 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/tests/lean/parser1.lean.expected.out @@ -1,28 +1,38 @@ result: -[(prelude "prelude") (eoi "")] +[(module.header [(module.prelude "prelude")] []) (eoi "")] result: -[(import "import" [(import_path [] `me)]) (eoi "")] +[(module.header [] [(module.import "import" [(module.import_path [] `me)])]) + (eoi "")] error at line 1, column 0: expected command partial syntax tree: -[(eoi "")] +[(module.header [] []) (eoi "")] error at line 1, column 6: unexpected end of file expected identifier partial syntax tree: -[(import "import" [(import_path [] ) ]) (eoi "")] -result: -[(prelude "prelude") - (import "import" [(import_path ["." "."] `a) (import_path [] `b)]) - (import "import" [(import_path [] `c)]) +[(module.header + [] + [(module.import "import" [(module.import_path [] ) ]) + ]) (eoi "")] result: -[(command.open +[(module.header + [(module.prelude "prelude")] + [(module.import + "import" + [(module.import_path ["." "."] `a) (module.import_path [] `b)]) + (module.import "import" [(module.import_path [] `c)])]) + (eoi "")] +result: +[(module.header [] []) + (command.open "open" [(command.open_spec `me [] [] [] []) (command.open_spec `you [] [] [] [])]) (eoi "")] result: -[(command.open +[(module.header [] []) + (command.open "open" [(command.open_spec `me @@ -38,7 +48,8 @@ result: error at line 1, column 11: expected command partial syntax tree: -[(command.open +[(module.header [] []) + (command.open "open" [(command.open_spec `me [] [] [] []) (command.open_spec `you [] [] [] [])]) (eoi "")] @@ -48,7 +59,8 @@ error at line 1, column 9: unexpected end of file expected identifier partial syntax tree: -[(command.open +[(module.header [] []) + (command.open "open" [(command.open_spec ) ]) @@ -60,11 +72,13 @@ partial syntax tree: error at line 1, column 8: expected command partial syntax tree: -[(command.open "open" [(command.open_spec `me [] [] [] [])]) +[(module.header [] []) + (command.open "open" [(command.open_spec `me [] [] [] [])]) (command.open "open" [(command.open_spec `you [] [] [] [])]) (eoi "")] result: -[(command.open "open" [(command.open_spec `a [] [] [] [])]) +[(module.header [] []) + (command.open "open" [(command.open_spec `a [] [] [] [])]) (command.section "section" [`b] @@ -79,10 +93,11 @@ result: [`b]) (eoi "")] result: -[(command.section "section" [`a] [] "end" []) (eoi "")] +[(module.header [] []) (command.section "section" [`a] [] "end" []) (eoi "")] Type (max u v) : Type ((max u v)+1) result: -[(command.check +[(module.header [] []) + (command.check "#check" (term.app (term.app @@ -103,7 +118,7 @@ error at line 229, column 12: unexpected '▸' expected ":=" result: -[(prelude "prelude") +[(module.header [(module.prelude "prelude")] []) (command.notation "notation" (command.notation_spec