refactor(library/compiler): preprocess_rec ==> preprocess

src/library/compiler/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess_rec.cpp
+add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess.cpp
   compiler_step_visitor.cpp elim_recursors.cpp comp_irrelevant.cpp
   inliner.cpp rec_fn_macro.cpp erase_irrelevant.cpp reduce_arity.cpp
   lambda_lifting.cpp simp_inductive.cpp vm_compiler.cpp init_module.cpp)

src/library/compiler/init_module.cpp

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/compiler/preprocess_rec.h"
+#include "library/compiler/preprocess.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/inliner.h"
 #include "library/compiler/rec_fn_macro.h"
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 void initialize_compiler_module() {
-    initialize_preprocess_rec();
+    initialize_preprocess();
     initialize_comp_irrelevant();
     initialize_inliner();
     initialize_rec_fn_macro();
@@ -29,6 +29,6 @@ void finalize_compiler_module() {
     finalize_rec_fn_macro();
     finalize_inliner();
     finalize_comp_irrelevant();
-    finalize_preprocess_rec();
+    finalize_preprocess();
 }
 }

src/library/compiler/preprocess.cpp

@@ -85,7 +85,7 @@ static expr expand_aux_recursors(environment const & env, expr const & e) {
 
 static name * g_tmp_prefix = nullptr;
 
-class preprocess_rec_fn {
+class preprocess_fn {
     environment    m_env;
 
     bool check(declaration const & d, expr const & v) {
@@ -94,7 +94,7 @@ class preprocess_rec_fn {
         type_checker tc(m_env, memoize, trusted_only);
         expr t = tc.check(v, d.get_univ_params());
         if (!tc.is_def_eq(d.get_type(), t))
-            throw exception("preprocess_rec failed");
+            throw exception("preprocess failed");
         return true;
     }
 
@@ -111,7 +111,7 @@ class preprocess_rec_fn {
     }
 
 public:
-    preprocess_rec_fn(environment const & env):
+    preprocess_fn(environment const & env):
         m_env(env) {}
 
     void operator()(declaration const & d, buffer<pair<name, expr>> & procs) {
@@ -154,11 +154,11 @@ public:
     }
 };
 
-void preprocess_rec(environment const & env, declaration const & d, buffer<pair<name, expr>> & result) {
-    return preprocess_rec_fn(env)(d, result);
+void preprocess(environment const & env, declaration const & d, buffer<pair<name, expr>> & result) {
+    return preprocess_fn(env)(d, result);
 }
 
-void initialize_preprocess_rec() {
+void initialize_preprocess() {
     register_trace_class("compiler");
     register_trace_class({"compiler", "input"});
     register_trace_class({"compiler", "expand_aux_recursors"});
@@ -174,7 +174,7 @@ void initialize_preprocess_rec() {
     g_tmp_prefix = new name(name::mk_internal_unique_name());
 }
 
-void finalize_preprocess_rec() {
+void finalize_preprocess() {
     delete g_tmp_prefix;
 }
 }

src/library/compiler/preprocess.h

@@ -13,8 +13,8 @@ namespace lean {
     eliminate nested (recursive) recursor applications.
     Each nested recursive application becomes a new definition.
 */
-void preprocess_rec(environment const & env, declaration const & d, buffer<pair<name, expr>> & result);
+void preprocess(environment const & env, declaration const & d, buffer<pair<name, expr>> & result);
 
-void initialize_preprocess_rec();
-void finalize_preprocess_rec();
+void initialize_preprocess();
+void finalize_preprocess();
 }

src/library/compiler/vm_compiler.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/erase_irrelevant.h"
-#include "library/compiler/preprocess_rec.h"
+#include "library/compiler/preprocess.h"
 
 namespace lean {
 class vm_compiler_fn {
@@ -270,7 +270,7 @@ environment vm_compile(environment const & env, buffer<pair<name, expr>> const &
 
 environment vm_compile(environment const & env, declaration const & d) {
     buffer<pair<name, expr>> procs;
-    preprocess_rec(env, d, procs);
+    preprocess(env, d, procs);
     return vm_compile(env, procs);
 }