From 006b92deaa1ce89cce115782b7728ba1fa4b4865 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 2 Dec 2021 10:34:20 +0100
Subject: [PATCH] feat: Rudamentary structure support

---
 DocGen4/Process.lean | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index c77c97f..fd42109 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -41,13 +41,19 @@ structure InductiveInfo extends Info where
   isNested : Bool
   deriving Repr
 
+structure StructureInfo extends Info where
+  fieldInfo : Array StructureFieldInfo
+  parents : Array Name
+  ctor : (Name × Syntax)
+  deriving Repr
+
 inductive DocInfo where
 | axiomInfo (info : AxiomInfo) : DocInfo
 | theoremInfo (info : TheoremInfo) : DocInfo
 | opaqueInfo (info : OpaqueInfo) : DocInfo
 | definitionInfo (info : DefinitionInfo) : DocInfo
 | inductiveInfo (info : InductiveInfo) : DocInfo
-| structureInfo : DocInfo
+| structureInfo (info : StructureInfo) : DocInfo
 | classInfo : DocInfo
 | classInductiveInfo : DocInfo
 
@@ -97,9 +103,19 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let ctors ← List.mapM (λ name => do (name, ←getConstructorType name)) v.ctors
   return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested
 
+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
+  match getStructureInfo? env v.name with
+  | some i => return StructureInfo.mk info i.fieldInfo parents (ctor, ctorType)
+  | none => panic! s!"{v.name} is not a structure"
+
 namespace DocInfo
 
-private def isBlackListed (declName : Name) : MetaM Bool := do
+def isBlackListed (declName : Name) : MetaM Bool := do
   let env ← getEnv
   declName.isInternal
   <||> isAuxRecursor env declName
@@ -122,7 +138,11 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
   -- - how we can access unnamed instances (they probably have internal names?, change the blacklist?)
   | ConstantInfo.defnInfo i => some $ definitionInfo (←DefinitionInfo.ofDefinitionVal i)
   -- TODO: Differentiate between all the different types of inductives (structures, classes etc.)
-  | ConstantInfo.inductInfo i => some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
+  | ConstantInfo.inductInfo i =>
+    if isStructure (←getEnv) i.name then
+      some $ structureInfo (←StructureInfo.ofInductiveVal i)
+    else
+      some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
   -- we ignore these for now
   | ConstantInfo.ctorInfo i => none
   | ConstantInfo.recInfo i => none
@@ -138,6 +158,9 @@ def prettyPrint (i : DocInfo) : CoreM String := do
   | inductiveInfo i =>
     let ctorString ← i.ctors.mapM (λ (name, type) => do s!"{name} : {←PrettyPrinter.formatTerm type}")
     s!"inductive {i.name} : {←PrettyPrinter.formatTerm i.type}, ctors: {ctorString}, doc string: {i.doc}"
+  | structureInfo i =>
+    let ctorString ← s!"{i.ctor.fst} : {←PrettyPrinter.formatTerm i.ctor.snd}"
+    s!"structure {i.name} : {←PrettyPrinter.formatTerm i.type}, ctor: {ctorString}, doc string: {i.doc}"
   | _ => ""
 
 end DocInfo