feat: tools for documenting syntax

Begin the ability to give grammars of syntactic forms using antiquotations

Manual/Language.lean

@@ -216,12 +216,88 @@ If `B : Prop`, then the function type is itself a `Prop`; otherwise, the functio
 #### Universe Variable Bindings
 
 Universe-polymorphic definitions bind universe variables.
+These bindings may be either explicit or implicit.
+Explicit universe variable binding and instantiaion occurs as a suffix to the definition's name, as in the following declaration of `map`, which declares two universe parameters (`u` and `v`) and instantiates the polymorphic `List` with each in turn:
+```lean (keep := false)
+def map.{u} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β
+  | [] => []
+  | x :: xs => f x :: map f xs
+```
 
-:::TODO
- * `universe` command
- * exact rules for binding universe vars
+Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters:
+```lean (keep := false)
+def map.{u} {α : Type u} {β : Type v} (f : α → β) : List α → List β
+  | [] => []
+  | x :: xs => f x :: map f xs
+```
+
+When the {TODO}[describe this option and add xref] `autoImplicits` option is set, it is not necessary to explicitly bind universe variables:
+```lean (keep := false)
+set_option autoImplicit true
+def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
+  | [] => []
+  | x :: xs => f x :: map f xs
+```
+
+Without this setting, the definition is rejected because `u` and `v` are not in scope:
+```lean (error := true) (name := uv)
+set_option autoImplicit false
+def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
+  | [] => []
+  | x :: xs => f x :: map f xs
+```
+```leanOutput uv
+unknown universe level 'u'
+```
+```leanOutput uv
+unknown universe level 'v'
+```
+
+In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[scope] using the `universe` command.
+
+:::syntax Lean.Parser.Command.universe
+```grammar
+universe $x:ident $xs:ident*
+```
+
+Declares one or more universe variables for the extent of the current scope.
+
+Just as the `variable` command causes a particular identifier to be treated as a parameter with a paricular type, the `universe` command causes the subsequent identifiers to be treated consistently as universe parameters, even if they are not mentioned in a signature or if the option `autoImplicit` is {lean}`false`.
 :::
 
+When `u` is declared to be a universe variable, it can be used as a parameter.
+```lean
+set_option autoImplicit false
+universe u
+def id₃ (α : Type u) (a : α) := a
+```
+
+Because automatic implicit arguments only insert parameters that are used in the declaration's {tech}[header], universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declaread with `universe` even when `autoImplicit` is `true`.
+This definition with an explicit universe parameter is accepted:
+```lean (keep := false)
+def L.{u} := List (Type u)
+```
+Even with automatic implicits, this definition is rejected, because `u` is not mentioned in the header, which precedes the `:=`:
+```lean (error := true) (name := unknownUni) (keep := false)
+set_option autoImplicit true
+def L := List (Type u)
+```
+```leanOutput unknownUni
+unknown universe level 'u'
+```
+With a universe declaration, `u` is accepted as a parameter even on the right-hand side:
+```lean (keep := false)
+universe u
+def L := List (Type u)
+```
+The resulting definition of `L` is universe-polymorphic, with `u` inserted as a universe parameter.
+Declarations in the scope of a `universe` command are not made polymorphic if the universe variables do not occur in them or in other automatically-inserted arguments.
+```lean
+universe u
+def L := List (Type 0)
+#check L
+```
+
 #### Universe Unification
 
 :::TODO
@@ -230,3 +306,27 @@ Universe-polymorphic definitions bind universe variables.
 :::
 
 ## Inductive Types
+
+
+# Organizational Features
+
+## Commands and Declarations
+
+### Headers
+
+The {deftech}[_header_] of a definition or declaration specifies the signature of the new constant that is defined.
+
+::: TODO
+* Precision and examples; list all of them here
+* Mention interaction with autoimplicits
+:::
+
+## Scopes
+%%%
+tag := "scopes"
+%%%
+
+::: TODO
+ * Many commands have an effect for the current {deftech}[_scope_]
+ * A scope ends when a namespace ends, a section ends, or a file ends
+:::

