diff options
| author | Guillaume Melquiond | 2020-12-27 10:42:33 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-10 10:24:10 +0100 |
| commit | 944757e10651fda0d63d9291a6bcb1b6fdbaa256 (patch) | |
| tree | 676b61021885d93290e74a1c9954e0dd80a3d9c2 /kernel/byterun | |
| parent | d009572893913b889320f2fa3435543ee4c63f82 (diff) | |
Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 1 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 28 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_emul.h | 4 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_native.h | 2 |
4 files changed, 0 insertions, 35 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index f562c15aa8..ab6e393178 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -61,7 +61,6 @@ void init_arity () { arity[CHECKDIV21INT63]= arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]= arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= - arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]= arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a124a51c7d..62683b87a6 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1497,34 +1497,6 @@ value coq_interprete Next; } - Instruct(CHECKLSLINT63CONST1) { - print_instr("CHECKLSLINT63CONST1"); - if (Is_uint63(accu)) { - pc++; - Uint63_lsl1(accu); - Next; - } else { - *--sp = uint63_one(); - *--sp = accu; - accu = Field(coq_global_data, *pc++); - goto apply2; - } - } - - Instruct(CHECKLSRINT63CONST1) { - print_instr("CHECKLSRINT63CONST1"); - if (Is_uint63(accu)) { - pc++; - Uint63_lsr1(accu); - Next; - } else { - *--sp = uint63_one(); - *--sp = accu; - accu = Field(coq_global_data, *pc++); - goto apply2; - } - } - Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 13568957c2..dd9b9e55be 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -119,12 +119,8 @@ DECLARE_BINOP(lor) #define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) -DECLARE_UNOP(lsl1) -#define Uint63_lsl1(x) CALL_UNOP(lsl1, x) DECLARE_BINOP(lsr) #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) -DECLARE_UNOP(lsr1) -#define Uint63_lsr1(x) CALL_UNOP(lsr1, x) DECLARE_BINOP(lt) #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) DECLARE_BINOP(lxor) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 27696e8856..731ae8f46e 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -55,8 +55,6 @@ else \ accu = uint63_zero; \ }while(0) -#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1)) -#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1)) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ /* (modulo 2^63) for p <= 63 */ |