feat(frontends/lean): parameter and variable binder type update

see issue #532

src/frontends/lean/decl_cmds.cpp

@@ -182,6 +182,29 @@ static void check_variable_kind(parser & p, variable_kind k) {
     }
 }
 
+static void update_local_binder_info(parser & p, variable_kind k, name const & n,
+                                     optional<binder_info> const & bi, pos_info const & pos) {
+    binder_info new_bi;
+    if (bi) new_bi = *bi;
+    if (k == variable_kind::Parameter) {
+        if (p.is_local_variable(n))
+            throw parser_error(sstream() << "invalid parameter binder type update, '"
+                               << n << "' is a variable", pos);
+        if (!p.update_local_binder_info(n, new_bi))
+            throw parser_error(sstream() << "invalid parameter binder type update, '"
+                               << n << "' is not a parameter", pos);
+    } else {
+        if (!p.update_local_binder_info(n, new_bi) || !p.is_local_variable(n))
+            throw parser_error(sstream() << "invalid variable binder type update, '"
+                               << n << "' is not a variable", pos);
+    }
+}
+
+static bool curr_is_binder_annotation(parser & p) {
+    return p.curr_is_token(get_lparen_tk()) || p.curr_is_token(get_lcurly_tk()) ||
+           p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk());
+}
+
 static environment variable_cmd_core(parser & p, variable_kind k, bool is_protected = false) {
     check_variable_kind(p, k);
     auto pos = p.pos();
@@ -196,12 +219,18 @@ static environment variable_cmd_core(parser & p, variable_kind k, bool is_protec
     parse_univ_params(p, ls_buffer);
     expr type;
     if (!p.curr_is_token(get_colon_tk())) {
-        buffer<expr> ps;
+        if (!curr_is_binder_annotation(p) && (k == variable_kind::Parameter || k == variable_kind::Variable)) {
-        unsigned rbp = 0;
+            p.parse_close_binder_info(bi);
-        auto lenv = p.parse_binders(ps, rbp);
+            update_local_binder_info(p, k, n, bi, pos);
-        p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
+            return p.env();
-        type = p.parse_scoped_expr(ps, lenv);
+        } else {
-        type = Pi(ps, type, p);
+            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();
@@ -242,11 +271,29 @@ 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_token(get_colon_tk())) {
+    while (p.curr_is_identifier()) {
-        name id = p.check_id_next("invalid parameters declaration, identifier expected");
+        name id = p.get_name_val();
+        p.next();
         ids.push_back(id);
     }
-    p.next();
+
+    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)
         scope1.emplace(p);
@@ -266,8 +313,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, bool is_prote
         new_ls = append(ls, new_ls);
         env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, is_protected);
     }
-    if (p.curr_is_token(get_lparen_tk()) || p.curr_is_token(get_lcurly_tk()) ||
+    if (curr_is_binder_annotation(p)) {
-        p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk())) {
         if (k == variable_kind::Constant || k == variable_kind::Axiom) {
             // Hack: temporarily update the parser environment.
             // We must do that to be able to process

src/frontends/lean/local_decls.h

@@ -36,6 +36,12 @@ public:
         m_counter++;
         m_entries = cons(mk_pair(k, v), m_entries);
     }
+    void update(name const & k, V const & v) {
+        if (auto it = m_map.find(k))
+            m_map.insert(k, mk_pair(v, it->second));
+        else
+            lean_unreachable();
+    }
     V const * find(name const & k) const { auto it = m_map.find(k); return it ? &(it->first) : nullptr; }
     unsigned find_idx(name const & k) const { auto it = m_map.find(k); return it ? it->second : 0; }
     bool contains(name const & k) const { return m_map.contains(k); }

src/frontends/lean/parser.cpp

@@ -515,6 +515,14 @@ void parser::add_parameter(name const & n, expr const & p) {
     m_has_params = true;
 }
 
+bool parser::update_local_binder_info(name const & n, binder_info const & bi) {
+    auto it = get_local(n);
+    if (!it) return false;
+    if (!is_local(*it)) return false;
+    m_local_decls.update(n, update_local(*it, bi));
+    return true;
+}
+
 unsigned parser::get_local_level_index(name const & n) const {
     return m_local_level_decls.find_idx(n);
 }

src/frontends/lean/parser.h

@@ -408,6 +408,8 @@ public:
     bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); }
     bool is_local_variable(name const & n) const { return m_variables.contains(n); }
     bool is_local_variable(expr const & e) const { return is_local_variable(local_pp_name(e)); }
