feat: class inductives
parent
27f8b50763
commit
8059940c30
|
@ -10,8 +10,8 @@ open Lean
|
|||
def classInstanceToHtml (name : Name) : HtmlM Html := do
|
||||
<li><a href={←declNameToLink name}>{name.toString}</a></li>
|
||||
|
||||
def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
|
||||
let instancesHtml ← i.instances.mapM classInstanceToHtml
|
||||
def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
|
||||
let instancesHtml ← instances.mapM classInstanceToHtml
|
||||
return <details «class»="instances">
|
||||
<summary>Instances</summary>
|
||||
<ul>
|
||||
|
@ -20,7 +20,7 @@ def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
|
|||
</details>
|
||||
|
||||
def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
|
||||
(←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i)
|
||||
(←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
|
||||
|
||||
end Output
|
||||
end DocGen4
|
||||
|
|
|
@ -0,0 +1,13 @@
|
|||
import DocGen4.Output.Template
|
||||
import DocGen4.Output.Class
|
||||
import DocGen4.Output.Inductive
|
||||
|
||||
|
||||
namespace DocGen4
|
||||
namespace Output
|
||||
|
||||
def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
|
||||
(←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
|
||||
|
||||
end Output
|
||||
end DocGen4
|
|
@ -9,6 +9,7 @@ import DocGen4.Output.Structure
|
|||
import DocGen4.Output.Class
|
||||
import DocGen4.Output.Definition
|
||||
import DocGen4.Output.Instance
|
||||
import DocGen4.Output.ClassInductive
|
||||
|
||||
namespace DocGen4
|
||||
namespace Output
|
||||
|
@ -77,6 +78,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
|
|||
| DocInfo.classInfo i => classToHtml i
|
||||
| DocInfo.definitionInfo i => definitionToHtml i
|
||||
| DocInfo.instanceInfo i => instanceToHtml i
|
||||
| DocInfo.classInductiveInfo i => classInductiveToHtml i
|
||||
| _ => #[]
|
||||
|
||||
return <div «class»="decl" id={doc.getName.toString}>
|
||||
|
|
|
@ -69,6 +69,10 @@ structure ClassInfo extends StructureInfo where
|
|||
instances : Array Name
|
||||
deriving Inhabited
|
||||
|
||||
structure ClassInductiveInfo extends InductiveInfo where
|
||||
instances : Array Name
|
||||
deriving Inhabited
|
||||
|
||||
inductive DocInfo where
|
||||
| axiomInfo (info : AxiomInfo) : DocInfo
|
||||
| theoremInfo (info : TheoremInfo) : DocInfo
|
||||
|
@ -78,6 +82,7 @@ inductive DocInfo where
|
|||
| inductiveInfo (info : InductiveInfo) : DocInfo
|
||||
| structureInfo (info : StructureInfo) : DocInfo
|
||||
| classInfo (info : ClassInfo) : DocInfo
|
||||
| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
|
||||
deriving Inhabited
|
||||
|
||||
namespace DocInfo
|
||||
|
@ -91,6 +96,7 @@ def getDeclarationRange : DocInfo → DeclarationRange
|
|||
| inductiveInfo i => i.declarationRange
|
||||
| structureInfo i => i.declarationRange
|
||||
| classInfo i => i.declarationRange
|
||||
| classInductiveInfo i => i.declarationRange
|
||||
|
||||
def lineOrder (l r : DocInfo) : Bool :=
|
||||
l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
|
||||
|
@ -253,12 +259,19 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
|
|||
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
|
||||
let sinfo ← StructureInfo.ofInductiveVal v
|
||||
let fn ← mkConstWithFreshMVarLevels v.name
|
||||
def getInstances (className : Name) : MetaM (Array Name) := do
|
||||
let fn ← mkConstWithFreshMVarLevels className
|
||||
let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
|
||||
let insts ← SynthInstance.getInstances (mkAppN fn xs)
|
||||
return ClassInfo.mk sinfo (insts.map Expr.constName!)
|
||||
insts.map Expr.constName!
|
||||
|
||||
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
|
||||
let sinfo ← StructureInfo.ofInductiveVal v
|
||||
return ClassInfo.mk sinfo (←getInstances v.name)
|
||||
|
||||
def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
|
||||
let info ← InductiveInfo.ofInductiveVal v
|
||||
return ClassInductiveInfo.mk info (←getInstances v.name)
|
||||
|
||||
namespace DocInfo
|
||||
|
||||
|
@ -314,7 +327,10 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
|
|||
else
|
||||
some $ structureInfo (←StructureInfo.ofInductiveVal i)
|
||||
else
|
||||
some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
|
||||
if isClass env i.name then
|
||||
some $ classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
|
||||
else
|
||||
some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
|
||||
-- we ignore these for now
|
||||
| ConstantInfo.ctorInfo i => none
|
||||
| ConstantInfo.recInfo i => none
|
||||
|
@ -329,6 +345,7 @@ def getName : DocInfo → Name
|
|||
| inductiveInfo i => i.name
|
||||
| structureInfo i => i.name
|
||||
| classInfo i => i.name
|
||||
| classInductiveInfo i => i.name
|
||||
|
||||
def getKind : DocInfo → String
|
||||
| axiomInfo _ => "axiom"
|
||||
|
@ -339,6 +356,7 @@ def getKind : DocInfo → String
|
|||
| inductiveInfo _ => "inductive"
|
||||
| structureInfo _ => "structure"
|
||||
| classInfo _ => "class"
|
||||
| classInductiveInfo _ => "class"
|
||||
|
||||
def getKindDescription : DocInfo → String
|
||||
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
|
||||
|
@ -359,6 +377,7 @@ def getKindDescription : DocInfo → String
|
|||
| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
|
||||
| structureInfo _ => "structure"
|
||||
| classInfo _ => "class"
|
||||
| classInductiveInfo _ => "class inductive"
|
||||
|
||||
def getType : DocInfo → CodeWithInfos
|
||||
| axiomInfo i => i.type
|
||||
|
@ -369,6 +388,7 @@ def getType : DocInfo → CodeWithInfos
|
|||
| inductiveInfo i => i.type
|
||||
| structureInfo i => i.type
|
||||
| classInfo i => i.type
|
||||
| classInductiveInfo i => i.type
|
||||
|
||||
def getArgs : DocInfo → Array Arg
|
||||
| axiomInfo i => i.args
|
||||
|
@ -379,6 +399,7 @@ def getArgs : DocInfo → Array Arg
|
|||
| inductiveInfo i => i.args
|
||||
| structureInfo i => i.args
|
||||
| classInfo i => i.args
|
||||
| classInductiveInfo i => i.args
|
||||
|
||||
end DocInfo
|
||||
|
||||
|
|
Loading…
Reference in New Issue