fix(frontends/lean/pp): pretty print 'let-expressions', closes #87

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 #include "library/typed_expr.h"
 #include "library/choice.h"
+#include "library/let.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
@@ -71,7 +72,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
     if (p.parse_local_notation_decl()) {
         return parse_let_body(p, pos);
     } else {
-        auto pos = p.pos();
+        auto id_pos = p.pos();
         name id  = p.check_atomic_id_next("invalid let declaration, identifier expected");
         bool is_fact   = false;
         optional<expr> type;
@@ -103,9 +104,10 @@ static expr parse_let(parser & p, pos_info const & pos) {
             v = p.save_pos(mk_typed_expr(*type, value), p.pos_of(value));
         else
             v = value;
-        v = p.save_pos(mk_let_value_annotation(v), pos);
+        v = p.save_pos(mk_let_value_annotation(v), id_pos);
         p.add_local_expr(id, v);
-        return parse_let_body(p, pos);
+        expr b = parse_let_body(p, pos);
+        return p.save_pos(mk_let(id, v, b), pos);
     }
 }
 

src/frontends/lean/pp.cpp

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #include "util/flet.h"
 #include "kernel/replace_fn.h"
 #include "kernel/free_vars.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 #include "library/annotation.h"
 #include "library/aliases.h"
 #include "library/scoped_ext.h"
@@ -17,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/typed_expr.h"
 #include "library/num.h"
+#include "library/let.h"
 #include "library/print.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/pp_options.h"
@@ -375,6 +378,50 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
     }
 }
 
+auto pretty_fn::pp_let(expr e) -> result {
+    buffer<std::tuple<name, optional<expr>, expr>> decls;
+    while (true) {
+        if (!is_let(e))
+            break;
+        name n   = get_let_var_name(e);
+        expr v   = get_let_value(e);
+        expr b   = get_let_body(e);
+        lean_assert(closed(b));
+        expr b1  = abstract(b, v);
+        if (closed(b1)) {
+            e = b1;
+        } else {
+            n = pick_unused_name(b1, n);
+            if (is_typed_expr(v))
+                decls.emplace_back(n, some_expr(get_typed_expr_type(v)), get_typed_expr_expr(v));
+            else
+                decls.emplace_back(n, none_expr(), v);
+            e = instantiate(b1, mk_constant(n));
+        }
+    }
+    if (decls.empty())
+        return pp(e);
+    format r    = g_let_fmt;
+    unsigned sz = decls.size();
+    for (unsigned i = 0; i < sz; i++) {
+        name n; optional<expr> t; expr v;
+        std::tie(n, t, v) = decls[i];
+        format beg        = i == 0 ? space() : line();
+        format sep        = i < sz - 1 ? comma() : format();
+        format entry      = format(n);
+        if (t) {
+            format t_fmt = pp_child(*t, 0).first;
+            entry += space() + colon() + nest(n.size() + 1 + 1 + 1, space() + t_fmt);
+        }
+        format v_fmt = pp_child(v, 0).first;
+        entry += space() + g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
+        r += nest(3 + 1, beg + group(entry));
+    }
+    format b = pp_child(e, 0).first;
+    r += line() + g_in_fmt + space() + nest(2 + 1, b);
+    return mk_result(r, 0);
+}
+
 auto pretty_fn::pp_num(mpz const & n) -> result {
     return mk_result(format(n));
 }
@@ -388,6 +435,7 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_placeholder(e))  return mk_result(g_placeholder_fmt);
     if (is_show(e))         return pp_show(e);
     if (is_have(e))         return pp_have(e);
+    if (is_let(e))          return pp_let(e);
     if (is_typed_expr(e))   return pp(get_typed_expr_expr(e));
     if (auto n = to_num(e)) return pp_num(*n);
     if (!m_metavar_args && is_meta(e))

src/frontends/lean/pp.h

@@ -70,6 +70,7 @@ private:
     result pp_show(expr const & e);
     result pp_macro(expr const & e);
     result pp_explicit(expr const & e);
+    result pp_let(expr e);
     result pp_num(mpz const & n);
     void set_options_core(options const & o);
 

src/library/CMakeLists.txt

@@ -8,6 +8,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp
-  print.cpp annotation.cpp typed_expr.cpp)
+  print.cpp annotation.cpp typed_expr.cpp let.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/let.cpp

