Avoid whnf on Nat

src/Lean/Environment.lean

@@ -206,8 +206,10 @@ def EnvironmentHeader.moduleNames (header : EnvironmentHeader) : Array Name :=
 namespace Kernel
 
 structure Diagnostics where
-  /-- Number of times each declaration has been unfolded by the kernel. -/
+  /-- Number of times each declaration has been unfolded by the kernel during defeq checking. -/
   unfoldCounter : PHashMap Name Nat := {}
+  /-- Number of times each declaration has been unfolded by the kernel during whnf reduction. -/
+  reduceCounter : PHashMap Name Nat := {}
   /-- If `enabled = true`, kernel records declarations that have been unfolded. -/
   enabled : Bool := false
   deriving Inhabited
@@ -344,13 +346,17 @@ def isDiagnosticsEnabled (env : Environment) : Bool :=
   env.diagnostics.enabled
 
 def resetDiag (env : Environment) : Environment :=
-  { env with diagnostics.unfoldCounter := {} }
+  { env with diagnostics.unfoldCounter := {}, diagnostics.reduceCounter := {} }
 
 @[export lean_kernel_record_unfold]
-def Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) : Diagnostics :=
+def Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) (inDefEq : Bool) : Diagnostics :=
   if d.enabled then
-    let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
-    { d with unfoldCounter := d.unfoldCounter.insert declName cNew }
+    if inDefEq then
+      let cNew := if let some c := d.unfoldCounter.find? declName then c + 1 else 1
+      { d with unfoldCounter := d.unfoldCounter.insert declName cNew }
+    else
+      let cNew := if let some c := d.reduceCounter.find? declName then c + 1 else 1
+      { d with reduceCounter := d.reduceCounter.insert declName cNew }
   else
     d
 

src/Lean/Meta/Diagnostics.lean

@@ -94,6 +94,7 @@ def reportDiag : MetaM Unit := do
     let inst ← mkDiagSummaryForUsedInstances
     let synthPending ← mkDiagSynthPendingFailure (← get).diag.synthPendingFailures
     let unfoldKernel ← mkDiagSummary `kernel (Kernel.getDiagnostics (← getEnv)).unfoldCounter
+    let reduceKernel ← mkDiagSummary `kernel (Kernel.getDiagnostics (← getEnv)).reduceCounter
     let m := #[]
     let m := appendSection m `reduction "unfolded declarations" unfoldDefault
     let m := appendSection m `reduction "unfolded instances" unfoldInstance
@@ -105,6 +106,7 @@ def reportDiag : MetaM Unit := do
     let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
     let m := appendSection m `reduction "Axioms (possibly imported non-exposed defs) that were tried to be unfolded" unfoldAxiom
     let m := appendSection m `kernel "unfolded declarations" unfoldKernel
+    let m := appendSection m `kernel "reduced declarations" reduceKernel
     unless m.isEmpty do
       let m := m.push "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo <| .trace { cls := `diag, collapsed := false } "Diagnostics" m

src/kernel/environment.cpp

@@ -22,13 +22,13 @@ extern "C" object* lean_environment_add(object*, object*);
 extern "C" object* lean_environment_find(object*, object*);
 extern "C" object* lean_environment_mark_quot_init(object*);
 extern "C" uint8 lean_environment_quot_init(object*);
-extern "C" object* lean_kernel_record_unfold (object*, object*);
+extern "C" object* lean_kernel_record_unfold (object*, object*, uint8);
 extern "C" object* lean_kernel_get_diag(object*);
 extern "C" object* lean_kernel_set_diag(object*, object*);
 extern "C" uint8* lean_kernel_diag_is_enabled(object*);
 
