feat: describe module headers

Manual/Language/Files.lean

@@ -133,10 +133,88 @@ Contexts in which keywords may be used as identifiers without guillemets, such a
 Identifiers that contain one or more `'.'` characters, and thus consist of more than one identifier component, are called {deftech}[hierarchical identifiers].
 Hierarchical identifiers are used to represent both module names and names in a namespace.
 
+## Structure
+
+
+
+:::syntax Lean.Parser.Module.module (open := false)
+```grammar
+$hdr:header $cmd:command*
+```
+
+A module consists of a {deftech}_module header_ followed by a sequence of {deftech}_commands_.
+
+:::
+
+
+### Module Headers
+
+The module header consists of a sequence of {deftech}[`import` statements].
+
+:::syntax Lean.Parser.Module.header (open := false)
+```grammar
+$i:import*
+```
+
+An optional keyword `prelude`, for use in Lean's implementation, is also allowed:
+
+```grammar
+prelude $«import»*
+```
+:::
+
+
+:::syntax Lean.Parser.Module.prelude (open := false)
+```grammar
+prelude
+```
+
+The `prelude` keyword indicates that the module is part of the implementation of the Lean {deftech}_prelude_, which is the code that is available without explicitly importing any modules—it should not be used outside of Lean's implementation.
+:::
+
+:::syntax Lean.Parser.Module.import
+```grammar
+import $mod:ident
+```
+
+Imports the module.
+Importing a module makes its contents available in the current module, as well as those from modules transitively imported by its imports.
+
+Modules do not necessarily correspond to namespaces.
+Modules may add names to any namespace, and importing a module has no effect on the set of currently open namespaces.
+
+The imported module name is translated to a filename by replacing dots (`'.'`) in its name with directory separators.
+Lean searches its include path for the corresponding importable module file.
+:::
+
+### Commands
+
+{tech}[Commands] are top-level statements in Lean.
+Some examples are inductive type declarations, theorems, function definitions, namespace modifiers like `open` or `variable`, and interactive queries such as `#check`.
+The syntax of commands is user-extensible.
+Specific Lean commands are documented in the corresponding chapters of this manual, rather than being listed here.
+
+::: TODO
+Make the index include links to all commands, then xref from here
+:::
+
+## Contents
+
+A module includes an {TODO}[def and xref] environment, which includes both the datatype and constant definitions from an environment and any data stored in {TODO}[xref] its environment extensions.
+As the module is processed by Lean, commands add content to the environment.
+A module's environment can be serialized to a {deftech (key:="olean")}[`.olean` file], which contains both the environment and a compacted heap region with the run-time objects needed by the environment.
+This means that an imported module can be loaded without re-executing all of its commands.
+
 
 # Packages, Libraries, and Targets
 
 Lean code is organized into {deftech}_packages_, which are units of code distribution.
 A {tech}[package] may contain multiple libraries or executables.
 
 Code in a package that is intended for use by other Lean packages is organized into {deftech (key:="library")}[libraries].
+Code that is intended to be compiled and run as independent programs is organized into {deftech (key:="executable")}[executables].
+Together, libraries and executables are referred to as {deftech}_targets_ in Lake, the standard Lean build tool. {TODO}[section xref]
+
+:::TODO
+Write Lake section, coordinate this content with it
+:::

Manual/Meta/Syntax.lean

@@ -20,36 +20,57 @@ def Block.syntax : Block where
 
 structure SyntaxConfig where
   name : Name
+  «open» : Bool := true
   aliases : List Name
 
+
 partial def many [Inhabited (f (List α))] [Applicative f] [Alternative f] (x : f α) : f (List α) :=
   ((· :: ·) <$> x <*> many x) <|> pure []
 
 def SyntaxConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] : ArgParse m SyntaxConfig :=
