From f54c192e6fc137c11b7535249f60e5aeeb7b9898 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 2 Feb 2022 11:22:15 +0100 Subject: [PATCH 1/3] feat: equations Equation implementation for definitions, right now lots of definitions simply dont generate equational lemmata at all so lots are left without them. --- DocGen4/Output/Definition.lean | 33 +++++++++++++++++++++++ DocGen4/Output/Module.lean | 2 ++ DocGen4/Process.lean | 49 +++++++++++++++++++++++++--------- lean-toolchain | 2 +- 4 files changed, 73 insertions(+), 13 deletions(-) create mode 100644 DocGen4/Output/Definition.lean diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean new file mode 100644 index 0000000..f92627c --- /dev/null +++ b/DocGen4/Output/Definition.lean @@ -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 +
  • [←infoFormatToHtml c]
    • + +def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do + if let some eqs ← i.equations then + let equationsHtml ← eqs.mapM equationToHtml + return
    + Equations + +
    + 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 + diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 914e26e..1a37ae9 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -7,6 +7,7 @@ import DocGen4.Output.Template import DocGen4.Output.Inductive import DocGen4.Output.Structure import DocGen4.Output.Class +import DocGen4.Output.Definition namespace DocGen4 namespace Output @@ -75,6 +76,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.inductiveInfo i => inductiveToHtml i | DocInfo.structureInfo i => structureToHtml i | DocInfo.classInfo i => classToHtml i + | DocInfo.definitionInfo i => definitionToHtml i | _ => #[] return
    diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index bc9eebd..4fd10a8 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -47,6 +47,7 @@ structure DefinitionInfo extends Info where --value : CodeWithInfos unsafeInformation : DefinitionSafety hints : ReducibilityHints + equations : Option (Array CodeWithInfos) deriving Inhabited abbrev InstanceInfo := DefinitionInfo @@ -160,11 +161,33 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do def isInstance (declName : Name) : MetaM Bool := do (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 let info ← Info.ofConstantVal v.toConstantVal - -- Elaborating the value yields weird exceptions - --let value ← prettyPrintTerm v.value - return DefinitionInfo.mk info v.safety v.hints + let mut eqs? := none + try + 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 let env ← getEnv @@ -254,7 +277,6 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i) | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i) | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i) - -- TODO: Find a way to extract equations nicely | ConstantInfo.defnInfo i => if ← (isProjFn i.name) then none @@ -342,14 +364,15 @@ def process : MetaM AnalyzerResult := do res := res.insert module (Module.mk module moduleDoc #[]) for cinfo in env.constants.toList do - let d := ←DocInfo.ofConstant cinfo - match d with - | some dinfo => - let some modidx ← env.getModuleIdxFor? cinfo.fst | unreachable! - let moduleName := env.allImportedModuleNames.get! modidx - let module := res.find! moduleName - res := res.insert moduleName {module with members := module.members.push dinfo} - | none => () + try + let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {} + if let some dinfo ← analysis then + let some modidx ← env.getModuleIdxFor? dinfo.getName | unreachable! + let moduleName := env.allImportedModuleNames.get! modidx + let module := res.find! moduleName + res := res.insert moduleName {module with members := module.members.push dinfo} + 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 let mut adj := Array.mkArray res.size (Array.mkArray res.size false) @@ -370,4 +393,6 @@ def process : MetaM AnalyzerResult := do importAdj := adj } + + end DocGen4 diff --git a/lean-toolchain b/lean-toolchain index 19c9eec..0085298 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2022-01-16 +leanprover/lean4:nightly-2022-02-04 From 419c1eb1e6289046b26220c36a0df00ecb0e3da0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 4 Feb 2022 22:48:08 +0100 Subject: [PATCH 2/3] feat: equations for instances --- DocGen4/Output/Class.lean | 8 ++++---- DocGen4/Output/Instance.lean | 10 ++++++++++ DocGen4/Output/Module.lean | 2 ++ 3 files changed, 16 insertions(+), 4 deletions(-) create mode 100644 DocGen4/Output/Instance.lean diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index d69f311..f803a6d 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -7,11 +7,11 @@ namespace Output open scoped DocGen4.Jsx open Lean -def instanceToHtml (name : Name) : HtmlM Html := do +def classInstanceToHtml (name : Name) : HtmlM Html := do
  • {name.toString}
    • -def instancesToHtml (i : ClassInfo) : HtmlM Html := do - let instancesHtml ← i.instances.mapM instanceToHtml +def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do + let instancesHtml ← i.instances.mapM classInstanceToHtml return
    Instances
      @@ -20,7 +20,7 @@ def instancesToHtml (i : ClassInfo) : HtmlM Html := do
    def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do - (←structureToHtml i.toStructureInfo).push (←instancesToHtml i) + (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i) end Output end DocGen4 diff --git a/DocGen4/Output/Instance.lean b/DocGen4/Output/Instance.lean new file mode 100644 index 0000000..bad10f1 --- /dev/null +++ b/DocGen4/Output/Instance.lean @@ -0,0 +1,10 @@ +import DocGen4.Output.Template +import DocGen4.Output.Definition + +namespace DocGen4 +namespace Output + +def instanceToHtml (i : InstanceInfo) : HtmlM (Array Html) := definitionToHtml i + +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 1a37ae9..d203241 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -8,6 +8,7 @@ import DocGen4.Output.Inductive import DocGen4.Output.Structure import DocGen4.Output.Class import DocGen4.Output.Definition +import DocGen4.Output.Instance namespace DocGen4 namespace Output @@ -77,6 +78,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.structureInfo i => structureToHtml i | DocInfo.classInfo i => classToHtml i | DocInfo.definitionInfo i => definitionToHtml i + | DocInfo.instanceInfo i => instanceToHtml i | _ => #[] return
    From 117c94031fcb564a4bf8add97f994995ead88112 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 5 Feb 2022 02:26:03 +0100 Subject: [PATCH 3/3] feat: equations for simple functions Functions without pattern matching or wf recursion don't have any equational lemma autogenerated for themselves so we have to generate it explicitly. The implementation is largely adapted from structural equation code in the compiler. --- DocGen4/Process.lean | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 4fd10a8..5a5df9e 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -177,17 +177,29 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do let final := stripArgs type prettyPrintTerm final +def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do + let env ← getEnv + withOptions (tactic.hygienic.set . false) do + lambdaTelescope v.value fun xs body => do + let us := v.levelParams.map mkLevelParam + let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body + let type ← mkForallFVars xs type + type + def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do let info ← Info.ofConstantVal v.toConstantVal - let mut eqs? := none try - eqs? ← getEqnsFor? v.name + let eqs? ← getEqnsFor? v.name + match eqs? with + | some eqs => + let prettyEqs ← eqs.mapM processEq + DefinitionInfo.mk info v.safety v.hints prettyEqs + | none => + let eq ← prettyPrintTerm $ stripArgs (←valueToEq v) + DefinitionInfo.mk info v.safety v.hints (some #[eq]) 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 - + return DefinitionInfo.mk info v.safety v.hints none def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do let env ← getEnv