diff options
| author | Guillaume Melquiond | 2020-12-27 14:55:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-10 10:24:10 +0100 |
| commit | 5820a964a5b380d82923be7905cdacd6fa6bd6c3 (patch) | |
| tree | 13854701b6ad63b08c49ebf29a9078f917829cdd /kernel/byterun | |
| parent | d1215d47c3cda09f4df2f07ce9362b3e6fc5b164 (diff) | |
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.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 10 |
2 files changed, 1 insertions, 11 deletions
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"); |
