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

feat(kernel/metavar): expose destructive assign

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 14:07:47 -07:00
parent b49902807c
commit a009225435
3 changed files with 11 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/metavar.cpp
View file

@ -57,20 +57,12 @@ void substitution::d_assign(name const & m, expr const & t, justification const
m_expr_jsts.insert(m, j);
}
void substitution::d_assign(name const & m, expr const & t) {
assign(m, t, justification());
}
void substitution::d_assign(name const & m, level const & l, justification const & j) {
m_level_subst.insert(m, l);
if (!j.is_none())
m_level_jsts.insert(m, j);
}
void substitution::d_assign(name const & m, level const & l) {
assign(m, l, justification());
}
substitution substitution::assign(name const & m, expr const & t, justification const & j) const {
substitution s(*this);
s.d_assign(m, t, j);

13
src/kernel/metavar.h
View file

@ -23,10 +23,6 @@ class substitution {
jst_map m_expr_jsts;
jst_map m_level_jsts;
void d_assign(name const & m, expr const & t, justification const & j);
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, 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, name_set * unassigned);
@ -55,6 +51,15 @@ public:
substitution assign(name const & m, level const & t, justification const & j) const;
substitution assign(name const & m, level const & t) const;
void d_assign(name const & m, expr const & t, justification const & j);
void d_assign(name const & m, expr const & t) { d_assign(m, t, justification()); }
void d_assign(expr const & m, expr const & t, justification const & j) { d_assign(mlocal_name(m), t, j); }
void d_assign(expr const & m, expr const & t) { d_assign(m, t, justification()); }
void d_assign(name const & m, level const & t, justification const & j);
void d_assign(name const & m, level const & t) { d_assign(m, t, justification ()); }
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 ()); }
template<typename F>
void for_each_expr(F && fn) const {
for_each(m_expr_subst, [=](name const & n, expr const & e) { fn(n, e, get_expr_jst(n)); });

4
src/library/unifier.cpp
View file

@ -486,7 +486,7 @@ struct unifier_fn {
*/
bool assign(expr const & m, expr const & v, justification const & j) {
lean_assert(is_metavar(m));
m_subst = m_subst.assign(m, v, j);
m_subst.d_assign(m, v, j);
expr m_type = mlocal_type(m);
expr v_type = m_tc.infer(v);
if (in_conflict())
@ -514,7 +514,7 @@ struct unifier_fn {
*/
bool assign(level const & m, level const & v, justification const & j) {
lean_assert(is_meta(m));
m_subst = m_subst.assign(m, v, j);
m_subst.d_assign(m, v, j);
auto it = m_mlvl_occs.find(meta_id(m));
if (it) {
cnstr_idx_set s = *it;