feat(frontends/lean/elaborator): elaborate lambdas

src/frontends/lean/elaborator.cpp

@@ -262,7 +262,7 @@ expr elaborator::ensure_function(expr const & e, expr const & ref) {
 
 expr elaborator::ensure_type(expr const & e, expr const & ref) {
     expr e_type = whnf(infer_type(e));
-    if (!is_sort(e_type)) {
+    if (!is_sort(e_type) && !is_metavar(e_type)) {
         throw elaborator_exception(ref, format("type expected at") + pp_indent(e));
     }
     return e;
@@ -726,9 +726,52 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
     }
 }
 
+static expr instantiate_rev(expr const & e, type_context::tmp_locals const & locals) {
+    return instantiate_rev(e, locals.as_buffer().size(), locals.as_buffer().data());
+}
+
 expr elaborator::visit_lambda(expr const & e, optional<expr> const & expected_type) {
-    // TODO(Leo)
-    lean_unreachable();
+    type_context::tmp_locals locals(m_ctx);
+    checkpoint C(*this);
+    expr it = e;
+    expr ex;
+    bool has_expected;
+    if (expected_type) {
+        ex = try_to_pi(*expected_type);
+        has_expected = true;
+    } else {
+        has_expected = false;
+    }
+    while (is_lambda(it)) {
+        expr d = instantiate_rev(binding_domain(it), locals);
+        expr new_d;
+        if (has_expected) {
+            if (is_pi(ex)) {
+                expr ex_d = binding_domain(ex);
+                new_d     = visit(d, some_expr(ex_d));
+            } else {
+                has_expected = false;
+            }
+        } else {
+            new_d = visit(d, none_expr());
+        }
+        new_d  = ensure_type(new_d, binding_domain(it));
+        expr l = locals.push_local(binding_name(it), new_d, binding_info(it));
+        it = binding_body(it);
+        if (has_expected && is_pi(ex)) {
+            ex = try_to_pi(instantiate(binding_body(ex), l));
+        }
+    }
+    expr b = instantiate_rev(it, locals);
+    expr new_b;
+    if (has_expected) {
+        new_b = visit(b, some_expr(ex));
+    } else {
+        new_b = visit(b, none_expr());
+    }
+    process_checkpoint(C);
+    expr r = instantiate_mvars(locals.mk_lambda(new_b));
+    return r;
 }
 
 expr elaborator::visit_pi(expr const & e, optional<expr> const & expected_type) {

tests/lean/elab7.lean

@@ -0,0 +1,10 @@
+set_option pp.all true
+set_option pp.purify_metavars false
+
+#elab λ x : nat, x + 1
+
+#elab λ x y : nat, x + y
+
+#elab λ x y, x + y + 1
+
+#elab λ x, (x + 1) :: []

tests/lean/elab7.lean.expected.out

@@ -0,0 +1,12 @@
+>> λ (x : nat), add x [prenum]
+>> λ (x : nat), @add.{1} nat nat_has_add x (@one.{1} nat nat_has_one)
+>> nat → nat
+>> λ (x y : nat), add x y
+>> λ (x y : nat), @add.{1} nat nat_has_add x y
+>> nat → nat → nat
+>> λ (x : _) (y : _), add (add x y) [prenum]
+>> λ (x y : nat), @add.{1} nat nat_has_add (@add.{1} nat nat_has_add x y) (@one.{1} nat nat_has_one)
+>> nat → nat → nat
+>> λ (x : _), list.cons (add x [prenum]) list.nil
+>> λ (x : nat), @list.cons.{1} nat (@add.{1} nat nat_has_add x (@one.{1} nat nat_has_one)) (@list.nil.{1} nat)
+>> nat → list.{1} nat