From a090875215836833a86ae20dfd88b2cad386836a Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sun, 10 Sep 2023 11:07:22 +0200
Subject: [PATCH] refactor: Remove unnecessary cases in type analysis

---
 DocGen4/Process/DefinitionInfo.lean | 38 ++++++-----------------------
 DocGen4/Process/NameInfo.lean       |  1 -
 2 files changed, 8 insertions(+), 31 deletions(-)

diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
index a260557..6f709c1 100644
--- a/DocGen4/Process/DefinitionInfo.lean
+++ b/DocGen4/Process/DefinitionInfo.lean
@@ -14,9 +14,6 @@ open Lean Meta Widget
 
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
-  | Expr.lam name _ body _ =>
-    let name := name.eraseMacroScopes
-    stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
   | Expr.forallE name _ body _ =>
     let name := name.eraseMacroScopes
     stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
@@ -27,39 +24,20 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do
   let final := stripArgs type
   prettyPrintTerm final
 
-def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
-  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
-      return type
-
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let isUnsafe := v.safety == DefinitionSafety.unsafe
   let isNonComputable := isNoncomputable (← getEnv) v.name
   try
     let eqs? ← getEqnsFor? v.name
-    match eqs? with
-    | some eqs =>
-      let equations ← eqs.mapM processEq
-      return {
-        toInfo := info,
-        isUnsafe,
-        hints := v.hints,
-        equations,
-        isNonComputable
-      }
-    | none =>
-      let equations := #[← prettyPrintTerm <| stripArgs (← valueToEq v)]
-      return {
-        toInfo := info,
-        isUnsafe,
-        hints := v.hints,
-        equations,
-        isNonComputable
-      }
+    let equations ← eqs?.mapM (·.mapM processEq)
+    return {
+      toInfo := info,
+      isUnsafe,
+      hints := v.hints,
+      equations,
+      isNonComputable
+    }
   catch err =>
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
     return {
diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
index 8cb0ed8..1ecd1c7 100644
--- a/DocGen4/Process/NameInfo.lean
+++ b/DocGen4/Process/NameInfo.lean
@@ -32,7 +32,6 @@ partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderI
       let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
       (#[arg] ++ args, final)
   match e.consumeMData with
-  | Expr.lam name type body binderInfo => helper name type body binderInfo
   | Expr.forallE name type body binderInfo => helper name type body binderInfo
   | _ => (#[], e)