michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/unifier): delay constraints where the lhs or rhs are of the form (?m ... (intro ...))

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-04 23:31:31 -07:00
parent 9e1d425a45
commit f242971b55
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/unifier.cpp
View file

@ -594,7 +594,7 @@ struct unifier_fn {
}
// We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) {
if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs) || is_meta_intro_app(lhs) || is_meta_intro_app(rhs)) {
add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
} else if (is_meta(lhs) && is_meta(rhs)) {
// flex-flex constraints are delayed the most.
@ -834,6 +834,16 @@ struct unifier_fn {
return is_eq_cnstr(c) && (is_elim_meta_app(cnstr_lhs_expr(c)) || is_elim_meta_app(cnstr_rhs_expr(c)));
}
/** \brief Return true iff \c e is of the form (?m ... (intro ...)) */
bool is_meta_intro_app(expr const & e) {
if (!is_app(e) || !is_meta(e))
return false;
expr arg = get_app_fn(app_arg(e));
if (!is_constant(arg))
return false;
return (bool) inductive::is_intro_rule(m_env, const_name(arg)); // NOLINT
}
/**
\brief Given (elim args) =?= t, where elim is the eliminator/recursor for the inductive declaration \c decl,
and the last argument of args is of the form (?m ...), we create a case split where we try to assign (?m ...)