From 211ade78283b4f7b9fa0cbcb46fac9628ced2df8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 9 Apr 2022 17:27:06 +0200 Subject: [PATCH 1/3] feat: doc strings in ctors and structure fields --- DocGen4/Process.lean | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 6de8304..4fd0c85 100644 --- a/DocGen4/Process.lean +++ b/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 (_, fields) := dropArgs field_function (ctor.numFields - parents) - let mut field_infos := #[] + let (fieldFunction, params) := dropArgs type (ctor.numParams + parents) + let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents) + let mut fieldInfos := #[] for (name, type) in fields do - field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type} - pure $ field_infos + fieldInfos := fieldInfos.push $ ←NameInfo.ofTypedName (struct.append name) type + 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 From 89dd2fa46e7aaad82ba2394881de41ef052d0992 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 9 Apr 2022 19:18:21 +0200 Subject: [PATCH 2/3] chore: upgrade compiler version --- DocGen4/Output/Base.lean | 4 ++-- DocGen4/Output/DocString.lean | 2 +- DocGen4/ToHtmlFormat.lean | 8 ++++---- lakefile.lean | 2 +- lean-toolchain | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 60923d2..4aef3b9 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -66,10 +66,10 @@ 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 + s := s.trimRight (front, s, back) partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 32fe1af..d729d38 100644 --- a/DocGen4/Output/DocString.lean +++ b/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 diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index 64e9b6a..c8f83d1 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/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 jsxAttrVal := strLit <|> group("{" term "}") +syntax jsxAttrName := ident <|> str +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))) diff --git a/lakefile.lean b/lakefile.lean index d18d59c..d7d73b6 100644 --- a/lakefile.lean +++ b/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" } ] } diff --git a/lean-toolchain b/lean-toolchain index 8e380ba..4b053c2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-03-06 +leanprover/lean4:nightly-2022-04-04 From a7c00d95e603eae0c6b0f4470e2e75208fad5f6b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 9 Apr 2022 21:39:34 +0200 Subject: [PATCH 3/3] feat: Render doc comments for structure fields --- DocGen4/Output/Structure.lean | 13 ++++++++++++- static/style.css | 7 ++++++- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index fb6105d..8bc03e5 100644 --- a/DocGen4/Output/Structure.lean +++ b/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
  • {s!"{shortName} "} : [←infoFormatToHtml f.type]
    • + if let some doc := f.doc then + let renderedDoc ← docStringToHtml doc + pure +
  • +
    [renderedDoc]
    +
    {s!"{shortName} "} : [←infoFormatToHtml f.type]
    +
    • + else + pure +
  • +
    {s!"{shortName} "} : [←infoFormatToHtml f.type]
    +
    • def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do let structureHtml := diff --git a/static/style.css b/static/style.css index d056b40..b6d7f34 100644 --- a/static/style.css +++ b/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;