refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable

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

src/kernel/abstract.cpp

@@ -49,5 +49,4 @@ expr FName(std::initializer_list<std::pair<expr const &, expr const &>> const &
 
 MkBinder(Fun);
 MkBinder(Pi);
-MkBinder(Let);
 }

src/kernel/abstract.h

@@ -46,21 +46,10 @@ inline expr Pi(expr const & n, expr const & t, expr const & b) { return mk_pi(co
 inline expr Pi(std::pair<expr const &, expr const &> const & p, expr const & b) { return Pi(p.first, p.second, b); }
        expr Pi(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
 
-/**
-   \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
-*/
-inline expr Let(name const & x, expr const & v, expr const & b) { return mk_let(x, v, abstract(b, mk_constant(x))); }
-inline expr Let(expr const & x, expr const & v, expr const & b) { return mk_let(const_name(x), v, abstract(b, x)); }
-inline expr Let(std::pair<expr const &, expr const &> const & p, expr const & b) { return Let(p.first, p.second, b); }
-       expr Let(std::initializer_list<std::pair<expr const &, expr const &>> const & l, expr const & b);
-/**
-   \brief Similar to Let(x, v, b), but returns v if x == b
-*/
-inline expr Let_simp(expr const & x, expr const & v, expr const & b) { return x == b ? v : Let(x, v, b); }
 
 /**
-   \brief Create a Let expression (Let x : t := v in b), the term b is abstracted using abstract(b, x).
+-   \brief Create a Let expression (Let x := v in b), the term b is abstracted using abstract(b, x).
-*/
+-*/
 inline expr Let(name const & x, expr const & t, expr const & v, expr const & b) { return mk_let(x, t, v, abstract(b, mk_constant(x))); }
 inline expr Let(expr const & x, expr const & t, expr const & v, expr const & b) { return mk_let(const_name(x), t, v, abstract(b, x)); }
 }

src/kernel/expr.cpp

@@ -62,11 +62,6 @@ void expr_cell::dec_ref(expr & e, buffer<expr_cell*> & todelete) {
     }
 }
 
-void expr_cell::dec_ref(optional<expr> & c, buffer<expr_cell*> & todelete) {
-    if (c)
-        dec_ref(*c, todelete);
-}
-
 optional<bool> expr_cell::is_arrow() const {
     // it is stored in bits 3-4
     unsigned r = (m_flags & (8+16)) >> 3;
@@ -168,8 +163,8 @@ expr_sort::expr_sort(level const & l):
 expr_sort::~expr_sort() {}
 
 // Expr Let
-expr_let::expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b):
+expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & b):
-    expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), v.has_metavar() || b.has_metavar() || ::lean::has_metavar(t),
+    expr_composite(expr_kind::Let, ::lean::hash(v.hash(), b.hash()), t.has_metavar() || v.has_metavar() || b.has_metavar(),
                    std::max({get_depth(t), get_depth(v), get_depth(b)}) + 1),
     m_name(n),
     m_type(t),
@@ -321,7 +316,7 @@ expr update_binder(expr const & e, expr const & new_domain, expr const & new_bod
         return e;
 }
 
-expr update_let(expr const & e, optional<expr> const & new_type, expr const & new_val, expr const & new_body) {
+expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body) {
     if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_val) || !is_eqp(let_body(e), new_body))
         return mk_let(let_name(e), new_type, new_val, new_body);
     else
@@ -403,16 +398,6 @@ class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp
     typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
     max_sharing_fn m_max_sharing_fn;
 
