refactor(library): rename light_checker to type_inferer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   context_to_lambda.cpp state.cpp update_expr.cpp reduce.cpp
-  light_checker.cpp placeholder.cpp ho_unifier.cpp expr_lt.cpp)
+  type_inferer.cpp placeholder.cpp ho_unifier.cpp expr_lt.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/elaborator/elaborator.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/instantiate.h"
 #include "kernel/builtin.h"
-#include "library/light_checker.h"
+#include "library/type_inferer.h"
 #include "library/update_expr.h"
 #include "library/reduce.h"
 #include "library/elaborator/elaborator.h"
@@ -128,7 +128,7 @@ class elaborator::imp {
     };
 
     environment const &                      m_env;
-    light_checker                            m_type_infer;
+    type_inferer                             m_type_inferer;
     normalizer                               m_normalizer;
     state                                    m_state;
     std::vector<std::unique_ptr<case_split>> m_case_splits;
@@ -656,7 +656,7 @@ class elaborator::imp {
         // unification_constraints_wrapper ucw;
         buffer<expr> arg_types;
         for (unsigned i = 1; i < num_a; i++) {
-            arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw));
+            arg_types.push_back(m_type_inferer(arg(a, i), ctx, &s, &ucw));
         }
 #endif
         return true;
@@ -682,7 +682,7 @@ public:
     imp(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs,
         options const & opts, std::shared_ptr<synthesizer> const & s, std::shared_ptr<elaborator_plugin> const & p):
         m_env(env),
-        m_type_infer(env),
+        m_type_inferer(env),
         m_normalizer(env),
         m_state(menv, num_cnstrs, cnstrs),
         m_synthesizer(s),
@@ -733,7 +733,7 @@ public:
 
     void interrupt() {
         m_interrupted = true;
-        m_type_infer.set_interrupt(true);
+        m_type_inferer.set_interrupt(true);
         m_normalizer.set_interrupt(true);
     }
 

src/library/ho_unifier.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/normalizer.h"
 #include "kernel/printer.h"
-#include "library/light_checker.h"
+#include "library/type_inferer.h"
 #include "library/reduce.h"
 #include "library/update_expr.h"
 #include "library/ho_unifier.h"
