From 60be2bf2aac7ab465578844333db2c1fc771d108 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Jan 2018 16:40:41 -0800
Subject: [PATCH] feat(frontends/lean/builtin_cmds): use `type_context` to
 implement `#reduce` command

---
 src/frontends/lean/builtin_cmds.cpp          |  7 +--
 src/library/normalize.cpp                    |  1 -
 tests/lean/smart_unfolding.lean              |  5 ++
 tests/lean/smart_unfolding.lean.expected.out |  8 +++
 tests/lean/whnf.lean.expected.out            | 62 +-------------------
 5 files changed, 18 insertions(+), 65 deletions(-)
 create mode 100644 tests/lean/smart_unfolding.lean
 create mode 100644 tests/lean/smart_unfolding.lean.expected.out

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3e0b6d5ef7..4175e4b39a 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -222,13 +222,12 @@ environment reduce_cmd(parser & p) {
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p, "_reduce");
     expr r;
+    type_context ctx(p.env(), p.get_options(), metavar_context(), local_context(), transparency_mode::All);
     if (whnf) {
-        type_checker tc(p.env(), true, false);
-        r = tc.whnf(e);
+        r = ctx.whnf(e);
     } else {
-        type_checker tc(p.env(), true, false);
         bool eta = false;
-        r = normalize(tc, e, eta);
+        r = normalize(ctx, e, eta);
     }
     auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION);
     out.set_caption("reduce result") << r;
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 7afde3e74c..b4fd5319a8 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -112,7 +112,6 @@ class normalize_fn {
     }
 
     expr normalize(expr e) {
-        // TODO(Leo): smart_reduction doesn't seem to work with normalize
         check_system("normalize");
         if (!m_pred(e))
             return e;
diff --git a/tests/lean/smart_unfolding.lean b/tests/lean/smart_unfolding.lean
new file mode 100644
index 0000000000..58ab4ef7b6
--- /dev/null
+++ b/tests/lean/smart_unfolding.lean
@@ -0,0 +1,5 @@
+constant n : nat
+#reduce n + (nat.succ n)
+
+set_option type_context.smart_unfolding false
+#reduce n + (nat.succ n)
diff --git a/tests/lean/smart_unfolding.lean.expected.out b/tests/lean/smart_unfolding.lean.expected.out
new file mode 100644
index 0000000000..f1243c7056
--- /dev/null
+++ b/tests/lean/smart_unfolding.lean.expected.out
@@ -0,0 +1,8 @@
+nat.succ (nat.add n n)
+nat.succ
+  ((nat.rec ⟨λ (a : ℕ), a, punit.star⟩
+      (λ (n : ℕ)
+       (ih : pprod (ℕ → ℕ) (nat.rec punit (λ (n : ℕ) (ih : Type), pprod (pprod (ℕ → ℕ) ih) punit) n)),
+         ⟨λ (a : ℕ), nat.succ (ih.fst a), ⟨ih, punit.star⟩⟩)
+      n).fst
+     n)
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
index 2f9c5ff274..2a13868ed4 100644
--- a/tests/lean/whnf.lean.expected.out
+++ b/tests/lean/whnf.lean.expected.out
@@ -1,62 +1,4 @@
-succ
-  ((⟨nat.rec
-       ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
-           (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
-              nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
-                (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
-                   id_rhs ℕ (succ ((_F.fst).fst a)))
-                _F)
-             a_1
-             a
-             _F)
-          0
-          punit.star,
-        punit.star⟩
-       (λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
-          ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
-              (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
-                 nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
-                   (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
-                      id_rhs ℕ (succ ((_F.fst).fst a)))
-                   _F)
-                a_1
-                a
-                _F)
-             (succ n)
-             ⟨ih, punit.star⟩,
-           ⟨ih, punit.star⟩⟩)
-       0,
-     punit.star⟩.fst).fst
-     2)
+succ (nat.add 2 0)
 3
-succ
-  ((⟨nat.rec
-       ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
-           (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
-              nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
-                (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
-                   id_rhs ℕ (succ ((_F.fst).fst a)))
-                _F)
-             a_1
-             a
-             _F)
-          0
-          punit.star,
-        punit.star⟩
-       (λ (n : ℕ) (ih : pprod ((λ (a : ℕ), ℕ → ℕ) n) (nat.below (λ (a : ℕ), ℕ → ℕ) n)),
-          ⟨(λ (a : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a) (a_1 : ℕ),
-              (λ (a a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) a_1),
-                 nat.cases_on a_1 (λ (_F : nat.below (λ (a : ℕ), ℕ → ℕ) 0), id_rhs ℕ a)
-                   (λ (a_1 : ℕ) (_F : nat.below (λ (a : ℕ), ℕ → ℕ) (succ a_1)),
-                      id_rhs ℕ (succ ((_F.fst).fst a)))
-                   _F)
-                a_1
-                a
-                _F)
-             (succ n)
-             ⟨ih, punit.star⟩,
-           ⟨ih, punit.star⟩⟩)
-       0,
-     punit.star⟩.fst).fst
-     a)
+succ (nat.add a 0)
 succ a