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

chore(runtime/object): remove fixpoint* primitives

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-27 13:17:25 -07:00
parent 414c03363c
commit d536ee347d
2 changed files with 0 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

101
src/runtime/object.cpp
View file

@ -1756,107 +1756,6 @@ object * array_push(obj_arg a, obj_arg v) {
return r;
}
// =======================================
// fixpoint
static inline object * ptr_to_weak_ptr(object * p) {
return reinterpret_cast<object*>(reinterpret_cast<uintptr_t>(p) | 1);
}
static inline object * weak_ptr_to_ptr(object * w) {
return reinterpret_cast<object*>((reinterpret_cast<uintptr_t>(w) >> 1) << 1);
}
obj_res fixpoint_aux(obj_arg rec, obj_arg weak_k, obj_arg a) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_2(rec, k, a);
}
obj_res fixpoint(obj_arg rec, obj_arg a) {
object * k = alloc_closure(fixpoint_aux, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_2(rec, k, a);
return r;
}
obj_res fixpoint_aux2(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_3(rec, k, a1, a2);
}
obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) {
object * k = alloc_closure(fixpoint_aux2, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_3(rec, k, a1, a2);
return r;
}
obj_res fixpoint_aux3(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_4(rec, k, a1, a2, a3);
}
obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = alloc_closure(fixpoint_aux3, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_4(rec, k, a1, a2, a3);
return r;
}
obj_res fixpoint_aux4(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_5(rec, k, a1, a2, a3, a4);
}
obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = alloc_closure(fixpoint_aux4, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_5(rec, k, a1, a2, a3, a4);
return r;
}
obj_res fixpoint_aux5(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_6(rec, k, a1, a2, a3, a4, a5);
}
obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = alloc_closure(fixpoint_aux5, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_6(rec, k, a1, a2, a3, a4, a5);
return r;
}
obj_res fixpoint_aux6(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_7(rec, k, a1, a2, a3, a4, a5, a6);
}
obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = alloc_closure(fixpoint_aux6, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_7(rec, k, a1, a2, a3, a4, a5, a6);
return r;
}
// =======================================
// Debugging helper functions

10
src/runtime/object.h
View file

@ -651,16 +651,6 @@ inline obj_res alloc_closure(object*(*fun)(object *, object *, object *, object
return alloc_closure(reinterpret_cast<void*>(fun), 8, num_fixed);
}
// =======================================
// Fixpoint
obj_res fixpoint(obj_arg rec, obj_arg a);
obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2);
obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3);
obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4);
obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5);
obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6);
// =======================================
// Array of objects