feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included)

src/frontends/lean/decl_cmds.cpp

@@ -222,31 +222,65 @@ static environment variable_cmd_core(parser & p, variable_kind k, bool is_protec
     check_variable_kind(p, k);
     auto pos = p.pos();
     optional<binder_info> bi = parse_binder_info(p, k);
-    name n = p.check_decl_id_next("invalid declaration, identifier expected");
-    buffer<name> ls_buffer;
-    if (p.curr_is_token(get_llevel_curly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable))
-        throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
     optional<parser::local_scope> scope1;
-    if (k == variable_kind::Constant || k == variable_kind::Axiom)
+    name n;
-        scope1.emplace(p);
-    parse_univ_params(p, ls_buffer);
     expr type;
-    if (!p.curr_is_token(get_colon_tk())) {
+    buffer<name> ls_buffer;
-        if (!curr_is_binder_annotation(p) && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
+    if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
-            p.parse_close_binder_info(bi);
+        /* instance implicit */
-            update_local_binder_info(p, k, n, bi, pos);
+        if (p.curr_is_identifier()) {
-            return p.env();
+            auto n_pos = p.pos();
+            n = p.get_name_val();
+            p.next();
+            if (p.curr_is_token(get_colon_tk())) {
+                /* simple decl: variable [decA : decidable A] */
+                p.next();
+                type = p.parse_expr();
+            } else if (p.curr_is_token(get_rbracket_tk())) {
+                /* annotation update: variable [decA] */
+                p.parse_close_binder_info(bi);
+                update_local_binder_info(p, k, n, bi, pos);
+                return p.env();
+            } else {
+                /* anonymous : variable [decidable A] */
+                expr left    = p.id_to_expr(n, n_pos);
+                n            = p.mk_anonymous_inst_name();
+                unsigned rbp = 0;
+                while (rbp < p.curr_expr_lbp()) {
+                    left = p.parse_led(left);
+                }
+                type = left;
+            }
         } else {
-            buffer<expr> ps;
+            /* anonymous : variable [forall x y, decidable (x = y)] */
-            unsigned rbp = 0;
+            n    = p.mk_anonymous_inst_name();
-            auto lenv = p.parse_binders(ps, rbp);
+            type = p.parse_expr();
-            p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
-            type = p.parse_scoped_expr(ps, lenv);
-            type = Pi(ps, type, p);
         }
     } else {
-        p.next();
+        /* non instance implicit cases */
-        type = p.parse_expr();
+        n = p.check_decl_id_next("invalid declaration, identifier expected");
+        if (p.curr_is_token(get_llevel_curly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable))
+            throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
+        if (k == variable_kind::Constant || k == variable_kind::Axiom)
+            scope1.emplace(p);
+        parse_univ_params(p, ls_buffer);
+        if (!p.curr_is_token(get_colon_tk())) {
+            if (!curr_is_binder_annotation(p) && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
+                p.parse_close_binder_info(bi);
+                update_local_binder_info(p, k, n, bi, pos);
+                return p.env();
+            } else {
+                buffer<expr> ps;
+                unsigned rbp = 0;
+                auto lenv = p.parse_binders(ps, rbp);
+                p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
+                type = p.parse_scoped_expr(ps, lenv);
+                type = Pi(ps, type, p);
+            }
+        } else {
+            p.next();
+            type = p.parse_expr();
+        }
     }
     p.parse_close_binder_info(bi);
     check_command_period_or_eof(p);
@@ -284,34 +318,75 @@ static environment variables_cmd_core(parser & p, variable_kind k, bool is_prote
 
     optional<binder_info> bi = parse_binder_info(p, k);
     buffer<name> ids;
-    while (p.curr_is_identifier()) {
-        name id = p.get_name_val();
-        p.next();
-        ids.push_back(id);
-    }
-
-    if (p.curr_is_token(get_colon_tk())) {
-        p.next();
-    } else {
-        if (k == variable_kind::Parameter || k == variable_kind::Variable) {
-            p.parse_close_binder_info(bi);
-            for (name const & id : ids) {
-                update_local_binder_info(p, k, id, bi, pos);
-            }
-            if (curr_is_binder_annotation(p))
-                return variables_cmd_core(p, k);
-            else
-                return env;
-        } else {
-            throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos);
-        }
-    }
-
     optional<parser::local_scope> scope1;
-    if (k == variable_kind::Constant || k == variable_kind::Axiom)
+    expr type;
-        scope1.emplace(p);
+    if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
-    expr type = p.parse_expr();
+        /* instance implicit */
+        if (p.curr_is_identifier()) {
+            auto id_pos = p.pos();
+            name id = p.get_name_val();
+            p.next();
+            if (p.curr_is_token(get_colon_tk())) {
+                /* simple decl: variables [decA : decidable A] */
+                p.next();
+                ids.push_back(id);
+                type = p.parse_expr();
+            } else if (p.curr_is_token(get_rbracket_tk())) {
+                /* annotation update: variables [decA] */
+                p.parse_close_binder_info(bi);
+                update_local_binder_info(p, k, id, bi, pos);
+                if (curr_is_binder_annotation(p))
+                    return variables_cmd_core(p, k);
+                else
+                    return env;
+            } else {
+                /* anonymous : variables [decidable A] */
+                expr left    = p.id_to_expr(id, id_pos);
+                id           = p.mk_anonymous_inst_name();
+                unsigned rbp = 0;
+                while (rbp < p.curr_expr_lbp()) {
+                    left = p.parse_led(left);
+                }
+                ids.push_back(id);
+                type = left;
+            }
+        } else {
+            /* anonymous : variables [forall x y, decidable (x = y)] */
+            name id = p.mk_anonymous_inst_name();
+            ids.push_back(id);
+            type = p.parse_expr();
+        }
+    } else {
+        /* non instance implicit cases */
+        while (p.curr_is_identifier()) {
+            name id = p.get_name_val();
+            p.next();
+            ids.push_back(id);
+        }
+        if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+        } else {
+            /* binder annotation update */
+            /* example: variables (A) */
+            if (k == variable_kind::Parameter || k == variable_kind::Variable) {
+                p.parse_close_binder_info(bi);
+                for (name const & id : ids) {
+                    update_local_binder_info(p, k, id, bi, pos);
+                }
+                if (curr_is_binder_annotation(p))
+                    return variables_cmd_core(p, k);
+                else
+                    return env;
+            } else {
+                throw parser_error("invalid variables/constants/axioms declaration, ':' expected", pos);
+            }
+        }
+        if (k == variable_kind::Constant || k == variable_kind::Axiom)
+            scope1.emplace(p);
+        type = p.parse_expr();
+    }
     p.parse_close_binder_info(bi);
