chore(library/compiler): erase_irrelevant ==> old_erase_irrelevant

src/frontends/lean/pp.cpp

@@ -35,7 +35,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/equations.h"
 #include "library/tactic/tactic_state.h"
 #include "library/compiler/comp_irrelevant.h"
-#include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/util.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/prenum.h"

src/library/compiler/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(compiler OBJECT old_util.cpp eta_expansion.cpp preprocess.cpp
   compiler_step_visitor.cpp comp_irrelevant.cpp
-  inliner.cpp erase_irrelevant.cpp reduce_arity.cpp
+  inliner.cpp old_erase_irrelevant.cpp reduce_arity.cpp
   lambda_lifting.cpp simp_inductive.cpp nat_value.cpp
   vm_compiler.cpp old_cse.cpp elim_unused_lets.cpp extract_values.cpp init_module.cpp
   ## New compiler

src/library/compiler/init_module.cpp

@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 #include "library/compiler/nat_value.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/inliner.h"
-#include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/vm_compiler.h"
 
+#include "library/compiler/util.h"
 #include "library/compiler/lcnf.h"
 #include "library/compiler/elim_dead_let.h"
 #include "library/compiler/cse.h"
@@ -22,10 +22,10 @@ void initialize_compiler_module() {
     initialize_nat_value();
     initialize_comp_irrelevant();
     initialize_inliner();
-    initialize_erase_irrelevant();
     initialize_simp_inductive();
     initialize_vm_compiler();
     //======
+    initialize_compiler_util();
     initialize_lcnf();
     initialize_elim_dead_let();
     initialize_cse();
@@ -35,10 +35,10 @@ void finalize_compiler_module() {
     finalize_cse();
     finalize_elim_dead_let();
     finalize_lcnf();
+    finalize_compiler_util();
     //======
     finalize_vm_compiler();
     finalize_simp_inductive();
-    finalize_erase_irrelevant();
     finalize_inliner();
     finalize_comp_irrelevant();
     finalize_nat_value();

src/library/compiler/lambda_lifting.cpp

@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/sorry.h"
 #include "library/compiler/old_util.h"
-#include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/compiler_step_visitor.h"
 #include "library/compiler/procedure.h"
 

src/library/compiler/old_cse.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/vm/vm.h"
 #include "library/compiler/procedure.h"
-#include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/util.h"
 #include "library/compiler/compiler_step_visitor.h"
 #include "library/compiler/simp_inductive.h"
 

src/library/compiler/old_erase_irrelevant.cpp

@@ -16,32 +16,13 @@ Author: Leonardo de Moura
 #include "library/compiler/compiler_step_visitor.h"
 
 namespace lean {
-static expr * g_neutral_expr     = nullptr;
-static expr * g_unreachable_expr = nullptr;
-
-expr mk_unreachable_expr() {
-    return *g_unreachable_expr;
-}
-
-expr mk_neutral_expr() {
-    return *g_neutral_expr;
-}
-
-bool is_neutral_expr(expr const & e) {
-    return e == *g_neutral_expr;
-}
-
-bool is_unreachable_expr(expr const & e) {
-    return e == *g_unreachable_expr;
-}
-
-class erase_irrelevant_fn : public compiler_step_visitor {
+class old_erase_irrelevant_fn : public compiler_step_visitor {
     virtual expr visit_sort(expr const &) override {
-        return *g_neutral_expr;
+        return mk_neutral_expr();
     }
 
     virtual expr visit_pi(expr const &) override {
-        return *g_neutral_expr;
+        return mk_neutral_expr();
     }
 
     bool is_comp_irrelevant(expr const & e) {
@@ -64,9 +45,9 @@ class erase_irrelevant_fn : public compiler_step_visitor {
 
     virtual expr visit_mdata(expr const & e) override {
         if (is_marked_as_comp_irrelevant(e)) {
-            return *g_neutral_expr;
+            return mk_neutral_expr();
         } else if (is_comp_irrelevant(e)) {
-            return *g_neutral_expr;
+            return mk_neutral_expr();
         } else {
             return visit(mdata_expr(e));
         }
@@ -74,16 +55,16 @@ class erase_irrelevant_fn : public compiler_step_visitor {
 
     virtual expr visit_local(expr const & e) override {
         if (is_comp_irrelevant(e))
-            return *g_neutral_expr;
+            return mk_neutral_expr();
         else
             return e;
     }
 
     virtual expr visit_constant(expr const & e) override {
         if (is_comp_irrelevant(e)) {
-            return *g_neutral_expr;
+            return mk_neutral_expr();
         } else if (const_name(e) == get_lc_unreachable_name()) {
-            return *g_unreachable_expr;
+            return mk_unreachable_expr();
         } else {
             /* Erase universe level information */
             return mk_constant(const_name(e));
@@ -94,7 +75,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         if (!has_loose_bvars(e) && !has_local(e))
             return e; // keep closed types for runtime debugger
         else
-            return *g_neutral_expr;
+            return mk_neutral_expr();
     }
 
     static bool is_irrelevant_lambda_let_body(expr e) {
@@ -181,7 +162,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         name const & rec_name       = const_name(fn);
         name const & I_name         = rec_name.get_prefix();
         if (I_name == get_false_name())
-            return *g_unreachable_expr;
+            return mk_unreachable_expr();
         constant_info I_info        = env().get(I_name);
         inductive_val I_val         = I_info.to_inductive_val();
         unsigned nparams            = I_val.get_nparams();
@@ -209,7 +190,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         name const & rec_name       = const_name(fn);
         name const & I_name         = rec_name.get_prefix();
         if (I_name == get_false_name())
-            return *g_unreachable_expr;
+            return mk_unreachable_expr();
 
         /* This preprocessing step assumes that recursive recursors have already been eliminated */
         lean_assert(!is_recursive_datatype(env(), I_name));
@@ -274,7 +255,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         if (!lhs_constructor || !rhs_constructor)
             throw exception(sstream() << "code generation failed, unsupported occurrence of '" << no_confusion_name << "', constructors expected");
         if (lhs_constructor != rhs_constructor)
-            return *g_unreachable_expr;
+            return mk_unreachable_expr();
         lean_assert(args.size() >= basic_arity + 1);
         expr major = args[nparams + nindices + 4];
         type_context_old::tmp_locals locals(ctx());
@@ -285,7 +266,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
 
         unsigned c_data_sz = get_constructor_arity(env(), *lhs_constructor) - nparams;
         for (unsigned i = 0; i < c_data_sz; i++)
-            r = mk_app(r, *g_neutral_expr); // add dummy proofs
+            r = mk_app(r, mk_neutral_expr()); // add dummy proofs
         /* add remaining arguments */
         return add_args(r, nparams + nindices + 5, args);
     }
@@ -302,7 +283,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
         lean_assert(args.size() >= 5);
         expr minor = visit(args[3]);
         expr major = visit(args[4]);
-        expr r     = mk_app(minor, major, *g_neutral_expr);
+        expr r     = mk_app(minor, major, mk_neutral_expr());
         return add_args(r, 5, args);
     }
 
@@ -364,7 +345,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
 
     virtual expr visit_app(expr const & e) override {
         if (is_comp_irrelevant(e))
-            return *g_neutral_expr;
+            return mk_neutral_expr();
         if (auto n = to_nat_value(ctx(), e))
             return *n;
         buffer<expr> args;
@@ -398,28 +379,18 @@ class erase_irrelevant_fn : public compiler_step_visitor {
             } else if (n == get_subtype_val_name()) {
                 return visit_subtype_val(args);
             } else if (n == get_lc_unreachable_name()) {
-                return *g_unreachable_expr;
+                return mk_unreachable_expr();
             }
         }
         return compiler_step_visitor::visit_app(e);
     }
 
 public:
-    erase_irrelevant_fn(environment const & env, abstract_context_cache & cache):
+    old_erase_irrelevant_fn(environment const & env, abstract_context_cache & cache):
         compiler_step_visitor(env, cache) {}
 };
 
-expr erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e) {
-    return erase_irrelevant_fn(env, cache)(e);
-}
-
-void initialize_erase_irrelevant() {
-    g_neutral_expr     = new expr(mk_constant("_neutral_"));
-    g_unreachable_expr = new expr(mk_constant("_unreachable_"));
-}
-
-void finalize_erase_irrelevant() {
-    delete g_neutral_expr;
-    delete g_unreachable_expr;
+expr old_erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e) {
+    return old_erase_irrelevant_fn(env, cache)(e);
 }
 }

src/library/compiler/old_erase_irrelevant.h

@@ -13,14 +13,5 @@ class abstract_context_cache;
 
     \remark The resultant term cannot be type checked. So, any preprocessing step
     that requires type inference cannot be applied after this transformation.  */
-expr erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e);
-/** \brief Neutral auxiliary term. */
-bool is_neutral_expr(expr const & e);
-bool is_unreachable_expr(expr const & e);
-
-expr mk_neutral_expr();
-expr mk_unreachable_expr();
-
-void initialize_erase_irrelevant();
-void finalize_erase_irrelevant();
+expr old_erase_irrelevant(environment const & env, abstract_context_cache & cache, expr const & e);
 }

src/library/compiler/old_util.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "library/compiler/util.h"
 namespace lean {
 class type_context_old;
 /** \brief Create a new name of the form prefix.suffix_idx that is not the name of a declaration and/or VM function.

src/library/compiler/preprocess.cpp

@@ -29,7 +29,7 @@ Author: Leonardo de Moura
 #include "library/compiler/nat_value.h"
 #include "library/compiler/eta_expansion.h"
 #include "library/compiler/inliner.h"
-#include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/old_erase_irrelevant.h"
 #include "library/compiler/reduce_arity.h"
 #include "library/compiler/lambda_lifting.h"
 #include "library/compiler/simp_inductive.h"
@@ -193,7 +193,7 @@ class preprocess_fn {
 
     void erase_irrelevant(buffer<procedure> & procs) {
         for (procedure & p : procs) {
-            p.m_code = ::lean::erase_irrelevant(m_env, m_cache, p.m_code);
+            p.m_code = ::lean::old_erase_irrelevant(m_env, m_cache, p.m_code);
         }
     }
 

src/library/compiler/simp_inductive.cpp

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/vm/vm.h"
 #include "library/compiler/old_util.h"
-#include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/compiler_step_visitor.h"
 #include "library/compiler/procedure.h"
 

src/library/compiler/util.cpp

@@ -249,4 +249,33 @@ unsigned get_lcnf_size(environment const & env, expr e) {
     }
     lean_unreachable();
 }
+
+static expr * g_neutral_expr     = nullptr;
+static expr * g_unreachable_expr = nullptr;
+
+expr mk_unreachable_expr() {
+    return *g_unreachable_expr;
+}
+
+expr mk_neutral_expr() {
+    return *g_neutral_expr;
+}
+
+bool is_neutral_expr(expr const & e) {
+    return e == *g_neutral_expr;
+}
+
+bool is_unreachable_expr(expr const & e) {
+    return e == *g_unreachable_expr;
+}
+
+void initialize_compiler_util() {
+    g_neutral_expr     = new expr(mk_constant("_neutral_"));
+    g_unreachable_expr = new expr(mk_constant("_unreachable_"));
+}
+
+void finalize_compiler_util() {
+    delete g_neutral_expr;
+    delete g_unreachable_expr;
+}
 }

src/library/compiler/util.h

@@ -91,4 +91,19 @@ expr replace_fvar(expr const & e, expr const & fvar, expr const & new_fvar);
 
 /* Return the "code" size for `e` */
 unsigned get_lcnf_size(environment const & env, expr e);
+
+// =======================================
+// Auxiliary expressions for erasure.
+// We use them after we have erased proofs and unnecessary type information.
+
+expr mk_neutral_expr();
+expr mk_unreachable_expr();
+
+bool is_neutral_expr(expr const & e);
+bool is_unreachable_expr(expr const & e);
+
+// =======================================
+
+void initialize_compiler_util();
+void finalize_compiler_util();
 }

src/library/compiler/vm_compiler.cpp

@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm.h"
 #include "library/vm/optimize.h"
 #include "library/compiler/simp_inductive.h"
-#include "library/compiler/erase_irrelevant.h"
+#include "library/compiler/util.h"
 #include "library/compiler/nat_value.h"
 #include "library/compiler/preprocess.h"
 #include "library/compiler/comp_irrelevant.h"