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

chore(kernel/type_checker): remove dead branch

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-16 12:22:28 -07:00
parent 871e7de673
commit 000db32e40
1 changed files with 10 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/type_checker.cpp
View file

@ -672,24 +672,16 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
s_n = whnf_core(*unfold_definition(s_n));
} 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 (!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);
}
// 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 (!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);
}
}
}