feat(frontends/lean/parser): cute binders

src/frontends/lean/parser.cpp

@@ -1076,6 +1076,54 @@ expr parser::parse_binder(unsigned rbp) {
     }
 }
 
+/* Lean allow binders of the form <tt>ID_1 ... ID_n 'op' S</tt>
+   Where 'op' is an infix operator, and s an expression (i.e., "collection").
+   This notation expands to:
+     (ID_1 ... ID_n : _) (H_1 : ID_1 'op' S) ... (H_n : ID_n 'op' S)
+
+   This method return true if the next token is an infix operator,
+   and populates r with the locals above.
+*/
+bool parser::parse_binder_collection(buffer<pair<pos_info, name>> const & names, binder_info const & bi, buffer<expr> & r) {
+    if (!curr_is_keyword())
+        return false;
+    name tk = get_token_info().value();
+    list<pair<notation::transition, parse_table>> trans_list = led().find(tk);
+    if (length(trans_list) != 1)
+        return false;
+    pair<notation::transition, parse_table> const & p = head(trans_list);
+    list<notation::accepting> const & acc_lst = p.second.is_accepting();
+    if (length(acc_lst) != 1)
+        return false; // no overloading
+    notation::accepting const & acc = head(acc_lst);
+    lean_assert(!acc.get_postponed());
+    expr pred     = acc.get_expr();
+    unsigned rbp  = p.first.get_action().rbp();
+    next(); // consume tk
+    expr S        = parse_expr(rbp);
+    unsigned old_sz = r.size();
+    /* Add (ID_1 ... ID_n : _) to r */
+    for (auto p : names) {
+        expr arg_type = save_pos(mk_expr_placeholder(), p.first);
+        save_identifier_info(p.first, p.second);
+        expr local = save_pos(mk_local(p.second, arg_type, bi), p.first);
+        add_local(local);
+        r.push_back(local);
+    }
+    /* Add (H_1 : ID_1 'op' S) ... (H_n : ID_n 'op' S) */
+    unsigned i = old_sz;
+    for (auto p : names) {
+        expr ID      = r[i];
+        expr args[2] = {ID, S};
+        expr ID_op_S = instantiate_rev(pred, 2, args);
+        expr local = save_pos(mk_local("H", ID_op_S, bi), p.first);
+        add_local(local);
+        r.push_back(local);
+        i++;
+    }
+    return true;
+}
+
 /**
    \brief Parse <tt>ID ... ID ':' expr</tt>, where the expression
    represents the type of the identifiers.
@@ -1092,6 +1140,8 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsign
     if (curr_is_token(get_colon_tk())) {
         next();
         type = parse_expr(rbp);
+    } else if (parse_binder_collection(names, bi, r)) {
+        return;
     }
     for (auto p : names) {
         expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);

src/frontends/lean/parser.h

@@ -199,6 +199,7 @@ class parser : public pos_info_provider {
     expr parse_inst_implicit_decl();
     void parse_inst_implicit_decl(buffer<expr> & r);
     expr parse_binder_core(binder_info const & bi, unsigned rbp);
+    bool parse_binder_collection(buffer<pair<pos_info, name>> const & names, binder_info const & bi, buffer<expr> & r);
     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);
     local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited,

tests/lean/run/cute_binders.lean

@@ -0,0 +1,21 @@
+definition set (A : Type) := A → Prop
+definition mem {A : Type} (a : A) (s : set A) : Prop :=
+s a
+definition range (lower : nat) (upper : nat) : set nat :=
+λ a, lower ≤ a ∧ a ≤ upper
+infix ` ∈ ` := mem
+
+local notation `[` L `, ` U `]` := range L U
+
+variables s : set nat
+variables p : nat → nat → Prop
+
+
+-- check a ∈ s
+set_option pp.binder_types true
+check ∀ b c a ∈ s, a + b + c > 0
+-- ∀ (b c a : ℕ), b ∈ s → c ∈ s → a ∈ s → a + b + c > 0 : Prop
+check ∀ a < 5, p a (a+1)
+-- ∀ (a : ℕ), a < 5 → p a (a + 1) : Prop
+check ∀ a b ∈ [2, 3], p a b
+-- ∀ (a b : ℕ), a ∈ [2, 3] → b ∈ [2, 3] → p a b