From 50973bb4f3fee9e61bd809fbc28ed063a300a280 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Nov 2014 12:46:04 -0800 Subject: [PATCH] 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 | 3 ++- src/frontends/lean/builtin_cmds.cpp | 9 ++++++++- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ++++ src/frontends/lean/tokens.h | 1 + src/kernel/converter.cpp | 11 +++++++++++ src/kernel/converter.h | 8 ++++++++ 7 files changed, 35 insertions(+), 3 deletions(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index b983fe862..17b08564b 100644 --- a/src/emacs/lean-syntax.el +++ b/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 diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 86f5e03ee..3a8c2b792 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 5f0fbf768..af90b6c94 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", "[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", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 0babb90c8..a8a60a88a 100644 --- a/src/frontends/lean/tokens.cpp +++ b/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; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 367a56757..4f9e02f9d 100644 --- a/src/frontends/lean/tokens.h +++ b/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(); diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 38cff810a..97d2b6018 100644 --- a/src/kernel/converter.cpp +++ b/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 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 diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 4d59a0189..a996778c4 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -25,6 +25,14 @@ public: pair 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 mk_dummy_converter(); std::unique_ptr mk_default_converter(environment const & env, optional mod_idx = optional(), bool memoize = true);