From 91994ff823c711ebd002b712c33e2edf86e3286a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Sep 2016 13:00:53 -0700
Subject: [PATCH] feat(frontends/lean/elaborator): switch to new let-decls

---
 library/init/classical.lean          | 11 +++--------
 library/init/function.lean           |  9 ++++-----
 library/init/logic.lean              |  3 ++-
 library/init/meta/environment.lean   |  6 ++----
 library/init/quot.lean               |  3 +--
 library/init/string.lean             |  2 +-
 src/frontends/lean/builtin_exprs.cpp | 22 +++++++++++-----------
 src/frontends/lean/elaborator.cpp    | 28 +++++++++++++++++++++++++---
 src/frontends/lean/elaborator.h      |  2 ++
 tests/lean/let1.lean                 |  1 +
 tests/lean/let1.lean.expected.out    | 16 ++++++++++------
 tests/lean/let3.lean                 |  4 ++--
 tests/lean/let3.lean.expected.out    |  2 +-
 tests/lean/let4.lean                 | 16 ++++++++--------
 tests/lean/let4.lean.expected.out    |  9 +++++++--
 tests/lean/run/choice_ctx.lean       |  4 ++--
 tests/lean/run/let1.lean             |  1 +
 tests/lean/run/let2.lean             |  1 +
 tests/lean/run/t6.lean               |  1 +
 19 files changed, 85 insertions(+), 56 deletions(-)

diff --git a/library/init/classical.lean b/library/init/classical.lean
index b723926d73..71d6ff3f99 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -20,8 +20,7 @@ theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
 nonempty.elim H (take x, exists.intro x trivial)
 
 noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
