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

chore: ignore closures at maxsharing

Browse source 
Closures may capture huge objects that user may be unaware.
For example, any closure created by the interpreter contains
a reference to the `Environment`.

@dselsam @kha I don't see many applications for maximizing sharing in
values captured by closures. If we want this feature, we should at
least wrap the `Environment` and `Decl` using external objects
at `mk_stub_closure` at `ir_interpreter.cpp`.
This commit is contained in:
Leonardo de Moura 2020-02-25 17:13:05 -08:00
parent 1653e75b6b
commit 131f2d202e
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/runtime/maxsharing.cpp
View file

@ -171,7 +171,7 @@ class max_sharing_fn {
// We do not maximize sharing for the following kinds of objects
case LeanMPZ: case LeanThunk:
case LeanTask: case LeanRef:
case LeanExternal:
case LeanExternal: case LeanClosure:
m_children.push_back(a);
return true;
default:
@ -216,12 +216,6 @@ class max_sharing_fn {
}
}
void visit_closure(b_obj_arg a) {
// TODO(Leo)
lean_inc(a);
save(a, a);
}
void visit_array(b_obj_arg a) {
clear_children();
bool missing_children = false;
@ -300,7 +294,7 @@ public:
b_obj_arg curr = m_todo.back();
// std::cout << "visiting " << curr << " " << static_cast<unsigned>(lean_ptr_tag(curr)) << "\n";
switch (lean_ptr_tag(curr)) {
case LeanClosure: visit_closure(curr); break;
case LeanClosure: lean_unreachable();
case LeanArray: visit_array(curr); break;
case LeanScalarArray: visit_sarray(curr); break;
case LeanString: visit_string(curr); break;