From e9c8de7bdf37aa73c32738f7bff48b1cebffc505 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 May 2015 11:49:55 -0700 Subject: [PATCH] feat(frontends/lean): remove unnecessary option --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/builtin_cmds.cpp | 21 ++------------------- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 ---- src/frontends/lean/tokens.h | 1 - tests/lean/eta_bug.lean | 2 +- 6 files changed, 5 insertions(+), 27 deletions(-) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 14271f222..3e54be38b 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -122,7 +122,7 @@ "\[coercion\]" "\[unfold-f\]" "\[constructor\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]" - "\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" + "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]" "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]")) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 633c4a02a..2be998019 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -481,25 +481,11 @@ environment check_cmd(parser & p) { return p.env(); } -class all_transparent_converter : public default_converter { -public: - all_transparent_converter(environment const & env): - default_converter(env) { - } - virtual bool is_opaque(declaration const &) const { - return false; - } -}; - environment eval_cmd(parser & p) { bool whnf = false; - bool all_transparent = false; if (p.curr_is_token(get_whnf_tk())) { p.next(); whnf = true; - } else if (p.curr_is_token(get_all_transparent_tk())) { - p.next(); - all_transparent = true; } expr e; level_param_names ls; std::tie(e, ls) = parse_local_expr(p); @@ -507,12 +493,9 @@ environment eval_cmd(parser & p) { if (whnf) { auto tc = mk_type_checker(p.env(), p.mk_ngen()); r = tc->whnf(e).first; - } else if (all_transparent) { - type_checker tc(p.env(), name_generator(), - std::unique_ptr(new all_transparent_converter(p.env()))); - r = normalize(tc, ls, e); } else { - r = normalize(p.env(), ls, e); + type_checker tc(p.env()); + r = normalize(tc, ls, e); } flycheck_information info(p.regular_stream()); if (info.enabled()) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 44c8defb0..8c73aa28c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -108,7 +108,7 @@ void init_token_table(token_table & t) { "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", - "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", + "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]", "[constructor]", "[unfold-c", "print", "end", "namespace", "section", "prelude", "help", "import", "inductive", "record", "structure", "module", "universe", "universes", "local", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 93355f5cc..a813977b7 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -75,7 +75,6 @@ static name * g_as = nullptr; static name * g_none = nullptr; static name * g_whnf = nullptr; static name * g_wf = nullptr; -static name * g_all_transparent = nullptr; static name * g_in = nullptr; static name * g_at = nullptr; static name * g_assign = nullptr; @@ -209,7 +208,6 @@ void initialize_tokens() { g_none = new name("[none]"); g_whnf = new name("[whnf]"); g_wf = new name("[wf]"); - g_all_transparent = new name("[all-transparent]"); g_in = new name("in"); g_at = new name("at"); g_assign = new name(":="); @@ -359,7 +357,6 @@ void finalize_tokens() { delete g_none; delete g_whnf; delete g_wf; - delete g_all_transparent; delete g_ellipsis; delete g_match; delete g_fun; @@ -480,7 +477,6 @@ name const & get_as_tk() { return *g_as; } name const & get_none_tk() { return *g_none; } name const & get_whnf_tk() { return *g_whnf; } name const & get_wf_tk() { return *g_wf; } -name const & get_all_transparent_tk() { return *g_all_transparent; } name const & get_in_tk() { return *g_in; } name const & get_at_tk() { return *g_at; } name const & get_assign_tk() { return *g_assign; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 975107570..859e7c61f 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -77,7 +77,6 @@ name const & get_as_tk(); name const & get_none_tk(); name const & get_whnf_tk(); name const & get_wf_tk(); -name const & get_all_transparent_tk(); name const & get_in_tk(); name const & get_at_tk(); name const & get_assign_tk(); diff --git a/tests/lean/eta_bug.lean b/tests/lean/eta_bug.lean index 9db364535..c376ac032 100644 --- a/tests/lean/eta_bug.lean +++ b/tests/lean/eta_bug.lean @@ -1,4 +1,4 @@ import logic -eval [all-transparent] λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂ +eval λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂ -- Should not reduce to -- λ (A : Type) (x y : A), eq.trans