diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 7 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 69 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 3 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 8 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 8 |
5 files changed, 48 insertions, 47 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 1ffb323748..1ba6a8c8fe 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -73,9 +73,10 @@ void init_arity () { arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]= - arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]= - arity[PROJ]=2; + arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= + arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]= + arity[PROJ]= + 2; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; /* instruction with arbitrary operands */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 72f6e12b0f..672ee60c6d 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1754,11 +1754,11 @@ value coq_interprete Next; } - - Instruct(ISINT_CAML_CALL2) { + Instruct(CHECKCAMLCALL2_1) { + // arity-2 callback, the last argument can be an accumulator value arg; - print_instr("ISINT_CAML_CALL2"); - if (Is_uint63(accu)) { + print_instr("CHECKCAMLCALL2_1"); + if (!Is_accu(accu)) { pc++; print_int(*pc); arg = sp[0]; @@ -1771,47 +1771,50 @@ value coq_interprete Next; } - Instruct(ISARRAY_CAML_CALL1) { - print_instr("ISARRAY_CAML_CALL1"); - if (Is_coq_array(accu)) { - pc++; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback(Field(coq_global_data, *pc),accu); - Restore_after_caml_call; - pc++; - } - else pc += *pc; - Next; + Instruct(CHECKCAMLCALL1) { + // arity-1 callback, no argument can be an accumulator + print_instr("CHECKCAMLCALL1"); + if (!Is_accu(accu)) { + pc++; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback(Field(coq_global_data, *pc), accu); + Restore_after_caml_call; + pc++; + } + else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL2) { + Instruct(CHECKCAMLCALL2) { + // arity-2 callback, no argument can be an accumulator value arg; - print_instr("ISARRAY_INT_CAML_CALL2"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { - pc++; - arg = sp[0]; - Setup_for_caml_call; - print_int(*pc); - accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); - Restore_after_caml_call; - sp += 1; - pc++; - } else pc += *pc; - Next; + print_instr("CHECKCAMLCALL2"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { + pc++; + arg = sp[0]; + Setup_for_caml_call; + print_int(*pc); + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + Next; } - Instruct(ISARRAY_INT_CAML_CALL3) { + Instruct(CHECKCAMLCALL3_1) { + // arity-3 callback, the last argument can be an accumulator value arg1; value arg2; - print_instr("ISARRAY_INT_CAML_CALL3"); - if (Is_coq_array(accu) && Is_uint63(sp[0])) { + print_instr("CHECKCAMLCALL3_1"); + if (!Is_accu(accu) && !Is_accu(sp[0])) { pc++; arg1 = sp[0]; arg2 = sp[1]; Setup_for_caml_call; print_int(*pc); - accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2); + accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2); Restore_after_caml_call; sp += 2; pc++; diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index f07018711b..0cdef34050 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -30,9 +30,6 @@ #define Is_double(v) (Tag_val(v) == Double_tag) #define Is_tailrec_switch(v) (Field(v,1) == Val_true) -/* coq array */ -#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1)) - /* coq values for primitive operations */ #define coq_tag_C1 2 #define coq_tag_C0 1 diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index c8c8f61d59..63abb50cc2 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -147,10 +147,10 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; - "ISINT_CAML_CALL2"; - "ISARRAY_CAML_CALL1"; - "ISARRAY_INT_CAML_CALL2"; - "ISARRAY_INT_CAML_CALL3"; + "CHECKCAMLCALL2_1"; + "CHECKCAMLCALL1"; + "CHECKCAMLCALL2"; + "CHECKCAMLCALL3_1"; "STOP" |] 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 |