diff options
Diffstat (limited to 'kernel/byterun/coq_interp.c')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 69 |
1 files changed, 68 insertions, 1 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 7588c1ce07..9921208e04 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 @@ -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){ |