From f6a1d1c864992aed6cf4d22ca2cadfd90528c70e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 14:24:30 -0700 Subject: [PATCH] fix(frontends/lean/parser): fixes #584 --- src/frontends/lean/parser.cpp | 37 ++++++++++++++++++++++++++++--- tests/lean/584a.lean | 18 +++++++++++++++ tests/lean/584a.lean.expected.out | 5 +++++ tests/lean/584b.lean | 27 ++++++++++++++++++++++ tests/lean/584b.lean.expected.out | 4 ++++ tests/lean/584c.lean | 29 ++++++++++++++++++++++++ tests/lean/584c.lean.expected.out | 5 +++++ 7 files changed, 122 insertions(+), 3 deletions(-) create mode 100644 tests/lean/584a.lean create mode 100644 tests/lean/584a.lean.expected.out create mode 100644 tests/lean/584b.lean create mode 100644 tests/lean/584b.lean.expected.out create mode 100644 tests/lean/584c.lean create mode 100644 tests/lean/584c.lean.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7ed84e08c..1bf3079d6 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/aliases.h" #include "library/constants.h" #include "library/private.h" +#include "library/locals.h" #include "library/protected.h" #include "library/choice.h" #include "library/placeholder.h" @@ -521,9 +522,39 @@ void parser::add_parameter(name const & n, expr const & p) { bool parser::update_local_binder_info(name const & n, binder_info const & bi) { auto it = get_local(n); - if (!it) return false; - if (!is_local(*it)) return false; - m_local_decls.update(n, update_local(*it, bi)); + if (!it || !is_local(*it)) return false; + + buffer> entries; + to_buffer(m_local_decls.get_entries(), entries); + std::reverse(entries.begin(), entries.end()); + unsigned idx = m_local_decls.find_idx(n); + lean_assert(idx > 0); + lean_assert_eq(entries[idx-1].second, *it); + + buffer old_locals; + buffer new_locals; + old_locals.push_back(*it); + expr new_l = update_local(*it, bi); + m_local_decls.update(n, new_l); + new_locals.push_back(new_l); + + for (unsigned i = idx; i < entries.size(); i++) { + name const & curr_n = entries[i].first; + expr const & curr_e = entries[i].second; + expr r = is_local(curr_e) ? mlocal_type(curr_e) : curr_e; + if (std::any_of(old_locals.begin(), old_locals.end(), [&](expr const & l) { return depends_on(r, l); })) { + r = instantiate_rev(abstract_locals(r, old_locals.size(), old_locals.data()), + new_locals.size(), new_locals.data()); + if (is_local(curr_e)) { + expr new_e = update_mlocal(curr_e, r); + old_locals.push_back(curr_e); + new_locals.push_back(new_e); + m_local_decls.update(curr_n, new_e); + } else { + m_local_decls.update(curr_n, r); + } + } + } return true; } diff --git a/tests/lean/584a.lean b/tests/lean/584a.lean new file mode 100644 index 000000000..58b7cd911 --- /dev/null +++ b/tests/lean/584a.lean @@ -0,0 +1,18 @@ +variables (A : Type) [H : inhabited A] (x : A) +include H + +definition foo := x +check foo -- A and x are explicit + +variables {A x} +definition foo' := x +check @foo' -- A is explicit, x is implicit + +open nat + +check foo nat 10 + +definition test : foo' = 10 := rfl + +set_option pp.implicit true +print test diff --git a/tests/lean/584a.lean.expected.out b/tests/lean/584a.lean.expected.out new file mode 100644 index 000000000..2fa0ac087 --- /dev/null +++ b/tests/lean/584a.lean.expected.out @@ -0,0 +1,5 @@ +foo : Π (A : Type) [H : inhabited A], A → A +foo' : Π {A : Type} [H : inhabited A] {x : A}, A +foo ℕ 10 : ℕ +definition test : ∀ {A : Type} [H : inhabited A], @foo' num num.is_inhabited 10 = 10 +λ (A : Type) (H : inhabited A), @rfl num (@foo' num num.is_inhabited 10) diff --git a/tests/lean/584b.lean b/tests/lean/584b.lean new file mode 100644 index 000000000..0fda05ad5 --- /dev/null +++ b/tests/lean/584b.lean @@ -0,0 +1,27 @@ +section + variable (A : Type) + + section + variables (a b : A) + variable (H : a = b) + + definition tst₁ := a + + check @tst₁ + + variable {A} + + definition tst₂ := a + + check @tst₂ -- A is implicit + + lemma symm₂ : b = a := eq.symm H + + check @symm₂ + end + + variable (a : A) + definition tst₃ := a + + check @tst₃ -- A is explicit again +end diff --git a/tests/lean/584b.lean.expected.out b/tests/lean/584b.lean.expected.out new file mode 100644 index 000000000..6fd6153f0 --- /dev/null +++ b/tests/lean/584b.lean.expected.out @@ -0,0 +1,4 @@ +tst₁ : Π (A : Type), A → A +tst₂ : Π {A : Type}, A → A +symm₂ : ∀ {A : Type} (a b : A), a = b → b = a +tst₃ : Π (A : Type), A → A diff --git a/tests/lean/584c.lean b/tests/lean/584c.lean new file mode 100644 index 000000000..a30a67448 --- /dev/null +++ b/tests/lean/584c.lean @@ -0,0 +1,29 @@ +section + parameter (A : Type) + + section + parameters (a b : A) + parameter (H : a = b) + + definition tst₁ := a + + parameter {A} + + definition tst₂ := a + + lemma symm₂ : b = a := eq.symm H + + parameters {a b} + lemma foo (c : A) (h₂ : c = b) : c = a := + eq.trans h₂ symm₂ + end + + parameter (a : A) + definition tst₃ := a +end + +check @tst₁ +check @tst₂ -- A is implicit +check @symm₂ +check @tst₃ -- A is explicit again +check @foo diff --git a/tests/lean/584c.lean.expected.out b/tests/lean/584c.lean.expected.out new file mode 100644 index 000000000..30a049fce --- /dev/null +++ b/tests/lean/584c.lean.expected.out @@ -0,0 +1,5 @@ +tst₁ : Π (A : Type), A → A +tst₂ : Π {A : Type}, A → A +symm₂ : ∀ {A : Type} (a b : A), a = b → b = a +tst₃ : Π (A : Type), A → A +foo : ∀ {A : Type} {a b : A}, a = b → (∀ (c : A), c = b → c = a)