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

@@ -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
   },

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
 

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 [] <missing>) <missing>]) (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 [] <missing>) <missing>])
+   <missing>])
  (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 <missing> <missing> <missing> <missing> <missing>)
    <missing>])
@@ -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