-    void write_core(optional<expr> const & a) {
-        serializer & s = get_owner();
-        if (a) {
-            s << true;
-            write_core(*a);
-        } else {
-            s << false;
-        }
-    }
-
     void write_core(expr const & a) {
         auto k = a.kind();
         super::write_core(a, static_cast<char>(k), [&]() {
@@ -460,15 +445,6 @@ public:
 class expr_deserializer : public object_deserializer<expr> {
     typedef object_deserializer<expr> super;
 public:
-    optional<expr> read_opt() {
-        deserializer & d = get_owner();
-        if (d.read_bool()) {
-            return some_expr(read());
-        } else {
-            return none_expr();
-        }
-    }
-
     expr read_binder(expr_kind k) {
         deserializer & d = get_owner();
         name n = read_name(d);
@@ -509,7 +485,7 @@ public:
                     return read_binder(k);
                 case expr_kind::Let: {
                     name n = read_name(d);
-                    optional<expr> t = read_opt();
+                    expr t = read();
                     expr v = read();
                     return mk_let(n, t, v, read());
                 }

src/kernel/expr.h

@@ -40,7 +40,7 @@ typedef list<level> levels;
           |   Lambda        name expr expr
           |   Pi            name expr expr
           |   Sigma         name expr expr
-          |   Let           name expr? expr expr
+          |   Let           name expr expr expr
 
           |   Macro         macro
 */
@@ -72,7 +72,6 @@ protected:
 
     friend class has_free_var_fn;
     static void dec_ref(expr & c, buffer<expr_cell*> & todelete);
-    static void dec_ref(optional<expr> & c, buffer<expr_cell*> & todelete);
 public:
     expr_cell(expr_kind k, unsigned h, bool has_mv);
     expr_kind kind() const { return static_cast<expr_kind>(m_kind); }
@@ -127,7 +126,7 @@ public:
     friend expr mk_pair(expr const & f, expr const & s, expr const & t);
     friend expr mk_proj(bool fst, expr const & p);
     friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e);
-    friend expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e);
+    friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e);
     friend expr mk_macro(macro * m);
 
     friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@@ -253,16 +252,16 @@ public:
 /** \brief Let expressions */
 class expr_let : public expr_composite {
     name    m_name;
-    optional<expr> m_type;
+    expr    m_type;
     expr    m_value;
     expr    m_body;
     friend class expr_cell;
     void dealloc(buffer<expr_cell*> & todelete);
 public:
-    expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b);
+    expr_let(name const & n, expr const & t, expr const & v, expr const & b);
     ~expr_let();
     name const & get_name() const   { return m_name; }
-    optional<expr> const & get_type() const { return m_type; }
+    expr const & get_type() const   { return m_type; }
     expr const & get_value() const  { return m_value; }
     expr const & get_body() const   { return m_body; }
 };
@@ -388,11 +387,7 @@ inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const &
 inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); }
 inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); }
 inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Sigma, n, t, e); }
-inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) {
+inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
-    return expr(new expr_let(n, t, v, e));
-}
-inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); }
-inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); }
 inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); }
 
 expr mk_Bool();