Manual/Meta.lean

@@ -10,7 +10,9 @@ import Verso.Code
 import SubVerso.Highlighting
 import SubVerso.Examples
 
+import Manual.Meta.Basic
 import Manual.Meta.Figure
+import Manual.Meta.Syntax
 
 open Lean Elab
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
@@ -27,24 +29,35 @@ def comment : DirectiveExpander
 def Block.TODO : Block where
   name := `Manual.TODO
 
+def Inline.TODO : Inline where
+  name := `Manual.TODO
+
 @[directive_expander TODO]
 def TODO : DirectiveExpander
   | args, blocks => do
     ArgParse.done.run args
     let content ← blocks.mapM elabBlock
     pure #[← `(Doc.Block.other Block.TODO #[$content,*])]
 
+@[role_expander TODO]
+def TODOinline : RoleExpander
+  | args, inlines => do
+    ArgParse.done.run args
+    let content ← inlines.mapM elabInline
+    pure #[← `(Doc.Inline.other Inline.TODO #[$content,*])]
+
+
 @[block_extension TODO]
 def TODO.descr : BlockDescr where
   traverse _ _ _ := do
     pure none
   toTeX := none
   extraCss := [r#"
-.TODO {
+div.TODO {
   border: 5px solid red;
   position: relative;
 }
-.TODO::before {
+div.TODO::before {
   content: "TODO";
   position: absolute;
   top: 0;
@@ -60,24 +73,35 @@ def TODO.descr : BlockDescr where
     some <| fun _ goB _ _ content => do
       pure {{<div class="TODO">{{← content.mapM goB}}</div>}}
 
+@[inline_extension TODO]
+def TODO.inlineDescr : InlineDescr where
+  traverse _ _ _ := do
+    pure none
+  toTeX := none
+  extraCss := [r#"
+span.TODO {
+  border: 3px solid red;
+  display: inline;
+  position: relative;
+  float: right;
+  width: 15vw;
+  margin-right: -17vw;
+  color: red;
+  font-size: large;
+  font-weight: bold;
+}
+"#]
+  toHtml :=
+    open Verso.Output.Html in
+    some <| fun go _ _ content => do
+      pure {{<span class="TODO">{{← content.mapM go}}</span>}}
+
+
 @[role_expander versionString]
 def versionString : RoleExpander
   | #[], #[] => do pure #[← ``(Verso.Doc.Inline.text $(quote Lean.versionString))]
   | _, _ => throwError "Unexpected arguments"
 
-def parserInputString [Monad m] [MonadFileMap m] (str : TSyntax `str) : m String := do
-  let preString := (← getFileMap).source.extract 0 (str.raw.getPos?.getD 0)
-  let mut code := ""
-  let mut iter := preString.iter
-  while !iter.atEnd do
-    if iter.curr == '\n' then code := code.push '\n'
-    else
-      for _ in [0:iter.curr.utf8Size] do
-        code := code.push ' '
-    iter := iter.next
-  code := code ++ str.getString
-  return code
-
 initialize leanOutputs : EnvExtension (NameMap (List (MessageSeverity × String))) ←
   registerEnvExtension (pure {})
 
@@ -131,6 +155,19 @@ def lean : CodeBlockExpander
       for t in cmdState.infoState.trees do
         pushInfoTree t
 
+
+      let mut hls := Highlighted.empty
+      for cmd in cmds do
+        hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees)
+
+      if config.show.getD true then
+        pure #[← `(Block.other {Block.lean with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])]
+      else
+        pure #[]
+    finally
+      if !config.keep.getD true then
+        setEnv origEnv
+
       if let some name := config.name then
         let msgs ← cmdState.messages.toList.mapM fun msg => do
 
@@ -155,17 +192,6 @@ def lean : CodeBlockExpander
           logMessage msg
         if cmdState.messages.hasErrors then
           throwErrorAt str "No error expected in code block, one occurred"
-
-      let mut hls := Highlighted.empty
-      for cmd in cmds do
-        hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees)
-
-      if config.show.getD true then
-        pure #[← `(Block.other {Block.lean with data := ToJson.toJson $(quote hls)} #[Block.code $(quote str.getString)])]
-      else
-        pure #[]
-    finally
-      if !config.keep.getD true then setEnv origEnv
 where
   withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
 
@@ -394,25 +420,6 @@ def syntaxError : CodeBlockExpander
         (.error, mkErrorStringWithPos  "<example>" pos msg)
       modifyEnv (leanOutputs.modifyState · (·.insert config.name msgs))
       return #[← `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)])]
-where
-  toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do
-    let mut errs := []
-    for (pos, _stk, err) in s.allErrors do
-      let pos := ctx.fileMap.toPosition pos
-      errs := (pos, toString err) :: errs
-    errs.reverse
-
-  runParserCategory (env : Environment) (opts : Lean.Options) (catName : Name) (input : String) : Except (List (Position × String)) Syntax :=
-    let fileName := "<example>"
-    let p := andthenFn whitespace (categoryParserFnImpl catName)
-    let ictx := mkInputContext input fileName
-    let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
-    if !s.allErrors.isEmpty  then
-      Except.error (toErrorMsg ictx s)
-    else if ictx.input.atEnd s.pos then
-      Except.ok s.stxStack.back
-    else
-      Except.error (toErrorMsg ictx (s.mkError "end of input"))
 
 @[block_extension syntaxError]
 def syntaxError.descr : BlockDescr where

Manual/Meta/Basic.lean

@@ -0,0 +1,56 @@
+import Lean.Data.Position
+import Lean.Parser
+
+open Lean
+
+namespace Manual
+
+def parserInputString [Monad m] [MonadFileMap m] (str : TSyntax `str) : m String := do
+  let preString := (← getFileMap).source.extract 0 (str.raw.getPos?.getD 0)
+  let mut code := ""
+  let mut iter := preString.iter
+  while !iter.atEnd do
+    if iter.curr == '\n' then code := code.push '\n'
+    else
+      for _ in [0:iter.curr.utf8Size] do
+        code := code.push ' '
+    iter := iter.next
+  code := code ++ str.getString
+  return code
+
+open Lean.Parser in
+def runParserCategory (env : Environment) (opts : Lean.Options) (catName : Name) (input : String) (fileName : String := "<example>") : Except (List (Position × String)) Syntax :=
+    let p := andthenFn whitespace (categoryParserFnImpl catName)
+    let ictx := mkInputContext input fileName
+    let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
+    if !s.allErrors.isEmpty  then
+      Except.error (toErrorMsg ictx s)
+    else if ictx.input.atEnd s.pos then
+      Except.ok s.stxStack.back
+    else
+      Except.error (toErrorMsg ictx (s.mkError "end of input"))
+where
+  toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do
+    let mut errs := []
+    for (pos, _stk, err) in s.allErrors do
+      let pos := ctx.fileMap.toPosition pos
+      errs := (pos, toString err) :: errs
+    errs.reverse
+
+open Lean.Parser in
+def runParser (env : Environment) (opts : Lean.Options) (p : Parser) (input : String) (fileName : String := "<example>") : Except (List (Position × String)) Syntax :=
+    let ictx := mkInputContext input fileName
+    let s := p.fn.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
+    if !s.allErrors.isEmpty  then
+      Except.error (toErrorMsg ictx s)
+    else if ictx.input.atEnd s.pos then
+      Except.ok s.stxStack.back
+    else
+      Except.error (toErrorMsg ictx (s.mkError "end of input"))
+where
+  toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do
+    let mut errs := []
+    for (pos, _stk, err) in s.allErrors do
+      let pos := ctx.fileMap.toPosition pos
+      errs := (pos, toString err) :: errs
+    errs.reverse