From 365c77b4945505be1131026db1f015553094e00f Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 14 Nov 2024 05:12:46 -0800 Subject: [PATCH] feat: improvements to `structure` output (#232) - Now the precise list of parent structures is shown, now that Lean records this information. Closes #223 - Fixes an issue where fields of a structure wouldn't be shown. Closes #229 - Grays out inherited fields and gives them a link to their definitions. - Fixes an issue where inherited fields would have an id attribute with a synthetic name, which could cause links to go to the wrong place. Now inherited fields don't have an id attribute. --- DocGen4/Output/Structure.lean | 17 ++++++++----- DocGen4/Process/Base.lean | 4 ++- DocGen4/Process/DocInfo.lean | 14 +++-------- DocGen4/Process/StructureInfo.lean | 39 +++++++++++++----------------- static/style.css | 9 +++++++ 5 files changed, 44 insertions(+), 39 deletions(-) diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean index b8f0aa45..3b92af86 100644 --- a/DocGen4/Output/Structure.lean +++ b/DocGen4/Output/Structure.lean @@ -11,20 +11,25 @@ open Lean /-- Render a single field consisting of its documentation, its name and its type as HTML. -/ -def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do +def fieldToHtml (f : Process.FieldInfo) : HtmlM Html := do let shortName := f.name.componentsRev.head!.toString let name := f.name.toString - if let some doc := f.doc then - let renderedDoc ← docStringToHtml doc name + if f.isDirect then + let doc : Array HTML ← + if let some doc := f.doc then + let renderedDoc ← docStringToHtml doc name + pure #[
[renderedDoc]
] + else + pure #[] pure
  • {s!"{shortName} "} : [← infoFormatToHtml f.type]
    -
    [renderedDoc]
    + [doc]
    • else pure -
  • -
    {s!"{shortName} "} : [← infoFormatToHtml f.type]
    +
  • +
    {s!"{shortName}"}{" "}: [← infoFormatToHtml f.type]
    • /-- diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean index 101015c6..efa80ed0 100644 --- a/DocGen4/Process/Base.lean +++ b/DocGen4/Process/Base.lean @@ -27,6 +27,8 @@ structure NameInfo where doc : Option String deriving Inhabited +structure FieldInfo extends NameInfo where + isDirect : Bool /-- An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`. @@ -127,7 +129,7 @@ structure StructureInfo extends Info where /-- Information about all the fields of the structure. -/ - fieldInfo : Array NameInfo + fieldInfo : Array FieldInfo /-- All the structures this one inherited from. -/ diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean index 0dbc718d..0017e7e9 100644 --- a/DocGen4/Process/DocInfo.lean +++ b/DocGen4/Process/DocInfo.lean @@ -130,20 +130,14 @@ def isBlackListed (declName : Name) : MetaM Bool := do -- TODO: Evaluate whether filtering out declarations without range is sensible | none => return true --- TODO: Is this actually the best way? +/-- Returns `true` if `declName` is a field projection or a parent projection for a structure. -/ def isProjFn (declName : Name) : MetaM Bool := do let env ← getEnv match declName with | Name.str parent name => - if isStructure env parent then - match getStructureInfo? env parent with - | some i => - match i.fieldNames.find? (·.toString == name) with - | some _ => return true - | none => return false - | none => panic! s!"{parent} is not a structure" - else - return false + let some si := getStructureInfo? env parent | return false + return getProjFnForField? env parent (Name.mkSimple name) == declName + || (si.parentInfo.any fun pi => pi.projFn == declName) | _ => return false def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean index 8481587b..2aff5c13 100644 --- a/DocGen4/Process/StructureInfo.lean +++ b/DocGen4/Process/StructureInfo.lean @@ -16,43 +16,38 @@ open Lean Meta Execute `k` with an array containing pairs `(fieldName, fieldType)`. `k` is executed in an updated local context which contains local declarations for the `structName` parameters. -/ -def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do +def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) : MetaM α := do let structName := info.name let us := info.levelParams.map mkLevelParam forallTelescopeReducing info.type fun params _ => withLocalDeclD `self (mkAppN (mkConst structName us) params) fun s => do let mut info := #[] - for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do + for fieldName in getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) do let proj ← mkProjection s fieldName info := info.push (fieldName, (← inferType proj)) k info -def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do +def getFieldTypes (parents : Array Name) (v : InductiveVal) : MetaM (Array FieldInfo) := do + let env ← getEnv withFields v fun fields => - fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type)) + fields.foldlM (init := #[]) (fun acc (name, type) => do + let some structForField := findField? env v.name name | unreachable! + -- We can't simply do `structForField == v.name` since the field might be from a parent that overlapped with another. + let isDirect := structForField == v.name && !parents.any fun parent => (getFieldInfo? env parent name).isSome + let some fi := getFieldInfo? env structForField name | unreachable! + return acc.push { ← NameInfo.ofTypedName fi.projFn type with isDirect }) def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv - let parents ← getAllParentStructures v.name + let parents := (getStructureParentInfo env v.name).map fun parent => parent.structName let ctorVal := getStructureCtor env v.name let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type - match getStructureInfo? env v.name with - | some i => - if i.fieldNames.size - parents.size > 0 then - return { - toInfo := info, - fieldInfo := ← getFieldTypes v, - parents, - ctor - } - else - return { - toInfo := info, - fieldInfo := #[], - parents, - ctor - } - | none => panic! s!"{v.name} is not a structure" + return { + toInfo := info, + fieldInfo := ← getFieldTypes parents v, + parents, + ctor + } end DocGen4.Process diff --git a/static/style.css b/static/style.css index 3f81d048..925880b6 100644 --- a/static/style.css +++ b/static/style.css @@ -757,6 +757,15 @@ a:hover { transition: opacity 1000ms ease-out; } +.inherited_field { + transition: opacity 300ms ease-in; +} + +.structure_fields:not(:hover) .inherited_field { + opacity: 30%; + transition: opacity 1000ms ease-out; +} + .gh_link { float: right; margin-left: 10px;