diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 3c36404cf..9eb05467c 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -93,7 +93,7 @@ substitution substitution::assign(name const & m, level const & l) const { return assign(m, l, justification()); } -std::pair substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt) { +std::pair 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 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 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 substitution::instantiate_metavars(expr const & e) const { +std::pair 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 substitution::d_instantiate_metavars(expr const & e) { - instantiate_metavars_fn fn(*this, true, true); +std::pair 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 substitution::updt_instantiate_metavars(expr const & e) const { +std::tuple 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 substitution::instantiate_metavars(level const & l) const { +std::pair 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 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 { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 2ddb8156d..f0b036b7f 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #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 d_instantiate_metavars(expr const & e); + std::pair 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 d_instantiate_metavars(level const & l, bool use_jst, bool updt); + std::pair 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 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 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 updt_instantiate_metavars(expr const & e) const; + std::tuple 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 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 instantiate_metavars(level const & l, name_set * unassigned = nullptr) const; /** \brief Instantiate metavariables in \c e assigned in the substitution \c s, diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 3c6ccc4f3..5a90566a6 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -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; }