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

test(library/blast/simplifier): add asserts

Browse source
This commit is contained in:
Daniel Selsam 2015-11-07 15:54:18 -08:00 committed by Leonardo de Moura
parent afc7a2af84
commit f1d5cc5d5b
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/blast/simplifier.cpp
View file

@ -131,7 +131,6 @@ class simplifier {
simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer<expr> & ls) { simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer<expr> & ls) {
simp_rule_sets srss = _srss; simp_rule_sets srss = _srss;
for (unsigned i = 0; i < ls.size(); i++) { for (unsigned i = 0; i < ls.size(); i++) {
// TODO(dhs): assert no metas
expr & l = ls[i]; expr & l = ls[i];
tmp_type_context tctx(env(), ios()); tmp_type_context tctx(env(), ios());
srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l); srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
@ -408,7 +407,7 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta()); blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e); if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
if (m_trace) { if (m_trace) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
@ -422,8 +421,10 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
expr const & m = sr.get_emeta(i); expr const & m = sr.get_emeta(i);
bool is_instance = sr.is_instance(i); bool is_instance = sr.is_instance(i);
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
lean_assert(!has_metavar(m_type));
if (is_instance) { if (is_instance) {
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
if (auto v = tmp_tctx->mk_class_instance(m_type)) { if (auto v = tmp_tctx->mk_class_instance(m_type)) {
if (!tmp_tctx->force_assign(m, *v)) { if (!tmp_tctx->force_assign(m, *v)) {
if (m_trace) { if (m_trace) {
@ -441,7 +442,6 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
if (tmp_tctx->is_mvar_assigned(i)) continue; if (tmp_tctx->is_mvar_assigned(i)) continue;
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
if (tmp_tctx->is_prop(m_type)) { if (tmp_tctx->is_prop(m_type)) {
flet<name> set_name(m_rel, get_iff_name()); flet<name> set_name(m_rel, get_iff_name());
result r_cond = simplify(m_type); result r_cond = simplify(m_type);
@ -563,6 +563,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
while (is_pi(m_type)) { while (is_pi(m_type)) {
expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data()); expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type)); expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type));
lean_assert(!has_metavar(l));
ls.push_back(l); ls.push_back(l);
m_type = instantiate(binding_body(m_type), l); m_type = instantiate(binding_body(m_type), l);
} }
@ -578,6 +579,8 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls)); flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs); h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
lean_assert(!has_metavar(h_lhs));
result r_congr_hyp = simplify(h_lhs); result r_congr_hyp = simplify(h_lhs);
expr hyp; expr hyp;
if (r_congr_hyp.is_none()) { if (r_congr_hyp.is_none()) {