From 9517f31a71f0c9769788246a9479b85cd4a3a051 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jul 2014 04:45:50 +0100 Subject: [PATCH] refactor(kernel/metavar): remove unnecessary functionality Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 47 +++++++++++++++--------------------- src/kernel/metavar.h | 21 +++++----------- src/library/unifier.cpp | 2 +- src/tests/kernel/metavar.cpp | 24 +++--------------- 4 files changed, 29 insertions(+), 65 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 2c71b33ed..97bfe1c23 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -83,7 +83,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, name_set * unassigned) { +std::pair substitution::d_instantiate_metavars(level const & l, bool use_jst, bool updt) { if (!has_meta(l)) return mk_pair(l, justification()); justification j; @@ -94,7 +94,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, unassigned); + auto p2 = d_instantiate_metavars(p1->first, use_jst, updt); if (use_jst) { justification new_jst = mk_composite1(p1->second, p2.second); if (updt) @@ -104,8 +104,6 @@ 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(); @@ -119,13 +117,11 @@ 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, m_unassigned_lvls); + auto p1 = m_subst.d_instantiate_metavars(l, m_use_jst, m_update); if (m_use_jst) save_jst(p1.second); return p1.first; @@ -153,19 +149,17 @@ protected: return p1->first; } else if (m_use_jst) { if (m_update) { - auto p2 = m_subst.d_instantiate_metavars(p1->first, m_unassigned_lvls, m_unassigned_exprs); + auto p2 = m_subst.d_instantiate_metavars(p1->first); 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, m_unassigned_lvls, m_unassigned_exprs); + auto p2 = m_subst.instantiate_metavars(p1->first); 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); @@ -175,8 +169,6 @@ protected: } } } else { - if (m_unassigned_exprs) - m_unassigned_exprs->insert(m_name); return m; } } @@ -207,54 +199,53 @@ protected: } public: - 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) {} + instantiate_metavars_fn(substitution & s, bool use_jst, bool updt): + m_subst(s), m_use_jst(use_jst), m_update(updt) {} justification const & get_justification() const { return m_jst; } }; -std::pair substitution::instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs) const { +std::pair substitution::instantiate_metavars(expr const & e) const { substitution s(*this); - instantiate_metavars_fn fn(s, true, false, unassigned_lvls, unassigned_exprs); + instantiate_metavars_fn fn(s, true, false); expr r = fn(e); return mk_pair(r, fn.get_justification()); } -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); +std::pair 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::tuple substitution::updt_instantiate_metavars(expr const & e, name_set * unassigned_lvls, - name_set * unassigned_exprs) const { +std::tuple substitution::updt_instantiate_metavars(expr const & e) const { substitution s(*this); - instantiate_metavars_fn fn(s, true, true, unassigned_lvls, unassigned_exprs); + instantiate_metavars_fn fn(s, true, true); expr r = fn(e); return std::make_tuple(r, fn.get_justification(), s); } -std::pair substitution::instantiate_metavars(level const & l, name_set * unassigned) const { +std::pair substitution::instantiate_metavars(level const & l) const { substitution s(*this); - return s.d_instantiate_metavars(l, true, false, unassigned); + return s.d_instantiate_metavars(l, true, false); } expr substitution::instantiate_metavars_wo_jst(expr const & e) const { substitution s(*this); - return instantiate_metavars_fn(s, false, false, nullptr, nullptr)(e); + return instantiate_metavars_fn(s, false, false)(e); } expr substitution::d_instantiate_metavars_wo_jst(expr const & e) { - return instantiate_metavars_fn(*this, false, true, nullptr, nullptr)(e); + return instantiate_metavars_fn(*this, false, true)(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, nullptr, nullptr)(e), s); + return mk_pair(instantiate_metavars_fn(s, false, true)(e), s); } level substitution::instantiate_metavars_wo_jst(level const & l) const { substitution s(*this); - return s.d_instantiate_metavars(l, false, false, nullptr).first; + return s.d_instantiate_metavars(l, false, false).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 4a668fe04..c9fa34b7e 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -23,9 +23,9 @@ class substitution { jst_map m_expr_jsts; jst_map m_level_jsts; - std::pair d_instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs); + std::pair d_instantiate_metavars(expr const & e); expr d_instantiate_metavars_wo_jst(expr const & e); - std::pair d_instantiate_metavars(level const & l, bool use_jst, bool updt, name_set * unassigned); + std::pair d_instantiate_metavars(level const & l, bool use_jst, bool updt); friend class instantiate_metavars_fn; justification get_expr_jst(name const & m) const { if (auto it = m_expr_jsts.find(m)) return *it; else return justification(); } @@ -87,12 +87,8 @@ public: /** \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; + std::pair instantiate_metavars(expr const & e) const; /** \brief Similar to the previous function, but it compress the substitution. @@ -100,15 +96,10 @@ 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, name_set * unassigned_lvls = nullptr, - name_set * unassigned_exprs = nullptr) const; + std::tuple updt_instantiate_metavars(expr const & e) 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 level metavariables in \c l. */ + std::pair instantiate_metavars(level const & l) const; /** \brief Instantiate metavariables in \c e assigned in the substitution \c s, diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 70a34b840..5c59289fe 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -760,7 +760,7 @@ struct unifier_fn { lean_assert(is_choice_cnstr(c)); expr const & m = cnstr_expr(c); choice_fn const & fn = cnstr_choice_fn(c); - auto m_type_jst = m_subst.instantiate_metavars(m_tc->infer(m), nullptr, nullptr); + auto m_type_jst = m_subst.instantiate_metavars(m_tc->infer(m)); lazy_list alts = fn(m, m_type_jst.first, m_subst, m_ngen.mk_child()); return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); } diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 6007a0a7f..f5edffcf8 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -143,36 +143,18 @@ static void tst4() { 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")); + lean_assert(s.instantiate_metavars(t).first == t); 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")); + lean_assert(s.instantiate_metavars(t).first == f(T1, T2, a, m3)); 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")); + lean_assert(s.instantiate_metavars(t).first == f(Bool, T2, a, m3)); } int main() {