From 8ed89c6ac3872ebda2f299261c550e8050de09ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Sep 2018 10:50:47 -0700 Subject: [PATCH] chore(library): remove `normalize.cpp` The command `#reduce` was also temporarily removed. --- src/frontends/lean/builtin_cmds.cpp | 25 --- src/frontends/lean/inductive_cmds.cpp | 7 +- src/frontends/lean/structure_cmd.cpp | 1 - src/frontends/lean/util.cpp | 1 - src/library/CMakeLists.txt | 2 +- src/library/compiler/elim_recursors.cpp | 1 - src/library/compiler/erase_irrelevant.cpp | 1 - src/library/compiler/inliner.cpp | 1 - src/library/compiler/lambda_lifting.cpp | 1 - src/library/compiler/simp_inductive.cpp | 1 - src/library/constructions/brec_on.cpp | 1 - src/library/constructions/cases_on.cpp | 1 - src/library/constructions/no_confusion.cpp | 1 - src/library/constructions/projection.cpp | 1 - src/library/constructions/rec_on.cpp | 1 - src/library/equations_compiler/equations.cpp | 1 - src/library/normalize.cpp | 170 ------------------- src/library/normalize.h | 15 -- src/library/vm/vm.cpp | 1 - 19 files changed, 5 insertions(+), 228 deletions(-) delete mode 100644 src/library/normalize.cpp delete mode 100644 src/library/normalize.h diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c9a9df6016..13d1bfbc15 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "library/export_decl.h" #include "library/protected.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/app_builder.h" #include "library/class.h" #include "library/user_recursors.h" @@ -209,29 +208,6 @@ environment check_cmd(parser & p) { return p.env(); } -environment reduce_cmd(parser & p) { - transient_cmd_scope cmd_scope(p); - bool whnf = false; - if (p.curr_is_token(get_whnf_tk())) { - p.next(); - whnf = true; - } - expr e; names ls; - std::tie(e, ls) = parse_local_expr(p, "_reduce"); - expr r; - type_context_old ctx(p.env(), p.get_options(), metavar_context(), local_context(), transparency_mode::All); - if (whnf) { - r = ctx.whnf(e); - } else { - bool eta = false; - r = normalize(ctx, e, eta); - } - auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION); - out.set_caption("reduce result") << r; - out.report(); - return p.env(); -} - environment exit_cmd(parser & p) { (p.mk_message(p.cmd_pos(), WARNING) << "using 'exit' to interrupt Lean").report(); throw interrupt_parser(); @@ -649,7 +625,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd)); add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); add_cmd(r, cmd_info("#check", "type check given expression, and display its type", check_cmd)); - add_cmd(r, cmd_info("#reduce", "reduce given expression", reduce_cmd)); add_cmd(r, cmd_info("#eval", "evaluate given expression using VM", eval_cmd)); add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); add_cmd(r, cmd_info("#help", "brief description of available commands and options", help_cmd)); diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 87ac428569..7ed6abef99 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -29,7 +29,6 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/type_context.h" #include "library/documentation.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/inductive_compiler/add_decl.h" #include "library/tactic/tactic_evaluator.h" #include "library/constructions/cases_on.h" @@ -416,8 +415,10 @@ class inductive_cmd_fn { /* Apply beta and zeta reduction */ expr normalize(expr const & e) { - type_context_old::transparency_scope scope(m_ctx, transparency_mode::None); - return ::lean::normalize(m_ctx, e); + // TODO(Leo) + return e; + // type_context_old::transparency_scope scope(m_ctx, transparency_mode::None); + // return ::lean::normalize(m_ctx, e); } void elaborate_inductive_decls(buffer const & params, buffer const & inds, buffer > const & intro_rules, diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 7f5a6d3bdb..fb72f0d39c 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/attribute_manager.h" #include "library/scoped_ext.h" -#include "library/normalize.h" #include "library/placeholder.h" #include "library/locals.h" #include "library/reducible.h" diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index fd623c7eb6..76dea35318 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -25,7 +25,6 @@ Author: Leonardo de Moura #include "library/string.h" #include "library/num.h" #include "library/util.h" -#include "library/normalize.h" #include "library/metavar_context.h" #include "library/replace_visitor.h" #include "library/compiler/vm_compiler.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index e532da0753..0a3f32c5b9 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -11,7 +11,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp aux_recursors.cpp trace.cpp attribute_manager.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp fun_info.cpp replace_visitor_with_tc.cpp aux_definition.cpp pattern_attribute.cpp - locals.cpp normalize.cpp mt_task_queue.cpp st_task_queue.cpp + locals.cpp mt_task_queue.cpp st_task_queue.cpp library_task_builder.cpp subscripted_name_set.cpp eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp check.cpp parray.cpp process.cpp diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index e23b1b088e..4a8da713eb 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/util.h" #include "library/trace.h" -#include "library/normalize.h" #include "library/compiler/util.h" #include "library/compiler/procedure.h" #include "library/compiler/comp_irrelevant.h" diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 94ab0c91fb..da8a63b850 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/string.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/aux_recursors.h" #include "library/inductive_compiler/ginductive.h" #include "library/compiler/util.h" diff --git a/src/library/compiler/inliner.cpp b/src/library/compiler/inliner.cpp index 1945084dec..46e43a3a2d 100644 --- a/src/library/compiler/inliner.cpp +++ b/src/library/compiler/inliner.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/module.h" #include "library/trace.h" -#include "library/normalize.h" #include "library/attribute_manager.h" #include "library/vm/vm.h" #include "library/compiler/util.h" diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 849914cf3c..14264221e1 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/for_each_fn.h" #include "kernel/inductive/inductive.h" -#include "library/normalize.h" #include "library/util.h" #include "library/trace.h" #include "library/scope_pos_info_provider.h" diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp index f36375ebd1..fd5d39ee27 100644 --- a/src/library/compiler/simp_inductive.cpp +++ b/src/library/compiler/simp_inductive.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/util.h" #include "library/projection.h" -#include "library/normalize.h" #include "library/constants.h" #include "library/vm/vm.h" #include "library/inductive_compiler/ginductive.h" diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index f99957bf1a..344bd0d2c5 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/bin_app.h" #include "library/util.h" -#include "library/normalize.h" #include "library/aux_recursors.h" #include "library/constructions/util.h" diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index 0db0d73827..f66b80acd6 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/reducible.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/aux_recursors.h" #include "library/constructions/util.h" diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index fb1ca06714..1720e8edbc 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/reducible.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/aux_recursors.h" #include "library/constructions/util.h" diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 5fa780b484..1419411c9a 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/projection.h" #include "library/module.h" #include "library/util.h" -#include "library/normalize.h" #include "library/scoped_ext.h" #include "library/kernel_serializer.h" #include "library/class.h" diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index 5e1fd06f57..972d623934 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/reducible.h" #include "library/protected.h" -#include "library/normalize.h" #include "library/aux_recursors.h" #include "library/constructions/util.h" diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index 5e4cf885fa..4b01f412e3 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -23,7 +23,6 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/locals.h" #include "library/constants.h" -#include "library/normalize.h" #include "library/pp_options.h" #include "library/equations_compiler/equations.h" diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp deleted file mode 100644 index 247bf430d1..0000000000 --- a/src/library/normalize.cpp +++ /dev/null @@ -1,170 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "runtime/interrupt.h" -#include "util/fresh_name.h" -#include "kernel/old_type_checker.h" -#include "kernel/replace_fn.h" -#include "kernel/instantiate.h" -#include "kernel/abstract.h" -#include "kernel/inductive/inductive.h" -#include "library/replace_visitor.h" -#include "library/reducible.h" -#include "library/util.h" -#include "library/scoped_ext.h" -#include "library/kernel_serializer.h" -#include "library/attribute_manager.h" - -namespace lean { -class normalize_fn { - abstract_type_context & m_ctx; - std::function m_pred; // NOLINT - bool m_use_eta; - bool m_eval_nested_prop; - - environment const & env() const { return m_ctx.env(); } - - expr normalize_binding(expr const & e) { - expr d = normalize(binding_domain(e)); - expr l = m_ctx.push_local(binding_name(e), d, binding_info(e)); - expr b = abstract(normalize(instantiate(binding_body(e), l)), 1, &l); - m_ctx.pop_local(); - return update_binding(e, d, b); - } - - optional is_constructor_like(expr const & e) { - if (is_constructor_app(env(), e)) - return some_expr(e); - else - return none_expr(); - } - - optional unfold_recursor_core(expr const & f, unsigned i, - buffer const & idxs, buffer & args, bool is_rec) { - if (i == idxs.size()) { - expr new_app = mk_rev_app(f, args); - if (is_rec) - return some_expr(normalize(new_app)); - else if (optional r = unfold_app(env(), new_app)) - return some_expr(normalize(*r)); - else - return none_expr(); - } else { - unsigned idx = idxs[i]; - if (idx >= args.size()) - return none_expr(); - expr & arg = args[args.size() - idx - 1]; - optional new_arg = is_constructor_like(arg); - if (!new_arg) - return none_expr(); - flet set_arg(arg, *new_arg); - return unfold_recursor_core(f, i+1, idxs, args, is_rec); - } - } - - optional unfold_recursor_like(expr const & f, list const & idx_lst, buffer & args) { - buffer idxs; - to_buffer(idx_lst, idxs); - return unfold_recursor_core(f, 0, idxs, args, false); - } - - optional unfold_recursor_major(expr const & f, unsigned idx, buffer & args) { - buffer idxs; - idxs.push_back(idx); - return unfold_recursor_core(f, 0, idxs, args, true); - } - - bool is_prop(expr const & e) { - return m_ctx.whnf(m_ctx.infer(e)) == mk_Prop(); - } - - expr normalize_app(expr const & e) { - buffer args; - bool modified = false; - expr f = get_app_rev_args(e, args); - for (expr & a : args) { - expr new_a = a; - if (m_eval_nested_prop || !is_prop(m_ctx.infer(a))) - new_a = normalize(a); - if (new_a != a) - modified = true; - a = new_a; - } - if (is_constant(f)) { - if (auto idx = inductive::get_elim_major_idx(env(), const_name(f))) { - if (auto r = unfold_recursor_major(f, *idx, args)) - return *r; - } - } - if (!modified) - return e; - expr r = mk_rev_app(f, args); - if (is_constant(f) && env().is_recursor(const_name(f))) { - return normalize(r); - } else { - return r; - } - } - - expr normalize(expr e) { - check_system("normalize"); - if (!m_pred(e)) - return e; - e = m_ctx.whnf(e); - switch (e.kind()) { - case expr_kind::BVar: case expr_kind::Const: case expr_kind::Sort: - case expr_kind::MVar: case expr_kind::FVar: case expr_kind::Lit: - return e; - case expr_kind::MData: - lean_unreachable(); - case expr_kind::Proj: - lean_unreachable(); - case expr_kind::Lambda: { - e = normalize_binding(e); - if (m_use_eta) - return try_eta(e); - else - return e; - } - case expr_kind::Pi: - return normalize_binding(e); - case expr_kind::App: - return normalize_app(e); - case expr_kind::Let: - // whnf unfolds let-exprs - lean_unreachable(); - - case expr_kind::Quote: - return e; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - -public: - normalize_fn(abstract_type_context & ctx, bool eta, bool nested_prop = true): - m_ctx(ctx), m_pred([](expr const &) { return true; }), - m_use_eta(eta), m_eval_nested_prop(nested_prop) { - } - - normalize_fn(abstract_type_context & ctx, std::function const & fn, bool eta, bool nested_prop = true): // NOLINT - m_ctx(ctx), m_pred(fn), m_use_eta(eta), m_eval_nested_prop(nested_prop) { - } - - expr operator()(expr const & e) { - return normalize(e); - } -}; - -expr normalize(environment const & env, expr const & e, bool eta) { - old_type_checker ctx(env); - return normalize_fn(ctx, eta)(e); -} - -expr normalize(abstract_type_context & ctx, expr const & e, bool eta) { - return normalize_fn(ctx, eta)(e); -} -} diff --git a/src/library/normalize.h b/src/library/normalize.h deleted file mode 100644 index fc64a6d3e5..0000000000 --- a/src/library/normalize.h +++ /dev/null @@ -1,15 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "kernel/abstract_type_context.h" - -namespace lean { -/** \brief Return the \c e normal form with respect to the environment \c env. */ -expr normalize(environment const & env, expr const & e, bool eta = false); -expr normalize(abstract_type_context & ctx, expr const & e, bool eta = false); -} diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 4c67ec0619..46e0f6701d 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -29,7 +29,6 @@ Author: Leonardo de Moura #include "library/vm/vm.h" #include "library/vm/vm_name.h" #include "library/vm/vm_option.h" -#include "library/normalize.h" #ifndef LEAN_DEFAULT_PROFILER_FREQ #define LEAN_DEFAULT_PROFILER_FREQ 1