@@ -81,7 +81,7 @@ class ho_unifier::imp {
 
     environment    m_env;
     normalizer     m_normalizer;
-    light_checker  m_type_infer;
+    type_inferer   m_type_inferer;
     state_stack    m_state_stack;
     unsigned       m_delayed;
     unsigned       m_next_state_id;
@@ -380,10 +380,10 @@ class ho_unifier::imp {
         // unification_constraints_wrapper ucw;
         buffer<expr> arg_types;
         for (unsigned i = 1; i < num_a; i++) {
-            arg_types.push_back(m_type_infer(arg(a, i), ctx, &s, &ucw));
+            arg_types.push_back(m_type_inferer(arg(a, i), ctx, &s, &ucw));
         }
         // Clear m_type_infer cache since we don't want a reference to s inside of m_type_infer
-        m_type_infer.clear();
+        m_type_inferer.clear();
         if (ucw.failed())
             return false;
         m_state_stack.pop_back();
@@ -637,7 +637,7 @@ public:
     imp(environment const & env, options const & opts):
         m_env(env),
         m_normalizer(env, opts),
-        m_type_infer(env) {
+        m_type_inferer(env) {
         m_interrupted       = false;
         m_delayed           = 0;
         m_max_solutions     = get_ho_unifier_max_solutions(opts);
@@ -691,7 +691,7 @@ public:
     void set_interrupt(bool flag) {
         m_interrupted = flag;
         m_normalizer.set_interrupt(flag);
-        m_type_infer.set_interrupt(flag);
+        m_type_inferer.set_interrupt(flag);
     }
 };
 

src/library/rewriter/rewriter.cpp

@@ -12,7 +12,7 @@
 #include "kernel/replace.h"
 #include "kernel/printer.h"
 #include "library/basic_thms.h"
-#include "library/light_checker.h"
+#include "library/type_inferer.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
 #include "util/buffer.h"
@@ -150,7 +150,7 @@ pair<expr, expr> then_rewriter_cell::operator()(environment const & env, context
     pair<expr, expr> new_result = result;
     for (rewriter const & rw : cdr(m_rwlist)) {
         new_result = rw(env, ctx, result.first);
-        expr const & ty = light_checker(env)(v, ctx);
+        expr const & ty = type_inferer(env)(v, ctx);
         if (v != new_result.first) {
             result = make_pair(new_result.first,
                                Trans(ty, v, result.first, new_result.first, result.second, new_result.second));
@@ -184,7 +184,7 @@ pair<expr, expr> try_rewriter_cell::operator()(environment const & env, context
         }
     }
     // If the execution reaches here, it means every rewriter failed.
-    expr const & t = light_checker(env)(v, ctx);
+    expr const & t = type_inferer(env)(v, ctx);
     return make_pair(v, Refl(t, v));
 }
 std::ostream & try_rewriter_cell::display(std::ostream & out) const {
@@ -215,7 +215,7 @@ pair<expr, expr> app_rewriter_cell::operator()(environment const & env, context
         // Information about f
         new_f = result.first;
         expr proof_f = result.second;
-        light_checker lc(env);
+        type_inferer lc(env);
         expr const & f_ty = lc(f, ctx);
         lean_assert(is_pi(f_ty));
         expr f_ty_domain = abst_domain(f_ty); // A
@@ -292,7 +292,7 @@ pair<expr, expr> lambda_type_rewriter_cell::operator()(environment const & env,
     expr const & ty = abst_domain(v);
     pair<expr, expr> result = m_rw(env, ctx, ty);
     expr const & new_ty = result.first;
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     if (ty != new_ty) {
         expr const & new_v = mk_lambda(abst_name(v), new_ty, abst_body(v));
@@ -326,7 +326,7 @@ pair<expr, expr> lambda_body_rewriter_cell::operator()(environment const & env,
     expr const & ty = abst_domain(v);
     context new_ctx = extend(ctx, n, ty);
     pair<expr, expr> result = m_rw(env, new_ctx, body);
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     expr const & new_body = result.first;
     if (body != new_body) {
@@ -376,7 +376,7 @@ pair<expr, expr> pi_type_rewriter_cell::operator()(environment const & env, cont
     expr const & ty = abst_domain(v);
     pair<expr, expr> result = m_rw(env, ctx, ty);
     expr const & new_ty = result.first;
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     if (ty != new_ty) {
         expr const & new_v = mk_pi(abst_name(v), new_ty, abst_body(v));
@@ -410,7 +410,7 @@ pair<expr, expr> pi_body_rewriter_cell::operator()(environment const & env, cont
     expr const & ty = abst_domain(v);
     context new_ctx = extend(ctx, n, ty);
     pair<expr, expr> result = m_rw(env, new_ctx, body);
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     expr const & new_body = result.first;
     if (body != new_body) {
@@ -458,7 +458,7 @@ pair<expr, expr> let_type_rewriter_cell::operator()(environment const & env, con
     expr const & ty = let_type(v);
     pair<expr, expr> result = m_rw(env, ctx, ty);
     expr const & new_ty = result.first;
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     if (ty != new_ty) {
         expr const & new_v = mk_let(let_name(v), new_ty, let_value(v), let_body(v));
@@ -489,7 +489,7 @@ pair<expr, expr> let_value_rewriter_cell::operator()(environment const & env, co
     expr const & val = let_value(v);
     pair<expr, expr> result = m_rw(env, ctx, val);
     expr const & new_val = result.first;
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     if (val != new_val) {
         expr const & new_v = mk_let(let_name(v), let_type(v), new_val, let_body(v));
@@ -524,7 +524,7 @@ pair<expr, expr> let_body_rewriter_cell::operator()(environment const & env, con
     expr const & val = let_value(v);
     context new_ctx = extend(ctx, n, ty);
     pair<expr, expr> result = m_rw(env, new_ctx, body);
-    light_checker lc(env);
+    type_inferer lc(env);
     expr const & ty_of_v = lc(v, ctx);
     expr const & new_body = result.first;
     if (body != new_body) {
@@ -578,7 +578,7 @@ std::ostream & fail_rewriter_cell::display(std::ostream & out) const {
 success_rewriter_cell::success_rewriter_cell():rewriter_cell(rewriter_kind::Success) { }
 success_rewriter_cell::~success_rewriter_cell() { }
 pair<expr, expr> success_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
-    expr const & t = light_checker(env)(v, ctx);
+    expr const & t = type_inferer(env)(v, ctx);
     return make_pair(v, Refl(t, v));
 }
 std::ostream & success_rewriter_cell::display(std::ostream & out) const {
@@ -591,7 +591,7 @@ repeat_rewriter_cell::repeat_rewriter_cell(rewriter const & rw):rewriter_cell(re
 repeat_rewriter_cell::~repeat_rewriter_cell() { }
 pair<expr, expr> repeat_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) {
     pair<expr, expr> result = mk_success_rewriter()(env, ctx, v);
-    light_checker lc(env);
+    type_inferer lc(env);
     try {
         while (true) {
             pair<expr, expr> new_result = m_rw(env, ctx, result.first);

src/library/type_inferer.cpp

@@ -14,10 +14,10 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/metavar.h"
 #include "library/reduce.h"
-#include "library/light_checker.h"
+#include "library/type_inferer.h"
 
 namespace lean {
-class light_checker::imp {
+class type_inferer::imp {
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
     typedef buffer<unification_constraint> unification_constraints;
 
@@ -209,15 +209,15 @@ public:
         m_menv_timestamp = 0;
     }
 };
-light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {}
+type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {}
-light_checker::~light_checker() {}
+type_inferer::~type_inferer() {}
-expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
+expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
     return m_ptr->operator()(e, ctx, menv, uc);
 }
-expr light_checker::operator()(expr const & e, context const & ctx) {
+expr type_inferer::operator()(expr const & e, context const & ctx) {
     buffer<unification_constraint> uc;
     return operator()(e, ctx, nullptr, uc);
 }
-void light_checker::clear() { m_ptr->clear(); }
+void type_inferer::clear() { m_ptr->clear(); }
-void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
+void type_inferer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 }

src/library/type_inferer.h

@@ -24,12 +24,12 @@ class metavar_env;
    That is, they are not meant for external users, but to sign that the
    type could not be inferred.
 */
-class light_checker {
+class type_inferer {
     class imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    light_checker(environment const & env);
+    type_inferer(environment const & env);
-    ~light_checker();
+    ~type_inferer();
 
     expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc);
     expr operator()(expr const & e, context const & ctx = context());

src/tests/library/CMakeLists.txt

@@ -1,6 +1,6 @@
-add_executable(light_checker light_checker.cpp)
+add_executable(type_inferer type_inferer.cpp)
-target_link_libraries(light_checker ${EXTRA_LIBS})
+target_link_libraries(type_inferer ${EXTRA_LIBS})
-add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker)
+add_test(type_inferer ${CMAKE_CURRENT_BINARY_DIR}/type_inferer)
 add_executable(ho_unifier ho_unifier.cpp)
 target_link_libraries(ho_unifier ${EXTRA_LIBS})
 add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier)

src/tests/library/type_inferer.cpp

@@ -10,14 +10,14 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
 #include "kernel/printer.h"
-#include "library/light_checker.h"
+#include "library/type_inferer.h"
 #include "library/arith/arith.h"
 #include "library/all/all.h"
 using namespace lean;
 
 static void tst1() {
     environment env = mk_toplevel();
-    light_checker type_of(env);
+    type_inferer type_of(env);
     expr f = Const("f");
     expr g = Const("g");
     expr a = Const("a");
@@ -48,7 +48,7 @@ static expr mk_big(unsigned val, unsigned depth) {
 
 static void tst2() {
     environment env = mk_toplevel();
-    light_checker type_of(env);
+    type_inferer type_of(env);
     type_checker  type_of_slow(env);
     expr t = mk_big(0, 10);
     {
@@ -82,7 +82,7 @@ static void tst3() {
     ctx2 = extend(ctx2, "f", Pi({A, Real}, vec2(A, Real)));
     expr F = Var(0)(Var(1));
     expr F_copy = F;
-    light_checker infer(env);
+    type_inferer infer(env);
     std::cout << infer(F, ctx1) << "\n";
     lean_assert_eq(infer(F, ctx1), vec1(Var(1), Int));
     lean_assert_eq(infer(F, ctx2), vec2(Var(1), Real));