faee08591f
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not. The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
577 lines
24 KiB
C++
577 lines
24 KiB
C++
/*
|
|
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"
|
|
|
|
namespace lean {
|
|
/**
|
|
\brief Predicate for deciding whether \c d is an opaque definition or not.
|
|
|
|
Here is the basic idea:
|
|
|
|
1) Each definition has an opaque flag. This flag cannot be modified after a definition is added to the environment.
|
|
The opaque flag affects the convertability check. The idea is to minimize the number of delta-reduction steps.
|
|
We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined.
|
|
We should view non-opaque definitions as "inline definitions" used in programming languages such as C++.
|
|
|
|
2) Whenever type checking an expression, the user can provide an additional set of definition names (m_extra_opaque) that
|
|
should be considered opaque. Note that, if \c t type checks when using an extra_opaque set S, then t also type checks
|
|
(modulo resource constraints) with the empty set. Again, the purpose of extra_opaque is to mimimize the number
|
|
of delta-reduction steps.
|
|
|
|
3) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as
|
|
transparent when we are type checking another definition/theorem D' also in M. This rule only applies if
|
|
D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field
|
|
m_module_idx that is not none when this rule should be applied.
|
|
*/
|
|
bool is_opaque(declaration const & d, name_set const & extra_opaque, optional<module_idx> const & mod_idx) {
|
|
lean_assert(d.is_definition());
|
|
if (d.is_theorem()) return true; // theorems are always opaque
|
|
if (extra_opaque.contains(d.get_name())) return true; // extra_opaque set overrides opaque flag
|
|
if (!d.is_opaque()) return false; // d is a transparent definition
|
|
if (mod_idx && d.get_module_idx() == *mod_idx) return false; // the opaque definitions in mod_idx are considered transparent
|
|
return true; // d is opaque
|
|
}
|
|
|
|
/** \brief Auxiliary method for \c is_delta */
|
|
static optional<declaration> is_delta_core(environment const & env, expr const & e, name_set const & extra_opaque, optional<module_idx> const & mod_idx) {
|
|
if (is_constant(e)) {
|
|
if (auto d = env.find(const_name(e)))
|
|
if (d->is_definition() && !is_opaque(*d, extra_opaque, mod_idx))
|
|
return d;
|
|
}
|
|
return none_declaration();
|
|
}
|
|
|
|
/**
|
|
\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> is_delta(environment const & env, expr const & e, name_set const & extra_opaque, optional<module_idx> const & mod_idx) {
|
|
return is_delta_core(env, get_app_fn(e), extra_opaque, mod_idx);
|
|
}
|
|
|
|
static optional<module_idx> g_opt_main_module_idx(g_main_module_idx);
|
|
optional<declaration> is_delta(environment const & env, expr const & e, name_set const & extra_opaque) {
|
|
return is_delta(env, e, extra_opaque, g_opt_main_module_idx);
|
|
}
|
|
|
|
static no_delayed_justification g_no_delayed_jst;
|
|
bool converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
|
|
return is_def_eq(t, s, c, g_no_delayed_jst);
|
|
}
|
|
|
|
/** \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 &, delayed_justification &) { return true; }
|
|
virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
|
|
};
|
|
|
|
std::unique_ptr<converter> mk_dummy_converter() {
|
|
return std::unique_ptr<converter>(new dummy_converter());
|
|
}
|
|
|
|
name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
|
|
expr converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
|
|
void converter::add_cnstr(type_checker & tc, constraint const & c) { return tc.add_cnstr(c); }
|
|
extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
|
|
static expr g_dont_care(Const("dontcare"));
|
|
|
|
struct default_converter : public converter {
|
|
environment m_env;
|
|
optional<module_idx> m_module_idx;
|
|
bool m_memoize;
|
|
name_set m_extra_opaque;
|
|
expr_struct_map<expr> m_whnf_core_cache;
|
|
expr_struct_map<expr> m_whnf_cache;
|
|
|
|
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize, name_set const & extra_opaque):
|
|
m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {
|
|
}
|
|
|
|
constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
|
|
return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
|
|
}
|
|
|
|
optional<expr> expand_macro(expr const & m, type_checker & c) {
|
|
lean_assert(is_macro(m));
|
|
return macro_def(m).expand(m, get_extension(c));
|
|
}
|
|
|
|
/** \brief Apply normalizer extensions to \c e. */
|
|
optional<expr> norm_ext(expr const & e, type_checker & c) {
|
|
return m_env.norm_ext()(e, get_extension(c));
|
|
}
|
|
|
|
/** \brief Return true if \c e may be reduced later after metavariables are instantiated. */
|
|
bool may_reduce_later(expr const & e, type_checker & c) {
|
|
return m_env.norm_ext().may_reduce_later(e, get_extension(c));
|
|
}
|
|
|
|
/** \brief Try to apply eta-reduction to \c e. */
|
|
expr try_eta(expr const & e) {
|
|
lean_assert(is_lambda(e));
|
|
expr const & b = binding_body(e);
|
|
if (is_lambda(b)) {
|
|
expr new_b = try_eta(b);
|
|
if (is_eqp(b, new_b)) {
|
|
return e;
|
|
} else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) {
|
|
return lower_free_vars(app_fn(new_b), 1);
|
|
} else {
|
|
return update_binding(e, binding_domain(e), new_b);
|
|
}
|
|
} else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) {
|
|
return lower_free_vars(app_fn(b), 1);
|
|
} else {
|
|
return e;
|
|
}
|
|
}
|
|
|
|
/** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */
|
|
expr whnf_core(expr const & e, type_checker & c) {
|
|
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:
|
|
return e;
|
|
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App:
|
|
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:
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
case expr_kind::Lambda:
|
|
r = (m_env.eta()) ? try_eta(e) : e;
|
|
break;
|
|
case expr_kind::Macro:
|
|
if (auto m = expand_macro(e, c))
|
|
r = whnf_core(*m, c);
|
|
else
|
|
r = e;
|
|
break;
|
|
case expr_kind::App: {
|
|
buffer<expr> args;
|
|
expr f0 = get_app_rev_args(e, args);
|
|
expr f = whnf_core(f0, c);
|
|
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()), c);
|
|
} else {
|
|
r = is_eqp(f, f0) ? e : mk_rev_app(f, args.size(), args.data());
|
|
}
|
|
break;
|
|
}}
|
|
|
|
if (m_memoize)
|
|
m_whnf_core_cache.insert(mk_pair(e, r));
|
|
return r;
|
|
}
|
|
|
|
bool is_opaque(declaration const & d) const {
|
|
return ::lean::is_opaque(d, m_extra_opaque, m_module_idx);
|
|
}
|
|
|
|
/** \brief Expand \c e if it is non-opaque constant with weight >= w */
|
|
expr unfold_name_core(expr e, unsigned w) {
|
|
if (is_constant(e)) {
|
|
if (auto d = m_env.find(const_name(e))) {
|
|
if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
|
|
return unfold_name_core(instantiate_univ_params(d->get_value(), d->get_univ_params(), const_levels(e)), w);
|
|
}
|
|
}
|
|
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 weight >= w.
|
|
*/
|
|
expr unfold_names(expr const & e, unsigned w) {
|
|
if (is_app(e)) {
|
|
expr f0 = get_app_fn(e);
|
|
expr f = unfold_name_core(f0, w);
|
|
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, w);
|
|
}
|
|
}
|
|
|
|
/**
|
|
\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> is_delta(expr const & e) {
|
|
return ::lean::is_delta(m_env, get_app_fn(e), m_extra_opaque, m_module_idx);
|
|
}
|
|
|
|
/**
|
|
\brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with
|
|
weight greater than or equal to \c w.
|
|
|
|
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 whnf_core(expr e, unsigned w, type_checker & c) {
|
|
while (true) {
|
|
expr new_e = unfold_names(whnf_core(e, c), w);
|
|
if (is_eqp(e, new_e))
|
|
return e;
|
|
e = new_e;
|
|
}
|
|
}
|
|
|
|
/** \brief Put expression \c t in weak head normal form */
|
|
virtual expr whnf(expr const & e_prime, type_checker & c) {
|
|
// 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:
|
|
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, c);
|
|
auto new_t = norm_ext(t1, c);
|
|
if (new_t) {
|
|
t = *new_t;
|
|
} else {
|
|
if (m_memoize)
|
|
m_whnf_cache.insert(mk_pair(e, t1));
|
|
return t1;
|
|
}
|
|
}
|
|
}
|
|
|
|
/**
|
|
\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 is_def_eq_binding(expr t, expr s, type_checker & c, delayed_justification & jst) {
|
|
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, c, jst))
|
|
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(c), 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()), c, jst);
|
|
}
|
|
|
|
bool is_def_eq(level const & l1, level const & l2, type_checker & c, delayed_justification & jst) {
|
|
if (is_equivalent(l1, l2)) {
|
|
return true;
|
|
} else if (has_meta(l1) || has_meta(l2)) {
|
|
add_cnstr(c, mk_level_eq_cnstr(l1, l2, jst.get()));
|
|
return true;
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool is_def_eq(levels const & ls1, levels const & ls2, type_checker & c, delayed_justification & jst) {
|
|
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), c, jst) && is_def_eq(tail(ls1), tail(ls2), c, jst);
|
|
else
|
|
return false;
|
|
}
|
|
|
|
/** \brief This is an auxiliary method for is_def_eq. It handles the "easy cases". */
|
|
lbool quick_is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
|
|
if (t == s)
|
|
return l_true; // t and s are structurally equal
|
|
if (is_meta(t) || is_meta(s)) {
|
|
// if t or s is a metavariable (or the application of a metavariable), then add constraint
|
|
add_cnstr(c, mk_eq_cnstr(t, s, jst.get()));
|
|
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, c, jst));
|
|
case expr_kind::Sort:
|
|
return to_lbool(is_def_eq(sort_level(t), sort_level(s), c, jst));
|
|
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:
|
|
// 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 is_def_eq_args(expr t, expr s, type_checker & c, delayed_justification & jst) {
|
|
while (is_app(t) && is_app(s)) {
|
|
if (!is_def_eq(app_arg(t), app_arg(s), c, jst))
|
|
return false;
|
|
t = app_fn(t);
|
|
s = app_fn(s);
|
|
}
|
|
return !is_app(t) && !is_app(s);
|
|
}
|
|
|
|
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
|
|
bool is_app_of(expr t, name const & f_name) {
|
|
t = get_app_fn(t);
|
|
return is_constant(t) && const_name(t) == f_name;
|
|
}
|
|
|
|
/** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */
|
|
bool try_eta_expansion(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
|
|
if (is_lambda(t) && !is_lambda(s)) {
|
|
type_checker::scope scope(c);
|
|
expr s_type = whnf(infer_type(c, s), c);
|
|
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));
|
|
return is_def_eq(t, new_s, c, jst);
|
|
} else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
/** Return true iff t is definitionally equal to s. */
|
|
virtual bool is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst) {
|
|
check_system("is_definitionally_equal");
|
|
lbool r = quick_is_def_eq(t, s, c, jst);
|
|
if (r != l_undef) return r == l_true;
|
|
|
|
// apply whnf (without using delta-reduction or normalizer extensions)
|
|
expr t_n = whnf_core(t, c);
|
|
expr s_n = whnf_core(s, c);
|
|
if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
|
|
r = quick_is_def_eq(t_n, s_n, c, jst);
|
|
if (r != l_undef) return r == l_true;
|
|
}
|
|
|
|
// lazy delta-reduction and then normalizer extensions
|
|
while (true) {
|
|
// first, keep applying lazy delta-reduction while applicable
|
|
while (true) {
|
|
auto d_t = is_delta(t_n);
|
|
auto d_s = is_delta(s_n);
|
|
if (!d_t && !d_s) {
|
|
break;
|
|
} else if (d_t && !d_s) {
|
|
t_n = whnf_core(unfold_names(t_n, 0), c);
|
|
} else if (!d_t && d_s) {
|
|
s_n = whnf_core(unfold_names(s_n, 0), c);
|
|
} else if (d_t->get_weight() > d_s->get_weight()) {
|
|
t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c);
|
|
} else if (d_t->get_weight() < d_s->get_weight()) {
|
|
s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c);
|
|
} else {
|
|
lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight());
|
|
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 ...)
|
|
break;
|
|
} 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()) {
|
|
type_checker::scope scope(c);
|
|
if (is_def_eq_args(t_n, s_n, c, jst))
|
|
return true;
|
|
}
|
|
}
|
|
}
|
|
t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c);
|
|
s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c);
|
|
}
|
|
r = quick_is_def_eq(t_n, s_n, c, jst);
|
|
if (r != l_undef) return r == l_true;
|
|
}
|
|
// try normalizer extensions
|
|
auto new_t_n = norm_ext(t_n, c);
|
|
auto new_s_n = norm_ext(s_n, c);
|
|
if (!new_t_n && !new_s_n)
|
|
break; // t_n and s_n are in weak head normal form
|
|
if (new_t_n)
|
|
t_n = whnf_core(*new_t_n, c);
|
|
if (new_s_n)
|
|
s_n = whnf_core(*new_s_n, c);
|
|
r = quick_is_def_eq(t_n, s_n, c, jst);
|
|
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), c, jst))
|
|
return true;
|
|
|
|
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n) &&
|
|
is_def_eq(mlocal_type(t_n), mlocal_type(s_n), c, jst))
|
|
return true;
|
|
|
|
optional<declaration> d_t, d_s;
|
|
bool delay_check = false;
|
|
if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
|
|
d_t = is_delta(t_n);
|
|
d_s = is_delta(s_n);
|
|
delay_check = d_t && d_s && is_eqp(*d_t, *d_s);
|
|
}
|
|
|
|
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
|
|
if (!delay_check && is_app(t_n) && is_app(s_n)) {
|
|
type_checker::scope scope(c);
|
|
buffer<expr> t_args;
|
|
buffer<expr> s_args;
|
|
expr t_fn = get_app_args(t_n, t_args);
|
|
expr s_fn = get_app_args(s_n, s_args);
|
|
if (is_def_eq(t_fn, s_fn, c, jst) && 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], c, jst))
|
|
break;
|
|
}
|
|
if (i == t_args.size()) {
|
|
scope.keep();
|
|
return true;
|
|
}
|
|
}
|
|
}
|
|
|
|
if (try_eta_expansion(t_n, s_n, c, jst) ||
|
|
try_eta_expansion(s_n, t_n, c, jst))
|
|
return true;
|
|
|
|
if (m_env.prop_proof_irrel()) {
|
|
// Proof irrelevance support for Prop (aka Type.{0})
|
|
type_checker::scope scope(c);
|
|
expr t_type = infer_type(c, t);
|
|
if (is_prop(t_type, c) && is_def_eq(t_type, infer_type(c, s), c, jst)) {
|
|
scope.keep();
|
|
return true;
|
|
}
|
|
}
|
|
|
|
list<name> const & cls_proof_irrel = m_env.cls_proof_irrel();
|
|
if (!is_nil(cls_proof_irrel)) {
|
|
// Proof irrelevance support for classes
|
|
type_checker::scope scope(c);
|
|
expr t_type = whnf(infer_type(c, t), c);
|
|
if (std::any_of(cls_proof_irrel.begin(), cls_proof_irrel.end(),
|
|
[&](name const & cls_name) { return is_app_of(t_type, cls_name); }) &&
|
|
is_def_eq(t_type, infer_type(c, s), c, jst)) {
|
|
scope.keep();
|
|
return true;
|
|
}
|
|
}
|
|
|
|
if (may_reduce_later(t_n, c) || may_reduce_later(s_n, c)) {
|
|
add_cnstr(c, mk_eq_cnstr(t_n, s_n, jst.get()));
|
|
return true;
|
|
}
|
|
|
|
if (delay_check) {
|
|
add_cnstr(c, mk_eq_cnstr(t_n, s_n, jst.get()));
|
|
return true;
|
|
}
|
|
|
|
return false;
|
|
}
|
|
|
|
bool is_prop(expr const & e, type_checker & c) {
|
|
return whnf(infer_type(c, e), c) == Prop;
|
|
}
|
|
|
|
virtual optional<module_idx> get_module_idx() const {
|
|
return m_module_idx;
|
|
}
|
|
};
|
|
|
|
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
|
|
bool memoize, name_set const & extra_opaque) {
|
|
return std::unique_ptr<converter>(new default_converter(env, mod_idx, memoize, extra_opaque));
|
|
}
|
|
std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize,
|
|
name_set const & extra_opaque) {
|
|
if (unfold_opaque_main)
|
|
return mk_default_converter(env, optional<module_idx>(0), memoize, extra_opaque);
|
|
else
|
|
return mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque);
|
|
}
|
|
}
|