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

refactor(kernel): remove converter class

Browse source 
This abstraction is not useful after refactoring.
This commit is contained in:
Leonardo de Moura 2016-03-19 15:58:15 -07:00
parent 856889a08d
commit 29ad781ec2
12 changed files with 523 additions and 809 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
formatter.cpp declaration.cpp environment.cpp pos_info_provider.cpp
converter.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
type_checker.cpp error_msgs.cpp kernel_exception.cpp
normalizer_extension.cpp init_module.cpp expr_cache.cpp
default_converter.cpp equiv_manager.cpp abstract_type_context.cpp)
equiv_manager.cpp abstract_type_context.cpp)

41
src/kernel/converter.cpp
View file

@ -1,41 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/interrupt.h"
#include "util/lbool.h"
#include "kernel/converter.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "kernel/free_vars.h"
#include "kernel/type_checker.h"
#include "kernel/default_converter.h"
namespace lean {
expr converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
/** \brief Do nothing converter */
struct dummy_converter : public converter {
virtual expr whnf(expr const & e, type_checker &) {
return e;
}
virtual bool is_def_eq(expr const &, expr const &, type_checker &) {
return true;
}
virtual bool is_opaque(declaration const &) const { return false; }
virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
virtual optional<expr> is_stuck(expr const &, type_checker &) { return none_expr(); }
};
std::unique_ptr<converter> mk_dummy_converter() {
return std::unique_ptr<converter>(new dummy_converter());
}
void initialize_converter() {
}
void finalize_converter() {
}
}

40
src/kernel/converter.h
View file

@ -1,40 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <functional>
#include "kernel/environment.h"
namespace lean {
class type_checker;
class converter {
protected:
expr infer_type(type_checker & tc, expr const & e);
public:
virtual ~converter() {}
virtual bool is_opaque(declaration const & d) const = 0;
virtual optional<declaration> is_delta(expr const & e) const = 0;
virtual optional<expr> is_stuck(expr const & e, type_checker & c) = 0;
virtual expr whnf(expr const & e, type_checker & c) = 0;
virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c) = 0;
};
/** \brief Converter that allows us to specify constants that should be considered opaque */
template<typename Converter>
class hint_converter : public Converter {
name_predicate m_pred;
public:
hint_converter(environment const & env, name_predicate const & p):Converter(env), m_pred(p) {}
virtual bool is_opaque(declaration const & d) const { return m_pred(d.get_name()) || Converter::is_opaque(d); }
};
std::unique_ptr<converter> mk_dummy_converter();
void initialize_converter();
void finalize_converter();
}

564
src/kernel/default_converter.cpp
View file

