feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations

To retrieve the previous behavior, we should use [strict] modifier

src/emacs/lean-syntax.el

@@ -116,7 +116,8 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
-               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]")) . 'font-lock-doc-face)
+               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]" "\[strict\]"))
+      . '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,10 +266,14 @@ environment check_cmd(parser & p) {
 }
 
 environment eval_cmd(parser & p) {
-    bool whnf = false;
+    bool whnf   = false;
+    bool strict = false;
     if (p.curr_is_token(get_whnf_tk())) {
         p.next();
         whnf = true;
+    } else if (p.curr_is_token(get_strict_tk())) {
+        p.next();
+        strict = true;
     }
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
@@ -277,7 +281,10 @@ environment eval_cmd(parser & p) {
     if (whnf) {
         auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
         r = tc->whnf(e).first;
+    } else if (strict) {
+        r = normalize(p.env(), ls, e);
     } else {
+        transparent_scope scope;
         r = normalize(p.env(), ls, e);
     }
     p.regular_stream() << r << endl;

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", "[whnf]", "[priority", "print", "end", "namespace", "section", "import",
+         "evaluate", "check", "eval", "[whnf]", "[strict]", "[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

@@ -52,6 +52,7 @@ static name * g_on           = nullptr;
 static name * g_off          = nullptr;
 static name * g_none         = nullptr;
 static name * g_whnf         = nullptr;
+static name * g_strict       = nullptr;
 static name * g_in           = nullptr;
 static name * g_assign       = nullptr;
 static name * g_visible      = nullptr;
@@ -141,6 +142,7 @@ void initialize_tokens() {
     g_off          = new name("[off]");
     g_none         = new name("[none]");
     g_whnf         = new name("[whnf]");
+    g_strict       = new name("[strict]");
     g_in           = new name("in");
     g_assign       = new name(":=");
     g_visible      = new name("[visible]");
@@ -247,6 +249,7 @@ void finalize_tokens() {
     delete g_off;
     delete g_none;
     delete g_whnf;
+    delete g_strict;
     delete g_ellipsis;
     delete g_fun;
     delete g_take;
@@ -320,6 +323,7 @@ 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_strict_tk() { return *g_strict; }
 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

@@ -54,6 +54,7 @@ name const & get_on_tk();
 name const & get_off_tk();
 name const & get_none_tk();
 name const & get_whnf_tk();
+name const & get_strict_tk();
 name const & get_in_tk();
 name const & get_assign_tk();
 name const & get_visible_tk();

src/kernel/converter.cpp

@@ -13,6 +13,16 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 
 namespace lean {
+// Temporary hack for ignoring opaque annotations in the kernel
+LEAN_THREAD_VALUE(unsigned, g_everything_transparent, false);
+
+transparent_scope::transparent_scope():m_old_value(g_everything_transparent) {
+    g_everything_transparent = true;
+}
+transparent_scope::~transparent_scope() {
+    g_everything_transparent = m_old_value;
+}
+
 /**
    \brief Predicate for deciding whether \c d is an opaque definition or not.
 
@@ -35,6 +45,7 @@ namespace lean {
 */
 bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx) {
     lean_assert(d.is_definition());
+    if (g_everything_transparent) return false; // temporary hack
     if (d.is_theorem()) return true;                               // theorems are always opaque
     if (pred(d.get_name())) return true;                           // extra_opaque predicate overrides opaque flag
     if (!d.is_opaque()) return false;                              // d is a transparent definition

src/kernel/converter.h

@@ -25,6 +25,14 @@ public:
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
+/** \brief Temporary hack for creating a scope where the opaque annotations are ignored in the kernel. */
+class transparent_scope {
+    bool m_old_value;
+public:
+    transparent_scope();
+    ~transparent_scope();
+};
+
 std::unique_ptr<converter> mk_dummy_converter();
 std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx = optional<module_idx>(),
                                                 bool memoize = true);