fix(library/scoped_ext): bug in local metadata in sections

The problem is described in issue #554
This commit is contained in:
Leonardo de Moura 2015-04-21 18:56:28 -07:00
parent 697a536d9e
commit bf8a7eb9b4
16 changed files with 99 additions and 36 deletions

View file

@ -316,6 +316,8 @@ if_pos unit.star
definition if_empty {A : Type} (t e : A) : (if empty then t else e) = e :=
if_neg not_empty
section
open eq.ops
definition if_cond_congr {c₁ c₂ : Type} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A)
: (if c₁ then t else e) = (if c₂ then t else e) :=
decidable.rec_on H₁
@ -357,3 +359,4 @@ decidable.rec
-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
definition dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl
end

View file

@ -249,6 +249,7 @@ namespace is_trunc
/- interaction with the Unit type -/
open equiv
-- A contractible type is equivalent to [Unit]. *)
definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit :=
equiv.mk (λ (x : A), ⋆)

View file

@ -630,6 +630,7 @@ end
/- instantiate ring theorems to int -/
section port_algebra
open [classes] algebra
theorem mul.left_comm : ∀a b c : , a * (b * c) = b * (a * c) := algebra.mul.left_comm
theorem mul.right_comm : ∀a b c : , (a * b) * c = (a * c) * b := algebra.mul.right_comm
theorem add.left_comm : ∀a b c : , a + (b + c) = b + (a + c) := algebra.add.left_comm

View file

@ -247,6 +247,7 @@ end
/- instantiate ordered ring theorems to int -/
section port_algebra
open [classes] algebra
definition ge [reducible] (a b : ) := algebra.has_le.ge a b
definition gt [reducible] (a b : ) := algebra.has_lt.gt a b
infix >= := int.ge

View file

@ -311,6 +311,7 @@ section
end
section port_algebra
open [classes] algebra
theorem mul.left_comm : ∀a b c : , a * (b * c) = b * (a * c) := algebra.mul.left_comm
theorem mul.right_comm : ∀a b c : , (a * b) * c = (a * c) * b := algebra.mul.right_comm

View file

@ -173,6 +173,7 @@ section
end
section port_algebra
open [classes] algebra
theorem add_pos_left : ∀{a : }, 0 < a → ∀b : , 0 < a + b :=
take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
theorem add_pos_right : ∀{a : }, 0 < a → ∀b : , 0 < b + a :=

View file

@ -384,6 +384,7 @@ match H a a with
| inr n := absurd rfl n
end
open eq.ops
theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = inr n :=
assume n,
match H a b with

View file

