refactor(library): move equations to equations_compiler

src/CMakeLists.txt

@@ -339,6 +339,8 @@ add_subdirectory(library/tactic/backward)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
 add_subdirectory(library/constructions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
+add_subdirectory(library/equations_compiler)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
 # add_subdirectory(library/blast)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
 # add_subdirectory(library/blast/backward)

src/frontends/lean/builtin_exprs.cpp

@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 #include "library/string.h"
 #include "library/trace.h"
 #include "library/tactic/elaborate.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"

src/frontends/lean/decl_cmds.cpp

@@ -24,7 +24,7 @@ Author: Leonardo de Moura
 #include "library/abbreviation.h"
 #include "library/flycheck.h"
 #include "library/error_handling.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/vm/vm.h"

src/frontends/lean/match_expr.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"

src/frontends/lean/old_elaborator.cpp

@@ -43,7 +43,7 @@ Author: Leonardo de Moura
 #include "library/class_instance_resolution.h"
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/vm/vm.h"

src/frontends/lean/parser.cpp

@@ -46,7 +46,7 @@ Author: Leonardo de Moura
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/legacy_type_context.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"

src/frontends/lean/pp.cpp

@@ -37,7 +37,7 @@ Author: Leonardo de Moura
 #include "library/string.h"
 #include "library/type_context.h"
 #include "library/idx_metavar.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/tactic/tactic_state.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/erase_irrelevant.h"

src/frontends/lean/type_util.h

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/old_util.h"
+#include "library/util.h"
 
 namespace lean {
 class parser;

src/library/constructions/CMakeLists.txt

@@ -1,5 +1,2 @@
 add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp
-  no_confusion.cpp projection.cpp brec_on.cpp equations.cpp
-  init_module.cpp
-#LEGACY
-  old_goal.cpp old_inversion.cpp)
+  no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp)

src/library/constructions/init_module.cpp

@@ -4,18 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/old_util.h"
-#include "library/constructions/equations.h"
 #include "library/constructions/projection.h"
 
 namespace lean{
 void initialize_constructions_module() {
-    initialize_equations();
     initialize_def_projection();
 }
 
 void finalize_constructions_module() {
     finalize_def_projection();
-    finalize_equations();
 }
 }

src/library/constructions/projection.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "library/util.h"
 
 namespace lean {
 /** \brief Create projections operators for the structure named \c n.

src/library/equations_compiler/equations.cpp

@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/normalize.h"
 #include "library/pp_options.h"
-#include "library/constructions/old_inversion.h"
+#include "library/equations_compiler/old_inversion.h"
 
 namespace lean {
 static name * g_equations_name                 = nullptr;

src/library/equations_compiler/old_goal.cpp

@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "library/metavar.h"
 #include "library/util.h"
 #include "library/old_util.h"
-#include "library/constructions/old_goal.h"
+#include "library/equations_compiler/old_goal.h"
 
 namespace lean {
 old_local_context old_goal::to_local_context() const {

src/library/equations_compiler/old_inversion.cpp

@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/reducible.h"
 #include "library/class_instance_resolution.h"
-#include "library/constructions/old_inversion.h"
+#include "library/equations_compiler/old_inversion.h"
 
 namespace lean {
 namespace inversion {

src/library/equations_compiler/old_inversion.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/metavar.h"
-#include "library/constructions/old_goal.h"
+#include "library/equations_compiler/old_goal.h"
 
 
 namespace lean {

src/library/old_util.cpp

@@ -262,22 +262,6 @@ bool is_some(expr const & e, expr & A, expr & a) {
     }
 }
 
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
-    switch (k) {
-    case implicit_infer_kind::Implicit: {
-        bool strict = true;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::RelaxedImplicit: {
-        bool strict = false;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::None:
-        return type;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
 bool has_expr_metavar_relaxed(expr const & e) {
     if (!has_expr_metavar(e))
         return false;

src/library/old_util.h

@@ -70,13 +70,6 @@ bool is_none(expr const & e, expr & A);
 /** \brief Return true iff \c e is of the form (@option.some A a), and update \c A and \c a */
 bool is_some(expr const & e, expr & A, expr & a);
 
-enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
-
-/** \brief Infer implicit parameter annotations for the first \c nparams using mode
-    specified by \c k.
-*/
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
-
 /** \brief Similar to has_expr_metavar, but ignores metavariables occurring in the type
     of local constants */
 bool has_expr_metavar_relaxed(expr const & e);

src/library/util.cpp

@@ -909,6 +909,22 @@ expr beta_eta_reduce(expr t) {
     return eta_beta_reduce_fn<true, true>()(t);
 }
 
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
+    switch (k) {
+    case implicit_infer_kind::Implicit: {
+        bool strict = true;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::RelaxedImplicit: {
+        bool strict = false;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::None:
+        return type;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
 void initialize_library_util() {
     g_true           = new expr(mk_constant(get_true_name()));
     g_true_intro     = new expr(mk_constant(get_true_intro_name()));

src/library/util.h

@@ -229,6 +229,12 @@ expr beta_reduce(expr t);
 expr eta_reduce(expr t);
 expr beta_eta_reduce(expr t);
 
+enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
+
+/** \brief Infer implicit parameter annotations for the first \c nparams using mode
+    specified by \c k. */
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
+
 void initialize_library_util();
 void finalize_library_util();
 }