Merge pull request #49 from leanprover/ctor-field-docs

Structure field doc strings

DocGen4/Output/Base.lean

@@ -66,7 +66,7 @@ def declNameToLink (name : Name) : HtmlM String := do
   pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
 
 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
-  let front := "".pushn ' ' (s.find (!Char.isWhitespace ·))
+  let front := "".pushn ' ' $ s.offsetOfPos (s.find (!Char.isWhitespace ·))
   let mut s := s.trimLeft
   let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
   s := s.trimRight

DocGen4/Output/DocString.lean

@@ -17,7 +17,7 @@ namespace Output
     let c := s.get i
     if p c then
       let i := s.next i
-      splitAroundAux s p i i (c.toString::s.extract b (i-1)::r)
+      splitAroundAux s p i i (c.toString::s.extract b (i-⟨1⟩)::r)
     else
       splitAroundAux s p b (s.next i) r
 

DocGen4/Output/Structure.lean

@@ -10,7 +10,18 @@ open Lean
 def fieldToHtml (f : NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
-  pure <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
+  if let some doc := f.doc then
+    let renderedDoc ← docStringToHtml doc
+    pure
+      <li id={name} «class»="structure_field">
+        <div «class»="structure_field_doc">[renderedDoc]</div>
+        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      </li>
+  else
+    pure
+      <li id={name} «class»="structure_field">
+        <div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
+      </li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
   let structureHtml :=

DocGen4/Process.lean

@@ -19,6 +19,7 @@ open Lean Meta PrettyPrinter Std Widget
 structure NameInfo where
   name  : Name
   type : CodeWithInfos
+  doc : Option String
   deriving Inhabited
 
 structure Arg where
@@ -28,7 +29,6 @@ structure Arg where
 
 structure Info extends NameInfo where
   args : Array Arg
-  doc : Option String
   declarationRange : DeclarationRange
   attrs : Array String
   deriving Inhabited
@@ -146,15 +146,19 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
   }
   pure $ tagExprInfos ctx infos tt
 
+def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
+  let env ← getEnv
+  pure { name := n, type := ←prettyPrintTerm t, doc := ←findDocString? env n}
+
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
   let (args, type) := typeToArgsType v.type
-  let type ← prettyPrintTerm type
   let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
   let doc ← findDocString? env v.name
+  let nameInfo ← NameInfo.ofTypedName v.name type
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
-  | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range (←getAllAttributes v.name)
+  | some range => pure $ Info.mk nameInfo args range.range (←getAllAttributes v.name)
   | none => panic! s!"{v.name} is a declaration without position"
 
 def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
@@ -228,16 +232,16 @@ def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
   else
     pure info
 
-def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
+def getConstructorType (ctor : Name) : MetaM Expr := do
   let env ← getEnv
   match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => prettyPrintTerm i.type
+  | some (ConstantInfo.ctorInfo i) => pure i.type
   | _ => panic! s!"Constructor {ctor} was requested but does not exist"
 
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let ctors ← v.ctors.mapM (λ name => do pure $ NameInfo.mk name (←getConstructorType name))
+  let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name))
   pure $ InductiveInfo.mk info ctors v.isUnsafe
 
 def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
@@ -251,25 +255,24 @@ def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
 
 def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
   let type := ctor.type
-  let (field_function, params) := dropArgs type (ctor.numParams + parents)
+  let (fieldFunction, params) := dropArgs type (ctor.numParams + parents)
-  let (_, fields) := dropArgs field_function (ctor.numFields - parents)
+  let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents)
-  let mut field_infos := #[]
+  let mut fieldInfos := #[]
   for (name, type) in fields do
-    field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
+    fieldInfos := fieldInfos.push $ ←NameInfo.ofTypedName (struct.append name) type
-  pure $ field_infos
+  pure $ fieldInfos
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
   let parents := getParentStructures env v.name
   let ctor := getStructureCtor env v.name
-  let ctorType ← prettyPrintTerm ctor.type
   match getStructureInfo? env v.name with
   | some i =>
     if i.fieldNames.size - parents.size > 0 then
-      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type)
     else
-      pure $ StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type)
   | none => panic! s!"{v.name} is not a structure"
 
 def getInstances (className : Name) : MetaM (Array Name) := do

DocGen4/ToHtmlFormat.lean

@@ -81,8 +81,8 @@ def jsxText : Parser :=
 @[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
 @[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
 
-syntax jsxAttrName := ident <|> strLit
+syntax jsxAttrName := ident <|> str
-syntax jsxAttrVal := strLit <|> group("{" term "}")
+syntax jsxAttrVal := str <|> group("{" term "}")
 syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
 syntax jsxAttrSpread := "[" term "]"
 syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
@@ -103,12 +103,12 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
     as ← match attr with
     | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
       let n ← match n with
-        | `(jsxAttrName| $n:strLit) => pure n
+        | `(jsxAttrName| $n:str) => pure n
         | `(jsxAttrName| $n:ident) => pure $ quote (toString n.getId)
         | _ => Macro.throwUnsupported
       let v ← match v with
         | `(jsxAttrVal| {$v}) => pure v
-        | `(jsxAttrVal| $v:strLit) => pure v
+        | `(jsxAttrVal| $v:str) => pure v
         | _ => Macro.throwUnsupported
       `(($as).push ($n, ($v : String)))
     | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))

lakefile.lean

@@ -19,7 +19,7 @@ package «doc-gen4» {
     },
     {
       name := `lake
-      src := Source.git "https://github.com/leanprover/lake" "9378575b5575f49a185d50130743a190a9be2f82"
+      src := Source.git "https://github.com/leanprover/lake" "d961d8cfaa1c354c10f3fed55b32de85c205f4ab"
     }
   ]
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-03-06
+leanprover/lean4:nightly-2022-04-04

static/style.css

@@ -460,7 +460,7 @@ main h2, main h3, main h4, main h5, main h6 {
     margin-left: 4ex; /* extra indentation */
 }
 
-.imports li, code, .decl_header, .attributes, .structure_field,
+.imports li, code, .decl_header, .attributes, .structure_field_info,
         .constructor, .instances li, .equation, #search_results div,
         .structure_ext_ctor {
     font-family: 'Source Code Pro', monospace;
@@ -491,6 +491,11 @@ pre code { padding: 0 0; }
     margin-left: 2ex;
 }
 
+.structure_field_doc {
+    text-indent: 0;
+    padding-top: 1ex;
+}
+
 .structure_ext_fields {
     display: block;
     padding-inline-start: 0;