-let u : {x \ (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
-inhabited.mk (elt_of u)
+inhabited.mk (elt_of (strong_indefinite_description (λa, true) H))
 
 noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
 inhabited_of_nonempty (exists.elim H (λ w Hw, nonempty.intro w))
@@ -29,15 +28,11 @@ inhabited_of_nonempty (exists.elim H (λ w Hw, nonempty.intro w))
 /- the Hilbert epsilon function -/
 
 noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
-let u : {x \ (∃y, P y) → P x} :=
-  strong_indefinite_description P H in
-elt_of u
+elt_of (strong_indefinite_description P H)
 
 theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
     P (@epsilon A H P) :=
-let u : {x \ (∃y, P y) → P x} :=
-  strong_indefinite_description P H in
-have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
+have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property (strong_indefinite_description P H),
 aux Hex
 
 theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
diff --git a/library/init/function.lean b/library/init/function.lean
index 3b71a7ae54..3dee872f2c 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -142,11 +142,10 @@ injf H
 theorem surjective_of_has_right_inverse {f : A → B} : has_right_inverse f → surjective f :=
 assume h, take b,
 exists.elim h (λ finv inv,
-let  a : A := finv b in
-have h : f a = b, from calc
-  f a  = f (finv b)   : rfl
-   ... = b            : eq.subst (inv b) rfl,
-exists.intro a h)
+have h : f (finv b) = b, from calc
+  f (finv b)  = f (finv b)   : rfl
+          ... = b            : eq.subst (inv b) rfl,
+exists.intro (finv b) h)
 
 theorem left_inverse_of_surjective_of_right_inverse {f : A → B} {g : B → A}
     (surjf : surjective f) (rfg : right_inverse f g) :
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 5c0db54cf9..062f457e51 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -988,7 +988,8 @@ theorem dif_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : dec
                       (h_e : ∀ (h : ¬c),   y (iff.mpr (not_iff_not_of_iff h_c) h) = v h) :
         (@dite b dec_b A x y) = (@dite c dec_c A u v) :=
 decidable.rec_on dec_b
-  (λ hn : ¬b, let h_nc : ¬b ↔ ¬c := not_iff_not_of_iff h_c in calc
+  (λ hn : ¬b,
+    have h_nc : ¬b ↔ ¬c, from not_iff_not_of_iff h_c, calc
     dite b x y = y hn                              : dif_neg hn
           ...  = y (iff.mpr h_nc (iff.mp h_nc hn)) : rfl
           ...  = v (iff.mp h_nc hn)                : h_e (iff.mp h_nc hn)
diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index a2bd2c2af7..c56fe7f6bf 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -58,12 +58,10 @@ meta_constant trans_for : environment → name → option name
 open expr
 
 meta_definition is_constructor_app (env : environment) (e : expr) : bool :=
-let f := get_app_fn e in
-is_constant f && is_constructor env (const_name f)
+is_constant (get_app_fn e) && is_constructor env (const_name (get_app_fn e))
 
 meta_definition is_refl_app (env : environment) (e : expr) : option (name × expr × expr) :=
-let f := get_app_fn e in
-match (refl_for env (const_name f)) with
+match (refl_for env (const_name (get_app_fn e))) with
 | (some n) :=
     if get_app_num_args e ≥ 2
     then some (n, app_arg (app_fn e), app_arg e)
diff --git a/library/init/quot.lean b/library/init/quot.lean
index 2f7029e259..aa5e422480 100644
--- a/library/init/quot.lean
+++ b/library/init/quot.lean
@@ -68,8 +68,7 @@ namespace quot
   protected definition rec
      (f : Π a, B ⟦a⟧) (H : ∀ (a b : A) (p : a ≈ b), eq.rec (f a) (sound p) = f b)
      (q : quot s) : B q :=
-  let p := lift (quot.indep f) (quot.indep_coherent f H) q in
-  eq.rec_on (quot.lift_indep_pr1 f H q) (p.2)
+  eq.rec_on (quot.lift_indep_pr1 f H q) ((lift (quot.indep f) (quot.indep_coherent f H) q).2)
 
   attribute [reducible]
   protected definition rec_on
diff --git a/library/init/string.lean b/library/init/string.lean
index 28cb7ee709..49de6dbe50 100644
--- a/library/init/string.lean
+++ b/library/init/string.lean
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.char init.list
-
+set_option new_elaborator true
 attribute [reducible]
 definition string := list char
 
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 128313ac15..51816a28ba 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -86,16 +86,20 @@ static expr mk_typed_expr_distrib_choice(parser & p, expr const & type, expr con
 }
 
 static expr parse_let(parser & p, pos_info const & pos) {
+    if (!p.use_new_elaborator()) {
+        throw parser_error("let-expressions are not supported in the old elaborator anymore", pos);
+    }
     parser::local_scope scope1(p);
     if (p.parse_local_notation_decl()) {
         return parse_let_body(p, pos);
     } else {
         auto id_pos     = p.pos();
         name id         = p.check_atomic_id_next("invalid let declaration, atomic identifier expected");
-        optional<expr> type;
+        expr type;
         expr value;
         if (p.curr_is_token(get_assign_tk())) {
             p.next();
+            type  = p.save_pos(mk_expr_placeholder(), id_pos);
             value = p.parse_expr();
         } else if (p.curr_is_token(get_colon_tk())) {
             p.next();
@@ -110,22 +114,18 @@ static expr parse_let(parser & p, pos_info const & pos) {
             if (p.curr_is_token(get_colon_tk())) {
                 p.next();
                 type  = p.parse_scoped_expr(ps, lenv);
-                type  = Pi(ps, *type, p);
+                type  = Pi(ps, type, p);
+            } else {
+                type  = p.save_pos(mk_expr_placeholder(), id_pos);
             }
             p.check_token_next(get_assign_tk(), "invalid let declaration, ':=' expected");
             value = p.parse_scoped_expr(ps, lenv);
             value = Fun(ps, value, p);
         }
-        expr v;
-        if (type)
-            v = mk_typed_expr_distrib_choice(p, *type, value, p.pos_of(value));
-        else
-            v = value;
-        v = p.save_pos(mk_let_value(v), id_pos);
-        p.add_local_expr(id, v);
+        expr x = p.save_pos(mk_local(id, type), id_pos);
+        p.add_local_expr(id, x);
         expr b = parse_let_body(p, pos);
-        // TODO(Leo): use let-expression after we reimplement elaborator
-        return p.save_pos(mk_let_macro(id, v, b), pos);
+        return p.save_pos(mk_let(id, type, value, abstract_local(b, x)), pos);
     }
 }
 
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 51baf07281..00b83190a1 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1563,6 +1563,16 @@ expr elaborator::push_local(type_context::tmp_locals & locals,
     return locals.push_local(n, type, binfo);
 }
 
+/* See method above */
+expr elaborator::push_let(type_context::tmp_locals & locals,
+                          name const & n, expr const & type, expr const & value, expr const & ref) {
+    if (m_ctx.lctx().get_instance_fingerprint() &&
+        m_ctx.is_class(type)) {
+        throw elaborator_exception(ref, "invalid occurrence of local instance, it must be a declaration parameter");
+    }
+    return locals.push_let(n, type, value);
+}
+
 expr elaborator::visit_lambda(expr const & e, optional<expr> const & expected_type) {
     type_context::tmp_locals locals(m_ctx);
     checkpoint C(*this);
@@ -1631,9 +1641,21 @@ expr elaborator::visit_pi(expr const & e) {
     return r;
 }
 
-expr elaborator::visit_let(expr const & /* e */, optional<expr> const & /* expected_type */) {
-    // TODO(Leo)
-    lean_unreachable();
+expr elaborator::visit_let(expr const & e, optional<expr> const & expected_type) {
+    expr ref = e;
+    checkpoint C(*this);
+    expr new_type  = visit(let_type(e), none_expr());
+    expr new_value = visit(let_value(e), some_expr(new_type));
+    new_value      = enforce_type(new_value, new_type, "invalid let-expression", let_value(e));
+    process_checkpoint(C);
+    new_type       = instantiate_mvars(new_type);
+    new_value      = instantiate_mvars(new_value);
+    type_context::tmp_locals locals(m_ctx);
+    push_let(locals, let_name(e), new_type, new_value, ref);
+    expr body      = instantiate_rev(let_body(e), locals);
+    expr new_body  = visit(body, expected_type);
+    expr new_e     = locals.mk_lambda(new_body);
+    return new_e;
 }
 
 expr elaborator::visit_placeholder(expr const & e, optional<expr> const & expected_type) {
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index cb183cc39e..a75c79d3a7 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -100,6 +100,8 @@ private:
 
     expr push_local(type_context::tmp_locals & locals, name const & n, expr const & type,
                     binder_info const & binfo, expr const & ref);
+    expr push_let(type_context::tmp_locals & locals,
+                  name const & n, expr const & type, expr const & value, expr const & ref);
 
     level mk_univ_metavar();
     expr mk_metavar(expr const & A);
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index b762e81109..fdd9fb0fdb 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -1,4 +1,5 @@
 prelude -- Correct version
+set_option new_elaborator true
 check let bool                      := Type.{0},
           and  (p q : bool)         := ∀ c : bool, (p → q → c) → c,
           infixl `∧`:25             := and,
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index 5bc36494e5..73082948ac 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -1,9 +1,13 @@
-let bool := Prop,
-    and := λ p q, Π c, (p → q → c) → c,
-    and_intro := λ p q H1 H2 c H, H H1 H2
+let bool : Type := Prop,
+    and : bool → bool → Prop := λ p q, Π c, (p → q → c) → c,
+    and_intro : Π p q, p → q → and p q := λ p q H1 H2 c H, H H1 H2,
+    and_elim_left : Π p q, and p q → p := λ p q H, H p (λ H1 H2, H1),
+    and_elim_right : Π p q, and p q → q := λ p q H, H q (λ H1 H2, H2)
 in and_intro :
   ∀ p q, p → q → ∀ c, (p → q → c) → c
-let1.lean:19:19: error: invalid type ascription, expression has type
-  ∀ p q, p → q → ∀ c, (p → q → c) → c
+let1.lean:20:19: error: invalid let-expression, expression
+  λ p q H1 H2 c H, H H1 H2
+has type
+  Π p q, p → q → Π c, (p → q → c) → c
 but is expected to have type
-  ∀ p q, p → q → (λ p q, ∀ c, (p → q → c) → c) q p
+  Π p q, p → q → and q p
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index a2769c9ef3..8eb3d8a438 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,10 +1,10 @@
 --
-
+set_option new_elaborator true
 
 constant f : num → num → num → num
 
 check
-  let a := 10
+  let a : num := 10
   in f a 10
 
 /-
diff --git a/tests/lean/let3.lean.expected.out b/tests/lean/let3.lean.expected.out
index 89cef1cbe2..4bf9a7af12 100644
--- a/tests/lean/let3.lean.expected.out
+++ b/tests/lean/let3.lean.expected.out
@@ -1 +1 @@
-f 10 10 : num → num
+let a : num := 10 in f a 10 : num → num
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 92b5e081a4..d613852b3c 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,17 +1,17 @@
 --
-
+set_option new_elaborator true
 
 constant f : num → num → num → num
 
 check
-  let a := 10,
-      b := 10,
-      c := 10
+  let a : num := 10,
+      b : num := 10,
+      c : num := 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
+  let a : num := 10,
+      b : num := let c : num := 10 in f a c (f a a (f 10 a c)),
+      d : num := 10,
+      e : num := f (f 10 10 d) (f d 10 10) a
   in f a b (f e d 10)
diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out
index 5c6ca5e03a..0182fdc9c8 100644
--- a/tests/lean/let4.lean.expected.out
+++ b/tests/lean/let4.lean.expected.out
@@ -1,2 +1,7 @@
-f 10 10 (f 10 10 10) : num
-let b := f 10 10 (f 10 10 (f 10 10 10)), e := f (f 10 10 10) (f 10 10 10) 10 in f 10 b (f e 10 10) : num
+let a : num := 10, b : num := 10, c : num := 10 in f a b (f a 10 c) : num
+let a : num := 10,
+    b : num := let c : num := 10 in f a c (f a a (f 10 a c)),
+    d : num := 10,
+    e : num := f (f 10 10 d) (f d 10 10) a
+in f a b (f e d 10) :
+  num
diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean
index d86efa2ac4..6643877ceb 100644
--- a/tests/lean/run/choice_ctx.lean
+++ b/tests/lean/run/choice_ctx.lean
@@ -1,7 +1,7 @@
 open nat
 open eq
 set_option pp.coercions true
-
+set_option new_elaborator true
 namespace foo
 theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
 trans H1 H2
@@ -11,7 +11,7 @@ open foo
 
 theorem tst (a b : nat) (H0 : b = a) (H : b = 0) : a = 0
 := have H1 : a = b, from symm H0,
-   trans H1 H
+   foo.trans H1 H
 
 definition f (a b : nat) :=
 let x := 3 in
diff --git a/tests/lean/run/let1.lean b/tests/lean/run/let1.lean
index 3c7d3868e0..abef480117 100644
--- a/tests/lean/run/let1.lean
+++ b/tests/lean/run/let1.lean
@@ -1,3 +1,4 @@
+set_option new_elaborator true
 check
   let f x y := x ∧ y,
       g x   := f x x,
diff --git a/tests/lean/run/let2.lean b/tests/lean/run/let2.lean
index e37b9f9b4b..c0f8859281 100644
--- a/tests/lean/run/let2.lean
+++ b/tests/lean/run/let2.lean
@@ -1,3 +1,4 @@
+set_option new_elaborator true
 definition b :=
       let a := true ∧ true,
           a := a ∧ a,
diff --git a/tests/lean/run/t6.lean b/tests/lean/run/t6.lean
index 07dc09eed6..cad90b6c66 100644
--- a/tests/lean/run/t6.lean
+++ b/tests/lean/run/t6.lean
@@ -1,4 +1,5 @@
 prelude
+set_option new_elaborator true
 precedence `+`  : 65
 precedence `++` : 100
 constant N : Type.{1}