From 999f23cbc077b9a2a93d4dfbe1abb63678a95354 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 14:47:11 -0800 Subject: [PATCH] feat(kernel/expr_eq_fn): take names into account when CompareBinderInfo is true This is the correct fix for the id declaration pretty printing discrepancy reported by Daniel. TODO: decide whether we need another eq-mode where names are ignored. For example, in blast, it makes sense to increase sharing by ignoring binder names. --- src/kernel/expr_eq_fn.cpp | 1 + src/tests/kernel/max_sharing.cpp | 2 +- tests/lean/congr1.lean.expected.out | 4 ++-- tests/lean/congr2.lean.expected.out | 4 ++-- tests/lean/extra/print_info.12.19.expected.out | 2 +- tests/lean/extra/print_info.12.20.expected.out | 2 +- tests/lean/extra/print_info.7.18.expected.out | 2 +- 7 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp index 90ff8491e6..bdce8c24a0 100644 --- a/src/kernel/expr_eq_fn.cpp +++ b/src/kernel/expr_eq_fn.cpp @@ -92,6 +92,7 @@ class expr_eq_fn { return apply(binding_domain(a), binding_domain(b)) && apply(binding_body(a), binding_body(b)) && + (!CompareBinderInfo || binding_name(a) == binding_name(b)) && (!CompareBinderInfo || binding_info(a) == binding_info(b)); case expr_kind::Sort: return sort_level(a) == sort_level(b); diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp index 0f2bac585f..16fe929e7e 100644 --- a/src/tests/kernel/max_sharing.cpp +++ b/src/tests/kernel/max_sharing.cpp @@ -28,7 +28,7 @@ static void tst1() { lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); F2 = max_fn(F1); std::cout << F2 << "\n"; - lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2))); + lean_assert(!is_eqp(app_arg(app_fn(F2)), app_arg(F2))); // name matter max_fn.clear(); } diff --git a/tests/lean/congr1.lean.expected.out b/tests/lean/congr1.lean.expected.out index 9d956c934a..e6910def5e 100644 --- a/tests/lean/congr1.lean.expected.out +++ b/tests/lean/congr1.lean.expected.out @@ -1,7 +1,7 @@ [fixed, fixed, eq, eq] -λ (A : Type) (c : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4 +λ (A : Type) (s : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4 : -∀ (A : Type) (c : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3) +∀ (A : Type) (s : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3) [eq, cast, fixed, eq, eq] λ (c c_1 : Prop) (e_1 : c = c_1) (H : decidable c) (A : Type) (t t_1 : A) (e_4 : t = t_1) (e e_2 : A) (e_5 : e = e_2), eq.drec (eq.drec (eq.drec (eq.refl (ite c t e)) e_5) e_4) e_1 diff --git a/tests/lean/congr2.lean.expected.out b/tests/lean/congr2.lean.expected.out index d4e797aac9..953b243529 100644 --- a/tests/lean/congr2.lean.expected.out +++ b/tests/lean/congr2.lean.expected.out @@ -1,7 +1,7 @@ [fixed, fixed, eq, eq] -λ (A : Type) (c : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4 +λ (A : Type) (s : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4 : -∀ (A : Type) (c : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3) +∀ (A : Type) (s : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3) [fixed, eq, eq] λ (A : Type) (a a_1 : list A) (e_2 : a = a_1) (a_2 a_3 : list A) (e_3 : a_2 = a_3), congr (congr_arg perm e_2) e_3 : diff --git a/tests/lean/extra/print_info.12.19.expected.out b/tests/lean/extra/print_info.12.19.expected.out index 1cc9c14272..2187569493 100644 --- a/tests/lean/extra/print_info.12.19.expected.out +++ b/tests/lean/extra/print_info.12.19.expected.out @@ -1,3 +1,3 @@ LEAN_INFORMATION -definition mul : Π {A : Type} [c : has_mul A], A → A → A +definition mul : Π {A : Type} [s : has_mul A], A → A → A END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.12.20.expected.out b/tests/lean/extra/print_info.12.20.expected.out index 1cc9c14272..2187569493 100644 --- a/tests/lean/extra/print_info.12.20.expected.out +++ b/tests/lean/extra/print_info.12.20.expected.out @@ -1,3 +1,3 @@ LEAN_INFORMATION -definition mul : Π {A : Type} [c : has_mul A], A → A → A +definition mul : Π {A : Type} [s : has_mul A], A → A → A END_LEAN_INFORMATION diff --git a/tests/lean/extra/print_info.7.18.expected.out b/tests/lean/extra/print_info.7.18.expected.out index 24056b2aed..e5417a85a7 100644 --- a/tests/lean/extra/print_info.7.18.expected.out +++ b/tests/lean/extra/print_info.7.18.expected.out @@ -1,3 +1,3 @@ LEAN_INFORMATION -definition add : Π {A : Type} [c : has_add A], A → A → A +definition add : Π {A : Type} [s : has_add A], A → A → A END_LEAN_INFORMATION