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

refactor(kernel/metavar): remove unnecessary functionality

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 04:45:50 +01:00
parent 50f76fd138
commit 9517f31a71
4 changed files with 29 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/kernel/metavar.cpp
View file

@ -83,7 +83,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, name_set * unassigned) {
std::pair<level, justification> 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<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, 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<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();
@ -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<expr, justification> substitution::instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs) const {
std::pair<expr, justification> 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<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);
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::tuple<expr, justification, substitution> substitution::updt_instantiate_metavars(expr const & e, name_set * unassigned_lvls,
name_set * unassigned_exprs) const {
std::tuple<expr, justification, substitution> 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<level, justification> substitution::instantiate_metavars(level const & l, name_set * unassigned) const {
std::pair<level, justification> 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<expr, substitution> 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 {

21
src/kernel/metavar.h
View file

@ -23,9 +23,9 @@ class substitution {
jst_map m_expr_jsts;
jst_map m_level_jsts;
std::pair<expr, justification> d_instantiate_metavars(expr const & e, name_set * unassigned_lvls, name_set * unassigned_exprs);
std::pair<expr, justification> d_instantiate_metavars(expr const & e);
expr d_instantiate_metavars_wo_jst(expr const & e);
std::pair<level, justification> d_instantiate_metavars(level const & l, bool use_jst, bool updt, name_set * unassigned);
std::pair<level, justification> 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<expr, justification> instantiate_metavars(expr const & e, name_set * unassigned_lvls = nullptr,
name_set * unassigned_exprs = nullptr) const;
std::pair<expr, justification> 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<expr, justification, substitution> updt_instantiate_metavars(expr const & e, name_set * unassigned_lvls = nullptr,
name_set * unassigned_exprs = nullptr) const;
std::tuple<expr, justification, substitution> 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<level, justification> instantiate_metavars(level const & l, name_set * unassigned = nullptr) const;
/** \brief Instantiate level metavariables in \c l. */
std::pair<level, justification> instantiate_metavars(level const & l) const;
/**
\brief Instantiate metavariables in \c e assigned in the substitution \c s,

2
src/library/unifier.cpp
View file

@ -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<constraints> 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));
}

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

@ -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() {