chore(library): remove normalize.cpp

The command `#reduce` was also temporarily removed.

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

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<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,

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"

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"

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

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"

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"

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"

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"

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"

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"
 

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"
 

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"
 

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"

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"
 

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"
 

src/library/normalize.cpp

@@ -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 <string>
-#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<bool(expr const &)> 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<expr> is_constructor_like(expr const & e) {
-        if (is_constructor_app(env(), e))
-            return some_expr(e);
-        else
-            return none_expr();
-    }
-
-    optional<expr> unfold_recursor_core(expr const & f, unsigned i,
-                                        buffer<unsigned> const & idxs, buffer<expr> & 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<expr> 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<expr> new_arg = is_constructor_like(arg);
-            if (!new_arg)
-                return none_expr();
-            flet<expr> set_arg(arg, *new_arg);
-            return unfold_recursor_core(f, i+1, idxs, args, is_rec);
-        }
-    }
-
-    optional<expr> unfold_recursor_like(expr const & f, list<unsigned> const & idx_lst, buffer<expr> & args) {
-        buffer<unsigned> idxs;
-        to_buffer(idx_lst, idxs);
-        return unfold_recursor_core(f, 0, idxs, args, false);
-    }
-
-    optional<expr> unfold_recursor_major(expr const & f, unsigned idx, buffer<expr> & args) {
-        buffer<unsigned> 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<expr> 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<bool(expr const &)> 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);
-}
-}

src/library/normalize.h

@@ -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 <functional>
-#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);
-}

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