feat(frontends/lean): annotate 'notation' subterms with 'noinfo' annotation (goal: improve typeinfo generation); fix initialization problem (with annotations)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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<std::unique_ptr<info_data>> 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<info_data>(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<bool> let(m_noinfo, true);
+            return visit(get_annotation_arg(e));
         } else {
             switch (e.kind()) {
             case expr_kind::Local:      return e;

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()); }
+}

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);
+}

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<expr> 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<name> const & terminator, bool right, unsigned rbp) {
+action mk_exprs_action(name const & sep, expr const & rec, expr const & ini,
+                       optional<name> 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<transition> & ts, std::function<void(unsigned, transition const *, list<expr> const &)> const & fn) const {

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<name, macro_definition, name_hash, name_eq> annotation_macros;
-static std::unique_ptr<annotation_macros> g_annotation_macros;
 annotation_macros & get_annotation_macros() {
+    static std::unique_ptr<annotation_macros> 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<annotation_macro_definition_cell const*>(macro_def(e).raw())->get_annotation_kind();
 }
 
 bool is_annotation(expr const & e, name const & kind) {
-    return is_annotation(e) && static_cast<annotation_macro_definition_cell const*>(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()); }
 }

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);

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); }