max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library): do not use mk_fresh_name

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-07 13:51:16 -08:00
parent 11e87545be
commit d54d759d56
3 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/noncomputable.cpp
View file

@ -166,7 +166,7 @@ struct get_noncomputable_reason_fn {
expr e = _e;
while (is_lambda(e) || is_pi(e)) {
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
expr l = mk_local(m_tc.next_name(), binding_name(e), d, binding_info(e));
ls.push_back(l);
e = binding_body(e);
}

8
src/library/quote.cpp
View file

@ -120,13 +120,16 @@ expr const & get_antiquote_expr(expr const & e) {
return get_annotation_arg(e);
}
static name * g_quote_fresh = nullptr;
expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
name x("_x");
name_generator ngen(*g_quote_fresh);
buffer<expr> locals;
buffer<expr> aqs;
expr s = replace(e, [&](expr const & t, unsigned) {
if (is_antiquote(t)) {
expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1),
expr local = mk_local(ngen.next(), x.append_after(locals.size() + 1),
mk_expr_placeholder(), binder_info());
locals.push_back(local);
aqs.push_back(get_antiquote_expr(t));
@ -147,6 +150,8 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) {
}
void initialize_quote() {
g_quote_fresh = new name("_quote_fresh");
register_name_generator_prefix(*g_quote_fresh);
g_expr_quote_macro = new name("expr_quote_macro");
g_expr_quote_opcode = new std::string("Quote");
g_expr = new expr(mk_app(Const(get_expr_name()), mk_bool_tt()));
@ -168,6 +173,7 @@ void initialize_quote() {
}
void finalize_quote() {
delete g_quote_fresh;
delete g_expr_quote_pre;
delete g_expr_quote_macro;
delete g_expr_quote_opcode;

6
src/library/util.cpp
View file

@ -232,7 +232,7 @@ bool is_reflexive_datatype(abstract_type_context & tc, name const & n) {
if (is_pi(arg) && find(arg, [&](expr const & e, unsigned) { return is_constant(e) && const_name(e) == n; })) {
return true;
}
expr local = mk_local(mk_fresh_name(), binding_domain(type));
expr local = mk_local(tc.next_name(), binding_domain(type));
type = instantiate(binding_body(type), local);
}
}
@ -429,9 +429,9 @@ expr to_telescope(type_checker & ctx, expr type, buffer<expr> & telescope, optio
type = new_type;
expr local;
if (binfo)
local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), *binfo);
local = mk_local(ctx.next_name(), binding_name(type), binding_domain(type), *binfo);
else
local = mk_local(mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type));
local = mk_local(ctx.next_name(), binding_name(type), binding_domain(type), binding_info(type));
telescope.push_back(local);
type = instantiate(binding_body(type), local);
new_type = ctx.whnf(type);