From 117c94031fcb564a4bf8add97f994995ead88112 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 5 Feb 2022 02:26:03 +0100
Subject: [PATCH] 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