fix(frontends/let): let-expression pretty printer

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

src/frontends/lean/builtin_exprs.cpp

@@ -104,7 +104,7 @@ 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), id_pos);
+        v = p.save_pos(mk_let_value(v), id_pos);
         p.add_local_expr(id, v);
         expr b = parse_let_body(p, pos);
         return p.save_pos(mk_let(id, v, b), pos);

src/frontends/lean/elaborator.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/opaque_hints.h"
 #include "library/locals.h"
+#include "library/let.h"
 #include "library/deep_copy.h"
 #include "library/typed_expr.h"
 #include "library/tactic/tactic.h"
@@ -1096,8 +1097,8 @@ public:
             cs += p->second;
             return p->first;
         } else {
-            auto ecs = visit(get_annotation_arg(e));
-            expr r = copy_tag(ecs.first, mk_let_value_annotation(ecs.first));
+            auto ecs = visit(get_let_value_expr(e));
+            expr r = copy_tag(ecs.first, mk_let_value(ecs.first));
             m_cache.insert(e, mk_pair(r, ecs.second));
             cs += ecs.second;
             return r;
@@ -1109,7 +1110,7 @@ public:
             return visit_placeholder(e, cs);
         } else if (is_choice(e)) {
             return visit_choice(e, none_expr(), cs);
-        } else if (is_let_value_annotation(e)) {
+        } else if (is_let_value(e)) {
             return visit_let_value(e, cs);
         } else if (is_by(e)) {
             return visit_by(e, none_expr(), cs);

src/frontends/lean/parser.cpp

@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/explicit.h"
-#include "library/annotation.h"
+#include "library/let.h"
 #include "library/num.h"
 #include "library/string.h"
 #include "library/sorry.h"
@@ -282,7 +282,7 @@ expr parser::rec_save_pos(expr const & e, pos_info p) {
 
 /** \brief Create a copy of \c e, and the position of new expression with p */
 expr parser::copy_with_new_pos(expr const & e, pos_info p) {
-    if (is_let_value_annotation(e))
+    if (is_let_value(e))
         return e;
     switch (e.kind()) {
     case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta:

src/frontends/lean/pp.cpp

@@ -324,7 +324,6 @@ static bool is_show(expr const & e) {
     return is_show_annotation(e) && is_app(get_annotation_arg(e)) &&
         is_lambda(app_fn(get_annotation_arg(e)));
 }
-static bool is_let_value(expr const & e) { return is_let_value_annotation(e); }
 
 auto pretty_fn::pp_have(expr const & e) -> result {
     expr proof   = app_arg(e);
@@ -431,7 +430,7 @@ auto pretty_fn::pp(expr const & e) -> result {
     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 (is_let_value(e))    return pp(get_annotation_arg(e));
+    if (is_let_value(e))    return pp(get_let_value_expr(e));
     if (auto n = to_num(e)) return pp_num(*n);
     if (!m_metavar_args && is_meta(e))
         return pp_meta(get_app_fn(e));

src/library/annotation.cpp

@@ -91,12 +91,6 @@ expr const & get_annotation_arg(expr const & e) {
     return macro_arg(e, 0);
 }
 
-name const & get_let_value_name() {
-    static name g_let("letv");
-    static register_annotation_fn g_let_annotation(g_let);
-    return g_let;
-}
-
 name const & get_have_name() {
     static name g_have("have");
     static register_annotation_fn g_have_annotation(g_have);
@@ -109,14 +103,11 @@ name const & get_show_name() {
     return g_show;
 }
 
-static name g_let_name  = get_let_value_name();  // force 'let value' annotation to be registered
 static name g_have_name = get_have_name(); // force 'have' annotation to be registered
 static name g_show_name = get_show_name(); // force 'show' annotation to be registered
 
-expr mk_let_value_annotation(expr const & e) { return mk_annotation(get_let_value_name(), e); }
 expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); }
 expr mk_show_annotation(expr const & e) { return mk_annotation(get_show_name(), e); }
-bool is_let_value_annotation(expr const & e) { return is_annotation(e, get_let_value_name()); }
 bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); }
 bool is_show_annotation(expr const & e) { return is_annotation(e, get_show_name()); }
 }

src/library/annotation.h

@@ -40,14 +40,10 @@ expr const & get_annotation_arg(expr const & e);
 */
 name const & get_annotation_kind(expr const & e);
 
-/** \brief Tag \c e as a 'let value'-expression. 'let value' is a pre-registered annotation. */
-expr mk_let_value_annotation(expr const & e);
 /** \brief Tag \c e as a 'have'-expression. 'have' is a pre-registered annotation. */
 expr mk_have_annotation(expr const & e);
 /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */
 expr mk_show_annotation(expr const & e);
-/** \brief Return true iff \c e was created using #mk_let_value_annotation. */
-bool is_let_value_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_have_annotation. */
 bool is_have_annotation(expr const & e);
 /** \brief Return true iff \c e was created using #mk_show_annotation. */

src/library/let.cpp

@@ -5,10 +5,71 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include "util/thread.h"
 #include "kernel/expr.h"
 #include "library/kernel_serializer.h"
 
 namespace lean {
+static name g_let_value("letv");
+std::string const & get_let_value_opcode() {
+    static std::string g_let_value_opcode("LetV");
+    return g_let_value_opcode;
+}
+
+static atomic<unsigned> g_next_let_value_id(0);
+static unsigned next_let_value_id() {
+    return atomic_fetch_add_explicit(&g_next_let_value_id, 1u, memory_order_seq_cst);
+}
+
+class let_value_definition_cell : public macro_definition_cell {
+    unsigned m_id;
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 1)
+            throw exception("invalid let-value expression");
+    }
+public:
+    let_value_definition_cell():m_id(next_let_value_id()) {}
+    virtual name get_name() const { return g_let_value; }
+    virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
+        check_macro(m);
+        return arg_types[0];
+    }
+    virtual optional<expr> expand(expr const & m, extension_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 0));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_let_value_opcode());
+    }
+    virtual bool operator==(macro_definition_cell const & other) const {
+        return
+            dynamic_cast<let_value_definition_cell const *>(&other) != nullptr &&
+            m_id == static_cast<let_value_definition_cell const&>(other).m_id;
+    }
+    virtual unsigned hash() const { return m_id; }
+};
+
+expr mk_let_value(expr const & e) {
+    auto d = macro_definition(new let_value_definition_cell());
+    return mk_macro(d, 1, &e);
+}
+
+bool is_let_value(expr const & e) {
+    return is_macro(e) && dynamic_cast<let_value_definition_cell const *>(macro_def(e).raw());
+}
+
+expr get_let_value_expr(expr const e) {
+    lean_assert(is_let_value(e));
+    return macro_arg(e, 0);
+}
+
+static register_macro_deserializer_fn
+let_value_des_fn(get_let_value_opcode(),
+               [](deserializer &, unsigned num, expr const * args) {
+                     if (num != 1) throw corrupted_stream_exception();
+                     return mk_let_value(args[0]);
+                 });
+
 static name g_let("let");
 std::string const & get_let_opcode() {
     static std::string g_let_opcode("Let");
@@ -67,8 +128,7 @@ expr const & get_let_body(expr const & e) {
 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();
+                   if (num != 2) throw corrupted_stream_exception();
                    name n;
                    d >> n;
                    return mk_let(n, args[0], args[1]);

src/library/let.h

@@ -8,6 +8,10 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
+expr mk_let_value(expr const & e);
+bool is_let_value(expr const & e);
+expr get_let_value_expr(expr const e);
+
 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);

src/util/thread.h

@@ -33,6 +33,7 @@ using std::atomic_fetch_sub_explicit;
 using std::memory_order_relaxed;
 using std::memory_order_release;
 using std::memory_order_acquire;
+using std::memory_order_seq_cst;
 using std::atomic_thread_fence;
 namespace chrono      = std::chrono;
 namespace this_thread = std::this_thread;
@@ -51,6 +52,7 @@ using boost::atomic;
 using boost::memory_order_relaxed;
 using boost::memory_order_acquire;
 using boost::memory_order_release;
+using boost::memory_order_seq_cst;
 using boost::condition_variable;
 using boost::unique_lock;
 using boost::lock_guard;
@@ -79,6 +81,7 @@ typedef unsigned milliseconds;
 constexpr int memory_order_relaxed = 0;
 constexpr int memory_order_release = 0;
 constexpr int memory_order_acquire = 0;
+constexpr int memory_order_seq_cst = 0;
 inline void atomic_thread_fence(int ) {}
 template<typename T>
 class atomic {

tests/lean/let4.lean

@@ -0,0 +1,19 @@
+import data.num
+using num
+
+variable f : num → num → num → num
+
+check
+  let a := 10,
+      b := 10,
+      c := 10
+  in f a b (f a 10 c)
+
+check
+  let a := 10,
+      b := let c := 10 in f a c (f a a (f 10 a c)),
+      d := 10,
+      e := f (f 10 10 d) (f d 10 10) a
+  in f a b (f e d 10)
+
+

tests/lean/let4.lean.expected.out

@@ -0,0 +1,7 @@
+let a := 10, b := 10, c := 10 in f a b (f a 10 c) : num
+let a := 10,
+    b := let c := 10 in f a c (f a a (f 10 a c)),
+    d := 10,
+    e := f (f 10 10 d) (f d 10 10) a
+in f a b (f e d 10) :
+  num