From 26b47c285251e3a84e82a2fdbd3bf74f035684f6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Jun 2018 08:57:22 -0700 Subject: [PATCH] chore(kernel/old_type_checker): cleanup --- src/kernel/old_type_checker.cpp | 6 ------ src/kernel/old_type_checker.h | 19 ++++--------------- 2 files changed, 4 insertions(+), 21 deletions(-) diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index 2581cca020..96888c832f 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -256,12 +256,6 @@ expr old_type_checker::ensure_pi(expr const & e, expr const & s) { return ensure_pi_core(e, s); } -bool old_type_checker::is_def_eq_types(expr const & t, expr const & s) { - expr t1 = infer_type_core(t, true); - expr t2 = infer_type_core(s, true); - return is_def_eq(t1, t2); -} - /** \brief Return true iff \c e is a proposition */ bool old_type_checker::is_prop(expr const & e) { return whnf(infer_type(e)) == mk_Prop(); diff --git a/src/kernel/old_type_checker.h b/src/kernel/old_type_checker.h index bf160613b3..3b405ab787 100644 --- a/src/kernel/old_type_checker.h +++ b/src/kernel/old_type_checker.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include #include #include -#include "runtime/flet.h" #include "util/lbool.h" #include "util/name_set.h" #include "util/name_generator.h" @@ -76,12 +75,13 @@ class old_type_checker : public abstract_type_context { reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n); lbool lazy_delta_reduction(expr & t_n, expr & s_n); bool is_def_eq_core(expr const & t, expr const & s); + optional expand_macro(expr const & m); + /** \brief Like \c check, but ignores undefined universes */ + expr check_ignore_undefined_universes(expr const & e); public: /** \brief Create a type checker for the given environment. - memoize: if true, then inferred types are memoized/cached. - - */ + memoize: if true, then inferred types are memoized/cached. */ old_type_checker(environment const & env, bool memoize = true, bool non_meta_only = true); ~old_type_checker(); @@ -100,13 +100,10 @@ public: Throw an exception if a type error is found. */ expr check(expr const & t, level_param_names const & ps); /** \brief Like \c check, but ignores undefined universes */ - expr check_ignore_undefined_universes(expr const & e); virtual expr check(expr const & t) { return check_ignore_undefined_universes(t); } /** \brief Return true iff t is definitionally equal to s. */ virtual bool is_def_eq(expr const & t, expr const & s); - /** \brief Return true iff types of \c t and \c s are (may be) definitionally equal. */ - bool is_def_eq_types(expr const & t, expr const & s); /** \brief Return true iff t is a proposition. */ bool is_prop(expr const & t); /** \brief Return the weak head normal form of \c t. */ @@ -128,14 +125,6 @@ public: expr ensure_type(expr const & e) { return ensure_sort(infer(e), e); } - - optional expand_macro(expr const & m); - - template - typename std::result_of::type with_params(level_param_names const & ps, F && f) { - flet updt(m_params, &ps); - return f(); - } }; typedef std::shared_ptr old_type_checker_ref;