@ -1,564 +0,0 @@
/*
Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/interrupt.h"
#include "util/flet.h"
#include "util/fresh_name.h"
#include "kernel/default_converter.h"
#include "kernel/instantiate.h"
#include "kernel/free_vars.h"
#include "kernel/type_checker.h"
#include "kernel/error_msgs.h"
#include "library/metavar.h"
#include "library/constraint.h"
namespace lean {
static expr * g_dont_care = nullptr;
default_converter::default_converter(environment const & env, bool memoize):
m_env(env), m_memoize(memoize) {
m_tc = nullptr;
m_jst = nullptr;
}
optional<expr> default_converter::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, *m_tc);
}
/** \brief Apply normalizer extensions to \c e. */
optional<expr> default_converter::norm_ext(expr const & e) {
return m_env.norm_ext()(e, *m_tc);
}
/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
bool default_converter::is_stuck(expr const & e) {
return static_cast<bool>(m_env.norm_ext().is_stuck(e, *m_tc));
}
optional<expr> default_converter::is_stuck(expr const & e, type_checker & c) {
if (is_meta(e)) {
return some_expr(e);
} else {
return m_env.norm_ext().is_stuck(e, c);
}
}
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
expr default_converter::whnf_core(expr const & e) {
check_system("whnf");
// handle easy cases
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
return e;
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
break;
}
// check cache
if (m_memoize) {
auto it = m_whnf_core_cache.find(e);
if (it != m_whnf_core_cache.end())
return it->second;
}
// do the actual work
expr r;
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Macro:
if (auto m = expand_macro(e))
r = whnf_core(*m);
else
r = e;
break;
case expr_kind::App: {
buffer<expr> args;
expr f0 = get_app_rev_args(e, args);
expr f = whnf_core(f0);
if (is_lambda(f)) {
unsigned m = 1;
unsigned num_args = args.size();
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
}
lean_assert(m <= num_args);
r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
} else {
r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()));
}
break;
}
case expr_kind::Let:
r = whnf_core(instantiate(let_body(e), let_value(e)));
break;
}
if (m_memoize)
m_whnf_core_cache.insert(mk_pair(e, r));
return r;
}
bool default_converter::is_opaque(declaration const &) const {
return false;
}
/** \brief Expand \c e if it is non-opaque constant with height >= h */
expr default_converter::unfold_name_core(expr e, unsigned h) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && !is_opaque(*d) && d->get_height() >= h &&
length(const_levels(e)) == d->get_num_univ_params())
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
}
}
return e;
}
/**
\brief Expand constants and application where the function is a constant.
The unfolding is only performend if the constant corresponds to
a non-opaque definition with height >= h.
*/
expr default_converter::unfold_names(expr const & e, unsigned h) {
if (is_app(e)) {
expr f0 = get_app_fn(e);
expr f = unfold_name_core(f0, h);
if (is_eqp(f, f0)) {
return e;
} else {
buffer<expr> args;
get_app_rev_args(e, args);
return mk_rev_app(f, args);
}
} else {
return unfold_name_core(e, h);
}
}
/**
\brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
to be expanded.
*/
optional<declaration> default_converter::is_delta(expr const & e) const {
expr const & f = get_app_fn(e);
if (is_constant(f)) {
if (auto d = m_env.find(const_name(f)))
if (d->is_definition() && !is_opaque(*d))
return d;
}
return none_declaration();
}
/**
\brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
height greater than or equal to \c h.
This method is based on <tt>whnf_core(expr const &)</tt> and \c unfold_names.
\remark This method does not use normalization extensions attached in the environment.
*/
expr default_converter::whnf_core(expr e, unsigned h) {
while (true) {
expr new_e = unfold_names(whnf_core(e), h);
if (is_eqp(e, new_e))
return e;
e = new_e;
}
}
/** \brief Put expression \c t in weak head normal form */
expr default_converter::whnf(expr const & e_prime) {
// Do not cache easy cases
switch (e_prime.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
return e_prime;
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Let:
break;
}
expr e = e_prime;
// check cache
if (m_memoize) {
auto it = m_whnf_cache.find(e);
if (it != m_whnf_cache.end())
return it->second;
}
expr t = e;
while (true) {
expr t1 = whnf_core(t, 0);
if (auto new_t = norm_ext(t1)) {
t = *new_t;
} else {
auto r = t1;
if (m_memoize)
m_whnf_cache.insert(mk_pair(e, r));
return r;
}
}
}
/**
\brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s.
t and s are definitionally equal
iff
domain(t) is definitionally equal to domain(s)
and
body(t) is definitionally equal to body(s)
*/
bool default_converter::is_def_eq_binding(expr t, expr s) {
lean_assert(t.kind() == s.kind());
lean_assert(is_binding(t));
expr_kind k = t.kind();
buffer<expr> subst;
do {
optional<expr> var_s_type;
if (binding_domain(t) != binding_domain(s)) {
var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
if (!is_def_eq(var_t_type, *var_s_type))
return false;
}
if (!closed(binding_body(t)) || !closed(binding_body(s))) {
// local is used inside t or s
if (!var_s_type)
var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s)));
} else {
subst.push_back(*g_dont_care); // don't care
}
t = binding_body(t);
s = binding_body(s);
} while (t.kind() == k && s.kind() == k);
return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
instantiate_rev(s, subst.size(), subst.data()));
}
bool default_converter::is_def_eq(level const & l1, level const & l2) {
if (is_equivalent(l1, l2)) {
return true;
} else {
return false;
}
}
bool default_converter::is_def_eq(levels const & ls1, levels const & ls2) {
if (is_nil(ls1) && is_nil(ls2)) {
return true;
} else if (!is_nil(ls1) && !is_nil(ls2)) {
return
is_def_eq(head(ls1), head(ls2)) &&
is_def_eq(tail(ls1), tail(ls2));
} else {
return false;
}
}
/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
lbool default_converter::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
if (m_eqv_manager.is_equiv(t, s, use_hash))
return l_true;
if (t.kind() == s.kind()) {
switch (t.kind()) {
case expr_kind::Lambda: case expr_kind::Pi:
return to_lbool(is_def_eq_binding(t, s));
case expr_kind::Sort:
return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
case expr_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Var: case expr_kind::Local: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
// We do not handle these cases in this method.
break;
}
}
return l_undef; // This is not an "easy case"
}
/**
\brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
This method is used to implement an optimization in the method \c is_def_eq.
*/
bool default_converter::is_def_eq_args(expr t, expr s) {
while (is_app(t) && is_app(s)) {
if (!is_def_eq(app_arg(t), app_arg(s)))
return false;
t = app_fn(t);
s = app_fn(s);
}
return !is_app(t) && !is_app(s);
}
/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
bool default_converter::try_eta_expansion_core(expr const & t, expr const & s) {
if (is_lambda(t) && !is_lambda(s)) {
expr s_type = whnf(infer_type(s));
constraint_seq aux_cs;
if (!is_pi(s_type))
return false;
expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type));
if (!is_def_eq(t, new_s))
return false;
return true;
} else {
return false;
}
}
/** \brief Return true if \c t and \c s are definitionally equal because they are applications of the form
<tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
\c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
Return false otherwise.
*/
bool default_converter::is_def_eq_app(expr const & t, expr const & s) {
if (is_app(t) && is_app(s)) {
buffer<expr> t_args;
buffer<expr> s_args;
expr t_fn = get_app_args(t, t_args);
expr s_fn = get_app_args(s, s_args);
if (is_def_eq(t_fn, s_fn) && t_args.size() == s_args.size()) {
unsigned i = 0;
for (; i < t_args.size(); i++) {
if (!is_def_eq(t_args[i], s_args[i]))
break;
}
if (i == t_args.size())
return true;
}
}
return false;
}
/** \brief remark: is_prop returns true only if \c e is reducible to Prop.
*/
bool default_converter::is_prop(expr const & e) {
return whnf(infer_type(e)) == mk_Prop();
}
/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
Return false otherwise.
*/
bool default_converter::is_def_eq_proof_irrel(expr const & t, expr const & s) {
if (!m_env.prop_proof_irrel())
return false;
// Proof irrelevance support for Prop (aka Type.{0})
expr t_type = infer_type(t);
expr s_type = infer_type(s);
return is_prop(t_type) && is_def_eq(t_type, s_type);
}
bool default_converter::failed_before(expr const & t, expr const & s) const {
if (t.hash() < s.hash()) {
return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
} else if (t.hash() > s.hash()) {
return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
} else {
return
m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
}
}
void default_converter::cache_failure(expr const & t, expr const & s) {
if (t.hash() <= s.hash())
m_failure_cache.insert(mk_pair(t, s));
else
m_failure_cache.insert(mk_pair(s, t));
}
/**
\brief Perform one lazy delta-reduction step.
Return
- l_true if t_n and s_n are definitionally equal.
- l_false if they are not definitionally equal.
- l_undef it the step did not manage to establish whether they are definitionally equal or not.
\remark t_n, s_n and cs are updated.
*/
auto default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
auto d_t = is_delta(t_n);
auto d_s = is_delta(s_n);
if (!d_t && !d_s) {
return reduction_status::DefUnknown;
} else if (d_t && !d_s) {
t_n = whnf_core(unfold_names(t_n, 0));
} else if (!d_t && d_s) {
s_n = whnf_core(unfold_names(s_n, 0));
} else if (!d_t->is_theorem() && d_s->is_theorem()) {
t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
} else if (!d_s->is_theorem() && d_t->is_theorem()) {
s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
} else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
} else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
} else {
if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
// If t_n and s_n are both applications of the same (non-opaque) definition,
if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
// We let the unifier deal with cases such as
// (f ...) =?= (f ...)
// when t_n or s_n contains metavariables
return reduction_status::DefUnknown;
} else {
// Optimization:
// We try to check if their arguments are definitionally equal.
// If they are, then t_n and s_n must be definitionally equal, and we can
// skip the delta-reduction step.
// If the flag use_conv_opt() is not true, then we skip this optimization
if (!is_opaque(*d_t) && d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) &&
is_def_eq_args(t_n, s_n)) {
return reduction_status::DefEqual;
} else {
cache_failure(t_n, s_n);
}
}
}
}
t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
}
switch (quick_is_def_eq(t_n, s_n)) {
case l_true: return reduction_status::DefEqual;
case l_false: return reduction_status::DefDiff;
case l_undef: return reduction_status::Continue;
}
lean_unreachable();
}
lbool default_converter::lazy_delta_reduction(expr & t_n, expr & s_n) {
while (true) {
switch (lazy_delta_reduction_step(t_n, s_n)) {
case reduction_status::Continue: break;
case reduction_status::DefUnknown: return l_undef;
case reduction_status::DefEqual: return l_true;
case reduction_status::DefDiff: return l_false;
}
}
}
auto default_converter::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
auto new_t_n = norm_ext(t_n);
auto new_s_n = norm_ext(s_n);
if (!new_t_n && !new_s_n)
return reduction_status::DefUnknown;
if (new_t_n)
t_n = whnf_core(*new_t_n);
if (new_s_n)
s_n = whnf_core(*new_s_n);
switch (quick_is_def_eq(t_n, s_n)) {
case l_true: return reduction_status::DefEqual;
case l_false: return reduction_status::DefDiff;
case l_undef: return reduction_status::Continue;
}
lean_unreachable();
}
// Apply lazy delta-reduction and then normalizer extensions
lbool default_converter::reduce_def_eq(expr & t_n, expr & s_n) {
while (true) {
// first, keep applying lazy delta-reduction while applicable
lbool r = lazy_delta_reduction(t_n, s_n);
if (r != l_undef) return r;
// try normalizer extensions
switch (ext_reduction_step(t_n, s_n)) {
case reduction_status::Continue: break;
case reduction_status::DefUnknown: return l_undef;
case reduction_status::DefEqual: return l_true;
case reduction_status::DefDiff: return l_false;
}
}
}
bool default_converter::postpone_is_def_eq(expr const & t, expr const & s) {
if (has_expr_metavar(t) || has_expr_metavar(s)) {
optional<declaration> d_t = is_delta(t);
optional<declaration> d_s = is_delta(s);
if (d_t && d_s && is_eqp(*d_t, *d_s))
return true;
else if (is_stuck(t) && is_stuck(s))
return true;
}
return false;
}
bool default_converter::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
bool use_hash = true;
lbool r = quick_is_def_eq(t, s, use_hash);
if (r != l_undef) return r == l_true;
// apply whnf (without using delta-reduction or normalizer extensions)
expr t_n = whnf_core(t);
expr s_n = whnf_core(s);
if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
r = quick_is_def_eq(t_n, s_n);
if (r != l_undef) return r == l_true;
}
r = reduce_def_eq(t_n, s_n);
if (r != l_undef) return r == l_true;
if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
is_def_eq(const_levels(t_n), const_levels(s_n)))
return true;
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
return true;
bool postpone = postpone_is_def_eq(t_n, s_n);
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
if (!postpone && is_def_eq_app(t_n, s_n))
return true;
if (try_eta_expansion(t_n, s_n))
return true;
if (is_def_eq_proof_irrel(t, s))
return true;
return false;
}
bool default_converter::is_def_eq(expr const & t, expr const & s) {
bool r = is_def_eq_core(t, s);
if (r)
m_eqv_manager.add_equiv(t, s);
return r;
}
/** Return true iff t is definitionally equal to s. */
bool default_converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
flet<type_checker*> set_tc(m_tc, &c);
return is_def_eq(t, s);
}
expr default_converter::whnf(expr const & e, type_checker & c) {
flet<type_checker*> set_tc(m_tc, &c);
return whnf(e);
}
void initialize_default_converter() {
g_dont_care = new expr(Const("dontcare"));
}
void finalize_default_converter() {
delete g_dont_care;
}
}

