diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 71 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 4 |
3 files changed, 75 insertions, 2 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 306643f758..814cdfe1d8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -75,6 +75,8 @@ 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; /* instruction with four operands */ arity[MAKESWITCHBLOCK]=4; diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 7588c1ce07..15cc451ea8 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -22,6 +22,7 @@ #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> +#include <caml/callback.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -111,7 +112,8 @@ if (sp - num_args < coq_stack_threshold) { \ /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } - +#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; } +#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; } /* Register optimization. Some compilers underestimate the use of the local variables representing @@ -1185,7 +1187,7 @@ value coq_interprete if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); - if (Field(*sp, 2) == Val_true) { + if (Is_tailrec_switch(*sp)) { for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2]; }else{ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5]; @@ -1771,6 +1773,71 @@ value coq_interprete Next; } + + Instruct(ISINT_CAML_CALL2) { + value arg; + print_instr("ISINT_CAML_CALL2"); + if (Is_uint63(accu)) { + pc++; + print_int(*pc); + arg = sp[0]; + Setup_for_caml_call; + accu = caml_callback2(Field(coq_global_data, *pc), accu, arg); + Restore_after_caml_call; + sp += 1; + pc++; + } else pc += *pc; + 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(ISARRAY_INT_CAML_CALL2) { + 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; + } + + Instruct(ISARRAY_INT_CAML_CALL3) { + value arg1; + value arg2; + print_instr("ISARRAY_INT_CAML_CALL3"); + if (Is_coq_array(accu) && Is_uint63(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); + Restore_after_caml_call; + sp += 2; + pc++; + } else pc += *pc; + Next; + } + /* Debugging and machine control */ Instruct(STOP){ diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index b027673ac7..a19f9b56c1 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,10 @@ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #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 |