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

refactor(library/simplifier): the simplifier expects relations to be transitivie and reflexive

Browse source
This commit is contained in:
Leonardo de Moura 2015-07-22 15:46:00 -07:00
parent cc396cba76
commit a07b42ad9e
3 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/simplifier/ceqv.cpp
View file

@ -18,6 +18,10 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
bool is_ceqv(type_checker & tc, expr e); bool is_ceqv(type_checker & tc, expr e);
bool is_simp_relation(environment const & env, name const & n) {
return is_trans_relation(env, n) && is_refl_relation(env, n);
}
/** \brief Auxiliary functional object for creating "conditional equations" */ /** \brief Auxiliary functional object for creating "conditional equations" */
class to_ceqvs_fn { class to_ceqvs_fn {
environment const & m_env; environment const & m_env;
@ -31,14 +35,10 @@ class to_ceqvs_fn {
return is_sort(m_tc.whnf(m_tc.infer(e).first).first); return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
} }
bool is_transitive(expr const & e) { bool is_relation(expr const & e) {
if (!is_app(e)) return false; if (!is_app(e)) return false;
expr const & fn = get_app_fn(e); expr const & fn = get_app_fn(e);
return is_constant(fn) && ::lean::is_trans_relation(m_env, const_name(fn)) && is_type(e); return is_constant(fn) && is_simp_relation(m_env, const_name(fn));
}
bool is_relation(expr const & e) {
return is_transitive(e);
} }
list<expr_pair> lift(expr const & local, list<expr_pair> const & l) { list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
@ -126,10 +126,10 @@ list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H) {
return to_ceqvs_fn(tc)(e, H); return to_ceqvs_fn(tc)(e, H);
} }
bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) { bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
buffer<expr> args; buffer<expr> args;
rel = get_app_args(e, args); rel = get_app_args(e, args);
if (!is_constant(rel) || !is_trans_relation(env, const_name(rel))) if (!is_constant(rel) || !is_simp_relation(env, const_name(rel)))
return false; return false;
relation_info const * rel_info = get_relation_info(env, const_name(rel)); relation_info const * rel_info = get_relation_info(env, const_name(rel));
if (!rel_info || rel_info->get_lhs_pos() >= args.size() || rel_info->get_rhs_pos() >= args.size()) if (!rel_info || rel_info->get_lhs_pos() >= args.size() || rel_info->get_rhs_pos() >= args.size())
@ -139,9 +139,9 @@ bool is_transitive(environment const & env, expr const & e, expr & rel, expr & l
return true; return true;
} }
bool is_transitive(environment const & env, expr const & e, expr & lhs, expr & rhs) { bool is_simp_relation(environment const & env, expr const & e, expr & lhs, expr & rhs) {
expr rel; expr rel;
return is_transitive(env, e, rel, lhs, rhs); return is_simp_relation(env, e, rel, lhs, rhs);
} }
bool is_ceqv(type_checker & tc, expr e) { bool is_ceqv(type_checker & tc, expr e) {
@ -183,7 +183,7 @@ bool is_ceqv(type_checker & tc, expr e) {
e = instantiate(binding_body(e), local); e = instantiate(binding_body(e), local);
} }
expr lhs, rhs; expr lhs, rhs;
if (!is_transitive(env, e, lhs, rhs)) if (!is_simp_relation(env, e, lhs, rhs))
return false; return false;
// traverse lhs, and remove found variables from to_find // traverse lhs, and remove found variables from to_find
for_each(lhs, visitor_fn); for_each(lhs, visitor_fn);
@ -246,7 +246,7 @@ bool is_permutation_ceqv(environment const & env, expr e) {
num_args++; num_args++;
} }
expr lhs, rhs; expr lhs, rhs;
if (is_transitive(env, e, lhs, rhs)) { if (is_simp_relation(env, e, lhs, rhs)) {
buffer<optional<unsigned>> permutation; buffer<optional<unsigned>> permutation;
permutation.resize(num_args); permutation.resize(num_args);
return is_permutation(lhs, rhs, 0, permutation); return is_permutation(lhs, rhs, 0, permutation);

2
src/library/simplifier/ceqv.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
namespace lean { namespace lean {
bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs); bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs);
/** \brief Given (H : e), return a list of (h_i : e_i) where e_i can be viewed as /** \brief Given (H : e), return a list of (h_i : e_i) where e_i can be viewed as
a "conditional" rewriting rule. Any equivalence relation registered using a "conditional" rewriting rule. Any equivalence relation registered using
the relation_manager is considered. the relation_manager is considered.

2
src/library/simplifier/simp_rule_set.cpp
View file

@ -117,7 +117,7 @@ simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s,
new_e = instantiate(binding_body(new_e), mvar); new_e = instantiate(binding_body(new_e), mvar);
} }
expr rel, lhs, rhs; expr rel, lhs, rhs;
if (is_transitive(env, new_e, rel, lhs, rhs) && is_constant(rel)) { if (is_simp_relation(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
new_s.insert(const_name(rel), simp_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm)); new_s.insert(const_name(rel), simp_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
} }
} }