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

refactor(frontends/lean): minimize the use of 'set_tag'

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-15 13:17:09 -07:00
parent 814778abb1
commit 8907dd5b91
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.h
View file

@ -70,7 +70,7 @@ class elaborator : public coercion_info_manager {
pair<expr, constraint_seq> whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); }
expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); }
expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); }
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a).set_tag(g); }
expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); }
void register_meta(expr const & meta);

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

@ -55,13 +55,13 @@ void local_context::set_ctx(list<expr> const & ctx) {
expr local_context::pi_abstract_context(expr e, tag g) const {
e = abstract_locals(e, m_ctx);
for (expr const & l : m_ctx_abstracted)
e = mk_pi(local_pp_name(l), mlocal_type(l), e, local_info(l)).set_tag(g);
e = mk_pi(local_pp_name(l), mlocal_type(l), e, local_info(l), g);
return e;
}
static expr apply_context_core(expr const & f, list<expr> const & ctx, tag g) {
if (ctx)
return mk_app(apply_context_core(f, tail(ctx), g), head(ctx)).set_tag(g);
return mk_app(apply_context_core(f, tail(ctx), g), head(ctx), g);
else
return f;
}
@ -72,9 +72,9 @@ expr local_context::apply_context(expr const & f, tag g) const {
expr local_context::mk_type_metavar(name_generator & ngen, tag g) {
name n = ngen.next();
expr s = mk_sort(mk_meta_univ(ngen.next())).set_tag(g);
expr s = mk_sort(mk_meta_univ(ngen.next()), g);
expr t = pi_abstract_context(s, g);
return ::lean::mk_metavar(n, t).set_tag(g);
return ::lean::mk_metavar(n, t, g);
}
expr local_context::mk_type_meta(name_generator & ngen, tag g) {
@ -85,7 +85,7 @@ expr local_context::mk_metavar(name_generator & ngen, optional<expr> const & typ
name n = ngen.next();
expr r_type = type ? *type : mk_type_meta(ngen, g);
expr t = pi_abstract_context(r_type, g);
return ::lean::mk_metavar(n, t).set_tag(g);
return ::lean::mk_metavar(n, t, g);
}
expr local_context::mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {

2
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -111,7 +111,7 @@ struct placeholder_elaborator : public choice_iterator {
pair<expr, constraint> ac = mk_placeholder_elaborator(m_C, some_expr(binding_domain(type)), g);
expr arg = ac.first;
cs.push_back(ac.second);
r = mk_app(r, arg).set_tag(g);
r = mk_app(r, arg, g);
type = instantiate(binding_body(type), arg);
}
r = Fun(locals, r);