From c7992f2cac639841a3d6e0b44d06402deac0842d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Nov 2014 20:39:50 -0800
Subject: [PATCH] feat(frontends/lean): add [whnf] modifier to eval command

---
 src/emacs/lean-syntax.el            |  2 +-
 src/frontends/lean/builtin_cmds.cpp | 13 ++++++++++++-
 src/frontends/lean/token_table.cpp  |  2 +-
 src/frontends/lean/tokens.cpp       |  4 ++++
 src/frontends/lean/tokens.h         |  1 +
 tests/lean/whnf.lean                |  9 +++++++++
 tests/lean/whnf.lean.expected.out   |  5 +++++
 7 files changed, 33 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/whnf.lean
 create mode 100644 tests/lean/whnf.lean.expected.out

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 0f7dc10ef..d08120689 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -116,7 +116,7 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
-               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
+               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]")) . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
      (,(rx (not (any "\.")) word-start
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index f8049bac0..86f5e03ee 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -266,9 +266,20 @@ environment check_cmd(parser & p) {
 }
 
 environment eval_cmd(parser & p) {
+    bool whnf = false;
+    if (p.curr_is_token(get_whnf_tk())) {
+        p.next();
+        whnf = true;
+    }
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
-    expr r = normalize(p.env(), ls, e);
+    expr r;
+    if (whnf) {
+        auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
+        r = tc->whnf(e).first;
+    } else {
+        r = normalize(p.env(), ls, e);
+    }
     p.regular_stream() << r << endl;
     return p.env();
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index c5833738a..5f0fbf768 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -82,7 +82,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
-         "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import",
+         "evaluate", "check", "eval", "[whnf]", "[priority", "print", "end", "namespace", "section", "import",
          "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 1d379c278..0babb90c8 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -51,6 +51,7 @@ static name * g_as           = nullptr;
 static name * g_on           = nullptr;
 static name * g_off          = nullptr;
 static name * g_none         = nullptr;
+static name * g_whnf         = nullptr;
 static name * g_in           = nullptr;
 static name * g_assign       = nullptr;
 static name * g_visible      = nullptr;
@@ -139,6 +140,7 @@ void initialize_tokens() {
     g_on           = new name("[on]");
     g_off          = new name("[off]");
     g_none         = new name("[none]");
+    g_whnf         = new name("[whnf]");
     g_in           = new name("in");
     g_assign       = new name(":=");
     g_visible      = new name("[visible]");
@@ -244,6 +246,7 @@ void finalize_tokens() {
     delete g_on;
     delete g_off;
     delete g_none;
+    delete g_whnf;
     delete g_ellipsis;
     delete g_fun;
     delete g_take;
@@ -316,6 +319,7 @@ name const & get_as_tk() { return *g_as; }
 name const & get_on_tk() { return *g_on; }
 name const & get_off_tk() { return *g_off; }
 name const & get_none_tk() { return *g_none; }
+name const & get_whnf_tk() { return *g_whnf; }
 name const & get_in_tk() { return *g_in; }
 name const & get_assign_tk() { return *g_assign; }
 name const & get_visible_tk() { return *g_visible; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index f79d9b8a6..367a56757 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -53,6 +53,7 @@ name const & get_as_tk();
 name const & get_on_tk();
 name const & get_off_tk();
 name const & get_none_tk();
+name const & get_whnf_tk();
 name const & get_in_tk();
 name const & get_assign_tk();
 name const & get_visible_tk();
diff --git a/tests/lean/whnf.lean b/tests/lean/whnf.lean
new file mode 100644
index 000000000..6988f71aa
--- /dev/null
+++ b/tests/lean/whnf.lean
@@ -0,0 +1,9 @@
+import data.nat
+open nat
+
+eval [whnf] (fun x, x + 1) 2
+eval (fun x, x + 1) 2
+
+variable a : nat
+eval [whnf] a + succ zero
+eval a + succ zero
diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out
new file mode 100644
index 000000000..9f039f504
--- /dev/null
+++ b/tests/lean/whnf.lean.expected.out
@@ -0,0 +1,5 @@
+whnf.lean:2:0: warning: imported file uses 'sorry'
+succ (nat.rec 2 (λ (n r : ℕ), succ r) zero)
+succ (succ (succ zero))
+succ (nat.rec a (λ (n r : ℕ), succ r) zero)
+succ a