fix(frontends/lean/parser): bug in 'using' construct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
8e0888828d
commit
7f3e2b3ef4
5 changed files with 26 additions and 4 deletions
|
@ -803,12 +803,12 @@ void parser_imp::parse_using() {
|
||||||
new_prefix = curr_name();
|
new_prefix = curr_name();
|
||||||
next();
|
next();
|
||||||
}
|
}
|
||||||
buffer<std::pair<name, expr>> to_add;
|
buffer<std::pair<name, name>> to_add;
|
||||||
for (auto it = m_env->begin_objects(); it != m_env->end_objects(); ++it) {
|
for (auto it = m_env->begin_objects(); it != m_env->end_objects(); ++it) {
|
||||||
if (it->has_type() && it->has_name() && !is_hidden_object(*it) && is_prefix_of(prefix, it->get_name())) {
|
if (it->has_type() && it->has_name() && !is_hidden_object(*it) && is_prefix_of(prefix, it->get_name())) {
|
||||||
auto n = replace_prefix(it->get_name(), prefix, new_prefix);
|
auto n = replace_prefix(it->get_name(), prefix, new_prefix);
|
||||||
if (!n.is_anonymous())
|
if (!n.is_anonymous())
|
||||||
to_add.emplace_back(n, mk_constant(it->get_name()));
|
to_add.emplace_back(n, it->get_name());
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
for (auto p : to_add) {
|
for (auto p : to_add) {
|
||||||
|
|
|
@ -247,7 +247,7 @@ expr parser_imp::parse_mixfixc(operator_info const & op) {
|
||||||
expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit_args) {
|
expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit_args) {
|
||||||
auto it = m_using_decls.find(id);
|
auto it = m_using_decls.find(id);
|
||||||
if (it != m_using_decls.end()) {
|
if (it != m_using_decls.end()) {
|
||||||
return it->second;
|
return get_name_ref(it->second, p, implicit_args);
|
||||||
} else {
|
} else {
|
||||||
lean_assert(!m_namespace_prefixes.empty());
|
lean_assert(!m_namespace_prefixes.empty());
|
||||||
auto it = m_namespace_prefixes.end();
|
auto it = m_namespace_prefixes.end();
|
||||||
|
|
|
@ -56,7 +56,7 @@ class parser_imp {
|
||||||
typedef name_map<expr> builtins;
|
typedef name_map<expr> builtins;
|
||||||
typedef expr_map<pos_info> expr_pos_info;
|
typedef expr_map<pos_info> expr_pos_info;
|
||||||
typedef expr_map<tactic> tactic_hints; // a mapping from placeholder to tactic
|
typedef expr_map<tactic> tactic_hints; // a mapping from placeholder to tactic
|
||||||
typedef scoped_map<name, expr, name_hash, name_eq> using_decls;
|
typedef scoped_map<name, name, name_hash, name_eq> using_decls;
|
||||||
enum class scope_kind { Scope, Namespace };
|
enum class scope_kind { Scope, Namespace };
|
||||||
|
|
||||||
std::weak_ptr<parser_imp> m_this;
|
std::weak_ptr<parser_imp> m_this;
|
||||||
|
|
12
tests/lean/using_bug1.lean
Normal file
12
tests/lean/using_bug1.lean
Normal file
|
@ -0,0 +1,12 @@
|
||||||
|
variables a b c d : Nat
|
||||||
|
axiom H : a + (b + c) = a + (b + d)
|
||||||
|
using Nat
|
||||||
|
check add_succr a
|
||||||
|
|
||||||
|
theorem mul_zerol2 (a : Nat) : 0 * a = 0
|
||||||
|
:= induction_on a
|
||||||
|
(have 0 * 0 = 0 : trivial)
|
||||||
|
(λ (n : Nat) (iH : 0 * n = 0),
|
||||||
|
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
|
||||||
|
... = 0 + 0 : { iH }
|
||||||
|
... = 0 : trivial)
|
10
tests/lean/using_bug1.lean.expected.out
Normal file
10
tests/lean/using_bug1.lean.expected.out
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
Set: pp::colors
|
||||||
|
Set: pp::unicode
|
||||||
|
Assumed: a
|
||||||
|
Assumed: b
|
||||||
|
Assumed: c
|
||||||
|
Assumed: d
|
||||||
|
Assumed: H
|
||||||
|
Using: Nat
|
||||||
|
Nat::add_succr a : ∀ b : ℕ, a + (b + 1) = a + b + 1
|
||||||
|
Proved: mul_zerol2
|
Loading…
Add table
Reference in a new issue