From 56d151ef7f7bcaeef38bfa166d209ddc8aa24401 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Aug 2014 22:08:10 -0700
Subject: [PATCH] feat(frontends/lean): 'partial' aliases. closes #24
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/frontends/lean/parser.cpp | 44 ++++++++++++++++++-----------------
tests/lean/run/ns1.lean | 10 ++++++++
2 files changed, 33 insertions(+), 21 deletions(-)
create mode 100644 tests/lean/run/ns1.lean
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 684a768dd..1d2f8e3ac 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -862,31 +862,13 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
next();
ls = to_list(lvl_buffer.begin(), lvl_buffer.end());
}
+
if (id.is_atomic()) {
// locals
if (auto it1 = m_local_decls.find(id))
return copy_with_new_pos(propagate_levels(*it1, ls), p);
- optional<expr> r;
- // globals
- if (m_env.find(id))
- r = save_pos(mk_constant(id, ls), p);
- // aliases
- auto as = get_expr_aliases(m_env, id);
- if (!is_nil(as)) {
- buffer<expr> new_as;
- if (r)
- new_as.push_back(*r);
- for (auto const & e : as) {
- new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
- }
- r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
- }
- if (!r && m_no_undef_id_error)
- r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
- if (!r)
- throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
- return *r;
} else {
+ lean_assert(!id.is_atomic());
name new_id = remove_root_prefix(id);
if (m_env.find(new_id)) {
return save_pos(mk_constant(new_id, ls), p);
@@ -897,8 +879,28 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
return save_pos(mk_constant(new_id, ls), p);
}
}
- throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
}
+
+ optional<expr> r;
+ // globals
+ if (m_env.find(id))
+ r = save_pos(mk_constant(id, ls), p);
+ // aliases
+ auto as = get_expr_aliases(m_env, id);
+ if (!is_nil(as)) {
+ buffer<expr> new_as;
+ if (r)
+ new_as.push_back(*r);
+ for (auto const & e : as) {
+ new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p));
+ }
+ r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
+ }
+ if (!r && m_no_undef_id_error)
+ r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
+ if (!r)
+ throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
+ return *r;
}
name parser::check_constant_next(char const * msg) {
diff --git a/tests/lean/run/ns1.lean b/tests/lean/run/ns1.lean
new file mode 100644
index 000000000..1448a1bc9
--- /dev/null
+++ b/tests/lean/run/ns1.lean
@@ -0,0 +1,10 @@
+import standard
+
+namespace foo
+namespace boo
+theorem tst : true := trivial
+end
+end
+
+using foo
+check boo.tst
\ No newline at end of file