test: dag

Motivation: when type checking big terms, we may get hash collisions
for big terms that are structurally different, but very similar.
In this kind of situation we may spend we often get hash collisions

See new test.

src/kernel/type_checker.h

@@ -18,18 +18,28 @@ Author: Leonardo de Moura
 #include "kernel/equiv_manager.h"
 
 namespace lean {
+
+struct expr_ptr_eq {
+    bool operator()(expr const & a, expr const & b) const {
+        return a.raw() == b.raw();
+    }
+};
+
+template<typename T>
+using expr_ptr_map = typename std::unordered_map<expr, T, expr_hash, expr_ptr_eq>;
+
+
 /** \brief Lean Type Checker. It can also be used to infer types, check whether a
     type \c A is convertible to a type \c B, etc. */
 class type_checker {
 public:
     class state {
-        typedef expr_map<expr> infer_cache;
         typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
         environment               m_env;
         name_generator            m_ngen;
-        infer_cache               m_infer_type[2];
-        expr_map<expr>            m_whnf_core;
-        expr_map<expr>            m_whnf;
+        expr_ptr_map<expr>        m_infer_type[2];
+        expr_ptr_map<expr>        m_whnf_core;
+        expr_ptr_map<expr>        m_whnf;
         equiv_manager             m_eqv_manager;
         expr_pair_set             m_failure;
         friend type_checker;

tests/bench/dag_issues/dag1.lean

@@ -0,0 +1,41 @@
+import Lean
+
+/-!
+This test produces a timeout if we don't use pointer equality at the
+kernel infer_type and whnf caches.
+Reason: it produces a hash collision for big, very similar, but structurally different terms.
+Then, `m_infer_type` cache gets lost comparing terms for equality.
+-/
+
+open Lean
+
+def mkDouble (e : Expr) :=
+  mkApp2 (mkConst ``Nat.add) e e
+
+def mkDag (e : Expr) : Nat → Expr
+  | 0 => e
+  | n+1 => mkDouble (mkDouble (mkDag e n))
+
+def foo (a b c d e : Nat) :=
+  a + b + c + d + e
+
+open Lean Meta
+def mkDef (name : Name) (n : Nat) : MetaM Unit := do
+  let type ← mkArrow (mkConst ``Nat) (mkConst ``Nat)
+  let big := mkDag (mkBVar 0) n
+  let body := mkApp5 (mkConst ``foo) big big big big big
+  let value := mkLambda `x .default (mkConst ``Nat) body
+  addDecl <| .defnDecl { name, levelParams := [], type, value, safety := .safe, hints := .abbrev }
+
+open Lean Meta
+def mkThm (name : Name) (fnName : Name) : MetaM Unit := do
+  let type ← mkEq (mkApp (mkConst fnName) (mkNatLit 0)) (mkNatLit 0)
+  let value ← mkEqRefl (mkNatLit 0)
+  addDecl <| .thmDecl { name, levelParams := [], type, value }
+
+set_option maxRecDepth 10000000
+
+#eval mkDef `test 12000
+
+set_option profiler true
+#eval mkThm `testEq `test

tests/bench/dag_issues/dag2.lean

@@ -0,0 +1,71 @@
+import Lean
+
+/-!
+This test produces a timeout if we don't use pointer equality at the
+kernel infer_type and whnf caches.
+Reason: it produces a hash collision for big, very similar, but structurally different terms.
+Then, `m_infer_type` cache gets lost comparing terms for equality.
+-/
+
+open Lean
+
+def f (_a : Nat) : Nat := 0
+
+def mkAdd (a b : Expr) :=
+  mkApp2 (mkConst ``Nat.add) a b
+
+def mkTree (d : Nat) (n : Nat) : Expr × Nat :=
+  match d with
+  | 0   => (mkApp (mkConst ``f) (mkRawNatLit n), n+1)
+  | d+1 =>
+    let (left, n) := mkTree d n
+    let (right, n) := mkTree d n
+    (mkAdd left right, n)
+
+def mkDag (e : Expr) (blob : Expr) : Nat → Expr
+  | 0 => e
+  | n+1 =>
+    let a := mkDag e blob n
+    mkAdd (mkAdd a blob) a
+
+open Lean Meta
+def mkDef (name : Name) (n m : Nat) : MetaM Unit := do
+  let type ← mkArrow (mkConst ``Nat) (mkConst ``Nat)
+  let (blob, _) := mkTree m 0
+  let body      := mkDag (mkBVar 0) blob n
+  let value := mkLambda `x .default (mkConst ``Nat) body
+  addDecl <| .defnDecl { name, levelParams := [], type, value, safety := .safe, hints := .abbrev }
+
+#eval mkDef `test 5 13
+
+open Lean Meta
+def mkThm (name : Name) (fnName : Name) : MetaM Unit := do
+  let type ← mkEq (mkApp (mkConst fnName) (mkNatLit 0)) (mkNatLit 0)
+  let value ← mkEqRefl (mkNatLit 0)
+  addDecl <| .thmDecl { name, levelParams := [], type, value }
+
+set_option maxHeartbeats 1000000
+
+set_option profiler true
+example : test 0 = 0 := by
+  simp (config := { decide := false, maxSteps := 1000000 }) [test, f]
+  done
+
+#exit
+
+example : test 0 = 0 := by
+  simp (config := { decide := false, maxSteps := 1000000 }) [test, f]
+  done
+-- set_option profiler true
+-- #eval mkThm `testEq `test
+
+
+
+#exit
+
+set_option maxRecDepth 10000000
+
+#eval mkDef `test 12000
+
+set_option profiler true
+#eval mkThm `testEq `test