From 3d65b1c25c74d3044d392fa826889df77f25dfd2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Oct 2014 15:41:55 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241 --- src/frontends/lean/elaborator.cpp | 13 +++++++------ src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/notation_cmd.cpp | 6 +++--- src/frontends/lean/parser.cpp | 8 ++++---- src/frontends/lean/util.cpp | 10 +++++----- src/library/annotation.cpp | 2 +- src/library/explicit.cpp | 14 +++++++------- src/library/explicit.h | 16 ++++++++-------- tests/lean/interactive/sec_info_bug.input | 14 ++++++++++++++ .../interactive/sec_info_bug.input.expected.out | 10 ++++++++++ 10 files changed, 60 insertions(+), 35 deletions(-) create mode 100644 tests/lean/interactive/sec_info_bug.input create mode 100644 tests/lean/interactive/sec_info_bug.input.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a25786d8b..a983cc9b8 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -121,7 +121,8 @@ optional elaborator::mvar_to_meta(expr const & mvar) { /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ void elaborator::save_type_data(expr const & e, expr const & r) { - if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) { + if (!m_no_info && infom() && pip() && + (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e))) { if (auto p = pip()->get_pos_info(e)) { expr t = m_tc[m_relax_main_opaque]->infer(r).first; m_pre_info_data.add_type_info(p->first, p->second, t); @@ -742,9 +743,9 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit(get_annotation_arg(e), cs); } else if (is_typed_expr(e)) { return visit_typed_expr(e, cs); - } else if (is_implicit(e)) { + } else if (is_as_atomic(e)) { // ignore annotation - return visit_core(get_implicit_arg(e), cs); + return visit_core(get_as_atomic_arg(e), cs); } else if (is_consume_args(e)) { // ignore annotation return visit_core(get_consume_args_arg(e), cs); @@ -789,10 +790,10 @@ pair elaborator::visit(expr const & e) { r = visit_core(e, cs); } else { bool consume_args = false; - if (is_implicit(e)) { - r = get_implicit_arg(e); + if (is_as_atomic(e)) { + flet let(m_no_info, true); + r = get_as_atomic_arg(e); if (is_explicit(r)) r = get_explicit_arg(r); - b = r; r = visit_core(r, cs); } else if (is_consume_args(e)) { consume_args = true; diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 2b90632d4..e056be54d 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -439,7 +439,7 @@ struct inductive_cmd_fn { [&](inductive_decl const & d) { return const_name(e) == inductive_decl_name(d); })) return none_expr(); // found target - expr r = mk_implicit(mk_app(mk_explicit(e), section_params)); + expr r = mk_as_atomic(mk_app(mk_explicit(e), section_params)); return some_expr(r); }); } diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index f92502d7c..1eea2520f 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -56,8 +56,8 @@ environment precedence_cmd(parser & p) { /** \brief Auxiliary function for #cleanup_section_notation. */ expr cleanup_section_notation_core(parser & p, expr const & e) { - if (is_implicit(e)) { - return cleanup_section_notation_core(p, get_implicit_arg(e)); + if (is_as_atomic(e)) { + return cleanup_section_notation_core(p, get_as_atomic_arg(e)); } else if (is_explicit(e)) { return cleanup_section_notation_core(p, get_explicit_arg(e)); } else if (is_app(e)) { @@ -96,7 +96,7 @@ expr cleanup_section_notation(parser & p, expr const & e) { if (is_local(e)) throw parser_error(sstream() << "invalid occurrence of local parameter '" << local_pp_name(e) << "' in (section) notation", p.pos_of(e)); - if (is_implicit(e)) + if (is_as_atomic(e)) return some_expr(cleanup_section_notation_core(p, e)); return none_expr(); }); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 589b11707..0d8931fec 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1066,8 +1066,8 @@ name parser::check_constant_next(char const * msg) { name id = check_id_next(msg); expr e = id_to_expr(id, p); - if (in_section_or_context(m_env) && is_implicit(e)) { - e = get_app_fn(get_implicit_arg(e)); + if (in_section_or_context(m_env) && is_as_atomic(e)) { + e = get_app_fn(get_as_atomic_arg(e)); if (is_explicit(e)) e = get_explicit_arg(e); } @@ -1423,8 +1423,8 @@ void parser::save_type_info(expr const & e) { return; if (is_explicit(e)) { save_type_info(get_explicit_arg(e)); - } else if (is_implicit(e)) { - save_type_info(get_implicit_arg(e)); + } else if (is_as_atomic(e)) { + save_type_info(get_as_atomic_arg(e)); } else if (is_choice(e)) { for (unsigned i = 0; i < get_num_choices(e); i++) save_type_info(get_choice(e, i)); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index a4a14045a..87798e058 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -111,13 +111,13 @@ expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_se buffer params; for (unsigned i = 0; i < num_sec_params; i++) params.push_back(mk_explicit(sec_params[i])); - return mk_implicit(mk_app(mk_explicit(mk_constant(n, sec_ls)), params)); + return mk_as_atomic(mk_app(mk_explicit(mk_constant(n, sec_ls)), params)); } bool is_section_local_ref(expr const & e) { - if (!is_implicit(e)) + if (!is_as_atomic(e)) return false; - expr const & imp_arg = get_implicit_arg(e); + expr const & imp_arg = get_as_atomic_arg(e); if (!is_app(imp_arg)) return false; buffer locals; @@ -136,7 +136,7 @@ expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, n if (locals_to_remove.empty() && lvls_to_remove.empty()) return e; buffer locals; - expr const & f = get_app_args(get_implicit_arg(e), locals); + expr const & f = get_app_args(get_as_atomic_arg(e), locals); lean_assert(is_explicit(f)); expr new_f; @@ -165,7 +165,7 @@ expr update_section_local_ref(expr const & e, name_set const & lvls_to_remove, n if (locals.empty()) { return get_explicit_arg(new_f); } else { - return mk_implicit(mk_app(new_f, locals)); + return mk_as_atomic(mk_app(new_f, locals)); } } diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index 625a36e04..25026f5c2 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -62,7 +62,7 @@ expr mk_annotation(name const & kind, expr const & e) { annotation_macros & ms = get_annotation_macros(); auto it = ms.find(kind); if (it != ms.end()) { - return mk_macro(it->second, 1, &e); + return copy_tag(e, mk_macro(it->second, 1, &e)); } else { throw exception(sstream() << "unknown annotation kind '" << kind << "'"); } diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 2cbe4a917..1a8472800 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { static name * g_explicit_name = nullptr; -static name * g_implicit_name = nullptr; +static name * g_as_atomic_name = nullptr; static name * g_as_is_name = nullptr; static name * g_consume_args_name = nullptr; @@ -24,9 +24,9 @@ expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); } bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); } expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); } -expr mk_implicit(expr const & e) { return mk_annotation(*g_implicit_name, e); } -bool is_implicit(expr const & e) { return is_annotation(e, *g_implicit_name); } -expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); } +expr mk_as_atomic(expr const & e) { return mk_annotation(*g_as_atomic_name, e); } +bool is_as_atomic(expr const & e) { return is_annotation(e, *g_as_atomic_name); } +expr const & get_as_atomic_arg(expr const & e) { lean_assert(is_as_atomic(e)); return get_annotation_arg(e); } expr mk_consume_args(expr const & e) { return mk_annotation(*g_consume_args_name, e); } bool is_consume_args(expr const & e) { return is_annotation(e, *g_consume_args_name); } @@ -34,19 +34,19 @@ expr const & get_consume_args_arg(expr const & e) { lean_assert(is_consume_args( void initialize_explicit() { g_explicit_name = new name("@"); - g_implicit_name = new name("@^-1"); + g_as_atomic_name = new name("as_atomic"); g_as_is_name = new name("as_is"); g_consume_args_name = new name("!"); register_annotation(*g_explicit_name); - register_annotation(*g_implicit_name); + register_annotation(*g_as_atomic_name); register_annotation(*g_as_is_name); register_annotation(*g_consume_args_name); } void finalize_explicit() { delete g_as_is_name; - delete g_implicit_name; + delete g_as_atomic_name; delete g_explicit_name; delete g_consume_args_name; } diff --git a/src/library/explicit.h b/src/library/explicit.h index 4e8f3fc2b..f1ac4fb68 100644 --- a/src/library/explicit.h +++ b/src/library/explicit.h @@ -33,16 +33,16 @@ bool is_as_is(expr const & e); */ expr const & get_as_is_arg(expr const & e); -/** \brief Create an implicit expression '@^-1 f'. - This only affects the elaborator behavior. This expression "cancels" the effect of '@' +/** \brief Create an expression that should be treated as an atom by the elaborator. + This expression also "cancels" the effect of a nested '@'. */ -expr mk_implicit(expr const & e); -/** \brief Return true iff \c e is an implicit expression. */ -bool is_implicit(expr const & e); -/** \brief Return the argument of an implicit expression. - \pre is_implicit(e) +expr mk_as_atomic(expr const & e); +/** \brief Return true iff \c e is an atomic expression. */ +bool is_as_atomic(expr const & e); +/** \brief Return the argument of an atomic expression. + \pre is_atomic(e) */ -expr const & get_implicit_arg(expr const & e); +expr const & get_as_atomic_arg(expr const & e); /** \brief Create the expression '! e'. This only affects the elaborator behavior. diff --git a/tests/lean/interactive/sec_info_bug.input b/tests/lean/interactive/sec_info_bug.input new file mode 100644 index 000000000..e32704304 --- /dev/null +++ b/tests/lean/interactive/sec_info_bug.input @@ -0,0 +1,14 @@ +VISIT cat.lean +SYNC 10 +import logic +constant category : Type -> Type +namespace category + section + parameters {ob : Type} {C : category ob} + variables {a b c d : ob} + definition hom : ob → ob → Type := let aux := C in sorry + definition foo := hom + end +end category +WAIT +INFO 8 \ No newline at end of file diff --git a/tests/lean/interactive/sec_info_bug.input.expected.out b/tests/lean/interactive/sec_info_bug.input.expected.out new file mode 100644 index 000000000..58cce95a6 --- /dev/null +++ b/tests/lean/interactive/sec_info_bug.input.expected.out @@ -0,0 +1,10 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGININFO +-- TYPE|8|20 +ob → ob → Type +-- ACK +-- IDENTIFIER|8|20 +hom +-- ACK +-- ENDINFO