From dc1613f535f5e87f9a512f26974ee67f03857122 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Aug 2014 15:07:14 -0700 Subject: [PATCH] feat(frontends/lean): annotate 'notation' subterms with 'noinfo' annotation (goal: improve typeinfo generation); fix initialization problem (with annotations) Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 13 +++++-- src/frontends/lean/noinfo.cpp | 19 ++++++++++ src/frontends/lean/noinfo.h | 19 ++++++++++ src/frontends/lean/parse_table.cpp | 61 +++++++++++++++++++++++++++--- src/kernel/annotation.cpp | 50 ++++++++++++++++-------- src/kernel/annotation.h | 5 +++ src/library/explicit.cpp | 37 ++++++++++++------ 8 files changed, 169 insertions(+), 37 deletions(-) create mode 100644 src/frontends/lean/noinfo.cpp create mode 100644 src/frontends/lean/noinfo.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index f68e66350..4f49bf3e2 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -5,6 +5,6 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp -structure_cmd.cpp sorry.cpp info_manager.cpp) +structure_cmd.cpp sorry.cpp info_manager.cpp noinfo.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 98d156182..92439052e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -35,6 +35,7 @@ Author: Leonardo de Moura #include "frontends/lean/tactic_hint.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/elaborator.h" +#include "frontends/lean/noinfo.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -303,8 +304,9 @@ class elaborator { constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct. local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. // this mapping is populated by the 'by tactic-expr' expression. - name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned - bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent + name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned + bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent. + bool m_noinfo; // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation. std::vector> m_pre_info_data; struct scope_ctx { @@ -902,7 +904,7 @@ public: /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ void save_info_data_core(expr const & e, expr const & r, bool replace) { - if (infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) { + if (!m_noinfo && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) { if (auto p = pip()->get_pos_info(e)) { type_checker::scope scope(*m_tc[m_relax_main_opaque]); expr t = m_tc[m_relax_main_opaque]->infer(r); @@ -924,7 +926,7 @@ public: } void save_synth_data(expr const & e, expr const & r) { - if (infom() && pip() && is_placeholder(e)) { + if (!m_noinfo && infom() && pip() && is_placeholder(e)) { if (auto p = pip()->get_pos_info(e)) { m_pre_info_data.push_back(std::unique_ptr(new synth_info_data(p->first, p->second, r))); } @@ -1035,6 +1037,9 @@ public: return visit_choice(e, none_expr()); } else if (is_by(e)) { return visit_by(e, none_expr()); + } else if (is_noinfo(e)) { + flet let(m_noinfo, true); + return visit(get_annotation_arg(e)); } else { switch (e.kind()) { case expr_kind::Local: return e; diff --git a/src/frontends/lean/noinfo.cpp b/src/frontends/lean/noinfo.cpp new file mode 100644 index 000000000..374184715 --- /dev/null +++ b/src/frontends/lean/noinfo.cpp @@ -0,0 +1,19 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "frontends/lean/noinfo.h" + +namespace lean { +name const & get_noinfo() { + static name g_noinfo("noinfo"); + static register_annotation_fn g_noinfo_annotation(g_noinfo); + return g_noinfo; +} +static name g_noinfo_name = get_noinfo(); // force 'noinfo' annotation to be registered + +expr mk_noinfo(expr const & e) { return mk_annotation(get_noinfo(), e); } +bool is_noinfo(expr const & e) { return is_annotation(e, get_noinfo()); } +} diff --git a/src/frontends/lean/noinfo.h b/src/frontends/lean/noinfo.h new file mode 100644 index 000000000..82430b9af --- /dev/null +++ b/src/frontends/lean/noinfo.h @@ -0,0 +1,19 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/annotation.h" + +namespace lean { +/** \brief Annotate \c e with no-information generation. + + Whenever the elaborator finds this annotation it does not generate + information for \c e or any subterm of \c e. +*/ +expr mk_noinfo(expr const & e); +/** \brief Return true iff \c e is a term annotated with mk_noinfo */ +bool is_noinfo(expr const & e); +} diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index b3d538da8..fb47b3951 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -11,9 +11,55 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "library/kernel_bindings.h" #include "frontends/lean/parse_table.h" +#include "frontends/lean/noinfo.h" namespace lean { namespace notation { +/** \brief Annotate subterms of "macro" \c e with noinfo annotation. + + 1- Variables are not annotated. + 2- A constant f in a macro (f ...) is not annotated if (root == true). + 3- Every other subterm is annotated with noinfo. +*/ +static expr annotate_macro_subterms(expr const & e, bool root = true) { + if (is_var(e) || is_noinfo(e)) + return e; + if (is_binding(e)) + return update_binding(e, + annotate_macro_subterms(binding_domain(e), root), + annotate_macro_subterms(binding_body(e), root)); + buffer args; + bool modified = false; + expr const & f = get_app_args(e, args); + expr new_f; + if ((is_constant(f) && root) || is_noinfo(f)) { + new_f = f; + } else if (is_annotation(f)) { + name const & k = get_annotation_kind(f); + expr const & arg = get_annotation_arg(f); + expr new_arg = annotate_macro_subterms(arg, true); + if (is_eqp(new_arg, arg)) { + new_f = f; + } else { + new_f = mk_annotation(k, new_arg); + modified = true; + } + } else { + new_f = mk_noinfo(f); + modified = true; + } + for (expr & arg : args) { + expr new_arg = annotate_macro_subterms(arg, false); + if (!is_eqp(new_arg, arg)) { + arg = new_arg; + modified = true; + } + } + if (!modified) + return e; + return mk_app(new_f, args); +} + struct action_cell { action_kind m_kind; MK_LEAN_RC(); // Declare m_rc counter @@ -183,14 +229,18 @@ action mk_binders_action() { return *r; } action mk_expr_action(unsigned rbp) { return action(new expr_action_cell(rbp)); } -action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, optional const & terminator, bool right, unsigned rbp) { +action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, + optional const & terminator, bool right, unsigned rbp) { if (get_free_var_range(rec) > 2) throw exception("invalid notation, the expression used to combine a sequence of expressions " "must not contain free variables with de Bruijn indices greater than 1"); - return action(new exprs_action_cell(sep, rec, ini, terminator, right, rbp)); + expr new_rec = annotate_macro_subterms(rec); + expr new_ini = annotate_macro_subterms(ini); + return action(new exprs_action_cell(sep, new_rec, new_ini, terminator, right, rbp)); } action mk_scoped_expr_action(expr const & rec, unsigned rb, bool lambda) { - return action(new scoped_expr_action_cell(rec, rb, lambda)); + expr new_rec = annotate_macro_subterms(rec); + return action(new scoped_expr_action_cell(new_rec, rb, lambda)); } action mk_ext_action(parse_fn const & fn) { return action(new ext_action_cell(fn)); } action mk_ext_lua_action(char const * fn) { return action(new ext_lua_action_cell(fn)); } @@ -297,8 +347,9 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons } parse_table parse_table::add(unsigned num, transition const * ts, expr const & a, bool overload) const { - validate_transitions(is_nud(), num, ts, a); - return add_core(num, ts, a, overload); + expr new_a = annotate_macro_subterms(a); + validate_transitions(is_nud(), num, ts, new_a); + return add_core(num, ts, new_a, overload); } void parse_table::for_each(buffer & ts, std::function const &)> const & fn) const { diff --git a/src/kernel/annotation.cpp b/src/kernel/annotation.cpp index 363e26cfe..54eb9fe0d 100644 --- a/src/kernel/annotation.cpp +++ b/src/kernel/annotation.cpp @@ -11,7 +11,10 @@ Author: Leonardo de Moura #include "kernel/annotation.h" namespace lean { -static name g_annotation("annotation"); +name const & get_annotation_name() { + static name g_annotation("annotation"); + return g_annotation; +} std::string const & get_annotation_opcode() { static std::string g_annotation_opcode("Annot"); @@ -29,8 +32,10 @@ class annotation_macro_definition_cell : public macro_definition_cell { } public: annotation_macro_definition_cell(name const & n):m_name(n) {} - name get_annotation_kind() const { return m_name; } - virtual name get_name() const { return g_annotation; } + name const & get_annotation_kind() const { return m_name; } + virtual name get_name() const { return get_annotation_name(); } + virtual format pp(formatter const &) const { return format(m_name); } + virtual void display(std::ostream & out) const { out << m_name; } virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const { check_macro(m); return arg_types[0]; @@ -46,14 +51,14 @@ public: }; typedef std::unordered_map annotation_macros; -static std::unique_ptr g_annotation_macros; annotation_macros & get_annotation_macros() { + static std::unique_ptr g_annotation_macros; if (!g_annotation_macros) g_annotation_macros.reset(new annotation_macros()); return *(g_annotation_macros.get()); } void register_annotation(name const & n) { - annotation_macros & ms = get_annotation_macros(); + annotation_macros & ms = get_annotation_macros(); lean_assert(ms.find(n) == ms.end()); ms.insert(mk_pair(n, macro_definition(new annotation_macro_definition_cell(n)))); } @@ -69,11 +74,16 @@ expr mk_annotation(name const & kind, expr const & e) { } bool is_annotation(expr const & e) { - return is_macro(e) && macro_def(e).get_name() == g_annotation; + return is_macro(e) && macro_def(e).get_name() == get_annotation_name(); +} + +name const & get_annotation_kind(expr const & e) { + lean_assert(is_annotation(e)); + return static_cast(macro_def(e).raw())->get_annotation_kind(); } bool is_annotation(expr const & e, name const & kind) { - return is_annotation(e) && static_cast(macro_def(e).raw())->get_annotation_kind() == kind; + return is_annotation(e) && get_annotation_kind(e) == kind; } expr const & get_annotation_arg(expr const & e) { @@ -81,12 +91,22 @@ expr const & get_annotation_arg(expr const & e) { return macro_arg(e, 0); } -static name g_let("let"); -static name g_have("have"); -register_annotation_fn g_let_annotation(g_let); -register_annotation_fn g_have_annotation(g_have); -expr mk_let_annotation(expr const & e) { return mk_annotation(g_let, e); } -expr mk_have_annotation(expr const & e) { return mk_annotation(g_have, e); } -bool is_let_annotation(expr const & e) { return is_annotation(e, g_let); } -bool is_have_annotation(expr const & e) { return is_annotation(e, g_have); } +name const & get_let_name() { + static name g_let("let"); + static register_annotation_fn g_let_annotation(g_let); + return g_let; +} + +name const & get_have_name() { + static name g_have("have"); + static register_annotation_fn g_have_annotation(g_have); + return g_have; +} +static name g_let_name = get_let_name(); // force 'let' annotation to be registered +static name g_have_name = get_have_name(); // force 'have' annotation to be registered + +expr mk_let_annotation(expr const & e) { return mk_annotation(get_let_name(), e); } +expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); } +bool is_let_annotation(expr const & e) { return is_annotation(e, get_let_name()); } +bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); } } diff --git a/src/kernel/annotation.h b/src/kernel/annotation.h index fb9389a38..ac1369d2b 100644 --- a/src/kernel/annotation.h +++ b/src/kernel/annotation.h @@ -34,6 +34,11 @@ bool is_annotation(expr const & e, name const & kind); \post get_annotation_arg(mk_annotation(k, e)) == e */ expr const & get_annotation_arg(expr const & e); +/** \brief Return the king of the annotated expression, \c e must have been created using #mk_annotation. + + \post get_annotation_arg(mk_annotation(k, e)) == k +*/ +name const & get_annotation_kind(expr const & e); /** \brief Tag \c e as a 'let'-expression. 'let' is a pre-registered annotation. */ expr mk_let_annotation(expr const & e); diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 7d6d891a0..039c26dbd 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -10,20 +10,33 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" namespace lean { -static name g_explicit_name("@"); -static name g_implicit_name("@^-1"); -static name g_as_is_name("as_is"); +name const & get_explicit_name() { + static name g_explicit_name("@"); + static register_annotation_fn g_explicit_annotation(g_explicit_name); + return g_explicit_name; +} -register_annotation_fn g_explicit_annotation(g_explicit_name); -register_annotation_fn g_implicit_annotation(g_implicit_name); -register_annotation_fn g_as_is_annotation(g_as_is_name); +name const & get_implicit_name() { + static name g_implicit_name("@^-1"); + static register_annotation_fn g_implicit_annotation(g_implicit_name); + return g_implicit_name; +} -expr mk_explicit(expr const & e) { return mk_annotation(g_explicit_name, e); } -bool is_explicit(expr const & e) { return is_annotation(e, g_explicit_name); } -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 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); } +name const & get_as_is_name() { + static name g_as_is_name("as_is"); + static register_annotation_fn g_as_is_annotation(g_as_is_name); + return g_as_is_name; +} +static name g_explicit_name = get_explicit_name(); // force '@' annotation to be registered +static name g_implicit_name = get_implicit_name(); // force '@^-1' annotation to be registered +static name g_as_is_name = get_as_is_name(); // force 'as_is' annotation to be registered + +expr mk_explicit(expr const & e) { return mk_annotation(get_explicit_name(), e); } +bool is_explicit(expr const & e) { return is_annotation(e, get_explicit_name()); } +expr mk_as_is(expr const & e) { return mk_annotation(get_as_is_name(), e); } +bool is_as_is(expr const & e) { return is_annotation(e, get_as_is_name()); } +expr mk_implicit(expr const & e) { return mk_annotation(get_implicit_name(), e); } +bool is_implicit(expr const & e) { return is_annotation(e, get_implicit_name()); } expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); } expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); } expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); }