+
     level_param_names ls = to_level_param_names(collect_univ_params(type));
     list<expr> ctx = p.locals_to_context();
     for (auto id : ids) {

src/frontends/lean/parser.cpp

@@ -425,6 +425,14 @@ name parser::mk_anonymous_inst_name() {
     return n;
 }
 
+bool parser::is_anonymous_inst_name(name const & n) const {
+    return
+        n.is_atomic() &&
+        n.is_string() &&
+        strlen(n.get_string()) >= strlen(g_anonymous_inst_name_prefix->get_string()) &&
+        memcmp(n.get_string(), g_anonymous_inst_name_prefix->get_string(), strlen(g_anonymous_inst_name_prefix->get_string())) == 0;
+}
+
 expr parser::save_pos(expr e, pos_info p) {
     auto t = get_tag(e);
     if (!m_pos_table.contains(t))
@@ -1067,7 +1075,8 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsign
     }
 }
 
-void parser::parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi) {
+expr parser::parse_inst_implicit_decl() {
+    binder_info bi = mk_inst_implicit_binder_info();
     auto id_pos = pos();
     name id;
     expr type;
@@ -1093,6 +1102,12 @@ void parser::parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi)
     save_identifier_info(id_pos, id);
     expr local = save_pos(mk_local(id, type, bi), id_pos);
     add_local(local);
+    return local;
+}
+
+
+void parser::parse_inst_implicit_decl(buffer<expr> & r) {
+    expr local = parse_inst_implicit_decl();
     r.push_back(local);
 }
 
