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

feat(kernel/metavar): add option to instantiate only expr metavars

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 05:54:05 +01:00
parent 80d1a6b993
commit a38dc76b37
2 changed files with 15 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/kernel/metavar.cpp
View file

@ -117,6 +117,7 @@ protected:
justification m_jst;
bool m_use_jst;
bool m_update;
bool m_only_expr;
void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
@ -132,10 +133,12 @@ protected:
}
virtual expr visit_sort(expr const & s) {
lean_assert(!m_only_expr);
return update_sort(s, visit_level(sort_level(s)));
}
virtual expr visit_constant(expr const & c) {
lean_assert(!m_only_expr);
return update_constant(c, visit_levels(const_levels(c)));
}
@ -191,7 +194,7 @@ protected:
}
virtual expr visit(expr const & e) {
if (!has_metavar(e)) {
if ((m_only_expr && !has_expr_metavar(e)) || (!m_only_expr && !has_metavar(e))) {
return e;
} else {
return replace_visitor::visit(e);
@ -199,8 +202,8 @@ protected:
}
public:
instantiate_metavars_fn(substitution & s, bool use_jst, bool updt):
m_subst(s), m_use_jst(use_jst), m_update(updt) {}
instantiate_metavars_fn(substitution & s, bool use_jst, bool updt, bool only_expr = false):
m_subst(s), m_use_jst(use_jst), m_update(updt), m_only_expr(only_expr) {}
justification const & get_justification() const { return m_jst; }
};
@ -211,10 +214,14 @@ std::pair<expr, justification> substitution::instantiate_metavars(expr const & e
return mk_pair(r, fn.get_justification());
}
std::pair<expr, justification> substitution::d_instantiate_metavars(expr const & e) {
instantiate_metavars_fn fn(*this, true, true);
expr r = fn(e);
return mk_pair(r, fn.get_justification());
std::pair<expr, justification> substitution::d_instantiate_metavars(expr const & e, bool only_expr) {
if ((only_expr && !has_expr_metavar(e)) || (!only_expr && !has_metavar(e))) {
return mk_pair(e, justification());
} else {
instantiate_metavars_fn fn(*this, true, true, only_expr);
expr r = fn(e);
return mk_pair(r, fn.get_justification());
}
}
std::tuple<expr, justification, substitution> substitution::updt_instantiate_metavars(expr const & e) const {

2
src/kernel/metavar.h
View file

@ -58,7 +58,7 @@ public:
void d_assign(level const & m, level const & t, justification const & j) { d_assign(meta_id(m), t, j); }
void d_assign(level const & m, level const & t) { d_assign(m, t, justification ()); }
std::pair<expr, justification> d_instantiate_metavars(expr const & e);
std::pair<expr, justification> d_instantiate_metavars(expr const & e, bool only_expr = false);
expr d_instantiate_metavars_wo_jst(expr const & e);
std::pair<level, justification> d_instantiate_metavars(level const & l) { return d_instantiate_metavars(l, true, true); }