@@ -484,7 +479,7 @@ inline expr const &   binder_body(expr_cell * e)          { return to_binder(e)-
 inline level const &  sort_level(expr_cell * e)           { return to_sort(e)->get_level(); }
 inline name const &   let_name(expr_cell * e)             { return to_let(e)->get_name(); }
 inline expr const &   let_value(expr_cell * e)            { return to_let(e)->get_value(); }
-inline optional<expr> const &  let_type(expr_cell * e)    { return to_let(e)->get_type(); }
+inline expr const &   let_type(expr_cell * e)             { return to_let(e)->get_type(); }
 inline expr const &   let_body(expr_cell * e)             { return to_let(e)->get_body(); }
 inline name const &   mlocal_name(expr_cell * e)          { return to_mlocal(e)->get_name(); }
 inline expr const &   mlocal_type(expr_cell * e)          { return to_mlocal(e)->get_type(); }
@@ -508,16 +503,14 @@ inline expr const &   binder_body(expr const & e)          { return to_binder(e)
 inline level const &  sort_level(expr const & e)           { return to_sort(e)->get_level(); }
 inline name const &   let_name(expr const & e)             { return to_let(e)->get_name(); }
 inline expr const &   let_value(expr const & e)            { return to_let(e)->get_value(); }
-inline optional<expr> const &  let_type(expr const & e)    { return to_let(e)->get_type(); }
+inline expr const &   let_type(expr const & e)             { return to_let(e)->get_type(); }
 inline expr const &   let_body(expr const & e)             { return to_let(e)->get_body(); }
 inline name const &   mlocal_name(expr const & e)          { return to_mlocal(e)->get_name(); }
 inline expr const &   mlocal_type(expr const & e)          { return to_mlocal(e)->get_type(); }
 
 inline bool is_constant(expr const & e, name const & n) { return is_constant(e) && const_name(e) == n; }
 inline bool has_metavar(expr const & e) { return e.has_metavar(); }
-inline bool has_metavar(optional<expr> const & e) { return e && has_metavar(*e); }
 unsigned get_depth(expr const & e);
-inline unsigned get_depth(optional<expr> const & e) { return e ? get_depth(*e) : 0; }
 // =======================================
 
 
@@ -565,7 +558,7 @@ expr update_app(expr const & e, expr const & new_fn, expr const & new_arg);
 expr update_proj(expr const & e, expr const & new_arg);
 expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type);
 expr update_binder(expr const & e, expr const & new_domain, expr const & new_body);
-expr update_let(expr const & e, optional<expr> const & new_type, expr const & new_val, expr const & new_body);
+expr update_let(expr const & e, expr const & new_type, expr const & new_val, expr const & new_body);
 expr update_mlocal(expr const & e, expr const & new_type);
 // =======================================
 

src/kernel/expr_eq_fn.cpp

@@ -7,15 +7,6 @@ Author: Leonardo de Moura
 #include "kernel/expr_eq_fn.h"
 
 namespace lean {
-bool expr_eq_fn::apply(optional<expr> const & a0, optional<expr> const & b0) {
-    if (is_eqp(a0, b0))
-        return true;
-    else if (!a0 || !b0)
-        return false;
-    else
-        return apply(*a0, *b0);
-}
-
 bool expr_eq_fn::apply(expr const & a, expr const & b) {
     check_system("expression equality test");
     if (is_eqp(a, b))          return true;

src/kernel/expr_eq_fn.h

@@ -16,7 +16,6 @@ namespace lean {
 */
 class expr_eq_fn {
     std::unique_ptr<expr_cell_pair_set> m_eq_visited;
-    bool apply(optional<expr> const & a0, optional<expr> const & b0);
     bool apply(expr const & a, expr const & b);
 public:
     bool operator()(expr const & a, expr const & b) { return apply(a, b); }

src/kernel/for_each_fn.cpp

@@ -67,8 +67,7 @@ void for_each_fn::apply(expr const & e, unsigned offset) {
         case expr_kind::Let:
             todo.emplace_back(let_body(e), offset + 1);
             todo.emplace_back(let_value(e), offset);
-            if (let_type(e))
+            todo.emplace_back(let_type(e), offset);
-                todo.emplace_back(*let_type(e), offset);
             goto begin_loop;
         }
     }

src/kernel/formatter.cpp

@@ -117,10 +117,8 @@ struct print_expr_fn {
             break;
         case expr_kind::Let:
             out() << "let " << let_name(a);
-            if (let_type(a)) {
             out() << " : ";
-                print(*let_type(a), c);
+            print(let_type(a), c);
-            }
             out() << " := ";
             print(let_value(a), c);
             out() << " in ";

src/kernel/free_vars.cpp

@@ -22,10 +22,6 @@ class has_free_vars_fn {
 protected:
     expr_cell_offset_set m_cached;
 
-    bool apply(optional<expr> const & e, unsigned offset) {
-        return e && apply(*e, offset);
-    }
-
     bool apply(expr const & e, unsigned offset) {
         // handle easy cases
         switch (e.kind()) {
@@ -113,10 +109,6 @@ class free_var_range_fn {
 
     static unsigned dec(unsigned s) { return (s == 0) ? 0 : s - 1; }
 
-    unsigned apply(optional<expr> const & e) {
-        return e ? apply(*e) : 0;
-    }
-
     unsigned apply(expr const & e) {
         // handle easy cases
         switch (e.kind()) {
@@ -191,10 +183,6 @@ protected:
     expr_cell_offset_set               m_cached;
     std::unique_ptr<free_var_range_fn> m_range_fn;
 
-    bool apply(optional<expr> const & e, unsigned offset) {
-        return e && apply(*e, offset);
-    }
-
     // Return true iff  m_low + offset <= vidx
     bool ge_lower(unsigned vidx, unsigned offset) const {
         unsigned low1 = m_low + offset;

src/kernel/max_sharing.cpp

@@ -26,13 +26,6 @@ struct max_sharing_fn::imp {
         m_cache.insert(a);
     }
 
-    optional<expr> apply(optional<expr> const & a) {
-        if (a)
-            return some_expr(apply(*a));
-        else
-            return a;
-    }
-
     expr apply(expr const & a) {
         check_system("max_sharing");
         auto r = m_cache.find(a);

src/kernel/replace_fn.cpp

@@ -115,19 +115,14 @@ expr replace_fn::operator()(expr const & e) {
             pop_rs(2);
             break;
         case expr_kind::Let:
-            if (check_index(f, 0) && let_type(e) && !visit(*let_type(e), offset))
+            if (check_index(f, 0) && !visit(let_type(e), offset))
                 goto begin_loop;
             if (check_index(f, 1) && !visit(let_value(e), offset))
                 goto begin_loop;
             if (check_index(f, 2) && !visit(let_body(e), offset + 1))
                 goto begin_loop;
-            if (let_type(e)) {
+            r = update_let(e, rs(-3), rs(-2), rs(-1));
-                r = update_let(e, some_expr(rs(-3)), rs(-2), rs(-1));
             pop_rs(3);
-            } else {
-                r = update_let(e, none_expr(), rs(-2), rs(-1));
-                pop_rs(2);
-            }
             break;
         }
         save_result(e, r, offset, f.m_shared);

src/kernel/replace_visitor.cpp

@@ -46,11 +46,10 @@ expr replace_visitor::visit_pi(expr const & e, context const & ctx) { return vis
 expr replace_visitor::visit_sigma(expr const & e, context const & ctx) { return visit_binder(e, ctx); }
 expr replace_visitor::visit_let(expr const & e, context const & ctx) {
     lean_assert(is_let(e));
-    optional<expr> new_t = visit(let_type(e), ctx);
+    expr new_t = visit(let_type(e), ctx);
     expr new_v = visit(let_value(e), ctx);
     freset<cache> reset(m_cache);
-    // TODO(Leo): decide what we should do with let-exprs
+    expr new_b = visit(let_body(e), extend(ctx, let_name(e), new_t));
-    expr new_b; // = visit(let_body(e), extend(ctx, let_name(e), new_t, new_v));
     return update_let(e, new_t, new_v, new_b);
 }
 expr replace_visitor::save_result(expr const & e, expr && r, bool shared) {
@@ -87,10 +86,4 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
 
     lean_unreachable(); // LCOV_EXCL_LINE
 }
-optional<expr> replace_visitor::visit(optional<expr> const & e, context const & ctx) {
-    if (e)
-        return some_expr(visit(*e, ctx));
-    else
-        return none_expr();
-}
 }

src/kernel/replace_visitor.h

@@ -42,7 +42,6 @@ protected:
     virtual expr visit_sigma(expr const &, context const &);
     virtual expr visit_let(expr const &, context const &);
     virtual expr visit(expr const &, context const &);
-    optional<expr> visit(optional<expr> const &, context const &);
 
     void set_ctx(context const & ctx) {
         if (!is_eqp(m_ctx, ctx)) {

src/tests/kernel/expr.cpp

@@ -272,7 +272,7 @@ static void tst13() {
 }
 
 static void tst14() {
-    expr l = mk_let("a", none_expr(), Const("b"), Var(0));
+    expr l = mk_let("a", Bool, Const("b"), Var(0));
     check_serializer(l);
     std::cout << l << "\n";
     lean_assert(closed(l));
@@ -295,7 +295,7 @@ static void tst15() {
     lean_assert(has_metavar(Pi({a, m}, a)));
     lean_assert(has_metavar(Fun({a, Type}, m)));
     lean_assert(has_metavar(Fun({a, m}, a)));
-    lean_assert(!has_metavar(Let({a, Type}, a)));
+    lean_assert(!has_metavar(Let(a, Type, Bool, a)));
     lean_assert(!has_metavar(mk_let(name("a"), Type, f(x), f(f(x)))));
     lean_assert(has_metavar(mk_let(name("a"), m, f(x), f(f(x)))));
     lean_assert(has_metavar(mk_let(name("a"), Type, f(m), f(f(x)))));
@@ -319,7 +319,7 @@ static void tst16() {
     check_copy(mk_metavar("M", Bool));
     check_copy(mk_lambda("x", a, Var(0)));
     check_copy(mk_pi("x", a, Var(0)));
-    check_copy(mk_let("x", none_expr(), a, Var(0)));
+    check_copy(mk_let("x", Bool, a, Var(0)));
 }
 
 static void tst17() {

src/tests/kernel/instantiate.cpp

@@ -36,7 +36,7 @@ static void tst2() {
     expr a = Const("a");
     expr f = Const("f");
     expr N = Const("N");
-    expr F1 = Let({x, a}, f(x));
+    expr F1 = Let(x, N, a, f(x));
     lean_assert(head_beta_reduce(F1) == F1);
 }