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

feat(kernel/metavar): collect unassigned metavariables while instantiating

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-21 16:57:47 -07:00
parent bf8f3318d8
commit fedbf8595b
3 changed files with 87 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/kernel/metavar.cpp
View file

@ -93,7 +93,7 @@ substitution substitution::assign(name const & m, level const & l) const {
return assign(m, l, justification());
}
std::pair<level, justification> substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt) {
std::pair<level, justification> substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt, name_set * unassigned) {
if (!has_meta(l))
return mk_pair(l, justification());
justification j;
@ -104,7 +104,7 @@ std::pair<level, justification> substitution::d_instantiate_metavars(level const
} else if (is_meta(l)) {
auto p1 = get_assignment(l);
if (p1) {
auto p2 = d_instantiate_metavars(p1->first, use_jst, updt);
auto p2 = d_instantiate_metavars(p1->first, use_jst, updt, unassigned);
if (use_jst) {
justification new_jst = mk_composite1(p1->second, p2.second);
if (updt)
@ -114,6 +114,8 @@ std::pair<level, justification> substitution::d_instantiate_metavars(level const
d_assign(meta_id(l), p2.first);
}
return some_level(p2.first);
} else if (unassigned) {
unassigned->insert(meta_id(l));
}
}
return none_level();
@ -127,11 +129,13 @@ protected:
justification m_jst;
bool m_use_jst;
bool m_update;
name_set * m_unassigned_lvls;
name_set * m_unassigned_exprs;
void save_jst(justification const & j) { m_jst = mk_composite1(m_jst, j); }
level visit_level(level const & l) {
auto p1 = m_subst.d_instantiate_metavars(l, m_use_jst, m_update);
auto p1 = m_subst.d_instantiate_metavars(l, m_use_jst, m_update, m_unassigned_lvls);
if (m_use_jst)
save_jst(p1.second);
return p1.first;
@ -159,17 +163,19 @@ protected:
return p1->first;
} else if (m_use_jst) {
if (m_update) {
auto p2 = m_subst.d_instantiate_metavars(p1->first);
auto p2 = m_subst.d_instantiate_metavars(p1->first, m_unassigned_lvls, m_unassigned_exprs);
justification new_jst = mk_composite1(p1->second, p2.second);
m_subst.d_assign(m_name, p2.first, new_jst);
save_jst(new_jst);
return p2.first;
} else {
auto p2 = m_subst.instantiate_metavars(p1->first);
auto p2 = m_subst.instantiate_metavars(p1->first, m_unassigned_lvls, m_unassigned_exprs);
save_jst(mk_composite1(p1->second, p2.second));
return p2.first;
}
} else {
lean_assert(m_unassigned_exprs == nullptr);
lean_assert(m_unassigned_lvls == nullptr);
if (m_update) {
expr r = m_subst.d_instantiate_metavars_wo_jst(p1->first);
m_subst.d_assign(m_name, r);
@ -179,6 +185,8 @@ protected:
}
}
} else {
if (m_unassigned_exprs)
m_unassigned_exprs->insert(m_name);
return m;
}
}
@ -209,53 +217,54 @@ 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, name_set * unassigned_lvls, name_set * unassigned_exprs):
m_subst(s), m_use_jst(use_jst), m_update(updt), m_unassigned_lvls(unassigned_lvls), m_unassigned_exprs(unassigned_exprs) {}
justification const & get_justification() const { return m_jst; }
};
std::pair<expr, justification> substitution::instantiate_metavars(expr const & e) const {
std::pair<expr, justification> substitution::instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs) const {
substitution s(*this);
instantiate_metavars_fn fn(s, true, false);
instantiate_metavars_fn fn(s, true, false, unassigned_lvls, unassigned_exprs);
expr r = fn(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);
std::pair<expr, justification> substitution::d_instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs) {
instantiate_metavars_fn fn(*this, true, true, unassigned_lvls, unassigned_exprs);
expr r = fn(e);
return mk_pair(r, fn.get_justification());
}
std::tuple<expr, justification, substitution> substitution::updt_instantiate_metavars(expr const & e) const {
std::tuple<expr, justification, substitution> substitution::updt_instantiate_metavars(expr const & e, name_set * unassigned_lvls,
name_set * unassigned_exprs) const {
substitution s(*this);
instantiate_metavars_fn fn(s, true, true);
instantiate_metavars_fn fn(s, true, true, unassigned_lvls, unassigned_exprs);
expr r = fn(e);
return std::make_tuple(r, fn.get_justification(), s);
}
std::pair<level, justification> substitution::instantiate_metavars(level const & l) const {
std::pair<level, justification> substitution::instantiate_metavars(level const & l, name_set * unassigned) const {
substitution s(*this);
return s.d_instantiate_metavars(l, true, false);
return s.d_instantiate_metavars(l, true, false, unassigned);
}
expr substitution::instantiate_metavars_wo_jst(expr const & e) const {
substitution s(*this);
return instantiate_metavars_fn(s, false, false)(e);
return instantiate_metavars_fn(s, false, false, nullptr, nullptr)(e);
}
expr substitution::d_instantiate_metavars_wo_jst(expr const & e) {
return instantiate_metavars_fn(*this, false, true)(e);
return instantiate_metavars_fn(*this, false, true, nullptr, nullptr)(e);
}
std::pair<expr, substitution> substitution::updt_instantiate_metavars_wo_jst(expr const & e) const {
substitution s(*this);
return mk_pair(instantiate_metavars_fn(s, false, true)(e), s);
return mk_pair(instantiate_metavars_fn(s, false, true, nullptr, nullptr)(e), s);
}
level substitution::instantiate_metavars_wo_jst(level const & l) const {
substitution s(*this);
return s.d_instantiate_metavars(l, false, false).first;
return s.d_instantiate_metavars(l, false, false, nullptr).first;
}
bool substitution::occurs_expr(name const & m, expr const & e) const {

26
src/kernel/metavar.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <utility>
#include "util/rb_map.h"
#include "util/optional.h"
#include "util/name_set.h"
#include "kernel/expr.h"
#include "kernel/justification.h"
@ -23,9 +24,9 @@ class substitution {
void d_assign(name const & m, expr const & t);
void d_assign(name const & m, level const & t, justification const & j);
void d_assign(name const & m, level const & t);
std::pair<expr, justification> d_instantiate_metavars(expr const & e);
std::pair<expr, justification> d_instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs);
expr d_instantiate_metavars_wo_jst(expr const & e);
std::pair<level, justification> d_instantiate_metavars(level const & l, bool use_jst, bool updt);
std::pair<level, justification> d_instantiate_metavars(level const & l, bool use_jst, bool updt, name_set * unassigned);
friend class instantiate_metavars_fn;
public:
substitution();
@ -69,8 +70,14 @@ public:
substitution assign(level const & m, level const & l, justification const & j) const { lean_assert(is_meta(m)); return assign(meta_id(m), l, j); }
substitution assign(level const & m, level const & l) { lean_assert(is_meta(m)); return assign(meta_id(m), l); }
/** \brief Instantiate metavariables in \c e assigned in this substitution. */
std::pair<expr, justification> instantiate_metavars(expr const & e) const;
/**
\brief Instantiate metavariables in \c e assigned in this substitution.
\remark If \c unassigned_exprs and \c unassigned_lvls are not nullptr, then this method
stores unassigned metavariables in them.
*/
std::pair<expr, justification> instantiate_metavars(expr const & e, name_set * unassigned_lvls = nullptr,
name_set * unassigned_exprs = nullptr) const;
/**
\brief Similar to the previous function, but it compress the substitution.
@ -78,10 +85,15 @@ public:
if s[m] = t, and t has asssigned metavariables, then s[m] <- instantiate_metavars(t, s).
The updated substitution is returned.
*/
std::tuple<expr, justification, substitution> updt_instantiate_metavars(expr const & e) const;
std::tuple<expr, justification, substitution> updt_instantiate_metavars(expr const & e, name_set * unassigned_lvls = nullptr,
name_set * unassigned_exprs = nullptr) const;
/** \brief Instantiate level metavariables in \c l. */
std::pair<level, justification> instantiate_metavars(level const & l) const;
/**
\brief Instantiate level metavariables in \c l.
\remark If \c unassigned is not nullptr, then store unassigned meta universe parameters in it.
*/
std::pair<level, justification> instantiate_metavars(level const & l, name_set * unassigned = nullptr) const;
/**
\brief Instantiate metavariables in \c e assigned in the substitution \c s,

40
src/tests/kernel/metavar.cpp
View file

@ -136,10 +136,50 @@ static void tst3() {
std::cout << s.instantiate_metavars(m1(a, b, g(a))).first << "\n";
}
static void tst4() {
expr m1 = mk_metavar("m1", Bool);
expr m2 = mk_metavar("m2", Bool);
expr m3 = mk_metavar("m3", Bool);
level l1 = mk_meta_univ("l1");
level u = mk_global_univ("u");
substitution s;
name_set exprs;
name_set lvls;
expr f = Const("f");
expr g = Const("g");
expr a = Const("a");
expr T1 = mk_sort(l1);
expr T2 = mk_sort(u);
expr t = f(T1, T2, m1, m2);
lean_assert(s.instantiate_metavars(t, &lvls, &exprs).first == t);
lean_assert(exprs.contains("m1"));
lean_assert(exprs.contains("m2"));
lean_assert(!exprs.contains("m3"));
lean_assert(lvls.contains("l1"));
s = s.assign(m1, a, justification());
s = s.assign(m2, m3, justification());
lvls = name_set();
exprs = name_set();
lean_assert(s.instantiate_metavars(t, &lvls, &exprs).first == f(T1, T2, a, m3));
lean_assert(!exprs.contains("m1"));
lean_assert(!exprs.contains("m2"));
lean_assert(exprs.contains("m3"));
lean_assert(lvls.contains("l1"));
s = s.assign(l1, level(), justification());
lvls = name_set();
exprs = name_set();
lean_assert(s.instantiate_metavars(t, &lvls, &exprs).first == f(Bool, T2, a, m3));
lean_assert(!exprs.contains("m1"));
lean_assert(!exprs.contains("m2"));
lean_assert(exprs.contains("m3"));
lean_assert(!lvls.contains("l1"));
}
int main() {
save_stack_info();
tst1();
tst2();
tst3();
tst4();
return has_violations() ? 1 : 0;
}