From 5820a964a5b380d82923be7905cdacd6fa6bd6c3 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 27 Dec 2020 14:55:17 +0100 Subject: Remove MAKEPROD. MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is never encountered in the fast path, this optimization is not worth the extra complexity. --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_interp.c | 10 ---------- 2 files changed, 1 insertion(+), 11 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 51ac290ad0..4bc6848ba7 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,7 +43,7 @@ void init_arity () { arity[GETFIELD0]=arity[GETFIELD1]= arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= + arity[ACCUMULATE]=arity[STOP]= 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a1537cd963..a9ea6d9f46 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1270,16 +1270,6 @@ value coq_interprete Next; } - Instruct(MAKEPROD) { - print_instr("MAKEPROD"); - *--sp=accu; - Alloc_small(accu,2,0); - Field(accu, 0) = sp[0]; - Field(accu, 1) = sp[1]; - sp += 2; - Next; - } - Instruct(BRANCH) { /* unconditional branching */ print_instr("BRANCH"); -- cgit v1.2.3