From 7f96c07a01ad6b303785c61827d283ac7bdad8a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Oct 2013 09:58:12 -0700 Subject: [PATCH] refactor(library): rename light_checker to type_inferer Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/elaborator/elaborator.cpp | 10 +++---- src/library/ho_unifier.cpp | 12 ++++----- src/library/rewriter/rewriter.cpp | 26 +++++++++---------- .../{light_checker.cpp => type_inferer.cpp} | 16 ++++++------ .../{light_checker.h => type_inferer.h} | 6 ++--- src/tests/library/CMakeLists.txt | 6 ++--- .../{light_checker.cpp => type_inferer.cpp} | 8 +++--- 8 files changed, 43 insertions(+), 43 deletions(-) rename src/library/{light_checker.cpp => type_inferer.cpp} (93%) rename src/library/{light_checker.h => type_inferer.h} (93%) rename src/tests/library/{light_checker.cpp => type_inferer.cpp} (96%) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index a6e8cc953..627699b4d 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index d1baf032b..7c4b621b2 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/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> m_case_splits; @@ -656,7 +656,7 @@ class elaborator::imp { // unification_constraints_wrapper ucw; buffer 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 const & s, std::shared_ptr 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); } diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp index 92b05c592..2f9fe1c0a 100644 --- a/src/library/ho_unifier.cpp +++ b/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 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); } }; diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 825ba53ad..e83886011 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/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 then_rewriter_cell::operator()(environment const & env, context pair 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 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 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 lambda_type_rewriter_cell::operator()(environment const & env, expr const & ty = abst_domain(v); pair 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 lambda_body_rewriter_cell::operator()(environment const & env, expr const & ty = abst_domain(v); context new_ctx = extend(ctx, n, ty); pair 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 pi_type_rewriter_cell::operator()(environment const & env, cont expr const & ty = abst_domain(v); pair 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 pi_body_rewriter_cell::operator()(environment const & env, cont expr const & ty = abst_domain(v); context new_ctx = extend(ctx, n, ty); pair 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 let_type_rewriter_cell::operator()(environment const & env, con expr const & ty = let_type(v); pair 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 let_value_rewriter_cell::operator()(environment const & env, co expr const & val = let_value(v); pair 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 let_body_rewriter_cell::operator()(environment const & env, con expr const & val = let_value(v); context new_ctx = extend(ctx, n, ty); pair 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 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 repeat_rewriter_cell::operator()(environment const & env, context & ctx, expr const & v) const throw(rewriter_exception) { pair result = mk_success_rewriter()(env, ctx, v); - light_checker lc(env); + type_inferer lc(env); try { while (true) { pair new_result = m_rw(env, ctx, result.first); diff --git a/src/library/light_checker.cpp b/src/library/type_inferer.cpp similarity index 93% rename from src/library/light_checker.cpp rename to src/library/type_inferer.cpp index 630fc6c67..cea5897d1 100644 --- a/src/library/light_checker.cpp +++ b/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 cache; typedef buffer unification_constraints; @@ -209,15 +209,15 @@ public: m_menv_timestamp = 0; } }; -light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {} -light_checker::~light_checker() {} -expr light_checker::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer & uc) { +type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {} +type_inferer::~type_inferer() {} +expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer & 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 uc; return operator()(e, ctx, nullptr, uc); } -void light_checker::clear() { m_ptr->clear(); } -void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } +void type_inferer::clear() { m_ptr->clear(); } +void type_inferer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } } diff --git a/src/library/light_checker.h b/src/library/type_inferer.h similarity index 93% rename from src/library/light_checker.h rename to src/library/type_inferer.h index 3c81da6e5..2c99900f5 100644 --- a/src/library/light_checker.h +++ b/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 m_ptr; public: - light_checker(environment const & env); - ~light_checker(); + type_inferer(environment const & env); + ~type_inferer(); expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer & uc); expr operator()(expr const & e, context const & ctx = context()); diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 09d01ee4b..8563b3d20 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,6 +1,6 @@ -add_executable(light_checker light_checker.cpp) -target_link_libraries(light_checker ${EXTRA_LIBS}) -add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker) +add_executable(type_inferer type_inferer.cpp) +target_link_libraries(type_inferer ${EXTRA_LIBS}) +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) diff --git a/src/tests/library/light_checker.cpp b/src/tests/library/type_inferer.cpp similarity index 96% rename from src/tests/library/light_checker.cpp rename to src/tests/library/type_inferer.cpp index 01fa88734..2078ca9a7 100644 --- a/src/tests/library/light_checker.cpp +++ b/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));