From b727d5810aaf83535dba76181bf18191159ec3fe Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 6 Nov 2015 21:02:04 -0800 Subject: [PATCH] feat(library/blast/simplifier): rewrite with tmp locals --- src/library/blast/simplifier.cpp | 90 ++++++++++++++++-------- tests/lean/simplifier1.lean | 10 +-- tests/lean/simplifier1.lean.expected.out | 1 - tests/lean/simplifier2.lean | 6 +- tests/lean/simplifier3.lean | 5 -- tests/lean/simplifier3.lean.expected.out | 2 - tests/lean/simplifier9.lean | 27 +++++++ 7 files changed, 92 insertions(+), 49 deletions(-) create mode 100644 tests/lean/simplifier9.lean diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index fad839bbd..cfc781180 100644 --- a/src/library/blast/simplifier.cpp +++ b/src/library/blast/simplifier.cpp @@ -98,6 +98,7 @@ class simplifier { name m_rel; list m_local_ctx; + simp_rule_sets m_ctx_srss; /* Logging */ unsigned m_num_steps{0}; @@ -129,6 +130,17 @@ class simplifier { return has_free_vars(binding_body(f_type)); } + simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer & ls) { + simp_rule_sets srss = _srss; + for (unsigned i = 0; i < ls.size(); i++) { + // TODO assert no metas? + expr & l = ls[i]; + tmp_type_context tctx(env(),ios()); + srss = add(tctx,srss,mlocal_name(l),tctx.infer(l),l); + } + return srss; + } + /* Results */ result lift_from_eq(expr const & x, result const & r); result join(result const & r1, result const & r2); @@ -143,9 +155,9 @@ class simplifier { result simplify_fun(expr const & e); /* Rewriting */ - result rewrite(expr const & e); + result rewrite(expr const & e); + result rewrite(expr const & e, simp_rule_sets const & srss); result rewrite(expr const & e, simp_rule const & sr); - void init_tmp_tctx_for(simp_rule_core const & sr); /* Congruence */ result congr(result const & r_f, result const & r_arg); @@ -168,6 +180,7 @@ simplifier::simplifier(branch const & b, name const & rel): m_app_builder(*m_tmp_tctx), m_branch(b), m_rel(rel) { } /* Cache */ + optional simplifier::cache_lookup(expr const & e) { simplify_cache & cache = m_simplify_caches[m_rel]; auto it = cache.find(e); @@ -179,7 +192,6 @@ void simplifier::cache_save(expr const & e, result const & r) { cache.insert(mk_pair(e,r)); } - /* Results */ result simplifier::lift_from_eq(expr const & x, result const & r) { @@ -375,29 +387,29 @@ result simplifier::simplify_fun(expr const & e) { result simplifier::rewrite(expr const & e) { result r(e); + while (true) { + result r_ctx = rewrite(r.get_new(),m_ctx_srss); + result r_new = rewrite(r_ctx.get_new(),get_simp_rule_sets(env())); + if (r_ctx.is_none() && r_new.is_none()) break; + r = join(join(r,r_ctx),r_new); + } + return r; +} - /* First, we rewrite with local hypotheses */ - //TODO - - /* Next, we rewrite with the [simp_rule_set] */ - simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel); +result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) { + result r(e); + + simp_rule_set const * sr = srss.find(m_rel); if (!sr) return r; list const * srs = sr->find_simp(e); if (!srs) return r; - bool modified = true; - while (modified) { - modified = false; - for_each(*srs,[&](simp_rule const & sr) { - result r_rew = rewrite(r.get_new(),sr); - if (r_rew.is_none()) return; - r = join(r,r_rew); - modified = true; - } - ); - } - + for_each(*srs,[&](simp_rule const & sr) { + result r_new = rewrite(r.get_new(),sr); + if (r_new.is_none()) return; + r = join(r,r_new); + }); return r; } @@ -407,9 +419,11 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e); if (m_trace) { - ios().get_diagnostic_channel() << "[" << sr.get_id() << "]\n"; + expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs()); + expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs()); + ios().get_diagnostic_channel() << "[" << sr.get_lhs() << " =?= " << sr.get_rhs() << "] ==> "; + ios().get_diagnostic_channel() << "[" << new_lhs << " =?= " << new_rhs << "]\n"; } - /* Traverse metavariables backwards */ for (int i = sr.get_num_emeta() - 1; i >= 0; --i) { @@ -428,11 +442,18 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) { if (tmp_tctx->is_mvar_assigned(i)) continue; + // TODO REMOVE DEBUG + expr m_assigned = tmp_tctx->instantiate_uvars_mvars(m); + if (tmp_tctx->is_prop(tmp_tctx->infer(m))) { // TODO try to prove return result(e); } + if (m_trace) { + ios().get_diagnostic_channel() << "failed to assign: " << m << "\n"; + } + /* We fail if there is a meta variable that we still cannot assign */ return result(e); } @@ -516,7 +537,8 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e); if (m_trace) { - ios().get_diagnostic_channel() << "<" << cr.get_id() << ">\n"; + ios().get_diagnostic_channel() << "<" << cr.get_id() << "> " + << e << " === " << cr.get_lhs() << "\n"; } /* First, iterate over the congruence hypotheses */ @@ -531,7 +553,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { while (is_pi(m_type)) { expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data()); expr l = tmp_tctx->mk_tmp_local(d,binding_info(e)); - ls.push_back(tmp_tctx->instantiate_uvars_mvars(l)); + ls.push_back(l); m_type = instantiate(binding_body(m_type),l); } @@ -539,10 +561,14 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { bool valid = is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel); lean_assert(valid); { + simplify_caches fresh_caches; + flet set_simplify_caches(m_simplify_caches,fresh_caches); flet set_name(m_rel,const_name(h_rel)); - flet > set_local_ctx(m_local_ctx,append(m_local_ctx,to_list(ls))); - simplify_caches fresh_caches; - flet set_simplify_caches(m_simplify_caches,fresh_caches); + + buffer ls_instantiated; + for (unsigned i = 0; i < ls.size(); i++) ls_instantiated.push_back(tmp_tctx->instantiate_uvars_mvars(ls[i])); + + flet set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls_instantiated)); h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs); result r_congr_hyp = simplify(h_lhs); @@ -554,11 +580,14 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { hyp = r_congr_hyp.get_proof(); simplified = true; } - hyp = Fun(ls,hyp); + + hyp = Fun(ls_instantiated,hyp); if (!tmp_tctx->is_def_eq(m,hyp)) failed = true; } }); + if (failed || !simplified) return result(e); + /* Traverse metavariables backwards, proving or synthesizing the rest */ for (int i = cr.get_num_emeta() - 1; i >= 0; --i) { expr const & m = cr.get_emeta(i); @@ -581,6 +610,11 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) { return result(e); } + if (m_trace) { + ios().get_diagnostic_channel() << "failed to assign: " << tmp_tctx->instantiate_uvars_mvars(m) << " : " + << tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)) << "\n"; + } + /* We fail if there is a meta variable that we still cannot assign */ return result(e); } diff --git a/tests/lean/simplifier1.lean b/tests/lean/simplifier1.lean index 3ce3521e0..c1eb2bc0c 100644 --- a/tests/lean/simplifier1.lean +++ b/tests/lean/simplifier1.lean @@ -4,13 +4,7 @@ constant T : Type.{l} constants (x y z : T) (f g h : T → T) constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) -#simplify eq 2 (f x) -- f x - attribute Hfxgy [simp] +#simplify eq 2 (f x) attribute Hgyhz [simp] - -set_option simplify.exhaustive false -#simplify eq 2 (f x) -- g y - -set_option simplify.exhaustive true -#simplify eq 2 (f x) -- h z +#simplify eq 2 (f x) diff --git a/tests/lean/simplifier1.lean.expected.out b/tests/lean/simplifier1.lean.expected.out index c260717a7..32e724152 100644 --- a/tests/lean/simplifier1.lean.expected.out +++ b/tests/lean/simplifier1.lean.expected.out @@ -1,3 +1,2 @@ - f x = g y f x = h z diff --git a/tests/lean/simplifier2.lean b/tests/lean/simplifier2.lean index e30fddbcb..5d2b5261f 100644 --- a/tests/lean/simplifier2.lean +++ b/tests/lean/simplifier2.lean @@ -5,11 +5,7 @@ constants (x y z : T) (f g h : T → T) constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) attribute Hfxgy [simp] -attribute Hgyhz [simp] - -set_option simplify.exhaustive false #simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y - -set_option simplify.exhaustive true +attribute Hgyhz [simp] #simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z diff --git a/tests/lean/simplifier3.lean b/tests/lean/simplifier3.lean index 2d1a07b0f..83e57752c 100644 --- a/tests/lean/simplifier3.lean +++ b/tests/lean/simplifier3.lean @@ -7,17 +7,12 @@ constant T : Type.{l} constants (x y z : T → T) (f g h : (T → T) → (T → T)) (a b c : T) constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c) -#simplify eq 2 (f x a) -- f x a attribute Hfxgy [simp] attribute Hgyhz [simp] attribute Hab [simp] attribute Hbc [simp] -set_option simplify.exhaustive false -#simplify eq 2 (f x a) -- g y b - -set_option simplify.exhaustive true #simplify eq 2 (f x a) -- h z c end test_congr diff --git a/tests/lean/simplifier3.lean.expected.out b/tests/lean/simplifier3.lean.expected.out index 6b78a0be1..ea10d9d83 100644 --- a/tests/lean/simplifier3.lean.expected.out +++ b/tests/lean/simplifier3.lean.expected.out @@ -1,4 +1,2 @@ - -f x a = g y b f x a = h z c f x = g x diff --git a/tests/lean/simplifier9.lean b/tests/lean/simplifier9.lean new file mode 100644 index 000000000..86e9f2d6b --- /dev/null +++ b/tests/lean/simplifier9.lean @@ -0,0 +1,27 @@ +-- Rewriting with (tmp)-local hypotheses +import logic.quantifiers + +universe l +constants (T : Type.{l}) (P Q : T → Prop) + +set_option simplify.max_steps 50000 +constants (x y : T) + +#simplify iff 0 x = y → x = y +#simplify iff 0 T → x = y → x = y +#simplify iff 0 ∀ z : T, x = z → x = y +#simplify iff 0 ∀ z : T, z = x → x = z +#simplify iff 0 ∀ (z w : T), x = y → x = y +#simplify iff 0 ∀ (z w : T), x = y → P x + +#simplify iff 0 ∀ (H : ∀ x, P x ↔ Q x), P x +#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x) (q : Prop), P x + +#simplify iff 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x +#simplify iff 0 (∀ (x : T), P x ↔ Q x) → P x +#simplify iff 0 (∀ (x : T), P x ↔ Q x) → P x +#simplify iff 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) → P x + +#simplify iff 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) → P x + +