max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel/old_type_checker): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-11 08:57:22 -07:00
parent bf165e0f51
commit 26b47c2852
2 changed files with 4 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/old_type_checker.cpp
View file

@ -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();

19
src/kernel/old_type_checker.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include <memory>
#include <utility>
#include <algorithm>
#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<expr> 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<expr> expand_macro(expr const & m);
template<typename F>
typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {
flet<level_param_names const *> updt(m_params, &ps);
return f();
}
};
typedef std::shared_ptr<old_type_checker> old_type_checker_ref;