From aefb5d1c50fcfc82821737815382f0e0f8171254 Mon Sep 17 00:00:00 2001
From: PratherConid <syxx2013050321@163.com>
Date: Wed, 1 Jan 2025 10:11:24 +0800
Subject: [PATCH] add type reduction feature

---
 Auto/Lib/MetaExtra.lean                | 19 +++++++++++++++++++
 Auto/Translation/LamReif.lean          |  2 +-
 Auto/Translation/Monomorphization.lean | 13 +------------
 Auto/Translation/Reduction.lean        | 16 ++++++++++++++++
 4 files changed, 37 insertions(+), 13 deletions(-)

diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean
index 149feb2..c0d5893 100644
--- a/Auto/Lib/MetaExtra.lean
+++ b/Auto/Lib/MetaExtra.lean
@@ -9,6 +9,25 @@ namespace Auto
 
 def Meta.isDefEqD (t s : Expr) : MetaM Bool := Meta.withDefault <| Meta.isDefEq t s
 
+def Meta.whnfNondependentForall (e : Expr) : MetaM Expr := do
+  let e' ← Meta.whnf e
+  match e' with
+  | .forallE _ _ body _ =>
+    if body.hasLooseBVar 0 then
+      return e
+    else
+      return e'
+  | _ => return e
+
+partial def Meta.normalizeNondependentForall (e : Expr) : MetaM Expr := do
+  let e' ← whnfNondependentForall e
+  match e' with
+  | .forallE name ty body bi =>
+    let ty' ← normalizeNondependentForall ty
+    let body' ← normalizeNondependentForall body
+    return .forallE name ty' body' bi
+  | _ => return e
+
 def Meta.withoutMVarAssignments (m : MetaM α) : MetaM α := do
   let mctx ← getMCtx
   Meta.withMCtx {mctx with eAssignment := {}, lAssignment := {}} m
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
index f7ded10..6f71693 100644
--- a/Auto/Translation/LamReif.lean
+++ b/Auto/Translation/LamReif.lean
@@ -1011,7 +1011,7 @@ private def reifTypeAux : Expr → ReifM LamSort
 | e => processTypeExpr e
 
 def reifType (e : Expr) : ReifM LamSort := do
-  let e ← prepReduceExpr e
+  let e ← prepReduceTypeForall e
   reifTypeAux e
 
 def newTermExpr (e : Expr) : ReifM LamTerm := do
diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean
index 9efed32..0b7b434 100644
--- a/Auto/Translation/Monomorphization.lean
+++ b/Auto/Translation/Monomorphization.lean
@@ -57,16 +57,6 @@ register_option auto.mono.termLikeDefEq.maxHeartbeats : Nat := {
   descr := "Heartbeats allocated to each unification of term-like expression"
 }
 
-register_option auto.mono.tyRed.mode : Meta.TransparencyMode := {
-  defValue := .reducible
-  descr := "Transparency level used when reducing types"
-}
-
-register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := {
-  defValue := .default
-  descr := "Transparency level used when testing definitional equality of types"
-}
-
 namespace Auto
 
 inductive MonoMode where
@@ -842,8 +832,7 @@ namespace FVarRep
 
   /-- Return : (reduce(e), whether reduce(e) contain bfvars) -/
   def processType (e : Expr) : FVarRepM (Expr × Bool) := do
-    let mode := auto.mono.tyRed.mode.get (← getOptions)
-    let e ← MetaState.runMetaM <| prepReduceExprWithMode e mode
+    let e ← MetaState.runMetaM <| prepReduceTypeForall e
     let bfvarSet ← getBfvarSet
     -- If `e` contains no bound variables
     if !e.hasAnyFVar bfvarSet.contains then
diff --git a/Auto/Translation/Reduction.lean b/Auto/Translation/Reduction.lean
index 7a0f3c0..2707a46 100644
--- a/Auto/Translation/Reduction.lean
+++ b/Auto/Translation/Reduction.lean
@@ -1,5 +1,6 @@
 import Lean
 import Auto.Lib.ExprExtra
+import Auto.Lib.MetaExtra
 open Lean Meta
 
 private instance : ToString TransparencyMode where
@@ -23,6 +24,16 @@ register_option auto.redMode : TransparencyMode := {
   descr := "TransparencyMode used when reducing collected facts"
 }
 
+register_option auto.mono.tyRed.mode : Meta.TransparencyMode := {
+  defValue := .reducible
+  descr := "Transparency level used when reducing types. The default mode `reducible` does nothing."
+}
+
+register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := {
+  defValue := .default
+  descr := "Transparency level used when testing definitional equality of types"
+}
+
 namespace Auto
 
 def unfoldProj (e : Expr) : MetaM Expr :=
@@ -79,4 +90,9 @@ def prepReduceDefeq (type : Expr) : MetaM (Option Expr) := do
     let eq' := Lean.mkApp3 (.const ``Eq lvls) ty lhs rhs
     return .some (← mkForallFVars xs eq')
 
+def prepReduceTypeForall (e : Expr) : MetaM Expr := do
+  let e ← prepReduceExpr e
+  let mode := auto.mono.tyRed.mode.get (← getOptions)
+  Meta.withTransparency mode <| Meta.normalizeNondependentForall e
+
 end Auto