fix: maxsharing hash and eq, and expand skeleton
This commit is contained in:
Leonardo de Moura
parent
fdc76934f5
commit
dae1a3172e
1 changed files with 124 additions and 28 deletions
|
|
@ -15,13 +15,23 @@ extern "C" uint8 lean_maxsharing_eq(b_obj_arg o1, b_obj_arg o2) {
|
|||
size_t sz1 = lean_object_byte_size(o1);
|
||||
size_t sz2 = lean_object_byte_size(o2);
|
||||
if (sz1 != sz2) return false;
|
||||
return memcmp(o1, o2, sz1) == 0;
|
||||
// compare relevant parts of the header
|
||||
if (lean_ptr_tag(o1) != lean_ptr_tag(o2)) return false;
|
||||
if (lean_ptr_other(o1) != lean_ptr_other(o2)) return false;
|
||||
size_t header_sz = sizeof(lean_object);
|
||||
lean_assert(sz1 >= header_sz);
|
||||
// compare objects' bodies
|
||||
return memcmp(reinterpret_cast<char*>(o1) + header_sz, reinterpret_cast<char*>(o2) + header_sz, sz1 - header_sz) == 0;
|
||||
}
|
||||
|
||||
extern "C" usize lean_maxsharing_hash(b_obj_arg o) {
|
||||
lean_assert(!lean_is_scalar(o));
|
||||
size_t sz = lean_object_byte_size(o);
|
||||
return hash_str(sz, reinterpret_cast<char const *>(o), 17);
|
||||
size_t header_sz = sizeof(lean_object);
|
||||
// hash relevant parts of the header
|
||||
unsigned init = hash(lean_ptr_tag(o), lean_ptr_other(o));
|
||||
// hash body
|
||||
return hash_str(sz - header_sz, reinterpret_cast<char const *>(o) + header_sz, init);
|
||||
}
|
||||
|
||||
// unsafe def mkObjectMap : Unit → ObjectMap
|
||||
|
|
@ -56,6 +66,7 @@ static obj_res mk_pair(obj_arg a, obj_arg b) {
|
|||
object * r = alloc_cnstr(0, 2, 0);
|
||||
lean_ctor_set(r, 0, a);
|
||||
lean_ctor_set(r, 1, b);
|
||||
// std::cout << "mk_pair " << a << " " << b << std::endl;
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
@ -69,24 +80,25 @@ extern "C" obj_res lean_maxsharing_mk_pstate(obj_arg) {
|
|||
|
||||
class max_sharing_state_core {
|
||||
protected:
|
||||
object * m;
|
||||
object * s;
|
||||
object * m_map;
|
||||
object * m_set;
|
||||
public:
|
||||
max_sharing_state_core(obj_arg s) {
|
||||
m = lean_ctor_get(s, 0); lean_inc_ref(m);
|
||||
s = lean_ctor_get(s, 1); lean_inc_ref(s);
|
||||
lean_dec_ref(s);
|
||||
}
|
||||
|
||||
~max_sharing_state_core() {
|
||||
lean_dec(m);
|
||||
m_map = lean_ctor_get(s, 0); lean_inc(m_map);
|
||||
m_set = lean_ctor_get(s, 1); lean_inc(m_set);
|
||||
// std::cout << "max_sharing_state_core " << m_map << " " << m_set << std::endl;
|
||||
lean_dec(s);
|
||||
}
|
||||
|
||||
~max_sharing_state_core() {
|
||||
lean_dec(m_map);
|
||||
lean_dec(m_set);
|
||||
}
|
||||
|
||||
obj_res pack(obj_arg a) {
|
||||
obj_res r = mk_pair(a, mk_pair(m, s));
|
||||
m = lean_box(0);
|
||||
s = lean_box(0);
|
||||
obj_res r = mk_pair(a, mk_pair(m_map, m_set));
|
||||
m_map = lean_box(0);
|
||||
m_set = lean_box(0);
|
||||
return r;
|
||||
}
|
||||
};
|
||||
|
|
@ -96,21 +108,21 @@ public:
|
|||
max_sharing_state(obj_arg s):max_sharing_state_core(s) {}
|
||||
|
||||
obj_res map_find(b_obj_arg k) {
|
||||
lean_inc_ref(m); lean_inc_ref(k);
|
||||
return lean_object_map_find(m, k);
|
||||
lean_inc(m_map); lean_inc(k);
|
||||
return lean_object_map_find(m_map, k);
|
||||
}
|
||||
|
||||
void map_insert(obj_arg k, obj_arg v) {
|
||||
m = lean_object_map_insert(m, k, v);
|
||||
m_map = lean_object_map_insert(m_map, k, v);
|
||||
}
|
||||
|
||||
obj_res set_find(b_obj_arg o) {
|
||||
lean_inc_ref(s); lean_inc_ref(o);
|
||||
return lean_object_set_find(s, o);
|
||||
lean_inc(m_set); lean_inc(o);
|
||||
return lean_object_set_find(m_set, o);
|
||||
}
|
||||
|
||||
void set_insert(obj_arg o) {
|
||||
s = lean_object_set_insert(s, o);
|
||||
m_set = lean_object_set_insert(m_set, o);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -119,21 +131,21 @@ public:
|
|||
max_sharing_pstate(obj_arg s):max_sharing_state_core(s) {}
|
||||
|
||||
obj_res map_find(b_obj_arg k) {
|
||||
lean_inc_ref(m); lean_inc_ref(k);
|
||||
return lean_object_pmap_find(m, k);
|
||||
lean_inc(m_map); lean_inc(k);
|
||||
return lean_object_pmap_find(m_map, k);
|
||||
}
|
||||
|
||||
void map_insert(obj_arg k, obj_arg v) {
|
||||
m = lean_object_pmap_insert(m, k, v);
|
||||
m_map = lean_object_pmap_insert(m_map, k, v);
|
||||
}
|
||||
|
||||
obj_res set_find(b_obj_arg o) {
|
||||
lean_inc_ref(s); lean_inc_ref(o);
|
||||
return lean_object_pset_find(s, o);
|
||||
lean_inc(m_set); lean_inc(o);
|
||||
return lean_object_pset_find(m_set, o);
|
||||
}
|
||||
|
||||
void set_insert(obj_arg o) {
|
||||
s = lean_object_pset_insert(s, o);
|
||||
m_set = lean_object_pset_insert(m_set, o);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -141,13 +153,97 @@ template<typename state>
|
|||
class max_sharing_fn {
|
||||
state m_state;
|
||||
|
||||
obj_res visit(obj_arg a) {
|
||||
obj_res visit_closure(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_array(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_sarray(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_string(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_mpz(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_thunk(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit_ctor(b_obj_arg a) {
|
||||
// TODO
|
||||
lean_inc(a);
|
||||
return a;
|
||||
}
|
||||
|
||||
obj_res visit(obj_arg a) {
|
||||
if (lean_is_scalar(a)) {
|
||||
return a;
|
||||
}
|
||||
obj_res o = m_state.map_find(a);
|
||||
if (o != lean_box(0)) {
|
||||
obj_res r = lean_ctor_get(o, 0);
|
||||
lean_inc(r);
|
||||
lean_dec(o);
|
||||
std::cout << "found cached:" << r << "\n";
|
||||
return r;
|
||||
}
|
||||
obj_res r;
|
||||
switch (lean_ptr_tag(a)) {
|
||||
case LeanClosure: r = visit_closure(a); break;
|
||||
case LeanArray: r = visit_array(a); break;
|
||||
case LeanScalarArray: r = visit_sarray(a); break;
|
||||
case LeanString: r = visit_string(a); break;
|
||||
case LeanMPZ: r = visit_mpz(a); break;
|
||||
case LeanThunk: r = visit_thunk(a); break;
|
||||
case LeanTask: return a;
|
||||
case LeanRef: return a;
|
||||
case LeanExternal: return a;
|
||||
case LeanReserved: lean_unreachable();
|
||||
default: r = visit_ctor(a); break;
|
||||
}
|
||||
|
||||
obj_res opt_new_r = m_state.set_find(r);
|
||||
if (opt_new_r != lean_box(0)) {
|
||||
lean_dec(r); // we already have a maximally shared term equivalent to `r`
|
||||
r = lean_ctor_get(opt_new_r, 0);
|
||||
lean_inc_n(r, 2);
|
||||
lean_dec(opt_new_r);
|
||||
m_state.map_insert(a, r);
|
||||
std::cout << "found shared:" << r << "\n";
|
||||
return r;
|
||||
}
|
||||
|
||||
lean_inc_n(r, 4);
|
||||
m_state.set_insert(r); // r is a new maximally shared term
|
||||
m_state.map_insert(a, r); // `r` is the maximally shared representation for `a`
|
||||
m_state.map_insert(r, r); // `r` is the maximally shared representation of itself
|
||||
std::cout << "new shared:" << r << " " << lean_maxsharing_hash(r) << "\n";
|
||||
return r;
|
||||
}
|
||||
|
||||
public:
|
||||
max_sharing_fn(obj_arg s):m_state(s) {}
|
||||
max_sharing_fn(obj_arg s):m_state(s) {
|
||||
}
|
||||
|
||||
obj_res operator()(obj_arg a) {
|
||||
return m_state.pack(visit(a));
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue