feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer

library/data/list/basic.lean

@@ -17,6 +17,7 @@ cons   : T → list T → list T
 
 namespace list
 infixr `::` := cons
+notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
 variable {T : Type}
 
@@ -32,9 +33,6 @@ protected definition rec_on {A : Type} {C : list A → Type} (l : list A)
     (H1 : C nil) (H2 : Π (h : A) (t : list A), C t → C (h::t)) : C l :=
   rec H1 H2 l
 
-notation `[` l:(foldr `,` (h t, h::t) nil) `]` := l
-
-
 -- Concat
 -- ------
 

src/frontends/lean/pp.cpp

@@ -728,6 +728,56 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                 }
                 break;
             case notation::action_kind::Exprs:
+                if (args.empty() || !args.back()) {
+                    return optional<result>();
+                } else {
+                    expr e = *args.back();
+                    args.pop_back();
+                    expr const & rec = a.get_rec();
+                    expr const & ini = a.get_initial();
+                    buffer<expr> rec_args;
+                    bool matched_once = false;
+                    while (true) {
+                        args.resize(args.size() + 2);
+                        if (!match(rec, e, args)) {
+                            args.pop_back();
+                            args.pop_back();
+                            break;
+                        }
+                        matched_once = true;
+                        optional<expr> new_e = args.back();
+                        args.pop_back();
+                        optional<expr> rec_arg = args.back();
+                        args.pop_back();
+                        if (!new_e || !rec_arg)
+                            return optional<result>();
+                        rec_args.push_back(*rec_arg);
+                        e = *new_e;
+                    }
+                    if (!matched_once)
+                        return optional<result>();
+                    if (!match(ini, e, args))
+                        return optional<result>();
+                    if (!a.is_fold_right())
+                        std::reverse(rec_args.begin(), rec_args.end());
+                    unsigned curr_lbp = token_lbp;
+                    if (auto t = a.get_terminator()) {
+                        curr = format(*t);
+                        curr_lbp = get_some_precedence(m_token_table, *t);
+                    }
+                    unsigned i       = rec_args.size();
+                    format sep_fmt   = format(a.get_sep());
+                    unsigned sep_lbp = get_some_precedence(m_token_table, a.get_sep());
+                    while (i > 0) {
+                        --i;
+                        result arg_res = pp_notation_child(rec_args[i], curr_lbp, a.rbp());
+                        if (i == 0)
+                            sep_fmt = format(tk);
+                        curr = sep_fmt + space() + arg_res.fmt() + space() + curr;
+                        curr_lbp = sep_lbp;
+                    }
+                    break;
+                }
             case notation::action_kind::Binder:
             case notation::action_kind::Binders:
             case notation::action_kind::ScopedExpr:

tests/lean/notation2.lean

@@ -1,5 +1,5 @@
 import data.list data.num
 open list
-
+infixr `::` := cons
 check 1 :: 2 :: nil
 check 1 :: 2 :: 3 :: 4 :: 5 :: nil

tests/lean/notation3.lean

@@ -0,0 +1,7 @@
+import data.prod data.list data.num
+open list prod num
+constants a b : num
+check [a, b, b]
+check (a, true, a = b, b)
+check (a, b)
+check [1, 2+2, 3]

tests/lean/notation3.lean.expected.out

@@ -0,0 +1,5 @@
+notation3.lean:2:0: warning: imported file uses 'sorry'
+[ a , b , b  ] : list num
+( a , true , a = b , b  ) : num × Prop × Prop × num
+( a , b  ) : num × num
+[ 1 , 2 + 2 , 3  ] : list num

tests/lean/t10.lean.expected.out

@@ -7,6 +7,6 @@ has type
   B
 but is expected to have type
   N
-cons x (cons y (cons z (cons x (cons y (cons y nil))))) : list
-cons x nil : list
+[ x , y , z , x , y , y  ] : list
+[ x  ] : list
 [ ] : list