From f48cdccd200acd0010a99e36b8cf7397bd3a2ef5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 May 2015 15:08:49 -0700 Subject: [PATCH] fix(frontends/lean/pp): abbreviation with parameters closes #639 --- src/frontends/lean/pp.cpp | 2 ++ src/library/abbreviation.cpp | 4 ++- src/library/normalize.cpp | 41 ++++++++++++++++-------------- src/library/normalize.h | 2 ++ tests/lean/640a.hlean | 40 +++++++++++++++++++++++++++++ tests/lean/640a.hlean.expected.out | 11 ++++++++ tests/lean/640b.lean | 2 ++ tests/lean/640b.lean.expected.out | 1 + 8 files changed, 83 insertions(+), 20 deletions(-) create mode 100644 tests/lean/640a.hlean create mode 100644 tests/lean/640a.hlean.expected.out create mode 100644 tests/lean/640b.lean create mode 100644 tests/lean/640b.lean.expected.out diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e082c6504..05c9ae5e9 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -532,6 +532,8 @@ optional pretty_fn::is_abbreviated(expr const & e) const { } auto pretty_fn::pp_const(expr const & e, optional const & num_ref_univ_params) -> result { + if (auto it = is_abbreviated(e)) + return pp_abbreviation(e, *it, false); if (!num_ref_univ_params) { if (auto r = pp_local_ref(e)) return *r; diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index 22652804c..cda7e3ffd 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/expr_lt.h" #include "library/util.h" +#include "library/normalize.h" namespace lean { typedef pair abbrev_entry; @@ -26,7 +27,8 @@ struct abbrev_state { throw exception(sstream() << "invalid abbreviation '" << n << "', it is not a definition"); m_abbrevs.insert(n, parsing_only); if (!parsing_only) { - m_inv_map.insert(d.get_value(), n); + expr v = try_eta(d.get_value()); + m_inv_map.insert(v, n); } } diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index df0f6803c..f8d750dd8 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -164,6 +164,28 @@ void finalize_normalize() { delete g_key; } +expr try_eta(expr const & e) { + if (is_lambda(e)) { + expr const & b = binding_body(e); + if (is_lambda(b)) { + expr new_b = try_eta(b); + if (is_eqp(b, new_b)) { + return e; + } else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) { + return lower_free_vars(app_fn(new_b), 1); + } else { + return update_binding(e, binding_domain(e), new_b); + } + } else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) { + return lower_free_vars(app_fn(b), 1); + } else { + return e; + } + } else { + return e; + } +} + class normalize_fn { type_checker & m_tc; name_generator m_ngen; @@ -267,25 +289,6 @@ class normalize_fn { } } - expr try_eta(expr const & e) { - lean_assert(is_lambda(e)); - expr const & b = binding_body(e); - if (is_lambda(b)) { - expr new_b = try_eta(b); - if (is_eqp(b, new_b)) { - return e; - } else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) { - return lower_free_vars(app_fn(new_b), 1); - } else { - return update_binding(e, binding_domain(e), new_b); - } - } else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) { - return lower_free_vars(app_fn(b), 1); - } else { - return e; - } - } - expr normalize(expr e) { check_system("normalize"); if (!m_pred(e)) diff --git a/src/library/normalize.h b/src/library/normalize.h index 238c54bbc..cd3f25a46 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -60,6 +60,8 @@ environment erase_constructor_hint(environment const & env, name const & n, bool /** \brief Retrieve the hint added with the procedure add_constructor_hint. */ optional has_constructor_hint(environment const & env, name const & d); +expr try_eta(expr const & e); + void initialize_normalize(); void finalize_normalize(); } diff --git a/tests/lean/640a.hlean b/tests/lean/640a.hlean new file mode 100644 index 000000000..224a7629a --- /dev/null +++ b/tests/lean/640a.hlean @@ -0,0 +1,40 @@ +section + parameter {A : Type} + definition relation : A → A → Type := λa b, a = b + local abbreviation R := relation + local abbreviation S [parsing-only] := relation + variable {a : A} + check relation a a + check R a a + check S a a +end + +section + parameter {A : Type} + definition relation' : A → A → Type := λa b, a = b + local infix `~1`:50 := relation' + local infix [parsing-only] `~2`:50 := relation' + variable {a : A} + check relation' a a + check a ~1 a + check a ~2 a +end + +section + parameter {A : Type} + definition relation'' : A → A → Type := λa b, a = b + local infix [parsing-only] `~2`:50 := relation'' + variable {a : A} + check relation'' a a + check a ~2 a + check a ~2 a +end + +section + parameter {A : Type} + definition relation''' : A → A → Type := λa b, a = b + local abbreviation S [parsing-only] := relation''' + variable {a : A} + check relation''' a a + check S a a +end diff --git a/tests/lean/640a.hlean.expected.out b/tests/lean/640a.hlean.expected.out new file mode 100644 index 000000000..c4dc8e832 --- /dev/null +++ b/tests/lean/640a.hlean.expected.out @@ -0,0 +1,11 @@ +R a a : Type +R a a : Type +R a a : Type +a ~1 a : Type +a ~1 a : Type +a ~1 a : Type +relation'' a a : Type +relation'' a a : Type +relation'' a a : Type +relation''' a a : Type +relation''' a a : Type diff --git a/tests/lean/640b.lean b/tests/lean/640b.lean new file mode 100644 index 000000000..09f4b5834 --- /dev/null +++ b/tests/lean/640b.lean @@ -0,0 +1,2 @@ +abbreviation bar [parsing-only] := @eq +check @bar diff --git a/tests/lean/640b.lean.expected.out b/tests/lean/640b.lean.expected.out new file mode 100644 index 000000000..e4a2c47cc --- /dev/null +++ b/tests/lean/640b.lean.expected.out @@ -0,0 +1 @@ +eq : Π {A : Type}, A → A → Prop