From 92ba4e8b2d040a799eda7deb8d2a7cdd3e69c496 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2014 08:34:04 -0800 Subject: [PATCH] feat(library/simplifier): add support for metavariables in conditional rewrite rules Signed-off-by: Leonardo de Moura --- src/library/simplifier/ceq.cpp | 20 ++++++++++++++------ src/library/simplifier/ceq.h | 3 ++- src/library/simplifier/rewrite_rule_set.cpp | 6 +++--- src/library/simplifier/rewrite_rule_set.h | 3 ++- src/library/simplifier/simplifier.cpp | 2 +- src/library/tactic/simplify_tactic.cpp | 2 +- tests/lua/ceq1.lua | 2 +- 7 files changed, 24 insertions(+), 14 deletions(-) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 12eb70d151..7a12c793c7 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -22,8 +22,9 @@ bool is_ceq(ro_environment const & env, expr e); \brief Auxiliary functional object for creating "conditional equations" */ class to_ceqs_fn { - ro_environment const & m_env; - unsigned m_idx; + ro_environment const & m_env; + optional const & m_menv; + unsigned m_idx; static list mk_singleton(expr const & e, expr const & H) { return list(mk_pair(e, H)); @@ -33,6 +34,10 @@ class to_ceqs_fn { return m_env->imported("if_then_else"); } + expr lift_free_vars(expr const & e, unsigned d) { + return ::lean::lift_free_vars(e, d, m_menv); + } + name mk_aux_name() { if (m_idx == 0) { m_idx = 1; @@ -114,15 +119,15 @@ class to_ceqs_fn { } } public: - to_ceqs_fn(ro_environment const & env):m_env(env), m_idx(0) {} + to_ceqs_fn(ro_environment const & env, optional const & menv):m_env(env), m_menv(menv), m_idx(0) {} list operator()(expr const & e, expr const & H) { return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, p.first); }); } }; -list to_ceqs(ro_environment const & env, expr const & e, expr const & H) { - return to_ceqs_fn(env)(e, H); +list to_ceqs(ro_environment const & env, optional const & menv, expr const & e, expr const & H) { + return to_ceqs_fn(env, menv)(e, H); } bool is_ceq(ro_environment const & env, expr e) { @@ -230,7 +235,10 @@ bool is_permutation_ceq(expr e) { static int to_ceqs(lua_State * L) { ro_shared_environment env(L, 1); - auto r = to_ceqs(env, to_expr(L, 2), to_expr(L, 3)); + optional menv; + if (!lua_isnil(L, 2)) + menv = to_metavar_env(L, 2); + auto r = to_ceqs(env, menv, to_expr(L, 3), to_expr(L, 4)); lua_newtable(L); int i = 1; for (auto p : r) { diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h index 0c397bee04..fce141f821 100644 --- a/src/library/simplifier/ceq.h +++ b/src/library/simplifier/ceq.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "util/lua.h" #include "kernel/environment.h" +#include "kernel/metavar.h" #include "library/expr_pair.h" namespace lean { /** @@ -26,7 +27,7 @@ namespace lean { \remark if the left-hand-side of an equation does not contain all variables, then it is discarded. That is, all elements in the resultant list satisfy the predicate \c is_ceq. */ -list to_ceqs(ro_environment const & env, expr const & e, expr const & H); +list to_ceqs(ro_environment const & env, optional const & menv, expr const & e, expr const & H); /** \brief Return true iff \c e is a conditional equation. diff --git a/src/library/simplifier/rewrite_rule_set.cpp b/src/library/simplifier/rewrite_rule_set.cpp index 88ef760b24..dffa631b01 100644 --- a/src/library/simplifier/rewrite_rule_set.cpp +++ b/src/library/simplifier/rewrite_rule_set.cpp @@ -25,9 +25,9 @@ rewrite_rule_set::rewrite_rule_set(rewrite_rule_set const & other): m_env(other.m_env), m_rule_set(other.m_rule_set), m_disabled_rules(other.m_disabled_rules), m_congr_thms(other.m_congr_thms) {} rewrite_rule_set::~rewrite_rule_set() {} -void rewrite_rule_set::insert(name const & id, expr const & th, expr const & proof) { +void rewrite_rule_set::insert(name const & id, expr const & th, expr const & proof, optional const & menv) { ro_environment env(m_env); - for (auto const & p : to_ceqs(env, th, proof)) { + for (auto const & p : to_ceqs(env, menv, th, proof)) { expr const & ceq = p.first; expr const & proof = p.second; bool is_perm = is_permutation_ceq(ceq); @@ -48,7 +48,7 @@ void rewrite_rule_set::insert(name const & th_name) { ro_environment env(m_env); auto obj = env->find_object(th_name); if (obj && (obj->is_theorem() || obj->is_axiom())) { - insert(th_name, obj->get_type(), mk_constant(th_name)); + insert(th_name, obj->get_type(), mk_constant(th_name), none_ro_menv()); } else { throw exception(sstream() << "'" << th_name << "' is not a theorem nor an axiom"); } diff --git a/src/library/simplifier/rewrite_rule_set.h b/src/library/simplifier/rewrite_rule_set.h index efc7fb5334..dfb7795fb2 100644 --- a/src/library/simplifier/rewrite_rule_set.h +++ b/src/library/simplifier/rewrite_rule_set.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "util/splay_tree.h" #include "util/name.h" #include "kernel/environment.h" +#include "kernel/metavar.h" #include "kernel/formatter.h" #include "library/io_state_stream.h" #include "library/simplifier/congr.h" @@ -59,7 +60,7 @@ public: \brief Convert the theorem \c th with proof \c proof into conditional rewrite rules, and insert the rules into this rule set. The new rules are tagged with the given \c id. */ - void insert(name const & id, expr const & th, expr const & proof); + void insert(name const & id, expr const & th, expr const & proof, optional const & menv); /** \brief Convert the theorem/axiom named \c th_name in the environment into conditional rewrite rules, diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 441f3d0e60..de0a945082 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -184,7 +184,7 @@ class simplifier_cell::imp { updt_rule_set(imp & fn, expr const & H): m_fn(fn), m_old(m_fn.m_rule_sets[0]), m_reset_cache(m_fn.m_cache) { lean_assert(const_type(H)); - m_fn.m_rule_sets[0].insert(g_local, *const_type(H), H); + m_fn.m_rule_sets[0].insert(g_local, *const_type(H), H, m_fn.m_menv.to_some_menv()); } ~updt_rule_set() { m_fn.m_rule_sets[0] = m_old; diff --git a/src/library/tactic/simplify_tactic.cpp b/src/library/tactic/simplify_tactic.cpp index d063f797b3..6dfa1347ca 100644 --- a/src/library/tactic/simplify_tactic.cpp +++ b/src/library/tactic/simplify_tactic.cpp @@ -43,7 +43,7 @@ static optional simplify_tactic(ro_environment const & env, io_stat for (auto const & p : g.get_hypotheses()) { if (tc.is_proposition(p.second, context(), menv)) { expr H = mk_constant(p.first, p.second); - rs.insert(g_assumption, p.second, H); + rs.insert(g_assumption, p.second, H, some_ro_menv(menv)); } } } diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua index fce48baac9..f4da598c01 100644 --- a/tests/lua/ceq1.lua +++ b/tests/lua/ceq1.lua @@ -11,7 +11,7 @@ end function test_ceq(name, expected, is_perm) local obj = env:find_object(name) - local r = to_ceqs(env, obj:get_type(), Const(name)) + local r = to_ceqs(env, nil, obj:get_type(), Const(name)) show_ceqs(r) assert(#r == expected) if is_perm ~= nil then