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

refactor(library/elaborator): remove hackish rule

Browse source 
After the recent fixes, the hack in process_metavar is not needed anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-01 10:55:32 -08:00
parent 5f29146e0b
commit 74cae2a154
3 changed files with 0 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/context.cpp
View file

@ -87,18 +87,4 @@ optional<context> context::remove(unsigned s, unsigned n, metavar_env const & me
return optional<context>();
}
}
static list<context_entry> insert_at_core(list<context_entry> const & l, unsigned i, name const & n, expr const & d,
metavar_env const & menv) {
if (i == 0) {
return cons(context_entry(n, d), l);
} else {
lean_assert(l);
return cons(lift_free_vars(head(l), i-1, 1, menv), insert_at_core(tail(l), i-1, n, d, menv));
}
}
context context::insert_at(unsigned i, name const & n, expr const & d, metavar_env const & menv) const {
return context(insert_at_core(m_list, i, n, d, menv));
}
}

12
src/kernel/context.h
View file

@ -78,18 +78,6 @@ public:
That is, the lower operations must be valid.
*/
optional<context> remove(unsigned s, unsigned n, metavar_env const & menv) const;
/**
\brief Return a new context where then entry n : d is inserted at position i.
The entries from [0, i) are lifted
That is, if this context is of the form
[ce_m, ..., ce_i, ce_{i-1}, ..., ce_0]
Then, the resultant context is of the form
[ce_m, ..., ce_i, n := v, lift(ce_{i-1}, 0, 1), ..., lift(ce_0, i-1, 1)]
\pre size() >= i
*/
context insert_at(unsigned i, name const & n, expr const & d, metavar_env const & menv) const;
friend bool operator==(context const & ctx1, context const & ctx2) { return ctx1.m_list == ctx2.m_list; }
friend bool operator!=(context const & ctx1, context const & ctx2) { return !(ctx1 == ctx2); }
};

14
src/library/elaborator/elaborator.cpp
View file

@ -492,20 +492,6 @@ class elaborator::imp {
m_conflict = justification(new unification_failure_justification(c));
return Failed;
}
} else if (me.is_inst() && is_proposition(b, ctx) && !is_proposition(me.v(), ctx)) {
// If b is a proposition, and the value in the local context is not,
// we ignore it, and create new constraint without the head of the local context.
// This is a little bit hackish. We do it because we want to preserve
// the structure of the proposition. This is similar to the trick used
// in the assign(a, b, c) branch above.
justification new_jst(new normalize_justification(c));
expr new_a = pop_meta_context(a);
expr new_b = lift_free_vars(b, me.s(), 1, m_state.m_menv);
context new_ctx = ctx.insert_at(me.s(), g_x_name, Type(), m_state.m_menv); // insert a dummy at position s
if (!is_lhs)
swap(new_a, new_b);
push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_jst);
return Processed;
}
}
}