diff options
| author | Guillaume Melquiond | 2020-12-27 10:36:31 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-10 10:24:10 +0100 |
| commit | d009572893913b889320f2fa3435543ee4c63f82 (patch) | |
| tree | f15d2920bb65b888f6c21754b3cd9ee2c9723bcf /kernel | |
| parent | 723440611965ccdecfd56e61c8f1f8618a08841d (diff) | |
Remove PUSHACC0, as it is strictly equivalent to PUSH.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 3 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 4 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 1 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 4 |
4 files changed, 5 insertions, 7 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1ba6a8c8fe..f562c15aa8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -31,7 +31,8 @@ int arity[STOP+1]; void init_arity () { /* instruction with zero operand */ arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= - arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]= + arity[ACC6]=arity[ACC7]= + arity[PUSH]=arity[PUSHACC1]= arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= arity[PUSHACC6]=arity[PUSHACC7]= arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 6255250218..a124a51c7d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -338,10 +338,6 @@ value coq_interprete print_instr("PUSH"); *--sp = accu; Next; } - Instruct(PUSHACC0) { - print_instr("PUSHACC0"); - *--sp = accu; Next; - } Instruct(PUSHACC1){ print_instr("PUSHACC1"); *--sp = accu; accu = sp[1]; Next; diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index dc2cd349ce..e2932ec330 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -28,7 +28,6 @@ let opcodes = "ACC7"; "ACC"; "PUSH"; - "PUSHACC0"; "PUSHACC1"; "PUSHACC2"; "PUSHACC3"; diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index c1d8fcb855..e70285d9ab 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -375,7 +375,9 @@ let rec emit env insns remaining = match insns with | (first::rest) -> emit env first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> - if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n); + if n = 0 then out env opPUSH + else if n < 8 then out env (opPUSHACC1 + n - 1) + else (out env opPUSHACC; out_int env n); emit env c remaining | Kpush :: Kenvacc n :: c -> if n >= 0 && n <= 3 |