@ -309,11 +309,11 @@ environment end_scoped_cmd(parser & p) {
p.pop_local_scope();
if (p.curr_is_identifier()) {
name n = p.check_atomic_id_next("invalid end of scope, atomic identifier expected");
environment env = pop_scope(p.env(), n);
environment env = pop_scope(p.env(), p.ios(), n);
redeclare_aliases(p, level_entries, entries);
return env;
} else {
environment env = pop_scope(p.env());
environment env = pop_scope(p.env(), p.ios());
redeclare_aliases(p, level_entries, entries);
return env;
}

View file

@ -1634,7 +1634,7 @@ bool parser::parse_commands() {
} catch (interrupt_parser) {
commit_info();
while (has_open_scopes(m_env))
m_env = pop_scope_core(m_env);
m_env = pop_scope_core(m_env, m_ios);
}
commit_info(m_scanner.get_line()+1, 0);
for (certified_declaration const & thm : m_theorem_queue.join()) {

View file

@ -102,7 +102,7 @@ struct aliases_ext : public environment_extension {
return env;
}
static environment push_scope(environment const & env, scope_kind k) {
static environment push_scope(environment const & env, io_state const &, scope_kind k) {
aliases_ext ext = get_extension(env);
ext.push(k != scope_kind::Namespace);
environment new_env = update(env, ext);
@ -111,7 +111,7 @@ struct aliases_ext : public environment_extension {
return new_env;
}
static environment pop_scope(environment const & env, scope_kind) {
static environment pop_scope(environment const & env, io_state const &, scope_kind) {
aliases_ext ext = get_extension(env);
ext.pop();
return update(env, ext);

View file

@ -161,7 +161,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
environment r = update(env, ext);
for (auto const & t : get_exts()) {
r = std::get<3>(t)(r, k);
r = std::get<3>(t)(r, ios, k);
}
if (k == scope_kind::Namespace)
r = using_namespace(r, ios, new_n);
@ -182,7 +182,7 @@ static void namespace_reader(deserializer & d, module_idx, shared_environment &,
});
}
environment pop_scope_core(environment const & env) {
environment pop_scope_core(environment const & env, io_state const & ios) {
scope_mng_ext ext = get_extension(env);
if (is_nil(ext.m_namespaces))
return env;
@ -192,19 +192,19 @@ environment pop_scope_core(environment const & env) {
ext.m_scope_kinds = tail(ext.m_scope_kinds);
environment r = update(env, ext);
for (auto const & t : get_exts()) {
r = std::get<4>(t)(r, k);
r = std::get<4>(t)(r, ios, k);
}
return r;
}
environment pop_scope(environment const & env, name const & n) {
environment pop_scope(environment const & env, io_state const & ios, name const & n) {
scope_mng_ext ext = get_extension(env);
if (is_nil(ext.m_namespaces))
throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
if (n != head(ext.m_headers))
throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
<< head(ext.m_headers) << "', and ends with '" << n << "'");
return pop_scope_core(env);
return pop_scope_core(env, ios);
}
bool has_open_scopes(environment const & env) {
@ -240,9 +240,9 @@ static int push_scope(lua_State * L) {
static int pop_scope(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 1)
return push_environment(L, pop_scope(to_environment(L, 1)));
return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L)));
else
return push_environment(L, pop_scope(to_environment(L, 1), to_name_ext(L, 2)));
return push_environment(L, pop_scope(to_environment(L, 1), get_io_state(L), to_name_ext(L, 2)));
}
void open_scoped_ext(lua_State * L) {

View file

@ -19,8 +19,8 @@ namespace lean {
enum class scope_kind { Namespace, Section, Context };
typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
typedef environment (*push_scope_fn)(environment const &, scope_kind);
typedef environment (*pop_scope_fn)(environment const &, scope_kind);
typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
typedef environment (*pop_scope_fn)(environment const &, io_state const &, scope_kind);
void register_scoped_ext(name const & n, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop);
/** \brief Use objects defined in the namespace \c n.
@ -37,11 +37,11 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
/** \brief Delete the most recent scope, all scoped extensions are notified.
\remark method throws an exception if there are no open scopes, or \c n does not match the name of the open scope
*/
environment pop_scope(environment const & env, name const & n = name());
environment pop_scope(environment const & env, io_state const & ios, name const & n = name());
/** \brief Similar to \c pop_scope, but it always succeed.
It always pops the current open scope, and does nothing if there are no open scope.
*/
environment pop_scope_core(environment const & env);
environment pop_scope_core(environment const & env, io_state const & ios);
/** \brief Return true iff there are open scopes */
bool has_open_scopes(environment const & env);
@ -93,10 +93,11 @@ class scoped_ext : public environment_extension {
state m_state;
list<state> m_scopes;
name_map<list<entry>> m_entries;
list<list<entry>> m_nonlocal_entries; // nonlocal entries per scope (for sections)
name_map<list<entry>> m_entries_map; // namespace -> entries
void using_namespace_core(environment const & env, io_state const & ios, name const & n) {
if (auto it = m_entries.find(n)) {
if (auto it = m_entries_map.find(n)) {
buffer<entry> entries;
to_buffer(*it, entries);
unsigned i = entries.size();
@ -108,10 +109,10 @@ class scoped_ext : public environment_extension {
}
void register_entry_core(name n, entry const & e) {
if (auto it = m_entries.find(n))
m_entries.insert(n, cons(e, *it));
if (auto it = m_entries_map.find(n))
m_entries_map.insert(n, cons(e, *it));
else
m_entries.insert(n, to_list(e));
m_entries_map.insert(n, to_list(e));
}
void add_entry_core(environment const & env, io_state const & ios, entry const & e) {
@ -130,6 +131,8 @@ class scoped_ext : public environment_extension {
scoped_ext _add_entry(environment const & env, io_state const & ios, entry const & e) const {
scoped_ext r(*this);
r.register_entry_core(get_namespace(env), e);
if (r.m_nonlocal_entries)
r.m_nonlocal_entries = cons(cons(e, head(r.m_nonlocal_entries)), tail(r.m_nonlocal_entries));
add_entry(env, ios, r.m_state, e);
return r;
}
@ -148,7 +151,7 @@ public:
}
environment export_namespace(environment env, io_state const & ios, name const & n) const {
if (auto it = m_entries.find(n)) {
if (auto it = m_entries_map.find(n)) {
buffer<entry> entries;
to_buffer(*it, entries);
unsigned i = entries.size();
@ -162,16 +165,26 @@ public:
scoped_ext push() const {
scoped_ext r(*this);
r.m_scopes = cons(m_state, r.m_scopes);
r.m_scopes = cons(m_state, r.m_scopes);
r.m_nonlocal_entries = cons(list<entry>(), r.m_nonlocal_entries);
return r;
}
scoped_ext pop() const {
pair<scoped_ext, list<entry>> pop(scope_kind k) const {
lean_assert(!is_nil(m_scopes));
scoped_ext r(*this);
r.m_state = head(m_scopes);
r.m_scopes = tail(m_scopes);
return r;
if (k == scope_kind::Section) {
auto entries = head(r.m_nonlocal_entries);
r.m_nonlocal_entries = tail(r.m_nonlocal_entries);
if (r.m_nonlocal_entries)
r.m_nonlocal_entries = cons(append(entries, head(r.m_nonlocal_entries)), tail(r.m_nonlocal_entries));
return mk_pair(r, entries);
} else {
r.m_nonlocal_entries = tail(r.m_nonlocal_entries);
return mk_pair(r, list<entry>());
}
}
struct reg {
@ -199,17 +212,20 @@ public:
static environment export_namespace_fn(environment const & env, io_state const & ios, name const & n) {
return get(env).export_namespace(env, ios, n);
}
static environment push_fn(environment const & env, scope_kind k) {
if (k != scope_kind::Section)
return update(env, get(env).push());
else
return env;
static environment push_fn(environment const & env, io_state const &, scope_kind) {
return update(env, get(env).push());
}
static environment pop_fn(environment const & env, scope_kind k) {
if (k != scope_kind::Section)
return update(env, get(env).pop());
else
return env;
static environment pop_fn(environment const & env, io_state const & ios, scope_kind k) {
auto p = get(env).pop(k);
environment new_env = update(env, p.first);
buffer<entry> entries;
to_buffer(p.second, entries);
unsigned i = entries.size();
while (i > 0) {
--i;
new_env = update(new_env, get(new_env)._add_tmp_entry(new_env, ios, entries[i]));
}
return new_env;
}
static environment register_entry(environment const & env, io_state const & ios, name const & n, entry const & e) {
return update(env, get(env)._register_entry(env, ios, n, e));
@ -243,7 +259,7 @@ public:
return get(env).m_state;
}
static list<entry> const * get_entries(environment const & env, name const & n) {
return get(env).m_entries.find(n);
return get(env).m_entries_map.find(n);
}
};

View file

@ -0,0 +1,24 @@
import logic
section
variables {A : Type}
variables f : A → A → A
local infixl `+++`:10 := f
variables a b c : A
check f a b
check a +++ b
definition foo : nat → bool :=
λn, bool.tt
notation `bla`:100 := 10
local attribute foo [coercion]
print coercions
end
print coercions -- should be empty
check bla
check 1 +++ 2 -- should say +++ is an invalid expression
open nat
print coercions

View file

@ -0,0 +1,6 @@
f a b : A
f a b : A
nat ↣ bool : foo
bla : num
local_notation_bug.lean:22:8: error: invalid expression
num ↣ nat : of_num

View file

@ -0,0 +1,7 @@
open nat
section
parameters (b : )
definition add_b (n : ) := n + b
local postfix `%`:max := add_b
end
eval 5% -- Error, unexpected token

View file

@ -0,0 +1 @@
local_notation_bug2.lean:7:6: error: unexpected token