Fix warnings and bugs related to unused variables.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
2b72c5f681
commit
651c5d6751
4 changed files with 11 additions and 8 deletions
|
@ -483,7 +483,7 @@ class elaborator::imp {
|
|||
return process(e, ctx).second;
|
||||
}
|
||||
|
||||
bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
|
||||
bool is_simple_ho_match(expr const & e1, context const & ctx) {
|
||||
if (is_app(e1) && is_metavar(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !empty(ctx)) {
|
||||
return true;
|
||||
} else {
|
||||
|
@ -712,10 +712,10 @@ class elaborator::imp {
|
|||
for (unsigned i = 0; i < num; i++) {
|
||||
m_constraints.push_back(constraint(arg(new_lhs, i), arg(new_rhs, i), c));
|
||||
}
|
||||
} else if (is_simple_ho_match(new_lhs, new_rhs, c.m_ctx)) {
|
||||
} else if (is_simple_ho_match(new_lhs, c.m_ctx)) {
|
||||
delayed = 0;
|
||||
unify_simple_ho_match(new_lhs, new_rhs, c);
|
||||
} else if (is_simple_ho_match(new_rhs, new_lhs, c.m_ctx)) {
|
||||
} else if (is_simple_ho_match(new_rhs, c.m_ctx)) {
|
||||
delayed = 0;
|
||||
unify_simple_ho_match(new_rhs, new_lhs, c);
|
||||
} else if (has_assigned_metavar(new_lhs)) {
|
||||
|
|
|
@ -708,7 +708,10 @@ class parser::imp {
|
|||
buffer<std::pair<pos_info, name>> names;
|
||||
parse_names(names);
|
||||
expr type;
|
||||
if (curr_is_colon()) {
|
||||
if (!suppress_type) {
|
||||
check_colon_next("invalid binder, ':' expected");
|
||||
type = parse_expr();
|
||||
} else if (curr_is_colon()) {
|
||||
next();
|
||||
type = parse_expr();
|
||||
}
|
||||
|
|
|
@ -97,7 +97,7 @@ class normalizer::imp {
|
|||
}
|
||||
};
|
||||
|
||||
svalue lookup(value_stack const & s, unsigned i, unsigned k) {
|
||||
svalue lookup(value_stack const & s, unsigned i) {
|
||||
unsigned j = i;
|
||||
value_stack const * it1 = &s;
|
||||
while (*it1) {
|
||||
|
@ -202,7 +202,7 @@ class normalizer::imp {
|
|||
}
|
||||
break;
|
||||
case expr_kind::Var:
|
||||
r = lookup(s, var_idx(a), k);
|
||||
r = lookup(s, var_idx(a));
|
||||
break;
|
||||
case expr_kind::Constant: {
|
||||
object const & obj = m_env.get_object(const_name(a));
|
||||
|
|
|
@ -285,12 +285,12 @@ class ho_unifier::imp {
|
|||
}
|
||||
|
||||
/** \brief Creates a subproblem based on the application arguments */
|
||||
bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned) {
|
||||
bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) {
|
||||
lean_assert(is_app(a) && is_app(b));
|
||||
if (num_args(a) != num_args(b)) {
|
||||
return false;
|
||||
} else {
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
for (unsigned i = start; i < num_args(a); i++) {
|
||||
add_constraint(ctx, arg(a, i), arg(b, i));
|
||||
}
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue