From cf35c077865e39448f9c724f780b28aff7fb2bae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Jul 2014 21:00:22 -0700
Subject: [PATCH] fix(frontends/lean): fix 'let' annotation placement and
 pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp |  4 ++--
 src/frontends/lean/pp.cpp            | 31 ++++++++++++++--------------
 tests/lean/let1.lean.expected.out    | 24 +++++++++++----------
 3 files changed, 30 insertions(+), 29 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index f36dd63a3..97dc2249f 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -55,8 +55,8 @@ static expr parse_let_body(parser & p, pos_info const & pos) {
 }
 
 static expr mk_let(parser & p, name const & id, expr const & t, expr const & v, expr const & b, pos_info const & pos, binder_info const & bi) {
-    expr l = p.save_pos(mk_lambda(id, t, b, bi), pos);
-    return p.save_pos(mk_let_annotation(p.save_pos(mk_app(l, v), pos)), pos);
+    expr l = p.save_pos(mk_let_annotation(p.save_pos(mk_lambda(id, t, b, bi), pos)), pos);
+    return p.mk_app(l, v, pos);
 }
 
 static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) {
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 3954f8cfd..297d772a6 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -298,16 +298,17 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
     }
 }
 
+static bool is_let(expr const & e) {
+    return is_app(e) && is_let_annotation(app_fn(e));
+}
+
 auto pretty_fn::pp_let(expr e) -> result {
     buffer<expr_pair> decls;
     while (true) {
-        if (!is_let_annotation(e))
-            break;
-        e = get_annotation_arg(e);
-        if (!is_app(e) || !is_lambda(app_fn(e)))
+        if (!is_let(e))
             break;
         expr v = app_arg(e);
-        auto p = binding_body_fresh(app_fn(e), true);
+        auto p = binding_body_fresh(get_annotation_arg(app_fn(e)), true);
         decls.emplace_back(p.second, v);
         e = p.first;
     }
@@ -332,17 +333,13 @@ auto pretty_fn::pp_let(expr e) -> result {
 }
 
 auto pretty_fn::pp_macro(expr const & e) -> result {
-    if (is_let_annotation(e)) {
-        return pp_let(e);
-    } else {
-        // TODO(Leo): have macro annotations
-        // fix macro<->pp interface
-        format r = compose(format("["), format(macro_def(e).get_name()));
-        for (unsigned i = 0; i < macro_num_args(e); i++)
-            r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).first));
-        r += format("]");
-        return mk_result(group(r));
-    }
+    // TODO(Leo): have macro annotations
+    // fix macro<->pp interface
+    format r = compose(format("["), format(macro_def(e).get_name()));
+    for (unsigned i = 0; i < macro_num_args(e); i++)
+        r += nest(m_indent, compose(line(), pp_child(macro_arg(e, i), max_bp()).first));
+    r += format("]");
+    return mk_result(group(r));
 }
 
 auto pretty_fn::pp(expr const & e) -> result {
@@ -353,6 +350,8 @@ auto pretty_fn::pp(expr const & e) -> result {
 
     if (is_placeholder(e))
         return mk_result(g_placeholder_fmt);
+    if (is_let(e))
+        return pp_let(e);
 
     switch (e.kind()) {
     case expr_kind::Var:       return pp_var(e);
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index d08ac4f68..ad69fd3e1 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -14,17 +14,19 @@ in and_intro :
   ∀ (p q : Prop),
     p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
 let1.lean:16:10: error: type mismatch at application
-  (λ (and_intro : ∀ (p q : Prop), p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p),
-     let and_elim_left : ∀ (p q : Prop),
-                           (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
-           λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-             H p (λ (H1 : p) (H2 : q), H1),
-         and_elim_right : ∀ (p q : Prop),
-                            (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
-           λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
-             H q (λ (H1 : p) (H2 : q), H2)
-     in and_intro)
-    (λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c), H H1 H2)
+  let and_intro : ∀ (p q : Prop),
+                    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
+        λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+          H H1 H2,
+      and_elim_left : ∀ (p q : Prop),
+                        (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
+        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
+          H p (λ (H1 : p) (H2 : q), H1),
+      and_elim_right : ∀ (p q : Prop),
+                         (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
+        λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
+          H q (λ (H1 : p) (H2 : q), H2)
+  in and_intro
 expected type:
   ∀ (p q : Prop),
     p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p