From 5d00936a8fb9483fcc5ebbd88b475bc8dc912f08 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 08:48:21 -0700 Subject: [PATCH] chore(*): remove some `old_type_checker` dependencies --- src/frontends/lean/builtin_cmds.cpp | 5 ++--- src/frontends/lean/builtin_exprs.cpp | 1 - src/frontends/lean/util.cpp | 1 - src/library/aux_definition.cpp | 1 - src/library/class.cpp | 1 - src/library/compiler/preprocess.cpp | 4 ++-- src/library/compiler/util.cpp | 1 - src/library/derive_attribute.cpp | 1 - src/library/equations_compiler/util.cpp | 1 - src/library/trace.cpp | 4 ++-- src/library/util.cpp | 1 - src/library/vm/interaction_state_imp.h | 1 - 12 files changed, 6 insertions(+), 16 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2d0c999ffd..32f4742397 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "runtime/compact.h" #include "util/timeit.h" #include "util/sexpr/option_declarations.h" -#include "kernel/old_type_checker.h" #include "kernel/replace_fn.h" #include "kernel/find_fn.h" #include "kernel/instantiate.h" @@ -180,8 +179,8 @@ environment check_cmd(parser & p) { expr e; names ls; transient_cmd_scope cmd_scope(p); std::tie(e, ls) = parse_local_expr(p, "_check"); - old_type_checker tc(p.env(), true, false); - expr type = tc.check(e, ls); + type_context_old tc(p.env()); + expr type = tc.infer(e); if (is_synthetic_sorry(e) && (is_synthetic_sorry(type) || is_metavar(type))) { // do not show useless type-checking results such as ?? : ?M_1 return p.env(); diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index e4e2ac6481..39e88fb81b 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "util/sexpr/option_declarations.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "kernel/old_type_checker.h" #include "library/annotation.h" #include "library/placeholder.h" #include "library/explicit.h" diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 991b5c794b..a10944bb0b 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -12,7 +12,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" -#include "kernel/old_type_checker.h" #include "library/error_msgs.h" #include "library/scoped_ext.h" #include "library/annotation.h" diff --git a/src/library/aux_definition.cpp b/src/library/aux_definition.cpp index 66966fa1cc..826675f4f5 100644 --- a/src/library/aux_definition.cpp +++ b/src/library/aux_definition.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "kernel/replace_fn.h" -#include "kernel/old_type_checker.h" #include "library/locals.h" #include "library/placeholder.h" #include "library/module.h" diff --git a/src/library/class.cpp b/src/library/class.cpp index 166b67c9b5..36d1c9b269 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "util/lbool.h" #include "util/fresh_name.h" #include "util/name_set.h" -#include "kernel/old_type_checker.h" #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" #include "library/scoped_ext.h" diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 92ef94be4c..7d77fcf1b5 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/declaration.h" -#include "kernel/old_type_checker.h" #include "kernel/replace_fn.h" #include "kernel/instantiate.h" +#include "kernel/type_checker.h" #include "kernel/for_each_fn.h" #include "library/scope_pos_info_provider.h" #include "library/trace.h" @@ -172,7 +172,7 @@ class preprocess_fn { bool check(constant_info const & d, expr const & v) { bool memoize = true; bool non_meta_only = false; - old_type_checker tc(m_env, memoize, non_meta_only); + type_checker tc(m_env, memoize, non_meta_only); expr t = tc.check(v, d.get_lparams()); if (!tc.is_def_eq(d.get_type(), t)) throw exception("preprocess failed"); diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index facc0161c7..119bcca524 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "kernel/find_fn.h" -#include "kernel/old_type_checker.h" #include "library/aux_recursors.h" #include "library/util.h" #include "library/vm/vm.h" diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index 0c1f7b159e..3493693fa3 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include #include "runtime/sstream.h" #include "kernel/find_fn.h" -#include "kernel/old_type_checker.h" #include "library/util.h" #include "library/scoped_ext.h" #include "library/user_recursors.h" diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 0ef3d94bb2..d20928c6ac 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/find_fn.h" -#include "kernel/old_type_checker.h" #include "library/scope_pos_info_provider.h" #include "library/util.h" #include "library/module.h" diff --git a/src/library/trace.cpp b/src/library/trace.cpp index 55eec9f12b..44418b3975 100644 --- a/src/library/trace.cpp +++ b/src/library/trace.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "util/sexpr/option_declarations.h" #include "kernel/environment.h" -#include "kernel/old_type_checker.h" +#include "kernel/type_checker.h" #include "library/io_state.h" #include "library/trace.h" #include "library/messages.h" @@ -175,7 +175,7 @@ struct silent_ios_helper { }; MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper); -MK_THREAD_LOCAL_GET(old_type_checker, get_dummy_tc, get_dummy_env()); +MK_THREAD_LOCAL_GET(type_checker, get_dummy_tc, get_dummy_env()); scope_trace_silent::scope_trace_silent(bool flag) { m_old_value = g_silent; diff --git a/src/library/util.cpp b/src/library/util.cpp index bf7563e444..6040dc90b7 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "util/fresh_name.h" #include "kernel/find_fn.h" #include "kernel/instantiate.h" -#include "kernel/old_type_checker.h" #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/abstract_type_context.h" diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index 243c152dc0..77d7c87f95 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -8,7 +8,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include "runtime/sstream.h" #include "util/fresh_name.h" #include "kernel/instantiate.h" -#include "kernel/old_type_checker.h" #include "library/profiling.h" #include "library/constants.h" #include "library/message_builder.h"