@@ -1115,7 +1130,7 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
                 rbp = 0;
                 last_block_delimited = true;
                 if (bi->is_inst_implicit()) {
-                    parse_inst_implicit_decl(r, *bi);
+                    parse_inst_implicit_decl(r);
                 } else {
                     if (simple_only || !parse_local_notation_decl(nentries))
                         parse_binder_block(r, *bi, rbp);

src/frontends/lean/parser.h

@@ -187,8 +187,6 @@ class parser {
     tag get_tag(expr e);
     expr copy_with_new_pos(expr const & e, pos_info p);
 
-    name mk_anonymous_inst_name();
-
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
     parse_table const & tactic_nud() const { return get_tactic_nud_table(env()); }
@@ -221,7 +219,8 @@ class parser {
     expr parse_numeral_expr(bool user_notation = true);
     expr parse_decimal_expr();
     expr parse_string_expr();
-    void parse_inst_implicit_decl(buffer<expr> & r, binder_info const & bi);
+    expr parse_inst_implicit_decl();
+    void parse_inst_implicit_decl(buffer<expr> & r);
     expr parse_binder_core(binder_info const & bi, unsigned rbp);
     void parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp);
     void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only);
@@ -286,6 +285,9 @@ public:
     bool ignore_noncomputable() const { return m_ignore_noncomputable; }
     void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
 
+    name mk_anonymous_inst_name();
+    bool is_anonymous_inst_name(name const & n) const;
+
     unsigned curr_expr_lbp() const { return curr_lbp_core(false); }
     unsigned curr_tactic_lbp() const { return curr_lbp_core(true); }
 

src/frontends/lean/util.cpp

@@ -128,6 +128,24 @@ static void collect_locals_ignoring_tactics(expr const & e, collected_locals & l
         });
 }
 
+static void collect_annonymous_inst_implicit(parser const & p, collected_locals & ls) {
+    for (auto const & entry : p.get_local_entries()) {
+        if (is_local(entry.second) && !ls.contains(entry.second) && local_info(entry.second).is_inst_implicit() &&
+            // remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones.
+            p.is_anonymous_inst_name(entry.first)) {
+            bool ok = true;
+            for_each(mlocal_type(entry.second), [&](expr const & e, unsigned) {
+                    if (!ok) return false; // stop
+                    if (is_local(e) && !ls.contains(e))
+                        ok = false;
+                    return true;
+                });
+            if (ok)
+                ls.insert(entry.second);
+        }
+    }
+}
+
 // Collect local constants occurring in type and value, sort them, and store in ctx_ps
 void collect_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & ctx_ps) {
     collected_locals ls;
@@ -141,6 +159,7 @@ void collect_locals(expr const & type, expr const & value, parser const & p, buf
     }
     collect_locals_ignoring_tactics(type, ls);
     collect_locals_ignoring_tactics(value, ls);
+    collect_annonymous_inst_implicit(p, ls);
     sort_locals(ls.get_collected(), p, ctx_ps);
 }
 
@@ -187,6 +206,7 @@ levels remove_local_vars(parser const & p, levels const & ls) {
 list<expr> locals_to_context(expr const & e, parser const & p) {
     collected_locals ls;
     collect_locals_ignoring_tactics(e, ls);
+    collect_annonymous_inst_implicit(p, ls);
     buffer<expr> locals;
     sort_locals(ls.get_collected(), p, locals);
     std::reverse(locals.begin(), locals.end());

tests/lean/auto_include.lean

@@ -0,0 +1,32 @@
+import algebra.group
+open algebra
+
+section
+variables {A : Type} [group A]
+variables {B : Type} [group B]
+
+definition foo (a b : A) : a * b = b * a :=
+sorry
+
+definition bla (b : B) : b * 1 = b :=
+sorry
+
+print foo
+print bla
+end
+
+section
+variable {A : Type}
+variable [group A]
+variable {B : Type}
+variable [group B]
+
+definition foo2 (a b : A) : a * b = b * a :=
+sorry
+
+definition bla2 (b : B) : b * 1 = b :=
+sorry
+
+print foo2
+print bla2
+end

tests/lean/auto_include.lean.expected.out

@@ -0,0 +1,8 @@
+definition foo : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
+λ (A : Type) (_inst_1 : group A) (a b : A), sorry
+definition bla : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
+λ (B : Type) (_inst_2 : group B) (b : B), sorry
+definition foo2 : ∀ {A : Type} [_inst_1 : group A] (a b : A), a * b = b * a :=
+λ (A : Type) (_inst_1 : group A) (a b : A), sorry
+definition bla2 : ∀ {B : Type} [_inst_2 : group B] (b : B), b * 1 = b :=
+λ (B : Type) (_inst_2 : group B) (b : B), sorry

tests/lean/run/t11.lean

@@ -5,7 +5,7 @@ check f a b
 section
   parameters A B : Type
   parameters {C D : Type}
-  parameters [e d : A]
+  parameters [e : A] [d : A]
   check A
   check B
   definition g (a : A) (b : B) (c : C) : A := e