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

chore(library/compiler): cleanup cce

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-21 10:25:35 -07:00
parent ff2e28e557
commit 097aa7ef14
3 changed files with 20 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/compiler/cse.cpp
View file

@ -204,13 +204,13 @@ public:
unsigned max_idx = get_max_fvar_idx(target);
if (max_idx >= first_var_idx) {
expr target_type = cheap_beta_reduce(type_checker(m_st, m_lctx).infer(target));
expr unit = mk_unit(mk_level_one());
expr unit_mk = mk_unit_mk(mk_level_one());
expr unit = mk_unit();
expr unit_mk = mk_unit_mk();
expr new_val = ::lean::mk_lambda("u", unit, target);
expr new_type = ::lean::mk_arrow(unit, target_type);
expr new_fvar = m_lctx.mk_local_decl(ngen(), mk_join_point_name(m_j.append_after(m_next_idx)), new_type, new_val);
new_fvar_names.insert(fvar_name(new_fvar));
expr jmp = ::lean::mk_let("_j", target_type, mk_app(new_fvar, unit_mk), mk_bvar(0));
expr jmp = mk_app(new_fvar, unit_mk);
if (is_let) {
/* We must insert new_fvar after fvar with idx == max_idx */
m_next_idx++;

15
src/library/util.cpp
View file

@ -431,6 +431,17 @@ expr mk_unit_mk(level const & l) {
return mk_constant(get_punit_star_name(), {l});
}
static expr * g_unit = nullptr;
static expr * g_unit_mk = nullptr;
expr mk_unit() {
return *g_unit;
}
expr mk_unit_mk() {
return *g_unit_mk;
}
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) {
level l1 = get_level(ctx, A);
level l2 = get_level(ctx, B);
@ -1020,6 +1031,8 @@ static std::string * g_version_string = nullptr;
std::string const & get_version_string() { return *g_version_string; }
void initialize_library_util() {
g_unit = new expr(mk_constant(get_unit_name()));
g_unit_mk = new expr(mk_constant(get_unit_star_name()));
g_true = new expr(mk_constant(get_true_name()));
g_true_intro = new expr(mk_constant(get_true_intro_name()));
g_and = new expr(mk_constant(get_and_name()));
@ -1066,5 +1079,7 @@ void finalize_library_util() {
delete g_and_elim_left;
delete g_and_elim_right;
delete g_tactic_unit;
delete g_unit_mk;
delete g_unit;
}
}

2
src/library/util.h
View file

@ -161,6 +161,8 @@ expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
expr mk_unit(level const & l);
expr mk_unit_mk(level const & l);
expr mk_unit();
expr mk_unit_mk();
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);