86
src/kernel/default_converter.h
View file

@ -1,86 +0,0 @@
/*
Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <unordered_set>
#include "util/lbool.h"
#include "kernel/environment.h"
#include "kernel/converter.h"
#include "kernel/expr_maps.h"
#include "kernel/equiv_manager.h"
#include "kernel/expr_pair.h"
#include "library/justification.h"
namespace lean {
/** \brief Converter used in the kernel */
class default_converter : public converter {
protected:
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
environment m_env;
bool m_memoize;
expr_struct_map<expr> m_whnf_core_cache;
expr_struct_map<expr> m_whnf_cache;
equiv_manager m_eqv_manager;
expr_pair_set m_failure_cache;
// The two auxiliary fields are set when the public methods whnf and is_def_eq are invoked.
// The goal is to avoid to keep carrying them around.
type_checker * m_tc;
delayed_justification * m_jst;
virtual bool is_stuck(expr const & e);
virtual optional<expr> norm_ext(expr const & e);
expr infer_type(expr const & e) { return converter::infer_type(*m_tc, e); }
optional<expr> expand_macro(expr const & m);
expr whnf_core(expr const & e);
expr unfold_name_core(expr e, unsigned w);
expr unfold_names(expr const & e, unsigned w);
expr whnf_core(expr e, unsigned w);
expr whnf(expr const & e_prime);
bool is_def_eq_binding(expr t, expr s);
bool is_def_eq(level const & l1, level const & l2);
bool is_def_eq(levels const & ls1, levels const & ls2);
lbool quick_is_def_eq(expr const & t, expr const & s, bool use_hash = false);
bool is_def_eq_args(expr t, expr s);
bool try_eta_expansion_core(expr const & t, expr const & s);
bool try_eta_expansion(expr const & t, expr const & s) {
return try_eta_expansion_core(t, s) || try_eta_expansion_core(s, t);
}
bool is_def_eq(expr const & t, expr const & s);
bool is_def_eq_app(expr const & t, expr const & s);
bool is_def_eq_proof_irrel(expr const & t, expr const & s);
bool failed_before(expr const & t, expr const & s) const;
void cache_failure(expr const & t, expr const & s);
bool is_prop(expr const & e);
bool is_def_eq_core(expr const & t, expr const & s);
enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
lbool lazy_delta_reduction(expr & t_n, expr & s_n);
reduction_status ext_reduction_step(expr & t_n, expr & s_n);
virtual lbool reduce_def_eq(expr & t_n, expr & s_n);
virtual bool postpone_is_def_eq(expr const & t, expr const & s);
public:
default_converter(environment const & env, bool memoize = true);
virtual optional<declaration> is_delta(expr const & e) const;
virtual bool is_opaque(declaration const & d) const;
virtual optional<expr> is_stuck(expr const & e, type_checker & c);
virtual expr whnf(expr const & e_prime, type_checker & c);
virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c);
};
void initialize_default_converter();
void finalize_default_converter();
}

