From 000db32e401b174e8ad1d4d1c6dbe4e06b8ef585 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Sep 2018 12:22:28 -0700 Subject: [PATCH] chore(kernel/type_checker): remove dead branch --- src/kernel/type_checker.cpp | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 610cdcb53e..f56b650fc2 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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); } } }