From ed1afe26bdab1b84e84e2b61db06bb082adf189a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Oct 2014 12:48:34 -0700
Subject: [PATCH] feat(frontends/lean/pp): support scopedexpr notation in the
 pretty printer

---
 src/frontends/lean/pp.cpp              | 50 ++++++++++++++++++++++++--
 tests/lean/notation4.lean              |  7 ++++
 tests/lean/notation4.lean.expected.out |  5 +++
 tests/lean/t11.lean.expected.out       |  4 +--
 4 files changed, 61 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/notation4.lean
 create mode 100644 tests/lean/notation4.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 24a28f466..965901054 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -697,6 +697,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
     } else {
         using notation::transition;
         buffer<transition> ts;
+        buffer<expr> locals; // from scoped_expr
         to_buffer(entry.get_transitions(), ts);
         format fmt;
         unsigned i         = ts.size();
@@ -725,8 +726,8 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                     curr = format(tk) + space() + e_fmt;
                     if (last)
                         last_rbp = a.rbp();
+                    break;
                 }
-                break;
             case notation::action_kind::Exprs:
                 if (args.empty() || !args.back()) {
                     return optional<result>();
@@ -779,10 +780,53 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
                     break;
                 }
             case notation::action_kind::Binder:
+                if (locals.size() != 1)
+                    return optional<result>();
+                curr = format(tk) + pp_binders(locals);
+                break;
             case notation::action_kind::Binders:
+                curr = format(tk) + pp_binders(locals);
+                break;
             case notation::action_kind::ScopedExpr:
-                // TODO(Leo)
-                return optional<result>();
+                if (args.empty() || !args.back()) {
+                    return optional<result>();
+                } else {
+                    expr e            = *args.back();
+                    bool first_scoped = locals.empty();
+                    unsigned i = 0;
+                    args.pop_back();
+                    expr const & rec = a.get_rec();
+                    while (true) {
+                        args.resize(args.size() + 1);
+                        if (!match(rec, e, args) || !args.back()) {
+                            args.pop_back();
+                            break;
+                        }
+                        expr b = *args.back();
+                        args.pop_back();
+                        if (!((is_lambda(b) && a.use_lambda_abstraction()) ||
+                              (is_pi(b) && !a.use_lambda_abstraction()))) {
+                            break;
+                        }
+                        auto p = binding_body_fresh(b, true);
+                        if (first_scoped) {
+                            locals.push_back(p.second);
+                        } else {
+                            if (i >= locals.size() || locals[i] != p.second)
+                                return optional<result>();
+                        }
+                        e = p.first;
+                        i++;
+                    }
+                    if (locals.empty())
+                        return optional<result>();
+                    result e_r   = pp_notation_child(e, token_lbp, a.rbp());
+                    format e_fmt = e_r.fmt();
+                    curr = format(tk) + space() + e_fmt;
+                    if (last)
+                        last_rbp = a.rbp();
+                    break;
+                }
             case notation::action_kind::Ext:
             case notation::action_kind::LuaExt:
                 return optional<result>();
diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean
new file mode 100644
index 000000000..e5bf751c2
--- /dev/null
+++ b/tests/lean/notation4.lean
@@ -0,0 +1,7 @@
+import logic data.sigma data.list
+open sigma
+
+check ∃ (A : Type₁) (x y : A), x = y
+check ∃ (x : num), x = 0
+check Σ (x : num), x = 10
+check Σ (A : Type₁), list A
diff --git a/tests/lean/notation4.lean.expected.out b/tests/lean/notation4.lean.expected.out
new file mode 100644
index 000000000..93f054583
--- /dev/null
+++ b/tests/lean/notation4.lean.expected.out
@@ -0,0 +1,5 @@
+notation4.lean:2:0: warning: imported file uses 'sorry'
+∃ (A : Type₁) (x y : A) , x = y : Prop
+∃ (x : num) , x = 0 : Prop
+Σ (x : num) , x = 10 : Type₁
+Σ (A : Type₁) , list A : Type₂
diff --git a/tests/lean/t11.lean.expected.out b/tests/lean/t11.lean.expected.out
index 18d187d6d..d6f8a97a8 100644
--- a/tests/lean/t11.lean.expected.out
+++ b/tests/lean/t11.lean.expected.out
@@ -1,3 +1,3 @@
-Exists (λ (x : A), p x) : bool
-Exists (λ (x : A), Exists (λ (y : A), q x y)) : bool
+∃ (x : A) , p x : bool
+∃ (x y : A) , q x y : bool
 λ (x : A), x : A → A