+    /** \brief Update binder information for the section parameter n, return true if success, and false if n is not a section parameter. */
+    bool update_local_binder_info(name const & n, binder_info const & bi);
     void include_variable(name const & n) { m_include_vars.insert(n); }
     void omit_variable(name const & n) { m_include_vars.erase(n); }
     bool is_include_variable(name const & n) const { return m_include_vars.contains(n); }

tests/lean/param_binder_update.lean

@@ -0,0 +1,83 @@
+section
+  parameter {A : Type}
+
+  parameter A
+
+  definition id (a : A) := a
+
+  parameter {A}
+
+  definition id₂ (a : A) := a
+end
+
+check @id
+check @id₂
+
+section
+  parameters {A : Type} {B : Type}
+
+  definition foo1 (a : A) (b : B) := a
+
+  parameters {A} (B)
+
+  definition foo2 (a : A) (b : B) := a
+
+  parameters (A) {B}
+
+  definition foo3 (a : A) (b : B) := a
+
+  parameters (A) (B)
+
+  definition foo4 (a : A) (b : B) := a
+
+  check @foo1
+  check @foo2
+  -- check @foo3 -- TODO
+  check @foo4
+end
+
+check @foo1
+check @foo2
+check @foo3
+check @foo4
+
+section
+  variables {A : Type} {B : Type}
+
+  definition boo1 (a : A) (b : B) := a
+
+  variables {A} (B)
+
+  definition boo2 (a : A) (b : B) := a
+
+  variables (A) {B}
+
+  definition boo3 (a : A) (b : B) := a
+
+  variables (A) (B)
+
+  definition boo4 (a : A) (b : B) := a
+
+  check @boo1
+  check @boo2
+  check @boo3
+  check @boo4
+end
+
+section
+  variables {A : Type} {B : Type}
+
+  parameter (A) -- ERROR
+  variable (C)  -- ERROR
+  variables (C) (D) -- ERROR
+  variables C -- ERROR
+
+  definition id3 (a : A) := a
+
+  parameter id3 -- ERROR
+
+  parameter (C : Type)
+
+  variables {C}  -- ERROR
+
+end

tests/lean/param_binder_update.lean.expected.out

@@ -0,0 +1,19 @@
+id : Π (A : Type), A → A
+id₂ : Π {A : Type}, A → A
+foo1 : A → B → A
+foo2 : A → B → A
+foo4 : A → B → A
+foo1 : Π {A : Type} {B : Type}, A → B → A
+foo2 : Π {A : Type} (B : Type), A → B → A
+foo3 : Π (A : Type) {B : Type}, A → B → A
+foo4 : Π (A : Type) (B : Type), A → B → A
+boo1 : Π {A : Type} {B : Type}, A → B → A
+boo2 : Π {A : Type} (B : Type), A → B → A
+boo3 : Π (A : Type) {B : Type}, A → B → A
+boo4 : Π (A : Type) (B : Type), A → B → A
+param_binder_update.lean:70:12: error: invalid parameter binder type update, 'A' is a variable
+param_binder_update.lean:71:11: error: invalid variable binder type update, 'C' is not a variable
+param_binder_update.lean:72:12: error: invalid variable binder type update, 'C' is not a variable
+param_binder_update.lean:73:12: error: invalid variable binder type update, 'C' is not a variable
+param_binder_update.lean:77:12: error: invalid parameter binder type update, 'id3' is not a parameter
+param_binder_update.lean:81:12: error: invalid variable binder type update, 'C' is not a variable