michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/expr_eq_fn): take names into account when CompareBinderInfo is true

Browse source 
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.
This commit is contained in:
Leonardo de Moura 2015-12-13 14:47:11 -08:00
parent 49eae56db4
commit 999f23cbc0
7 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/expr_eq_fn.cpp
View file

@ -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);

2
src/tests/kernel/max_sharing.cpp
View file

@ -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();
}

4
tests/lean/congr1.lean.expected.out
View file

@ -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

4
tests/lean/congr2.lean.expected.out
View file

@ -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
:

2
tests/lean/extra/print_info.12.19.expected.out
View file

@ -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

2
tests/lean/extra/print_info.12.20.expected.out
View file

@ -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

2
tests/lean/extra/print_info.7.18.expected.out
View file

@ -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