3
src/kernel/environment.h
View file

@ -229,8 +229,7 @@ class name_generator;
Only the type_checker class can create certified declarations.
*/
class certified_declaration {
friend certified_declaration check(environment const & env, declaration const & d,
name_predicate const & opaque_hints);
friend certified_declaration check(environment const & env, declaration const & d);
environment_id m_id;
declaration m_declaration;
certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}

6
src/kernel/init_module.cpp
View file

@ -5,21 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/environment.h"
#include "kernel/converter.h"
#include "kernel/type_checker.h"
#include "kernel/expr.h"
#include "kernel/formatter.h"
#include "kernel/level.h"
#include "kernel/declaration.h"
#include "kernel/default_converter.h"
namespace lean {
void initialize_kernel_module() {
initialize_level();
initialize_expr();
initialize_declaration();
initialize_default_converter();
initialize_converter();
initialize_type_checker();
initialize_environment();
initialize_formatter();
@ -28,8 +24,6 @@ void finalize_kernel_module() {
finalize_formatter();
finalize_environment();
finalize_type_checker();
finalize_converter();
finalize_default_converter();
finalize_declaration();
finalize_expr();
finalize_level();

523
src/kernel/type_checker.cpp
View file

@ -13,7 +13,6 @@ Author: Leonardo de Moura
#include "util/scoped_map.h"
#include "util/fresh_name.h"
#include "kernel/type_checker.h"
#include "kernel/default_converter.h"
#include "kernel/expr_maps.h"
#include "kernel/instantiate.h"
#include "kernel/free_vars.h"
@ -23,27 +22,25 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
namespace lean {
static expr * g_dont_care = nullptr;
optional<expr> type_checker::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, *this);
}
/**
\brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant.
*/
/** \brief Return the body of the given binder, where the free variable #0 is replaced with a fresh local constant.
It also returns the fresh local constant. */
pair<expr, expr> type_checker::open_binding_body(expr const & e) {
expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
return mk_pair(instantiate(binding_body(e), local), local);
}
/**
\brief Make sure \c e "is" a sort, and return the corresponding sort.
If \c e is not a sort, then the whnf procedure is invoked.
/** \brief Make sure \c e "is" a sort, and return the corresponding sort.
If \c e is not a sort, then the whnf procedure is invoked.
\remark \c s is used to extract position (line number information) when an
error message is produced
*/
\remark \c s is used to extract position (line number information) when an
error message is produced */
expr type_checker::ensure_sort_core(expr e, expr const & s) {
if (is_sort(e))
return e;
@ -198,11 +195,8 @@ expr type_checker::infer_let(expr const & e, bool infer_only) {
return infer_type_core(instantiate(let_body(e), let_value(e)), infer_only);
}
/**
\brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
\pre closed(e)
*/
/** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
\pre closed(e) */
expr type_checker::infer_type_core(expr const & e, bool infer_only) {
if (is_var(e))
throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e);
@ -260,14 +254,10 @@ expr type_checker::ensure_pi(expr const & e, expr const & s) {
return ensure_pi_core(e, s);
}
bool type_checker::is_def_eq(expr const & t, expr const & s) {
return m_conv->is_def_eq(t, s, *this);
}
bool 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 m_conv->is_def_eq(t1, t2, *this);
return is_def_eq(t1, t2);
}
/** \brief Return true iff \c e is a proposition */
@ -275,36 +265,483 @@ bool type_checker::is_prop(expr const & e) {
return m_env.impredicative() && whnf(infer_type(e)) == mk_Prop();
}
expr type_checker::whnf(expr const & t) {
return m_conv->whnf(t, *this);
/** \brief Apply normalizer extensions to \c e. */
optional<expr> type_checker::norm_ext(expr const & e) {
return m_env.norm_ext()(e, *this);
}
bool type_checker::is_opaque(declaration const & d) const {
return m_conv->is_opaque(d);
/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
optional<expr> type_checker::is_stuck(expr const & e) {
if (is_meta(e)) {
return some_expr(e);
} else {
return m_env.norm_ext().is_stuck(e, *this);
}
}
bool type_checker::is_opaque(expr const & c) const {
lean_assert(is_constant(c));
if (auto d = m_env.find(const_name(c)))
return d->is_definition() && is_opaque(*d);
else
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
expr type_checker::whnf_core(expr const & e) {
check_system("whnf");
// handle easy cases
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
return e;
case expr_kind::Macro: case expr_kind::App: case expr_kind::Let:
break;
}
// check cache
if (m_memoize) {
auto it = m_whnf_core_cache.find(e);
if (it != m_whnf_core_cache.end())
return it->second;
}
// do the actual work
expr r;
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local:
case expr_kind::Pi: case expr_kind::Constant: case expr_kind::Lambda:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Macro:
if (auto m = expand_macro(e))
r = whnf_core(*m);
else
r = e;
break;
case expr_kind::App: {
buffer<expr> args;
expr f0 = get_app_rev_args(e, args);
expr f = whnf_core(f0);
if (is_lambda(f)) {
unsigned m = 1;
unsigned num_args = args.size();
while (is_lambda(binding_body(f)) && m < num_args) {
f = binding_body(f);
m++;
}
lean_assert(m <= num_args);
r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()));
} else {
r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()));
}
break;
}
case expr_kind::Let:
r = whnf_core(instantiate(let_body(e), let_value(e)));
break;
}
if (m_memoize)
m_whnf_core_cache.insert(mk_pair(e, r));
return r;
}
/** \brief Expand \c e if it is non-opaque constant with height >= h */
expr type_checker::unfold_name_core(expr e, unsigned h) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e))) {
if (d->is_definition() && d->get_height() >= h &&
length(const_levels(e)) == d->get_num_univ_params())
return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), h);
}
}
return e;
}
/** \brief Expand constants and application where the function is a constant.
The unfolding is only performend if the constant corresponds to
a non-opaque definition with height >= h. */
expr type_checker::unfold_names(expr const & e, unsigned h) {
if (is_app(e)) {
expr f0 = get_app_fn(e);
expr f = unfold_name_core(f0, h);
if (is_eqp(f, f0)) {
return e;
} else {
buffer<expr> args;
get_app_rev_args(e, args);
return mk_rev_app(f, args);
}
} else {
return unfold_name_core(e, h);
}
}
/** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
to be expanded. */
optional<declaration> type_checker::is_delta(expr const & e) const {
expr const & f = get_app_fn(e);
if (is_constant(f)) {
if (auto d = m_env.find(const_name(f)))
if (d->is_definition())
return d;
}
return none_declaration();
}
/** \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
height greater than or equal to \c h.
This method is based on <tt>whnf_core(expr const &)</tt> and \c unfold_names.
\remark This method does not use normalization extensions attached in the environment. */
expr type_checker::whnf_core(expr e, unsigned h) {
while (true) {
expr new_e = unfold_names(whnf_core(e), h);
if (is_eqp(e, new_e))
return e;
e = new_e;
}
}
/** \brief Put expression \c t in weak head normal form */
expr type_checker::whnf(expr const & e_prime) {
// Do not cache easy cases
switch (e_prime.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
return e_prime;
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Let:
break;
}
expr e = e_prime;
// check cache
if (m_memoize) {
auto it = m_whnf_cache.find(e);
if (it != m_whnf_cache.end())
return it->second;
}
expr t = e;
while (true) {
expr t1 = whnf_core(t, 0);
if (auto new_t = norm_ext(t1)) {
t = *new_t;
} else {
auto r = t1;
if (m_memoize)
m_whnf_cache.insert(mk_pair(e, r));
return r;
}
}
}
/** \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s.
t and s are definitionally equal
iff
domain(t) is definitionally equal to domain(s)
and
body(t) is definitionally equal to body(s) */
bool type_checker::is_def_eq_binding(expr t, expr s) {
lean_assert(t.kind() == s.kind());
lean_assert(is_binding(t));
expr_kind k = t.kind();
buffer<expr> subst;
do {
optional<expr> var_s_type;
if (binding_domain(t) != binding_domain(s)) {
var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
expr var_t_type = instantiate_rev(binding_domain(t), subst.size(), subst.data());
if (!is_def_eq(var_t_type, *var_s_type))
return false;
}
if (!closed(binding_body(t)) || !closed(binding_body(s))) {
// local is used inside t or s
if (!var_s_type)
var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
subst.push_back(mk_local(mk_fresh_name(), binding_name(s), *var_s_type, binding_info(s)));
} else {
subst.push_back(*g_dont_care); // don't care
}
t = binding_body(t);
s = binding_body(s);
} while (t.kind() == k && s.kind() == k);
return is_def_eq(instantiate_rev(t, subst.size(), subst.data()),
instantiate_rev(s, subst.size(), subst.data()));
}
bool type_checker::is_def_eq(level const & l1, level const & l2) {
if (is_equivalent(l1, l2)) {
return true;
} else {
return false;
}
}
type_checker::type_checker(environment const & env, std::unique_ptr<converter> && conv, bool memoize):
m_env(env), m_conv(std::move(conv)),
m_memoize(memoize), m_params(nullptr) {
bool type_checker::is_def_eq(levels const & ls1, levels const & ls2) {
if (is_nil(ls1) && is_nil(ls2)) {
return true;
} else if (!is_nil(ls1) && !is_nil(ls2)) {
return
is_def_eq(head(ls1), head(ls2)) &&
is_def_eq(tail(ls1), tail(ls2));
} else {
return false;
}
}
/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
lbool type_checker::quick_is_def_eq(expr const & t, expr const & s, bool use_hash) {
if (m_eqv_manager.is_equiv(t, s, use_hash))
return l_true;
if (t.kind() == s.kind()) {
switch (t.kind()) {
case expr_kind::Lambda: case expr_kind::Pi:
return to_lbool(is_def_eq_binding(t, s));
case expr_kind::Sort:
return to_lbool(is_def_eq(sort_level(t), sort_level(s)));
case expr_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Var: case expr_kind::Local: case expr_kind::App:
case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let:
// We do not handle these cases in this method.
break;
}
}
return l_undef; // This is not an "easy case"
}
/** \brief Return true if arguments of \c t are definitionally equal to arguments of \c s.
This method is used to implement an optimization in the method \c is_def_eq. */
bool type_checker::is_def_eq_args(expr t, expr s) {
while (is_app(t) && is_app(s)) {
if (!is_def_eq(app_arg(t), app_arg(s)))
return false;
t = app_fn(t);
s = app_fn(s);
}
return !is_app(t) && !is_app(s);
}
/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
bool type_checker::try_eta_expansion_core(expr const & t, expr const & s) {
if (is_lambda(t) && !is_lambda(s)) {
expr s_type = whnf(infer_type(s));
if (!is_pi(s_type))
return false;
expr new_s = mk_lambda(binding_name(s_type), binding_domain(s_type), mk_app(s, Var(0)), binding_info(s_type));
if (!is_def_eq(t, new_s))
return false;
return true;
} else {
return false;
}
}
/** \brief Return true if \c t and \c s are definitionally equal because they are applications of the form
<tt>(f a_1 ... a_n)</tt> <tt>(g b_1 ... b_n)</tt>, and \c f and \c g are definitionally equal, and
\c a_i and \c b_i are also definitionally equal for every 1 <= i <= n.
Return false otherwise. */
bool type_checker::is_def_eq_app(expr const & t, expr const & s) {
if (is_app(t) && is_app(s)) {
buffer<expr> t_args;
buffer<expr> s_args;
expr t_fn = get_app_args(t, t_args);
expr s_fn = get_app_args(s, s_args);
if (is_def_eq(t_fn, s_fn) && t_args.size() == s_args.size()) {
unsigned i = 0;
for (; i < t_args.size(); i++) {
if (!is_def_eq(t_args[i], s_args[i]))
break;
}
if (i == t_args.size())
return true;
}
}
return false;
}
/** \brief Return true if \c t and \c s are definitionally equal due to proof irrelevant.
Return false otherwise. */
bool type_checker::is_def_eq_proof_irrel(expr const & t, expr const & s) {
if (!m_env.prop_proof_irrel())
return false;
// Proof irrelevance support for Prop (aka Type.{0})
expr t_type = infer_type(t);
expr s_type = infer_type(s);
return is_prop(t_type) && is_def_eq(t_type, s_type);
}
bool type_checker::failed_before(expr const & t, expr const & s) const {
if (t.hash() < s.hash()) {
return m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end();
} else if (t.hash() > s.hash()) {
return m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
} else {
return
m_failure_cache.find(mk_pair(t, s)) != m_failure_cache.end() ||
m_failure_cache.find(mk_pair(s, t)) != m_failure_cache.end();
}
}
void type_checker::cache_failure(expr const & t, expr const & s) {
if (t.hash() <= s.hash())
m_failure_cache.insert(mk_pair(t, s));
else
m_failure_cache.insert(mk_pair(s, t));
}
/** \brief Perform one lazy delta-reduction step.
Return
- l_true if t_n and s_n are definitionally equal.
- l_false if they are not definitionally equal.
- l_undef it the step did not manage to establish whether they are definitionally equal or not.
\remark t_n, s_n and cs are updated. */
auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
auto d_t = is_delta(t_n);
auto d_s = is_delta(s_n);
if (!d_t && !d_s) {
return reduction_status::DefUnknown;
} else if (d_t && !d_s) {
t_n = whnf_core(unfold_names(t_n, 0));
} else if (!d_t && d_s) {
s_n = whnf_core(unfold_names(s_n, 0));
} else if (!d_t->is_theorem() && d_s->is_theorem()) {
t_n = whnf_core(unfold_names(t_n, d_t->get_height()));
} else if (!d_s->is_theorem() && d_t->is_theorem()) {
s_n = whnf_core(unfold_names(s_n, d_s->get_height()));
} else if (!d_t->is_theorem() && d_t->get_height() > d_s->get_height()) {
t_n = whnf_core(unfold_names(t_n, d_s->get_height() + 1));
} else if (!d_s->is_theorem() && d_t->get_height() < d_s->get_height()) {
s_n = whnf_core(unfold_names(s_n, d_t->get_height() + 1));
} else {
if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) {
// If t_n and s_n are both applications of the same (non-opaque) definition,
if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
// We let the unifier deal with cases such as
// (f ...) =?= (f ...)
// when t_n or s_n contains metavariables
return reduction_status::DefUnknown;
} else {
// Optimization:
// We try to check if their arguments are definitionally equal.
// If they are, then t_n and s_n must be definitionally equal, and we can
// skip the delta-reduction step.
// If the flag use_conv_opt() is not true, then we skip this optimization
if (d_t->use_conv_opt() && !failed_before(t_n, s_n)) {
if (is_def_eq(const_levels(get_app_fn(t_n)), const_levels(get_app_fn(s_n))) &&
is_def_eq_args(t_n, s_n)) {
return reduction_status::DefEqual;
} else {
cache_failure(t_n, s_n);
}
}
}
}
t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1));
s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1));
}
switch (quick_is_def_eq(t_n, s_n)) {
case l_true: return reduction_status::DefEqual;
case l_false: return reduction_status::DefDiff;
case l_undef: return reduction_status::Continue;
}
lean_unreachable();
}
lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
while (true) {
switch (lazy_delta_reduction_step(t_n, s_n)) {
case reduction_status::Continue: break;
case reduction_status::DefUnknown: return l_undef;
case reduction_status::DefEqual: return l_true;
case reduction_status::DefDiff: return l_false;
}
}
}
auto type_checker::ext_reduction_step(expr & t_n, expr & s_n) -> reduction_status {
auto new_t_n = norm_ext(t_n);
auto new_s_n = norm_ext(s_n);
if (!new_t_n && !new_s_n)
return reduction_status::DefUnknown;
if (new_t_n)
t_n = whnf_core(*new_t_n);
if (new_s_n)
s_n = whnf_core(*new_s_n);
switch (quick_is_def_eq(t_n, s_n)) {
case l_true: return reduction_status::DefEqual;
case l_false: return reduction_status::DefDiff;
case l_undef: return reduction_status::Continue;
}
lean_unreachable();
}
// Apply lazy delta-reduction and then normalizer extensions
lbool type_checker::reduce_def_eq(expr & t_n, expr & s_n) {
while (true) {
// first, keep applying lazy delta-reduction while applicable
lbool r = lazy_delta_reduction(t_n, s_n);
if (r != l_undef) return r;
// try normalizer extensions
switch (ext_reduction_step(t_n, s_n)) {
case reduction_status::Continue: break;
case reduction_status::DefUnknown: return l_undef;
case reduction_status::DefEqual: return l_true;
case reduction_status::DefDiff: return l_false;
}
}
}
bool type_checker::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
bool use_hash = true;
lbool r = quick_is_def_eq(t, s, use_hash);
if (r != l_undef) return r == l_true;
// apply whnf (without using delta-reduction or normalizer extensions)
expr t_n = whnf_core(t);
expr s_n = whnf_core(s);
if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
r = quick_is_def_eq(t_n, s_n);
if (r != l_undef) return r == l_true;
}
r = reduce_def_eq(t_n, s_n);
if (r != l_undef) return r == l_true;
if (is_constant(t_n) && is_constant(s_n) && const_name(t_n) == const_name(s_n) &&
is_def_eq(const_levels(t_n), const_levels(s_n)))
return true;
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
return true;
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
if (is_def_eq_app(t_n, s_n))
return true;
if (try_eta_expansion(t_n, s_n))
return true;
if (is_def_eq_proof_irrel(t, s))
return true;
return false;
}
bool type_checker::is_def_eq(expr const & t, expr const & s) {
bool r = is_def_eq_core(t, s);
if (r)
m_eqv_manager.add_equiv(t, s);
return r;
}
type_checker::type_checker(environment const & env, bool memoize):
type_checker(env, std::unique_ptr<converter>(new default_converter(env, memoize)), memoize) {}
m_env(env), m_memoize(memoize), m_params(nullptr) {
}
type_checker::~type_checker() {}
optional<expr> type_checker::is_stuck(expr const & e) {
return m_conv->is_stuck(e, *this);
}
void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
if (has_metavar(e))
throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); });
@ -338,13 +775,13 @@ static void check_duplicated_params(environment const & env, declaration const &
}
}
certified_declaration check(environment const & env, declaration const & d, name_predicate const & pred) {
certified_declaration check(environment const & env, declaration const & d) {
if (d.is_definition())
check_no_mlocal(env, d.get_name(), d.get_value(), false);
check_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name());
check_duplicated_params(env, d);
type_checker checker(env, std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred)));
type_checker checker(env);
expr sort = checker.check(d.get_type(), d.get_univ_params());
checker.ensure_sort(sort, d.get_type());
if (d.is_definition()) {
@ -358,13 +795,11 @@ certified_declaration check(environment const & env, declaration const & d, name
return certified_declaration(env.get_id(), d);
}
certified_declaration check(environment const & env, declaration const & d) {
return check(env, d, [](name const &) { return false; });
}
void initialize_type_checker() {
g_dont_care = new expr(Const("dontcare"));
}
void finalize_type_checker() {
delete g_dont_care;
}
}

