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

Cleanup meta_entry code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-16 19:29:19 -07:00
parent 99a163f11d
commit da09e7217a
5 changed files with 26 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -581,7 +581,7 @@ class elaborator::imp {
return false;
meta_ctx const & ctx = metavar_ctx(e);
meta_entry const & entry = head(ctx);
if (entry.kind() == meta_entry_kind::Lift) {
if (entry.is_lift()) {
c = ::lean::mk_metavar(metavar_idx(e), tail(ctx));
add_trace(e, c);
s = entry.s();
@ -600,7 +600,7 @@ class elaborator::imp {
return false;
meta_ctx const & ctx = metavar_ctx(e);
meta_entry const & entry = head(ctx);
if (entry.kind() == meta_entry_kind::Inst) {
if (entry.is_inst()) {
c = ::lean::mk_metavar(metavar_idx(e), tail(ctx));
add_trace(e, c);
s = entry.s();

10
src/frontends/lean/pp.cpp
View file

@ -1032,14 +1032,14 @@ class pp_fn {
unsigned r_weight = 1;
for (meta_entry const & e : metavar_ctx(a)) {
format e_fmt;
switch (e.kind()) {
case meta_entry_kind::Lift: e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())}; break;
case meta_entry_kind::Inst: {
if (e.is_lift()) {
e_fmt = format{g_lift_fmt, colon(), format(e.s()), colon(), format(e.n())};
} else {
lean_assert(e.is_inst());
auto p_e = pp_child_with_paren(e.v(), depth);
r_weight += p_e.second;
e_fmt = format{g_inst_fmt, colon(), format(e.s()), space(), nest(m_indent, p_e.first)};
break;
}}
}
if (first) {
ctx_fmt = e_fmt;
first = false;

5
src/kernel/expr.h
View file

@ -292,9 +292,10 @@ public:
friend meta_entry mk_inst(unsigned s, expr const & v);
meta_entry_kind kind() const { return m_kind; }
bool is_inst() const { return kind() == meta_entry_kind::Inst; }
bool is_lift() const { return kind() == meta_entry_kind::Lift; }
unsigned s() const { return m_s; }
unsigned n() const { lean_assert(kind() == meta_entry_kind::Lift); return m_n; }
expr const & v() const { lean_assert(kind() == meta_entry_kind::Inst); return m_v; }
unsigned n() const { lean_assert(is_lift()); return m_n; }
expr const & v() const { lean_assert(is_inst()); return m_v; }
};
inline meta_entry mk_lift(unsigned s, unsigned n) { return meta_entry(s, n); }
inline meta_entry mk_inst(unsigned s, expr const & v) { return meta_entry(s, v); }

22
src/kernel/metavar.cpp
View file

@ -71,12 +71,12 @@ expr instantiate(expr const & s, meta_ctx const & ctx, metavar_env const & env)
if (ctx) {
expr r = instantiate(s, tail(ctx), env);
meta_entry const & e = head(ctx);
switch (e.kind()) {
case meta_entry_kind::Lift: return lift_free_vars(r, e.s(), e.n());
case meta_entry_kind::Inst: return ::lean::instantiate(r, e.s(), instantiate_metavars(e.v(), env));
if (e.is_lift()) {
return lift_free_vars(r, e.s(), e.n());
} else {
lean_assert(e.is_inst());
return ::lean::instantiate(r, e.s(), instantiate_metavars(e.v(), env));
}
lean_unreachable();
return s;
} else {
return s;
}
@ -129,13 +129,11 @@ expr add_lift(expr const & m, unsigned s, unsigned n) {
meta_ctx add_inst(meta_ctx const & ctx, unsigned s, expr const & v) {
if (ctx) {
meta_entry e = head(ctx);
if (e.kind() == meta_entry_kind::Lift) {
if (e.s() <= s && s < e.s() + e.n()) {
if (e.n() == 1)
return tail(ctx);
else
return add_lift(tail(ctx), e.s(), e.n() - 1);
}
if (e.is_lift() && e.s() <= s && s < e.s() + e.n()) {
if (e.n() == 1)
return tail(ctx);
else
return add_lift(tail(ctx), e.s(), e.n() - 1);
}
}
return cons(mk_inst(s, v), ctx);

9
src/library/printer.cpp
View file

@ -82,9 +82,12 @@ struct print_expr_fn {
bool first = true;
for (meta_entry const & e : metavar_ctx(a)) {
if (first) first = false; else out() << ", ";
switch (e.kind()) {
case meta_entry_kind::Lift: out() << "lift:" << e.s() << ":" << e.n(); break;
case meta_entry_kind::Inst: out() << "inst:" << e.s() << " "; print_child(e.v(), c); break;
if (e.is_lift()) {
out() << "lift:" << e.s() << ":" << e.n();
} else {
lean_assert(e.is_inst());
out() << "inst:" << e.s() << " ";
print_child(e.v(), c);
}
}
out() << "]";