From 118189eaacd1af7d6dfeb4450761e5a16ddb78f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 18:05:07 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): bug in translation function This commit fixes the bug reported in the lean discussion list: https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc --- src/frontends/lean/elaborator.cpp | 19 +++++++++++-------- tests/lean/run/scope_bug.lean | 4 ++++ 2 files changed, 15 insertions(+), 8 deletions(-) create mode 100644 tests/lean/run/scope_bug.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 6443865968..5145e742bd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1890,12 +1890,19 @@ std::tuple elaborator::operator()( } // Auxiliary procedure for #translate -static expr translate_local_name(list const & ctx, name const & local_name, +static expr translate_local_name(environment const & env, + list const & ctx, name const & local_name, expr const & src) { for (expr const & local : ctx) { if (local_pp_name(local) == local_name) return copy(local); } + if (env.find(local_name)) { + if (is_local(src)) + return mk_constant(local_name); + else + return src; + } throw_elaborator_exception(sstream() << "unknown identifier '" << local_name << "'", src); } @@ -1908,14 +1915,10 @@ static expr translate(environment const & env, list const & ctx, expr cons if (is_placeholder(e) || is_by(e)) { return some_expr(e); // ignore placeholders } else if (is_constant(e)) { - if (!env.find(const_name(e))) { - expr new_e = copy_tag(e, translate_local_name(ctx, const_name(e), e)); - return some_expr(new_e); - } else { - return none_expr(); - } + expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e)); + return some_expr(new_e); } else if (is_local(e)) { - expr new_e = copy_tag(e, translate_local_name(ctx, local_pp_name(e), e)); + expr new_e = copy_tag(e, translate_local_name(env, ctx, local_pp_name(e), e)); return some_expr(new_e); } else { return none_expr(); diff --git a/tests/lean/run/scope_bug.lean b/tests/lean/run/scope_bug.lean new file mode 100644 index 0000000000..223572f06f --- /dev/null +++ b/tests/lean/run/scope_bug.lean @@ -0,0 +1,4 @@ +definition s : Type := sorry + +example (A : Type) (s : A) : A := by exact s +example (A : Type) : A → A := by intro s; exact s