From b5aed34bb8bbdda27646720db29a8d47c79653b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Mar 2018 15:41:50 +0100
Subject: Moving the VM global data to a ML reference.

---
 kernel/byterun/coq_interp.c | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'kernel/byterun/coq_interp.c')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index af89712d5e..ced2a175d0 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,8 +163,11 @@ extern void caml_process_pending_signals(void);
 /* The interpreter itself */
 
 value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args)
+(code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args)
 {
+  /* coq_accu is not allocated on the OCaml heap */
+  CAMLparam1(coq_global_data);
+
   /*Declaration des variables */
 #ifdef PC_REG
   register code_t pc PC_REG;
@@ -196,7 +199,7 @@ value coq_interprete
     coq_instr_table = (char **) coq_jumptable;
     coq_instr_base = coq_Jumptbl_base;
 #endif
-    return Val_unit;
+    CAMLreturn(Val_unit);
   }
 #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
   coq_jumptbl_base = coq_Jumptbl_base;
@@ -1460,7 +1463,7 @@ value coq_interprete
       Instruct(STOP){
 	print_instr("STOP");
 	coq_sp = sp;
-	return accu;
+        CAMLreturn(accu);
       }
       
   
@@ -1512,12 +1515,12 @@ value coq_push_vstack(value stk, value max_stack_size) {
   return Val_unit;
 }
 
-value  coq_interprete_ml(value tcode, value a, value e, value ea) {
+value  coq_interprete_ml(value tcode, value a, value g, value e, value ea) {
   print_instr("coq_interprete");
-  return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+  return coq_interprete((code_t)tcode, a, g, e, Long_val(ea));
   print_instr("end coq_interprete");
 }
 
-value coq_eval_tcode (value tcode, value e) {
-  return coq_interprete_ml(tcode, Val_unit, e, 0);
+value coq_eval_tcode (value tcode, value g, value e) {
+  return coq_interprete_ml(tcode, Val_unit, g, e, 0);
 }
-- 
cgit v1.2.3


From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 3 Mar 2018 19:43:02 +0100
Subject: Moving the VM global atom table to a ML reference.

---
 kernel/byterun/coq_interp.c | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'kernel/byterun/coq_interp.c')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ced2a175d0..cfeb0a9ee1 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,10 +163,10 @@ extern void caml_process_pending_signals(void);
 /* The interpreter itself */
 
 value coq_interprete
-(code_t coq_pc, value coq_accu, value coq_global_data, value coq_env, long coq_extra_args)
+(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args)
 {
   /* coq_accu is not allocated on the OCaml heap */
-  CAMLparam1(coq_global_data);
+  CAMLparam2(coq_atom_tbl, coq_global_data);
 
   /*Declaration des variables */
 #ifdef PC_REG
@@ -1515,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) {
   return Val_unit;
 }
 
-value  coq_interprete_ml(value tcode, value a, value g, value e, value ea) {
+value  coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
   print_instr("coq_interprete");
-  return coq_interprete((code_t)tcode, a, g, e, Long_val(ea));
+  return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea));
   print_instr("end coq_interprete");
 }
 
-value coq_eval_tcode (value tcode, value g, value e) {
-  return coq_interprete_ml(tcode, Val_unit, g, e, 0);
+value coq_interprete_byte(value* argv, int argn){
+  return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]);
+}
+
+value coq_eval_tcode (value tcode, value t, value g, value e) {
+  return coq_interprete_ml(tcode, Val_unit, t, g, e, 0);
 }
-- 
cgit v1.2.3