Merge pull request #13 from leanprover/structure

Structure support

DocGen4/Output/Base.lean

@@ -30,7 +30,6 @@ def getCurrentName : HtmlM (Option Name) := do (←read).currentName
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base
 
--- TODO: Change this to HtmlM and auto add the root URl
 def moduleNameToLink (n : Name) : HtmlM String := do
   let parts := n.components.map Name.toString
   (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"

DocGen4/Output/Inductive.lean

@@ -5,7 +5,6 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-
 def ctorToHtml (i : NameInfo) : HtmlM Html := do
   let name := i.name.components'.head!.toString
   return <li «class»="constructor" id={name}>{name} : [←infoFormatToHtml i.type]</li>

DocGen4/Output/Module.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 import DocGen4.Output.Template
 import DocGen4.Output.Inductive
+import DocGen4.Output.Structure
 
 namespace DocGen4
 namespace Output
@@ -30,6 +31,19 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   else
     html
 
+def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
+  let mut nodes := #[]
+  if s.parents.size > 0 then
+    nodes := nodes.push <span «class»="decl_extends">extends</span>
+    let mut parents := #[]
+    for parent in s.parents do
+      let link := <a «class»="break_within" href={←declNameToLink parent}>{parent.toString}</a>
+      let inner := Html.element "span" true #[("class", "fn")] #[link]
+      let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
+      parents := parents.push html
+    nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
+  nodes
+
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
   -- TODO: noncomputable, partial
@@ -44,14 +58,18 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
     </span>
   for arg in doc.getArgs do
     nodes := nodes.push (←argToHtml arg)
+
+  if let DocInfo.structureInfo i := doc then
+    nodes := nodes.append (←structureInfoHeader i)
+
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
-  -- TODO: The final type of the declaration
   return <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
-  let doc_html := match doc with
+  let doc_html ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
+  | DocInfo.structureInfo i => structureToHtml i
   | _ => #[]
 
   return <div «class»="decl" id={doc.getName.toString}>

DocGen4/Output/Structure.lean

@@ -0,0 +1,15 @@
+import DocGen4.Output.Template
+
+namespace DocGen4
+namespace Output
+
+open scoped DocGen4.Jsx
+
+def fieldToHtml (f : NameInfo) : HtmlM Html := do
+  return <li «class»="structure_field" id={f.name.toString}>{s!"{f.name} : "} [←infoFormatToHtml f.type]</li>
+
+def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
+  #[Html.element "ul" false #[("class", "structure_fields"), ("id", s!"{i.name.toString}.mk")] (←i.fieldInfo.mapM fieldToHtml)]
+
+end Output
+end DocGen4

DocGen4/Process.lean

@@ -56,13 +56,8 @@ structure InductiveInfo extends Info where
   isUnsafe : Bool
   deriving Inhabited
 
-structure FieldInfo extends NameInfo where
-  projFn : Name
-  subobject? : Option Name
-  deriving Inhabited
-
 structure StructureInfo extends Info where
-  fieldInfo : Array FieldInfo
+  fieldInfo : Array NameInfo
   parents : Array Name
   ctor : NameInfo
   deriving Inhabited
@@ -155,40 +150,42 @@ def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type
   | _ => panic! s!"Constructor {ctor} was requested but does not exist"
 
--- TODO: Obtain parameters that come after the inductive Name
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
   let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
   return InductiveInfo.mk info ctors v.isUnsafe
 
-def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) :=
-  match type with
-  | Expr.forallE `self _ b .. => (b, (`self :: vars))
-  | Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars)
-  | _ => (type, vars)
+def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
+  match type, n with
+  | e, 0 => (e, [])
+  | Expr.forallE name type body _, x + 1 =>
+    let body := body.instantiate1 $ mkFVar ⟨name⟩
+    let next := dropArgs body x
+    { next with snd := (name, type) :: next.snd}
+  | e, x + 1 => panic! s!"No forallE left"
 
-def getFieldType (projFn : Name) : MetaM Expr := do
-  let fn ← mkConstWithFreshMVarLevels projFn
-  let type ← inferType fn
-  let (type, vars) := getFieldTypeAux type []
-  type.instantiate $ vars.toArray.map mkConst
-
-def FieldInfo.ofStructureFieldInfo (i : StructureFieldInfo) : MetaM FieldInfo := do
-  let type ← getFieldType i.projFn
-  let ni := NameInfo.mk i.fieldName (←prettyPrintTerm type)
-  FieldInfo.mk ni i.projFn i.subobject?
+def getFieldTypes (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 := #[]
+  for (name, type) in fields do
+    field_infos := field_infos.push { name := name, type := ←prettyPrintTerm type}
+  field_infos
 
 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 |>.name
-  let ctorType ← getConstructorType ctor
+  let ctor := getStructureCtor env v.name
+  let ctorType ← prettyPrintTerm ctor.type
   match getStructureInfo? env v.name with
   | some i =>
-    let fieldInfos ← i.fieldInfo.mapM FieldInfo.ofStructureFieldInfo
-    return StructureInfo.mk info fieldInfos parents ⟨ctor, ctorType⟩
+    if i.fieldNames.size - parents.size > 0 then
+      return StructureInfo.mk info (←getFieldTypes ctor parents.size) parents ⟨ctor.name, ctorType⟩
+    else
+      return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
   | none => panic! s!"{v.name} is not a structure"
 
 def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do

static/style.css

@@ -421,7 +421,7 @@ main h2, main h3, main h4, main h5, main h6 {
     border-radius: 5px;
 }
 
-.decl_args, .decl_type {
+.decl_args, .decl_type .decl_parent {
     font-weight: normal;
 }
 
@@ -430,7 +430,7 @@ main h2, main h3, main h4, main h5, main h6 {
     white-space: nowrap;
 }
 
-.decl_kind, .decl_name {
+.decl_kind, .decl_name, .decl_extends {
     font-weight: bold;
 }
 
@@ -480,14 +480,7 @@ pre code { padding: 0 0; }
 
 .structure_field {
     display: block;
-}
-.structure_field:before {
-    content: '(';
-    color: gray;
-}
-.structure_field:after {
-    content: ')';
-    color: gray;
+    margin-left: 2ex;
 }
 
 .constructor {