feat(frontends/lean): add [whnf] modifier to eval command

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

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();
 }

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",

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; }

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();

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

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