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

feat(library/compiler/llnf): unique names for lambda arguments

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-25 12:51:32 -08:00
parent 4b66b442c9
commit 2016e1bce5
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/llnf.cpp
View file

@ -446,7 +446,7 @@ class to_llnf_fn {
buffer<expr> binding_fvars;
while (is_lambda(e)) {
lean_assert(!has_loose_bvars(binding_domain(e)));
expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
binding_fvars.push_back(new_fvar);
e = binding_body(e);
}
@ -924,7 +924,7 @@ public:
}
};
static expr get_constant_ll_type(environment const & env, name const & c) {
expr get_constant_ll_type(environment const & env, name const & c) {
if (optional<expr> type = get_builtin_constant_ll_type(c)) {
return *type;
} else {
@ -1111,7 +1111,7 @@ class explicit_boxing_fn {
buffer<expr> binding_fvars;
while (is_lambda(e)) {
lean_assert(!has_loose_bvars(binding_domain(e)));
expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
binding_fvars.push_back(new_fvar);
e = binding_body(e);
}
@ -1842,7 +1842,7 @@ class explicit_rc_fn {
unsigned i = 0;
while (is_lambda(e)) {
lean_assert(!has_loose_bvars(binding_domain(e)));
expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(e), binding_domain(e), binding_info(e));
expr new_fvar = m_lctx.mk_local_decl(ngen(), next_name(), binding_domain(e), binding_info(e));
lean_assert(i < borrowed.size());
if (borrowed[i])
m_borrowed.insert(fvar_name(new_fvar));

2
src/library/compiler/llnf.h
View file

@ -41,6 +41,8 @@ inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_s
inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
expr get_constant_ll_type(environment const & env, name const & c);
void initialize_llnf();
void finalize_llnf();
}