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

refactor(library/tactic/rewrite_tactic): use default_converter

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 16:44:51 -08:00
parent c04c0e8381
commit e04250f0d8
3 changed files with 26 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/default_converter.cpp
View file

@ -24,6 +24,9 @@ default_converter::default_converter(environment const & env, optional<module_id
default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize): default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {} default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {}
default_converter::default_converter(environment const & env, bool relax_main_opaque, bool memoize):
default_converter(env, relax_main_opaque ? optional<module_idx>(0) : optional<module_idx>(), memoize) {}
constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx)); return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
} }

3
src/kernel/default_converter.h
View file

@ -74,7 +74,8 @@ protected:
public: public:
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize, default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
extra_opaque_pred const & pred); extra_opaque_pred const & pred);
default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize); default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);
virtual bool is_opaque(declaration const & d) const; virtual bool is_opaque(declaration const & d) const;
virtual optional<module_idx> get_module_idx() const { return m_module_idx; } virtual optional<module_idx> get_module_idx() const { return m_module_idx; }

34
src/library/tactic/rewrite_tactic.cpp
View file

@ -13,6 +13,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/replace_fn.h" #include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h" #include "kernel/for_each_fn.h"
#include "kernel/default_converter.h"
#include "kernel/inductive/inductive.h" #include "kernel/inductive/inductive.h"
#include "library/normalize.h" #include "library/normalize.h"
#include "library/kernel_serializer.h" #include "library/kernel_serializer.h"
@ -479,22 +480,29 @@ class rewrite_fn {
return m_g.mk_meta(m_ngen.next(), type); return m_g.mk_meta(m_ngen.next(), type);
} }
class rewriter_converter : public default_converter {
list<name> const & m_to_unfold;
bool & m_unfolded;
public:
rewriter_converter(environment const & env, bool relax_main_opaque, list<name> const & to_unfold,
bool & unfolded):
default_converter(env, relax_main_opaque),
m_to_unfold(to_unfold), m_unfolded(unfolded) {}
virtual bool is_opaque(declaration const & d) const {
if (std::find(m_to_unfold.begin(), m_to_unfold.end(), d.get_name()) != m_to_unfold.end()) {
m_unfolded = true;
return false;
} else {
return true;
}
}
};
optional<expr> reduce(expr const & e, list<name> const & to_unfold) { optional<expr> reduce(expr const & e, list<name> const & to_unfold) {
bool unfolded = !to_unfold; bool unfolded = !to_unfold;
extra_opaque_pred pred([&](name const & n) {
// everything is opaque but to_unfold
if (std::find(to_unfold.begin(), to_unfold.end(), n) != to_unfold.end()) {
unfolded = true;
return false;
} else {
return true;
}
});
bool relax_main_opaque = false; bool relax_main_opaque = false;
bool memoize = true;
auto tc = new type_checker(m_env, m_ngen.mk_child(), auto tc = new type_checker(m_env, m_ngen.mk_child(),
mk_default_converter(m_env, relax_main_opaque, std::unique_ptr<converter>(new rewriter_converter(m_env, relax_main_opaque, to_unfold, unfolded)));
memoize, pred));
constraint_seq cs; constraint_seq cs;
expr r = normalize(*tc, e, cs); expr r = normalize(*tc, e, cs);
if (!unfolded || cs) // FAIL if didn't unfolded or generated constraints if (!unfolded || cs) // FAIL if didn't unfolded or generated constraints