diff options
| author | Pierre Roux | 2019-05-02 08:41:45 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-05-03 16:12:07 +0200 |
| commit | 09cdf7b1fad8761cdf7048bf38a468c8558eb0d5 (patch) | |
| tree | 723b5e14dd8142529f0d18cd8261d35cda93550f /kernel | |
| parent | dd60b4a292b870e08c23ddcb363630cbb2ed1227 (diff) | |
Remove now useless commented code
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 15 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_emul.h | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_native.h | 1 |
3 files changed, 4 insertions, 14 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e38d458b36..1b348ae777 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -29,13 +29,6 @@ #include "coq_uint63_emul.h" #endif -/* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)(val)) >> 1) -#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) -#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) -/* /spiwack */ - /* Registers for the abstract machine: @@ -1298,12 +1291,6 @@ value coq_interprete /*returns the multiplication on a pair */ print_instr("MULCINT63"); CheckInt2(); - /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */ - /* TODO: implement - p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1)); - AllocPair(); */ - /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/ - /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/ Uint63_mulc(accu, *sp, sp); *--sp = accu; AllocPair(); @@ -1587,7 +1574,7 @@ value coq_push_vstack(value stk, value max_stack_size) { print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); sp = coq_sp; - CHECK_STACK(uint32_of_value(max_stack_size)); + CHECK_STACK(uint_of_value(max_stack_size)); return Val_unit; } diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index d982f67566..528cc6fc1f 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -6,6 +6,8 @@ #define Is_uint63(v) (Tag_val(v) == Custom_tag) +#define uint_of_value(val) (((uint32_t)(val)) >> 1) + # define DECLARE_NULLOP(name) \ value uint63_##name() { \ static value* cb = 0; \ diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 8dee0d69d3..1fdafc9d8f 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -1,5 +1,6 @@ #define Is_uint63(v) (Is_long(v)) +#define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) /* 2^63 * y + x as a value */ |