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

feat(library/match): extend match_plugin interface, and allow them to recursively invoke the matcher

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-04 18:28:14 -07:00
parent c34c2f4f5c
commit f4031b620f
2 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/match.cpp
View file

@ -105,7 +105,7 @@ class match_fn : public match_context {
(*m_name_subst)[binding_name(p)] = binding_name(t); (*m_name_subst)[binding_name(p)] = binding_name(t);
expr p_d = instantiate_rev(binding_domain(p), ls.size(), ls.data()); expr p_d = instantiate_rev(binding_domain(p), ls.size(), ls.data());
expr t_d = instantiate_rev(binding_domain(t), ls.size(), ls.data()); expr t_d = instantiate_rev(binding_domain(t), ls.size(), ls.data());
if (!match(p_d, t_d)) if (!_match(p_d, t_d))
return false; return false;
expr l = mk_local(m_ngen.next(), binding_name(t), t_d, binding_info(t)); expr l = mk_local(m_ngen.next(), binding_name(t), t_d, binding_info(t));
ls.push_back(l); ls.push_back(l);
@ -116,13 +116,13 @@ class match_fn : public match_context {
return false; return false;
p = instantiate_rev(p, ls.size(), ls.data()); p = instantiate_rev(p, ls.size(), ls.data());
t = instantiate_rev(t, ls.size(), ls.data()); t = instantiate_rev(t, ls.size(), ls.data());
return match(p, t); return _match(p, t);
} }
bool match_macro(expr const & p, expr const & t) { bool match_macro(expr const & p, expr const & t) {
if (macro_def(p) == macro_def(t) && macro_num_args(p) == macro_num_args(t)) { if (macro_def(p) == macro_def(t) && macro_num_args(p) == macro_num_args(t)) {
for (unsigned i = 0; i < macro_num_args(p); i++) { for (unsigned i = 0; i < macro_num_args(p); i++) {
if (!match(macro_arg(p, i), macro_arg(t, i))) if (!_match(macro_arg(p, i), macro_arg(t, i)))
return false; return false;
} }
return true; return true;
@ -131,7 +131,7 @@ class match_fn : public match_context {
} }
bool match_app(expr const & p, expr const & t) { bool match_app(expr const & p, expr const & t) {
return match_core(app_fn(p), app_fn(t)) && match(app_arg(p), app_arg(t)); return match_core(app_fn(p), app_fn(t)) && _match(app_arg(p), app_arg(t));
} }
bool match_level_core(level const & p, level const & l) { bool match_level_core(level const & p, level const & l) {
@ -203,12 +203,7 @@ class match_fn : public match_context {
lean_unreachable(); // LCOV_EXCL_LINE lean_unreachable(); // LCOV_EXCL_LINE
} }
public: bool _match(expr const & p, expr const & t) {
match_fn(buffer<optional<expr>> & esubst, buffer<optional<level>> & lsubst, name_generator const & ngen,
name_map<name> * name_subst, match_plugin const * plugin):
m_esubst(esubst), m_lsubst(lsubst), m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin) {}
bool match(expr const & p, expr const & t) {
if (is_var(p)) { if (is_var(p)) {
auto s = _get_subst(p); auto s = _get_subst(p);
if (s) { if (s) {
@ -242,6 +237,13 @@ public:
return match_core(p, t); return match_core(p, t);
} }
public:
match_fn(buffer<optional<expr>> & esubst, buffer<optional<level>> & lsubst, name_generator const & ngen,
name_map<name> * name_subst, match_plugin const * plugin):
m_esubst(esubst), m_lsubst(lsubst), m_ngen(ngen), m_name_subst(name_subst), m_plugin(plugin) {}
virtual bool match(expr const & p, expr const & t) { return _match(p, t); }
}; };
bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buffer<optional<level>> & lsubst, bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buffer<optional<level>> & lsubst,

1
src/library/match.h
View file

@ -38,6 +38,7 @@ public:
\pre \c x is not assigned, \c x was created using #mk_idx_meta_univ. \pre \c x is not assigned, \c x was created using #mk_idx_meta_univ.
*/ */
virtual void assign(level const & x, level const & l) = 0; virtual void assign(level const & x, level const & l) = 0;
virtual bool match(expr const & p, expr const & t) = 0;
}; };
/** \brief Callback for extending the higher-order pattern matching procedure. /** \brief Callback for extending the higher-order pattern matching procedure.