-void diagnostics::record_unfold(name const & decl_name) {
-    m_obj = lean_kernel_record_unfold(m_obj, decl_name.to_obj_arg());
+void diagnostics::record_unfold(name const & decl_name, bool in_defeq) {
+    m_obj = lean_kernel_record_unfold(m_obj, decl_name.to_obj_arg(), in_defeq);
 }
 
 scoped_diagnostics::scoped_diagnostics(environment const & env, bool collect) {

src/kernel/environment.h

@@ -33,7 +33,7 @@ public:
     explicit diagnostics(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit diagnostics(obj_arg o):object_ref(o) {}
     ~diagnostics() {}
-    void record_unfold(name const & decl_name);
+    void record_unfold(name const & decl_name, bool defeq);
 };
 
 /*

src/kernel/type_checker.cpp

@@ -459,7 +459,7 @@ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
                 if (m_diag) {
                     auto f = get_app_fn(e);
                     if (is_constant(f))
-                        m_diag->record_unfold(const_name(f));
+                        m_diag->record_unfold(const_name(f), false);
                 }
                 /* iota-reduction and quotient reduction rules */
                 return whnf_core(*r, cheap_rec, cheap_proj);
@@ -482,6 +482,25 @@ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
     return r;
 }
 
+/** \brief Returns true if \c e is a literal or constructor application */
+bool type_checker::is_value(expr const & e) const {
+    if (is_sort(e) || is_lit(e)) return true;
+    expr const & f = get_app_fn(e);
+    if (is_constant(f)) {
+        // Special case: Do not trigger this if we have `Nat.succ`, else
+        // example (a : Nat) : (a - 8000) + 1 = Nat.succ (a - 8000) := rfl
+        // explodes, because on `Nat`, `whnf` is often `nf`.
+        if (f == *g_nat_succ)
+            return false;
+        if (optional<constant_info> info = env().find(const_name(f)))
+            if (info->is_constructor())
+                return true;
+    } else if (is_fvar(f)) {
+        return true;
+    }
+    return false;
+}
+
 /** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
     to be expanded. */
 optional<constant_info> type_checker::is_delta(expr const & e) const {
@@ -494,14 +513,14 @@ optional<constant_info> type_checker::is_delta(expr const & e) const {
     return none_constant_info();
 }
 
-optional<expr> type_checker::unfold_definition_core(expr const & e) {
+optional<expr> type_checker::unfold_definition_core(expr const & e, bool in_defeq) {
     if (is_constant(e)) {
         if (auto d = is_delta(e)) {
             levels const & us = const_levels(e);
             unsigned len = length(us);
             if (len == d->get_num_lparams()) {
                 if (m_diag) {
-                    m_diag->record_unfold(d->get_name());
+                    m_diag->record_unfold(d->get_name(), in_defeq);
                 }
                 if (len > 0) {
                     auto it = m_st->m_unfold.find(e);
@@ -520,10 +539,10 @@ optional<expr> type_checker::unfold_definition_core(expr const & e) {
 }
 
 /* Unfold head(e) if it is a constant */
-optional<expr> type_checker::unfold_definition(expr const & e) {
+optional<expr> type_checker::unfold_definition(expr const & e, bool in_defeq) {
     if (is_app(e)) {
         expr f0 = get_app_fn(e);
-        if (auto f  = unfold_definition_core(f0)) {
+        if (auto f  = unfold_definition_core(f0, in_defeq)) {
             buffer<expr> args;
             get_app_rev_args(e, args);
             return some_expr(mk_rev_app(*f, args));
@@ -531,7 +550,7 @@ optional<expr> type_checker::unfold_definition(expr const & e) {
             return none_expr();
         }
     } else {
-        return unfold_definition_core(e);
+        return unfold_definition_core(e, in_defeq);
     }
 }
 
@@ -672,7 +691,7 @@ expr type_checker::whnf(expr const & e) {
         } else if (auto v = reduce_nat(t1)) {
             m_st->m_whnf.insert(mk_pair(e, *v));
             return *v;
-        } else if (auto next_t = unfold_definition(t1)) {
+        } else if (auto next_t = unfold_definition(t1, false)) {
             t = *next_t;
         } else {
             auto r = t1;
@@ -900,21 +919,21 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
         if (auto s_n_new = try_unfold_proj_app(s_n)) {
             s_n = *s_n_new;
         } else {
-            t_n = whnf_core(*unfold_definition(t_n), false, true);
+            t_n = whnf_core(*unfold_definition(t_n, true), false, true);
         }
     } else if (!d_t && d_s) {
         /* If `t_n` is a projection application, we try to unfold it instead. See comment above. */
         if (auto t_n_new = try_unfold_proj_app(t_n)) {
             t_n = *t_n_new;
         } else {
-            s_n = whnf_core(*unfold_definition(s_n), false, true);
+            s_n = whnf_core(*unfold_definition(s_n, true), false, true);
         }
     } else {
         int c = compare(d_t->get_hints(), d_s->get_hints());
         if (c < 0) {
-            t_n = whnf_core(*unfold_definition(t_n), false, true);
+            t_n = whnf_core(*unfold_definition(t_n, true), false, true);
         } else if (c > 0) {
-            s_n = whnf_core(*unfold_definition(s_n), false, true);
+            s_n = whnf_core(*unfold_definition(s_n, true), false, true);
         } else {
             if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s) && d_t->get_hints().is_regular()) {
                 // Optimization:
@@ -930,8 +949,8 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
                     }
                 }
             }
-            t_n = whnf_core(*unfold_definition(t_n), false, true);
-            s_n = whnf_core(*unfold_definition(s_n), false, true);
+            t_n = whnf_core(*unfold_definition(t_n, true), false, true);
+            s_n = whnf_core(*unfold_definition(s_n, true), false, true);
         }
     }
     switch (quick_is_def_eq(t_n, s_n)) {
@@ -1089,6 +1108,12 @@ bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
     r = is_def_eq_proof_irrel(t_n, s_n);
     if (r != l_undef) return r == l_true;
 
+    if (is_value(t_n)) { s_n = whnf(s_n); }
+    if (is_value(s_n)) { t_n = whnf(t_n); }
+
+    r = quick_is_def_eq(t_n, s_n);
+    if (r != l_undef) return r == l_true;
+
     /* NB: `lazy_delta_reduction` updates `t_n` and `s_n` even when returning `l_undef`. */
     r = lazy_delta_reduction(t_n, s_n);
     if (r != l_undef) return r == l_true;

src/kernel/type_checker.h

@@ -74,8 +74,9 @@ private:
     optional<expr> reduce_proj_core(expr c, unsigned idx);
     optional<expr> reduce_proj(expr const & e, bool cheap_rec, bool cheap_proj);
     expr whnf_fvar(expr const & e, bool cheap_rec, bool cheap_proj);
+    bool is_value(expr const & e) const;
     optional<constant_info> is_delta(expr const & e) const;
-    optional<expr> unfold_definition_core(expr const & e);
+    optional<expr> unfold_definition_core(expr const & e, bool in_defeq);
 
     bool is_def_eq_binding(expr t, expr s);
     bool is_def_eq(level const & l1, level const & l2);
@@ -166,7 +167,7 @@ public:
     expr whnf_core_cheap(expr const & e) {
         return whnf_core(e, true, true);
     }
-    optional<expr> unfold_definition(expr const & e);
+    optional<expr> unfold_definition(expr const & e, bool in_defeq);
 };
 
 void initialize_type_checker();

tests/lean/run/ack.lean

@@ -14,13 +14,6 @@ trace: [simp] Diagnostics
   [simp] tried theorems (max: 57, num: 1):
     [simp] ack.eq_3 ↦ 57, succeeded: 57
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
----
-trace: [diag] Diagnostics
-  [kernel] unfolded declarations (max: 176, num: 3):
-    [kernel] OfNat.ofNat ↦ 176
-    [kernel] Add.add ↦ 60
-    [kernel] HAdd.hAdd ↦ 60
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics.threshold 50 in
@@ -40,13 +33,6 @@ trace: [simp] Diagnostics
   [simp] tried theorems (max: 57, num: 1):
     [simp] ack.eq_3 ↦ 57, succeeded: 57
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
----
-trace: [diag] Diagnostics
-  [kernel] unfolded declarations (max: 174, num: 3):
-    [kernel] OfNat.ofNat ↦ 174
-    [kernel] Add.add ↦ 58
-    [kernel] HAdd.hAdd ↦ 58
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics.threshold 50 in
@@ -66,13 +52,6 @@ trace: [simp] Diagnostics
   [simp] tried theorems (max: 57, num: 1):
     [simp] ack.eq_3 ↦ 57, succeeded: 57
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
----
-trace: [diag] Diagnostics
-  [kernel] unfolded declarations (max: 174, num: 3):
-    [kernel] OfNat.ofNat ↦ 174
-    [kernel] Add.add ↦ 58
-    [kernel] HAdd.hAdd ↦ 58
-  use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics.threshold 50 in
@@ -93,10 +72,6 @@ trace: [simp] Diagnostics
 trace: [diag] Diagnostics
   [def_eq] heuristic for solving `f a =?= f b` (max: 60, num: 1):
     [def_eq] ack ↦ 60
-  [kernel] unfolded declarations (max: 174, num: 3):
-    [kernel] OfNat.ofNat ↦ 174
-    [kernel] Add.add ↦ 58
-    [kernel] HAdd.hAdd ↦ 58
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in