-  SyntaxConfig.mk <$> .positional `name .name <*> (many (.named `alias .name false) <* .done)
+  SyntaxConfig.mk <$>
+    .positional `name .name <*>
+    ((·.getD true) <$> (.named `open .bool true)) <*>
+    (many (.named `alias .name false) <* .done)
 
 @[directive_expander «syntax»]
 partial def «syntax» : DirectiveExpander
   | args, blocks => do
     let config ← SyntaxConfig.parse.run args
-    let content ← blocks.mapM fun b => do
-      match b with
-      | `<low|(Verso.Syntax.codeblock (column ~col@(.atom _ _col)) ~«open» ~(.node i `null #[nameStx, .node _ `null argsStx]) ~str@(.atom info contents) ~close )> =>
-        if nameStx.getId == `grammar then elabGrammar config.name argsStx (Syntax.mkStrLit contents info) col «open» i info close
-        else elabBlock b
-      | _ => elabBlock b
+    let mut content := #[]
+    let mut firstGrammar := true
+    let productionCount := blocks.filterMap isGrammar? |>.size
+    for b in blocks do
+      match isGrammar? b with
+      | some (argsStx, contents, info, col, «open», i, close) =>
+        let grm ← elabGrammar config firstGrammar productionCount argsStx (Syntax.mkStrLit contents info) col «open» i info close
+        content := content.push grm
+        firstGrammar := false
+      | _ =>
+        content := content.push <| ← elabBlock b
     pure #[← `(Doc.Block.other Block.syntax #[$content,*])]
 where
+  isGrammar? : Syntax → Option (Array Syntax × String × SourceInfo × Syntax × Syntax × SourceInfo × Syntax)
+  | `<low|(Verso.Syntax.codeblock (column ~col@(.atom _ _col)) ~«open» ~(.node i `null #[nameStx, .node _ `null argsStx]) ~str@(.atom info contents) ~close )> =>
+    if nameStx.getId == `grammar then some (argsStx, contents, info, col, «open», i, close) else none
+  | _ => none
+
   antiquoteOf : Name → Option Name
   | .str n "antiquot" => pure n
   | _ => none
 
-  nonTerm (x : Name) : String := s!"⟨{x.toString.toUpper}⟩"
+  nonTerm : Name → String
+  | .str x "pseudo" => nonTerm x
+  | .str _ x => s!"⟨{x.toUpper}⟩"
+  | x => s!"⟨{x.toString.toUpper}⟩"
 
   production : Syntax → String
   | .atom _ str => s!"“{str}”"
   | .missing => "<missing>"
-  | .ident _ _ x _ => x.toString
+  | .ident _ _ x _ =>
+    match x with
+    | .str x' "pseudo" => x'.toString
+    | _ => x.toString
   | .node _ k args =>
     match k, antiquoteOf k, args with
     | `many.antiquot_suffix_splice, _, #[stx, star] => "{" ++ production stx ++ "}"
@@ -63,25 +84,28 @@ where
         if kind == k then return catName
     failure
 
-  elabGrammar name (argsStx : Array Syntax) (str : TSyntax `str) col «open» i info close := do
+  elabGrammar config isFirst howMany (argsStx : Array Syntax) (str : TSyntax `str) col «open» i info close := do
     let args ← parseArgs <| argsStx.map (⟨·⟩)
     let #[] := args
       | throwErrorAt str "Expected 0 arguments"
     let altStr ← parserInputString str
-    let p := andthen ⟨{}, whitespace⟩ <| andthen {fn := (fun _ => (·.pushSyntax (mkIdent name)))} (parserOfStack 0)
+    let p := andthen ⟨{}, whitespace⟩ <| andthen {fn := (fun _ => (·.pushSyntax (mkIdent config.name)))} (parserOfStack 0)
     match runParser (← getEnv) (← getOptions) p altStr (← getFileName) with
     | .ok stx =>
-      let mut bnf := s!"{nonTerm ((categoryOf (← getEnv) name).getD name)} ::="
-      bnf := bnf ++ " ...\n"
-      bnf := bnf ++ "  | " ++ production stx
+      let mut bnf := s!"{nonTerm ((categoryOf (← getEnv) config.name).getD config.name)} ::="
+      bnf := bnf ++ if config.open || (!config.open && !isFirst) then " ...\n" else if howMany = 1 then "" else "\n"
+      bnf := bnf ++ if !config.open && isFirst then
+          if howMany != 1 then "  " else " "
+        else "  | "
+      bnf := bnf ++ production stx
 
       elabBlock `<low|(Verso.Syntax.codeblock (column ~col) ~«open» ~(.node i `null #[]) ~(.atom info bnf) ~close)>
     | .error es =>
-      dbg_trace es.length
       for (pos, msg) in es do
         log (severity := .error) (mkErrorStringWithPos  "<example>" pos msg)
       `(asldfkj)
 
+
 @[block_extension «syntax»]
 def syntax.descr : BlockDescr where
   traverse _ _ _ := do

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "000647872db8486c7f520f3c411134a8a9c9868e",
+   "rev": "fdea7b9a3f525a632a7702edeb1c196f963f22d4",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",