feat: equations

Equation implementation for definitions, right now lots of definitions
simply dont generate equational lemmata at all so lots are left
without them.
main
Henrik Böving 2022-02-02 11:22:15 +01:00
parent b1abc677a0
commit f54c192e6f
4 changed files with 73 additions and 13 deletions

View File

@ -0,0 +1,33 @@
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean Widget
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
<li «class»="equation">[←infoFormatToHtml c]</li>
def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
if let some eqs ← i.equations then
let equationsHtml ← eqs.mapM equationToHtml
return <details>
<summary>Equations</summary>
<ul «class»="equations">
[equationsHtml]
</ul>
</details>
else
return none
def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
let equationsHtml ← equationsToHtml i
if let some equationsHtml ← equationsHtml then
#[equationsHtml]
else
#[]
end Output
end DocGen4

View File

@ -7,6 +7,7 @@ import DocGen4.Output.Template
import DocGen4.Output.Inductive import DocGen4.Output.Inductive
import DocGen4.Output.Structure import DocGen4.Output.Structure
import DocGen4.Output.Class import DocGen4.Output.Class
import DocGen4.Output.Definition
namespace DocGen4 namespace DocGen4
namespace Output namespace Output
@ -75,6 +76,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.inductiveInfo i => inductiveToHtml i | DocInfo.inductiveInfo i => inductiveToHtml i
| DocInfo.structureInfo i => structureToHtml i | DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i | DocInfo.classInfo i => classToHtml i
| DocInfo.definitionInfo i => definitionToHtml i
| _ => #[] | _ => #[]
return <div «class»="decl" id={doc.getName.toString}> return <div «class»="decl" id={doc.getName.toString}>

View File

@ -47,6 +47,7 @@ structure DefinitionInfo extends Info where
--value : CodeWithInfos --value : CodeWithInfos
unsafeInformation : DefinitionSafety unsafeInformation : DefinitionSafety
hints : ReducibilityHints hints : ReducibilityHints
equations : Option (Array CodeWithInfos)
deriving Inhabited deriving Inhabited
abbrev InstanceInfo := DefinitionInfo abbrev InstanceInfo := DefinitionInfo
@ -160,11 +161,33 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
def isInstance (declName : Name) : MetaM Bool := do def isInstance (declName : Name) : MetaM Bool := do
(instanceExtension.getState (←getEnv)).instanceNames.contains declName (instanceExtension.getState (←getEnv)).instanceNames.contains declName
partial def stripArgs (e : Expr) : Expr :=
match e.consumeMData with
| Expr.lam name type body data =>
let name := name.eraseMacroScopes
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
| Expr.forallE name type body data =>
let name := name.eraseMacroScopes
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
| _ => e
def processEq (eq : Name) : MetaM CodeWithInfos := do
let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
let final := stripArgs type
prettyPrintTerm final
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
-- Elaborating the value yields weird exceptions let mut eqs? := none
--let value ← prettyPrintTerm v.value try
return DefinitionInfo.mk info v.safety v.hints eqs? ← getEqnsFor? v.name
catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
let prettyEqs ← eqs?.mapM (λ eqs => eqs.mapM processEq)
return DefinitionInfo.mk info v.safety v.hints prettyEqs
def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
let env ← getEnv let env ← getEnv
@ -254,7 +277,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
| ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i) | ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i)
| ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i) | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i)
| ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
-- TODO: Find a way to extract equations nicely
| ConstantInfo.defnInfo i => | ConstantInfo.defnInfo i =>
if ← (isProjFn i.name) then if ← (isProjFn i.name) then
none none
@ -342,14 +364,15 @@ def process : MetaM AnalyzerResult := do
res := res.insert module (Module.mk module moduleDoc #[]) res := res.insert module (Module.mk module moduleDoc #[])
for cinfo in env.constants.toList do for cinfo in env.constants.toList do
let d := ←DocInfo.ofConstant cinfo try
match d with let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
| some dinfo => if let some dinfo ← analysis then
let some modidx ← env.getModuleIdxFor? cinfo.fst | unreachable! let some modidx ← env.getModuleIdxFor? dinfo.getName | unreachable!
let moduleName := env.allImportedModuleNames.get! modidx let moduleName := env.allImportedModuleNames.get! modidx
let module := res.find! moduleName let module := res.find! moduleName
res := res.insert moduleName {module with members := module.members.push dinfo} res := res.insert moduleName {module with members := module.members.push dinfo}
| none => () catch e =>
IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}"
-- TODO: This is definitely not the most efficient way to store this data -- TODO: This is definitely not the most efficient way to store this data
let mut adj := Array.mkArray res.size (Array.mkArray res.size false) let mut adj := Array.mkArray res.size (Array.mkArray res.size false)
@ -370,4 +393,6 @@ def process : MetaM AnalyzerResult := do
importAdj := adj importAdj := adj
} }
end DocGen4 end DocGen4

View File

@ -1 +1 @@
leanprover/lean4:nightly-2022-01-16 leanprover/lean4:nightly-2022-02-04