@@ -0,0 +1,76 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "kernel/expr.h"
+#include "library/kernel_serializer.h"
+
+namespace lean {
+static name g_let("let");
+std::string const & get_let_opcode() {
+    static std::string g_let_opcode("Let");
+    return g_let_opcode;
+}
+
+class let_macro_definition_cell : public macro_definition_cell {
+    name m_var_name;
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 2)
+            throw exception("invalid let expression");
+    }
+public:
+    let_macro_definition_cell(name const & n):m_var_name(n) {}
+    name const & get_var_name() const { return m_var_name; }
+    virtual name get_name() const { return g_let; }
+    virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
+        check_macro(m);
+        return arg_types[1];
+    }
+    virtual optional<expr> expand(expr const & m, extension_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 1));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_let_opcode());
+        s << m_var_name;
+    }
+};
+
+expr mk_let(name const & n, expr const & v, expr const & b) {
+    auto d = macro_definition(new let_macro_definition_cell(n));
+    expr args[2] = {v, b};
+    return mk_macro(d, 2, args);
+}
+
+bool is_let(expr const & e) {
+    return is_macro(e) && dynamic_cast<let_macro_definition_cell const *>(macro_def(e).raw()) != nullptr;
+}
+
+name const & get_let_var_name(expr const & e) {
+    lean_assert(is_let(e));
+    return static_cast<let_macro_definition_cell const *>(macro_def(e).raw())->get_var_name();
+}
+
+expr const & get_let_value(expr const & e) {
+    lean_assert(is_let(e));
+    return macro_arg(e, 0);
+}
+
+expr const & get_let_body(expr const & e) {
+    lean_assert(is_let(e));
+    return macro_arg(e, 1);
+}
+
+static register_macro_deserializer_fn
+let_des_fn(get_let_opcode(),
+               [](deserializer & d, unsigned num, expr const * args) {
+                   if (num != 2)
+                       throw corrupted_stream_exception();
+                   name n;
+                   d >> n;
+                   return mk_let(n, args[0], args[1]);
+           });
+}

src/library/let.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+expr mk_let(name const & n, expr const & v, expr const & b);
+bool is_let(expr const & e);
+name const & get_let_var_name(expr const & e);
+expr const & get_let_value(expr const & e);
+expr const & get_let_body(expr const & e);
+}

src/library/print.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
 #include "library/annotation.h"
+#include "library/let.h"
 #include "library/print.h"
 
 namespace lean {
@@ -18,7 +19,8 @@ bool is_used_name(expr const & t, name const & n) {
     return static_cast<bool>(
         find(t, [&](expr const & e, unsigned) {
                 return (is_constant(e) && const_name(e) == n)  // t has a constant named n
-                    || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)); // t has a local constant named n
+                    || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)) // t has a local constant named n
+                    || (is_let(e) && get_let_var_name(e) == n);
             }));
 }
 

src/library/print.h

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 namespace lean {
 /** \brief Return true iff \c t contains a constant named \c n or a local constant with named (pp or not) \c n */
 bool is_used_name(expr const & t, name const & n);
+name pick_unused_name(expr const & t, name const & s);
 /**
     \brief Return the body of the binding \c b, where variable #0 is replaced by a local constant with a "fresh" name.
     The name is considered fresh if it is not used by a constant or local constant occuring in the body of \c b.
@@ -19,9 +20,6 @@ bool is_used_name(expr const & t, name const & n);
 */
 pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type = false);
 
-/** \brief Return the body of the let-expression \c l, where variable #0 is replaced by a local constant with a "fresh" name. */
-pair<expr, expr> let_body_fresh(expr const & l, bool preserve_type = false);
-
 /** \brief Create a simple formatter object based on operator for "print" procedure.
 
     \remark The print procedure is only used for debugging purposes.

tests/lean/let1.lean.expected.out

@@ -1,10 +1,13 @@
-λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+let bool := Prop,
-  H H1 H2 :
+    and := λ (p q : bool), Π (c : bool), (p → q → c) → c,
+    and_intro := λ (p q : bool) (H1 : p) (H2 : q) (c : bool) (H : p → q → c), H H1 H2
+in and_intro :
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)
 let1.lean:19:19: error: type mismatch at term
   λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
-    H H1 H2has type
+    H H1 H2
+has type
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)
 but is expected to have type