diff options
| author | Guillaume Melquiond | 2020-08-31 14:50:59 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:14:34 +0100 |
| commit | b6fadbf6f08860609961f6dbad8a036346925265 (patch) | |
| tree | d54fcf732cea3b60ec76b2d0b2c3d938816eb656 /kernel/vmemitcodes.ml | |
| parent | 20c511d4a80c26a54004a9b44b3108669baa86c3 (diff) | |
Make callback opcodes more generic.
This does not make the code any slower, since
Is_coq_array(accu) && Is_uint63(sp[0])
and
!Is_accu(accu) && !Is_accu(sp[0])
take the exact same number of tests to pass in the concrete case.
In the accumulator case, it takes one more test to fail, but we do not
care about the performances then.
Diffstat (limited to 'kernel/vmemitcodes.ml')
| -rw-r--r-- | kernel/vmemitcodes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index 0bd3375169..592bdf775f 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -251,11 +251,11 @@ let check_prim_op = function | Float64ldshiftexp -> opCHECKLDSHIFTEXP | Float64next_up -> opCHECKNEXTUPFLOAT | Float64next_down -> opCHECKNEXTDOWNFLOAT - | Arraymake -> opISINT_CAML_CALL2 - | Arrayget -> opISARRAY_INT_CAML_CALL2 - | Arrayset -> opISARRAY_INT_CAML_CALL3 + | Arraymake -> opCHECKCAMLCALL2_1 + | Arrayget -> opCHECKCAMLCALL2 + | Arrayset -> opCHECKCAMLCALL3_1 | Arraydefault | Arraycopy | Arraylength -> - opISARRAY_CAML_CALL1 + opCHECKCAMLCALL1 let emit_instr env = function | Klabel lbl -> define_label env lbl |