feat(frontends/lean): add Haskell-like for converting infix notation into functions

Examples:

 qsort (<) [20, 5, 10, 3, 2, 14, 1]

 foldl (+) 0 [1, 2, 3]

src/frontends/lean/builtin_exprs.cpp

@@ -781,7 +781,59 @@ static void consume_rparen(parser_state & p) {
     p.check_token_next(get_rparen_tk(), "invalid expression, `)` expected");
 }
 
+/* Check whether notation such as (<) (+ 10) is applicable.
+   Like Haskell,
+     (<) is notation for (fun x y, x < y)
+     (+ 10) is notation for (fun x, x + 10)
+
+   This kind of notation is applicable when
+   1- The current token is a keyword.
+   2- There is no entry for this token in the nud table
+   3- There is an entry for this token in the led table,
+      and exactly one Expr transition to an accepting state.
+
+   If the notation is applicable, this function returns the accepting list.
+*/
+static list<notation::accepting> is_infix_paren_notation(parser_state & p) {
+    if (p.curr_is_keyword() &&
+        !p.nud().find(p.get_token_info().value())) {
+        list<pair<transition, parse_table>> ts = p.led().find(p.get_token_info().value());
+        if (ts && !tail(ts) && head(ts).second.is_accepting()) {
+            notation::action const & act = head(ts).first.get_action();
+            if (act.kind() == notation::action_kind::Expr) {
+                return head(ts).second.is_accepting();
+            }
+        }
+    }
+    return list<notation::accepting>();
+}
+
+static expr parse_infix_paren(parser_state & p, list<notation::accepting> const & accs, pos_info const & pos) {
+    expr args[2];
+    buffer<expr> vars;
+    args[0] = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
+    vars.push_back(args[0]);
+    p.next();
+    if (p.curr_is_token(get_rparen_tk())) {
+        p.next();
+        args[1] = mk_local(mk_fresh_name(), "_y", mk_expr_placeholder(), binder_info());
+        vars.push_back(args[1]);
+    } else {
+        args[1] = p.parse_expr();
+        consume_rparen(p);
+    }
+    buffer<expr> cs;
+    for (notation::accepting const & acc : accs) {
+        expr r = p.copy_with_new_pos(acc.get_expr(), pos);
+        r = Fun(vars, instantiate_rev(r, 2, args), p);
+        cs.push_back(r);
+    }
+    return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
+}
+
 static expr parse_lparen(parser_state & p, unsigned, expr const *, pos_info const & pos) {
+    if (auto accs = is_infix_paren_notation(p))
+        return parse_infix_paren(p, accs, pos);
     expr e = p.parse_expr();
     if (p.curr_is_token(get_comma_tk())) {
         buffer<expr> args;

src/frontends/lean/parser.h

@@ -94,10 +94,6 @@ class parser : public abstract_parser {
     void protected_call(std::function<void()> && f, std::function<void()> && sync);
 
     tag get_tag(expr e);
-    expr copy_with_new_pos(expr const & e, pos_info p);
-
-    parse_table const & nud() const { return get_nud_table(env()); }
-    parse_table const & led() const { return get_led_table(env()); }
 
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
@@ -241,6 +237,10 @@ public:
     expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
     expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
 
+    parse_table const & nud() const { return get_nud_table(env()); }
+    parse_table const & led() const { return get_led_table(env()); }
+    expr copy_with_new_pos(expr const & e, pos_info p);
+
     /** \brief Read the next token. */
     void scan();
     /** \brief Return the current token */

src/frontends/lean/token_table.cpp

@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
-         {"(*", 0}, {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
+         {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
          {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},

tests/lean/run/infix_paren.lean

@@ -0,0 +1,11 @@
+open list
+
+vm_eval filter (< 10) [20, 5, 10, 3, 2, 14, 1]
+vm_eval qsort (<) [20, 5, 10, 3, 2, 14, 1]
+vm_eval foldl (+) 0 [1, 2, 3]
+
+example : foldl (+) 0 [3, 4, 1] = 8 :=
+rfl
+
+example : foldl (*) 2 [3, 4, 1] = 24 :=
+rfl