62
src/kernel/type_checker.h
View file

@ -5,15 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <unordered_set>
#include <memory>
#include <utility>
#include <algorithm>
#include "util/lbool.h"
#include "util/flet.h"
#include "util/name_set.h"
#include "util/fresh_name.h"
#include "kernel/environment.h"
#include "kernel/converter.h"
#include "kernel/expr_pair.h"
#include "kernel/expr_maps.h"
#include "kernel/equiv_manager.h"
#include "kernel/abstract_type_context.h"
namespace lean {
@ -25,13 +28,16 @@ class type_checker : public abstract_type_context {
The type of (lambda x : A, t) is (Pi x : A, typeof(t))
The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) */
typedef expr_bi_struct_map<expr> cache;
environment m_env;
std::unique_ptr<converter> m_conv;
cache m_infer_type_cache[2];
bool m_memoize;
level_param_names const * m_params;
typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
environment m_env;
bool m_memoize;
cache m_infer_type_cache[2];
expr_struct_map<expr> m_whnf_core_cache;
expr_struct_map<expr> m_whnf_cache;
equiv_manager m_eqv_manager;
expr_pair_set m_failure_cache;
level_param_names const * m_params;
friend class converter; // allow converter to access the following methods
pair<expr, expr> open_binding_body(expr const & e);
expr ensure_sort_core(expr e, expr const & s);
expr ensure_pi_core(expr e, expr const & s);
@ -44,12 +50,36 @@ class type_checker : public abstract_type_context {
expr infer_let(expr const & e, bool infer_only);
expr infer_type_core(expr const & e, bool infer_only);
expr infer_type(expr const & e);
public:
/** \brief Create a type checker for the given environment. The auxiliary names created by this
type checker are based on the given name generator.
enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
optional<expr> norm_ext(expr const & e);
expr whnf_core(expr const & e);
expr unfold_name_core(expr e, unsigned h);
expr unfold_names(expr const & e, unsigned h);
optional<declaration> is_delta(expr const & e) const;
expr whnf_core(expr e, unsigned h);
bool is_def_eq_binding(expr t, expr s);
bool is_def_eq(level const & l1, level const & l2);
bool is_def_eq(levels const & ls1, levels const & ls2);
lbool quick_is_def_eq(expr const & t, expr const & s, bool use_hash = false);
bool is_def_eq_args(expr t, expr s);
bool try_eta_expansion_core(expr const & t, expr const & s);
bool try_eta_expansion(expr const & t, expr const & s) {
return try_eta_expansion_core(t, s) || try_eta_expansion_core(s, t);
}
bool is_def_eq_app(expr const & t, expr const & s);
bool is_def_eq_proof_irrel(expr const & t, expr const & s);
bool failed_before(expr const & t, expr const & s) const;
void cache_failure(expr const & t, expr const & s);
reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);
lbool lazy_delta_reduction(expr & t_n, expr & s_n);
reduction_status ext_reduction_step(expr & t_n, expr & s_n);
lbool reduce_def_eq(expr & t_n, expr & s_n);
bool is_def_eq_core(expr const & t, expr const & s);
public:
/** \brief Create a type checker for the given environment.
memoize: if true, then inferred types are memoized/cached */
type_checker(environment const & env, std::unique_ptr<converter> && conv, bool memoize = true);
type_checker(environment const & env, bool memoize = true);
~type_checker();
@ -96,18 +126,9 @@ public:
optional<expr> expand_macro(expr const & m);
/** \brief Return true iff \c d is opaque with respect to this type checker. */
bool is_opaque(declaration const & d) const;
/** \brief Return true iff the constant \c c is opaque with respect to this type checker. */
bool is_opaque(expr const & c) const;
/** \brief Return a metavariable that may be stucking the \c e's reduction. */
virtual optional<expr> is_stuck(expr const & e);
optional<declaration> is_delta(expr const & e) const { return m_conv->is_delta(e); }
bool may_reduce_later(expr const & e) { return !is_meta(e) && static_cast<bool>(m_conv->is_stuck(e, *this)); }
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);
@ -122,7 +143,6 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b
/** \brief Type check the given declaration, and return a certified declaration if it is type correct.
Throw an exception if the declaration is type incorrect. */
certified_declaration check(environment const & env, declaration const & d);
certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints);
void initialize_type_checker();
void finalize_type_checker();

1
src/library/tactic/expr_to_tactic.cpp
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include "util/sstream.h"
#include "util/optional.h"
#include "kernel/instantiate.h"
#include "kernel/default_converter.h"
#include "library/annotation.h"
#include "library/string.h"
#include "library/explicit.h"

1
src/library/tactic/induction_tactic.cpp
View file

@ -7,7 +7,6 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "kernel/default_converter.h"
#include "library/util.h"
#include "library/user_recursors.h"
#include "library/constants.h"

1
src/library/util.cpp
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/error_msgs.h"
#include "kernel/abstract.h"
#include "kernel/default_converter.h"
#include "kernel/inductive/inductive.h"
#include "library/metavar.h"
#include "library/locals.h"