Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

10 files changed, 1724 insertions, 0 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
new file mode 100644
index 00000000..4616580d
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.c
@@ -0,0 +1,166 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h> 
+#include "config.h"
+#include "misc.h"
+#include "mlvalues.h"
+#include "fail.h"
+#include "memory.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+
+#ifdef THREADED_CODE
+char ** coq_instr_table;
+char * coq_instr_base;
+int arity[STOP+1];
+
+void init_arity () {
+  /* instruction with zero operand */
+  arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
+    arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
+    arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]=
+    arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]=
+    arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]=
+    arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+    arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
+    arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+    arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
+    arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
+    arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0;
+  /* instruction with one operand */
+  arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
+    arity[PUSH_RETADDR]=
+    arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]=
+    arity[GRAB]=arity[COGRAB]=
+    arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]=
+    arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
+    arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]=
+    arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]=
+    arity[ACCUMULATECOND]= 1;
+  /* instruction with two operands */
+  arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2;
+  /* instruction with four operands */ 
+  arity[MAKESWITCHBLOCK]=4;
+  /* instruction with arbitrary operands */
+  arity[CLOSUREREC]=arity[SWITCH]=0;
+}
+
+#endif /*  THREADED_CODE */
+
+
+void * coq_stat_alloc (asize_t sz)
+{
+  void * result = malloc (sz);
+  if (result == NULL) raise_out_of_memory ();
+  return result;
+}
+
+value coq_makeaccu (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = VALINSTR(MAKEACCU);
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_accucond (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = VALINSTR(ACCUMULATECOND);
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_pushpop (value i) {
+  code_t res;
+  int n;
+  n = Int_val(i);
+  if (n == 0) {
+    res = coq_stat_alloc(4);
+    *res = VALINSTR(STOP);
+    return (value)res;
+  }
+  else {
+    code_t q;
+    res = coq_stat_alloc(12);
+    q = res;
+    *q++ = VALINSTR(POP);
+    *q++ = (opcode_t)n;
+    *q = VALINSTR(STOP);
+    return (value)res;
+  }
+}
+
+value coq_is_accumulate_code(value code){
+  code_t q;
+  int res;
+  q = (code_t)code;
+  res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE);
+  return Val_bool(res);
+}
+
+#ifdef ARCH_BIG_ENDIAN
+#define Reverse_32(dst,src) {                                               \
+  char * _p, * _q;							    \
+  char _a, _b;                                                              \
+  _p = (char *) (src);                                                      \
+  _q = (char *) (dst);                                                      \
+  _a = _p[0];                                                               \
+  _b = _p[1];                                                               \
+  _q[0] = _p[3];                                                            \
+  _q[1] = _p[2];                                                            \
+  _q[3] = _a;                                                               \
+  _q[2] = _b;                                                               \
+}
+#define COPY32(dst,src) Reverse_32(dst,src)
+#else
+#define COPY32(dst,src) (*dst=*src)
+#endif /* ARCH_BIG_ENDIAN */
+
+value coq_tcode_of_code (value code, value size) {
+  code_t p, q, res; 
+  asize_t len = (asize_t) Long_val(size);
+  res = coq_stat_alloc(len);
+  q = res;
+  len /= sizeof(opcode_t);
+  for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {  
+    opcode_t instr;
+    COPY32(&instr,p); 
+    p++;
+    if (instr < 0 || instr > STOP){
+      instr = STOP;
+    };
+    *q++ = VALINSTR(instr);
+    if (instr == SWITCH) {
+      uint32 i, sizes, const_size, block_size;
+      COPY32(q,p); p++;
+      sizes=*q++;
+      const_size = sizes & 0xFFFF;
+      block_size = sizes >> 16;
+      sizes = const_size + block_size;
+      for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
+    } else if (instr == CLOSUREREC) {
+      uint32 i, n;
+      COPY32(q,p); p++; /* ndefs */
+      n = 3 + 2*(*q);  /* ndefs, nvars, start, typlbls,lbls*/
+      q++;
+      for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
+    } else {
+      uint32 i, ar;
+      ar = arity[instr]; 
+      for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
+    }
+  }
+  return (value)res;
+}
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
new file mode 100644
index 00000000..035d5b9b
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.h
@@ -0,0 +1,34 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+
+#ifndef _COQ_FIX_CODE_
+#define _COQ_FIX_CODE_
+
+#include "mlvalues.h"
+void * coq_stat_alloc (asize_t sz);
+
+#ifdef THREADED_CODE
+extern char ** coq_instr_table;
+extern char * coq_instr_base;
+void init_arity();
+#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
+#else
+#define VALINSTR(instr) instr
+#endif /*  THREADED_CODE */
+
+#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
+
+value coq_tcode_of_code(value code, value len);
+value coq_makeaccu (value i);
+value coq_pushpop (value i);
+value coq_accucond (value i);
+value coq_is_accumulate_code(value code);
+#endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
new file mode 100644
index 00000000..2f085326
--- /dev/null
+++ b/kernel/byterun/coq_gc.h
@@ -0,0 +1,48 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_CAML_GC_
+#define _COQ_CAML_GC_
+#include "mlvalues.h"
+#include "alloc.h"
+
+typedef void (*scanning_action) (value, value *);
+
+
+CAMLextern char *young_ptr;
+CAMLextern char *young_limit;
+CAMLextern void (*scan_roots_hook) (scanning_action);
+CAMLextern void minor_collection (void);
+
+#define Caml_white (0 << 8)
+#define Caml_black (3 << 8)
+
+#define Make_header(wosize, tag, color)                                 \
+  (((header_t) (((header_t) (wosize) << 10)                             \
+		+ (color)                                               \
+		+ (tag_t) (tag)))   					\
+   )
+
+
+#define Alloc_small(result, wosize, tag) do{                            \
+  young_ptr -= Bhsize_wosize (wosize);                                  \
+  if (young_ptr < young_limit){                                         \
+    young_ptr += Bhsize_wosize (wosize);                                \
+    Setup_for_gc;                                                       \
+    minor_collection ();                                                \
+    Restore_after_gc;                                                   \
+    young_ptr -= Bhsize_wosize (wosize);                                \
+  }                                                                     \
+  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
+  (result) = Val_hp (young_ptr);                                        \
+  }while(0) 
+
+
+#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
new file mode 100644
index 00000000..d3b07526
--- /dev/null
+++ b/kernel/byterun/coq_instruct.h
@@ -0,0 +1,39 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_INSTRUCT_
+#define _COQ_INSTRUCT_
+
+enum instructions {
+  ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
+  PUSH, 
+  PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
+  PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, 
+  POP,
+  ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
+  PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
+  PUSH_RETADDR,
+  APPLY, APPLY1, APPLY2, APPLY3,
+  APPTERM, APPTERM1, APPTERM2, APPTERM3,
+  RETURN, RESTART, GRAB, GRABREC, COGRAB, 
+  CLOSURE, CLOSUREREC, 
+  OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
+  PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, 
+  PUSHOFFSETCLOSURE,
+  GETGLOBAL, PUSHGETGLOBAL,
+  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, 
+  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD,
+  FORCE, SWITCH, PUSHFIELD,
+  CONST0, CONST1, CONST2, CONST3, CONSTINT,
+  PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
+  ACCUMULATE, ACCUMULATECOND, STOP
+};
+
+#endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
new file mode 100644
index 00000000..8bfe78eb
--- /dev/null
+++ b/kernel/byterun/coq_interp.c
@@ -0,0 +1,974 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+/* The bytecode interpreter */
+
+#include <stdio.h>
+#include "coq_gc.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+#include "coq_memory.h"  
+#include "coq_values.h"
+
+
+/* Registers for the abstract machine:
+        pc         the code pointer
+        sp         the stack pointer (grows downward)
+        accu       the accumulator
+        env        heap-allocated environment
+        trapsp     pointer to the current trap frame
+        extra_args number of extra arguments provided by the caller
+
+sp is a local copy of the global variable extern_sp. */
+
+
+
+/* Instruction decoding */
+
+
+#ifdef THREADED_CODE
+#  define Instruct(name) coq_lbl_##name: 
+#  if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+#    define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
+#  else
+#    define coq_Jumptbl_base ((char *) 0)
+#    define coq_jumptbl_base ((char *) 0)
+#  endif
+#  ifdef DEBUG
+#    define Next goto next_instr
+#  else
+#    ifdef __ia64__
+#      define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++)
+#    else
+#      define Next goto *(void *)(coq_jumptbl_base + *pc++)
+#    endif
+#  endif
+#else 
+#  define Instruct(name) case name:
+#  define Next break
+#endif 
+
+/* #define _COQ_DEBUG_ */
+
+#ifdef _COQ_DEBUG_ 
+#   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
+#   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
+# else 
+#   define print_instr(s) 
+#   define print_int(i) 
+#endif
+
+/* 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; }
+
+
+/* Register optimization.
+   Some compilers underestimate the use of the local variables representing
+   the abstract machine registers, and don't put them in hardware registers,
+   which slows down the interpreter considerably.
+   For GCC, Xavier Leroy have hand-assigned hardware registers for 
+   several architectures.
+*/
+
+#if defined(__GNUC__) && !defined(DEBUG)
+#ifdef __mips__
+#define PC_REG asm("$16")
+#define SP_REG asm("$17")
+#define ACCU_REG asm("$18")
+#endif
+#ifdef __sparc__
+#define PC_REG asm("%l0")
+#define SP_REG asm("%l1")
+#define ACCU_REG asm("%l2")
+#endif
+#ifdef __alpha__
+#ifdef __CRAY__
+#define PC_REG asm("r9")
+#define SP_REG asm("r10")
+#define ACCU_REG asm("r11")
+#define JUMPTBL_BASE_REG asm("r12")
+#else
+#define PC_REG asm("$9")
+#define SP_REG asm("$10")
+#define ACCU_REG asm("$11")
+#define JUMPTBL_BASE_REG asm("$12")
+#endif
+#endif
+#ifdef __i386__
+#define PC_REG asm("%esi")
+#define SP_REG asm("%edi")
+#define ACCU_REG
+#endif
+#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#define PC_REG asm("26")
+#define SP_REG asm("27")
+#define ACCU_REG asm("28")
+#endif
+#ifdef __hppa__
+#define PC_REG asm("%r18")
+#define SP_REG asm("%r17")
+#define ACCU_REG asm("%r16")
+#endif
+#ifdef __mc68000__
+#define PC_REG asm("a5")
+#define SP_REG asm("a4")
+#define ACCU_REG asm("d7")
+#endif
+#ifdef __arm__
+#define PC_REG asm("r9")
+#define SP_REG asm("r8")
+#define ACCU_REG asm("r7")
+#endif
+#ifdef __ia64__
+#define PC_REG asm("36")
+#define SP_REG asm("37")
+#define ACCU_REG asm("38")
+#define JUMPTBL_BASE_REG asm("39")
+#endif
+#endif
+
+/* The interpreter itself */
+
+value coq_interprete
+(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args)
+{
+  /*Declaration des variables */
+#ifdef PC_REG
+  register code_t pc PC_REG;
+  register value * sp SP_REG;
+  register value accu ACCU_REG;
+#else
+  register code_t pc;
+  register value * sp;
+  register value accu;
+#endif
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+#ifdef JUMPTBL_BASE_REG
+  register char * coq_jumptbl_base JUMPTBL_BASE_REG;
+#else
+  register char * coq_jumptbl_base;
+#endif
+#endif
+#ifdef THREADED_CODE
+  static void * coq_jumptable[] = {
+#    include "coq_jumptbl.h"
+  };
+#else 
+  opcode_t curr_instr;
+#endif
+    print_instr("Enter Interpreter");
+  if (coq_pc == NULL) {           /* Interpreter is initializing */
+    print_instr("Interpreter is initializing");
+#ifdef THREADED_CODE
+    coq_instr_table = (char **) coq_jumptable;
+    coq_instr_base = coq_Jumptbl_base;
+#endif
+    return Val_unit;
+  }
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+  coq_jumptbl_base = coq_Jumptbl_base;
+#endif
+
+  /* Initialisation */
+  sp = coq_sp;
+  pc = coq_pc;
+  accu = coq_accu;
+#ifdef THREADED_CODE
+  goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */
+#else
+  while(1) {
+    curr_instr = *pc++;
+    switch(curr_instr) {
+#endif
+/* Basic stack operations */
+      
+      Instruct(ACC0){
+	print_instr("ACC0");
+	accu = sp[0]; Next;
+      }
+      Instruct(ACC1){
+	print_instr("ACC1");
+	accu = sp[1]; Next;
+      }
+      Instruct(ACC2){
+	print_instr("ACC2");
+	accu = sp[2]; Next;
+      }
+      Instruct(ACC3){
+	print_instr("ACC3");
+	accu = sp[3]; Next;
+      }
+      Instruct(ACC4){
+	print_instr("ACC4");
+	accu = sp[4]; Next;
+      }
+      Instruct(ACC5){
+	print_instr("ACC5");
+	accu = sp[5]; Next;
+      }
+      Instruct(ACC6){
+	print_instr("ACC6");
+	accu = sp[6]; Next;
+      }
+      Instruct(ACC7){
+	print_instr("ACC7");
+        accu = sp[7]; Next;
+      }      
+      Instruct(PUSH){
+	print_instr("PUSH");
+	*--sp = accu; Next;
+      }
+      Instruct(PUSHACC0) {
+	print_instr("PUSHACC0");
+        *--sp = accu; Next;
+      }
+      Instruct(PUSHACC1){
+	print_instr("PUSHACC1");
+        *--sp = accu; accu = sp[1]; Next;
+      }
+      Instruct(PUSHACC2){
+	print_instr("PUSHACC2");
+        *--sp = accu; accu = sp[2]; Next;
+      }
+      Instruct(PUSHACC3){
+	print_instr("PUSHACC3");
+	*--sp = accu; accu = sp[3]; Next;
+      }
+      Instruct(PUSHACC4){
+	print_instr("PUSHACC4");
+	*--sp = accu; accu = sp[4]; Next;
+      }
+      Instruct(PUSHACC5){
+	print_instr("PUSHACC5");
+	*--sp = accu; accu = sp[5]; Next;
+      }
+      Instruct(PUSHACC6){
+	print_instr("PUSHACC5");
+	*--sp = accu; accu = sp[6]; Next;
+      }
+      Instruct(PUSHACC7){
+	print_instr("PUSHACC7");
+	*--sp = accu; accu = sp[7]; Next;
+      }
+      Instruct(PUSHACC){
+	print_instr("PUSHACC");
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      
+      Instruct(ACC){
+	print_instr("ACC");
+	accu = sp[*pc++];
+        Next;
+      }
+      
+      Instruct(POP){
+	print_instr("POP");
+	sp += *pc++;
+	Next;
+      }
+      /* Access in heap-allocated environment */
+      
+      Instruct(ENVACC1){
+	print_instr("ENVACC1");
+	accu = Field(coq_env, 1); Next;
+      }
+      Instruct(ENVACC2){
+	print_instr("ENVACC2");
+	accu = Field(coq_env, 2); Next;
+      }
+      Instruct(ENVACC3){
+	print_instr("ENVACC3");
+	accu = Field(coq_env, 3); Next;
+      }
+      Instruct(ENVACC4){
+	print_instr("ENVACC4");
+	accu = Field(coq_env, 4); Next;
+      }
+      Instruct(PUSHENVACC1){
+	print_instr("PUSHENVACC1");
+	*--sp = accu; accu = Field(coq_env, 1); Next;
+      }
+      Instruct(PUSHENVACC2){
+	print_instr("PUSHENVACC2");
+	*--sp = accu; accu = Field(coq_env, 2); Next;
+      }
+      Instruct(PUSHENVACC3){
+	print_instr("PUSHENVACC3");
+	*--sp = accu; accu = Field(coq_env, 3); Next;
+      }
+      Instruct(PUSHENVACC4){
+	print_instr("PUSHENVACC4");
+	*--sp = accu; accu = Field(coq_env, 4); Next;
+      }
+      Instruct(PUSHENVACC){
+	print_instr("PUSHENVACC");
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(ENVACC){
+	print_instr("ENVACC");
+	accu = Field(coq_env, *pc++);
+        Next;
+      }
+      /* Function application */
+      
+      Instruct(PUSH_RETADDR) {
+	print_instr("PUSH_RETADDR");
+	sp -= 3;
+	sp[0] = (value) (pc + *pc);
+	sp[1] = coq_env;
+	sp[2] = Val_long(coq_extra_args);
+	coq_extra_args = 0;
+	pc++;
+	Next;
+      }
+      Instruct(APPLY) {
+	print_instr("APPLY");
+	coq_extra_args = *pc - 1;
+	pc = Code_val(accu);
+	coq_env = accu;
+	goto check_stacks;
+      }
+      Instruct(APPLY1) {
+	value arg1 = sp[0];
+	print_instr("APPLY1");
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = (value)pc;
+	sp[2] = coq_env;
+	sp[3] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 0;
+	goto check_stacks;
+      }
+      Instruct(APPLY2) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	print_instr("APPLY2");
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = (value)pc;
+	sp[3] = coq_env;
+	sp[4] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 1;
+	goto check_stacks;
+      }
+      Instruct(APPLY3) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	value arg3 = sp[2];
+	print_instr("APPLY3");
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = arg3;
+	sp[3] = (value)pc;
+	sp[4] = coq_env;
+	sp[5] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 2;
+	goto check_stacks;
+      }
+
+      Instruct(APPTERM) {
+	int nargs = *pc++;
+	int slotsize = *pc;
+	value * newsp;
+	int i;
+	print_instr("APPTERM");
+	/* Slide the nargs bottom words of the current frame to the top
+	   of the frame, and discard the remainder of the frame */
+	newsp = sp + slotsize - nargs;
+	for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+	sp = newsp;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += nargs - 1;
+	goto check_stacks;
+      }
+      Instruct(APPTERM1) {
+	value arg1 = sp[0];
+	print_instr("APPTERM1");
+	sp = sp + *pc - 1;
+	sp[0] = arg1;
+	pc = Code_val(accu);
+	coq_env = accu;
+	goto check_stacks;
+      }
+      Instruct(APPTERM2) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	print_instr("APPTERM2");
+	sp = sp + *pc - 2;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += 1;
+	goto check_stacks;
+      }
+      Instruct(APPTERM3) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	value arg3 = sp[2];
+	print_instr("APPTERM3");
+	sp = sp + *pc - 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = arg3;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += 2;
+	goto check_stacks;
+      }
+      
+      Instruct(RETURN) {
+	print_instr("RETURN");
+	sp += *pc++;
+	if (coq_extra_args > 0) {
+	  coq_extra_args--;
+	  pc = Code_val(accu);
+	  coq_env = accu;
+	} else {
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+      
+      Instruct(RESTART) {
+	int num_args = Wosize_val(coq_env) - 2;
+	int i;
+	print_instr("RESTART");
+	sp -= num_args;
+	for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+	coq_env = Field(coq_env, 1);
+	coq_extra_args += num_args;
+	Next;
+      }
+      
+      Instruct(GRAB) {
+	int required = *pc++;
+	print_instr("GRAB");
+	/*	printf("GRAB %d\n",required); */
+	if (coq_extra_args >= required) {
+	  coq_extra_args -= required;
+	} else {
+	  mlsize_t num_args, i;
+	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
+          Alloc_small(accu, num_args + 2, Closure_tag); 
+	  Field(accu, 1) = coq_env;
+	  for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	  Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+	  sp += num_args;
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+
+      Instruct(COGRAB){
+	int required = *pc++;
+	print_instr("COGRAB");
+	if(forcable == Val_true) {
+	  print_instr("true");
+	  /* L'instruction précédante est FORCE */
+	  if (coq_extra_args > 0) coq_extra_args--;
+	  pc++;
+	  forcable = Val_false;
+	} else { /* L'instruction précédante est APPLY */
+	  mlsize_t num_args, i;
+	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
+	  Alloc_small(accu, num_args + 2, Closure_tag); 
+	  Field(accu, 1) = coq_env;
+	  for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	  Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+	  sp += num_args;
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+      Instruct(GRABREC) { 
+	int rec_pos = *pc++; /* commence a zero */
+	print_instr("GRABREC");
+	if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
+	  pc++;/* On saute le Restart */
+	} else {
+	  if (coq_extra_args < rec_pos) {
+	    mlsize_t num_args, i;
+	    num_args = 1 + coq_extra_args; /* arg1 + extra args */
+	    Alloc_small(accu, num_args + 2, Closure_tag); 
+	    Field(accu, 1) = coq_env;
+	    for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	    Code_val(accu) = pc - 3; 
+	    sp += num_args;
+	    pc = (code_t)(sp[0]);
+	    coq_env = sp[1];
+	    coq_extra_args = Long_val(sp[2]);
+	    sp += 3;
+	  } else {
+	    /* L'argument recursif est un accumulateur */
+	    mlsize_t num_args, i;
+	    /* Construction du PF partiellement appliqué */ 
+	    Alloc_small(accu, rec_pos + 2, Closure_tag); 
+	    Field(accu, 1) = coq_env;
+	    for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i];
+	    Code_val(accu) = pc;
+	    sp += rec_pos;
+	    *--sp = accu;
+	      /* Construction de l'atom */
+	    Alloc_small(accu, 2, ATOM_FIX_TAG);
+	    Field(accu,1) = sp[0];
+	    Field(accu,0)  = sp[1];
+	    sp++; sp[0] = accu;
+	      /* Construction de l'accumulateur */
+	    num_args = coq_extra_args - rec_pos;
+	    Alloc_small(accu, 2+num_args, Accu_tag);
+	    Code_val(accu) = accumulate;
+	    Field(accu,1) = sp[0]; sp++;
+	    for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
+	    sp += num_args;
+	    pc = (code_t)(sp[0]);
+	    coq_env = sp[1];
+	    coq_extra_args = Long_val(sp[2]);
+	    sp += 3;
+	  }
+	}
+	Next;
+      }
+	
+      Instruct(CLOSURE) {
+	int nvars = *pc++;
+	int i;
+	print_instr("CLOSURE");
+	print_int(nvars);
+	if (nvars > 0) *--sp = accu;
+	Alloc_small(accu, 1 + nvars, Closure_tag);
+	Code_val(accu) = pc + *pc;
+	pc++;
+	for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+	sp += nvars;
+	Next;
+      }
+
+      Instruct(CLOSUREREC) {
+	int nfuncs = *pc++;
+	int nvars = *pc++;
+	int start = *pc++;
+	int i;
+	value * p;
+	print_instr("CLOSUREREC");
+	if (nvars > 0) *--sp = accu;
+	/* construction du vecteur de type */
+	Alloc_small(accu, nfuncs, 0);
+	for(i = 0; i < nfuncs; i++) {
+	  Field(accu,i) = (value)(pc+pc[i]);
+	}
+	pc += nfuncs;
+	*--sp=accu;
+	Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
+	Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
+	/* On remplie la partie pour les variables libres */
+	p = &Field(accu, nfuncs * 2 - 1);
+	for (i = 0; i < nvars; i++) {
+	  *p++ = *sp++;
+	}
+	p = &Field(accu, 0);
+	*p = (value) (pc + pc[0]);
+	p++;
+	for (i = 1; i < nfuncs; i++) {
+	  *p = Make_header(i * 2, Infix_tag, Caml_white);
+	  p++;                                /* color irrelevant. */
+	  *p = (value) (pc + pc[i]);
+	  p++;
+	}
+	pc += nfuncs;
+	accu = accu + 2 * start * sizeof(value);
+	Next;
+      }
+     
+      Instruct(PUSHOFFSETCLOSURE) {
+	print_instr("PUSHOFFSETCLOSURE");
+	*--sp = accu;
+      } /* fallthrough */
+      Instruct(OFFSETCLOSURE) {
+	print_instr("OFFSETCLOSURE");
+	accu = coq_env + *pc++ * sizeof(value); Next;
+      }
+      Instruct(PUSHOFFSETCLOSUREM2) {
+	print_instr("PUSHOFFSETCLOSUREM2");
+	*--sp = accu;
+      } /* fallthrough */
+      Instruct(OFFSETCLOSUREM2) {
+	print_instr("OFFSETCLOSUREM2");
+	accu = coq_env - 2 * sizeof(value); Next;
+      }
+      Instruct(PUSHOFFSETCLOSURE0) {
+	print_instr("PUSHOFFSETCLOSURE0");
+	*--sp = accu; 
+      }/* fallthrough */
+      Instruct(OFFSETCLOSURE0) {
+	print_instr("OFFSETCLOSURE0");
+	accu = coq_env; Next;
+      }
+      Instruct(PUSHOFFSETCLOSURE2){
+	print_instr("PUSHOFFSETCLOSURE2");
+	*--sp = accu; /* fallthrough */
+      }
+      Instruct(OFFSETCLOSURE2) {
+	print_instr("OFFSETCLOSURE2");
+	accu = coq_env + 2 * sizeof(value); Next;
+      }
+
+/* Access to global variables */
+
+      Instruct(PUSHGETGLOBAL) {
+	print_instr("PUSHGETGLOBAL");
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(GETGLOBAL){
+	print_instr("GETGLOBAL");
+	accu = Field(coq_global_data, *pc);
+        pc++;
+        Next;
+      }    
+
+/* Allocation of blocks */
+
+      Instruct(MAKEBLOCK) {
+	mlsize_t wosize = *pc++;
+	tag_t tag = *pc++;
+	mlsize_t i;
+	value block;
+	print_instr("MAKEBLOCK");
+	Alloc_small(block, wosize, tag);
+	Field(block, 0) = accu;
+	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK1) {
+	
+	tag_t tag = *pc++;
+	value block;
+	print_instr("MAKEBLOCK1");
+	Alloc_small(block, 1, tag);
+	Field(block, 0) = accu;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK2) {
+	
+	tag_t tag = *pc++;
+	value block;
+	print_instr("MAKEBLOCK2");
+	Alloc_small(block, 2, tag);
+	Field(block, 0) = accu;
+	Field(block, 1) = sp[0];
+	sp += 1;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK3) {
+	tag_t tag = *pc++;
+	value block;
+	print_instr("MAKEBLOCK3");
+	Alloc_small(block, 3, tag);
+	Field(block, 0) = accu;
+	Field(block, 1) = sp[0];
+	Field(block, 2) = sp[1];
+	sp += 2;
+	accu = block;
+	Next;
+      }
+
+  
+/* Access to components of blocks */
+        
+	
+/* Branches and conditional branches */
+      Instruct(FORCE) {
+	print_instr("FORCE");
+	if (Is_block(accu) && Tag_val(accu) == Closure_tag) {
+	  forcable = Val_true;
+	  /* On pousse l'addresse de retour et l'argument */
+	  sp -= 3;
+	  sp[0] = (value) (pc - 1);
+	  sp[1] = coq_env;
+	  sp[2] = Val_long(coq_extra_args);
+	  /* On evalue le cofix */
+	  coq_extra_args = 0;
+	  pc = Code_val(accu);
+	  coq_env = accu;
+	  goto check_stacks;
+	} else {
+	  if (Is_block(accu)) print_int(Tag_val(accu));
+	  else print_instr("Not a block");
+	}
+	Next;
+      }
+           
+    
+      Instruct(SWITCH) {
+	uint32 sizes = *pc++;
+	print_instr("SWITCH");
+	print_int(sizes);
+	if (Is_block(accu)) {
+	  long index = Tag_val(accu);
+	  print_instr("block");
+	  print_int(index);
+	  pc += pc[(sizes & 0xFFFF) + index];
+	} else {
+	  long index = Long_val(accu);
+	  print_instr("constant");
+	  print_int(index);
+	  pc += pc[index];
+	}
+	  Next;
+      }
+      Instruct(PUSHFIELD){
+	int i;
+	int size = *pc++;
+	print_instr("PUSHFIELD");
+	sp -= size;
+	for(i=0;i<size;i++)sp[i] = Field(accu,i);
+	Next;
+      }
+	
+      Instruct(MAKESWITCHBLOCK) {
+	mlsize_t sz;
+	int i, annot;
+	code_t typlbl,swlbl;
+	print_instr("MAKESWITCHBLOCK");
+	typlbl = (code_t)pc + *pc; 
+	pc++;
+	swlbl = (code_t)pc + *pc; 
+	pc++;
+	annot = *pc++;
+	sz = *pc++;
+	*--sp = accu;
+	*--sp=Field(coq_global_data, annot);
+	/* On sauve la pile */
+	if (sz == 0) accu = Atom(0);
+	else {
+	  Alloc_small(accu, sz, Default_tag);
+	  if (Field(*sp, 2) == Val_true) {
+	    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];
+	  }
+	}
+	*--sp = accu;
+	/* On cree le zipper switch */
+	Alloc_small(accu, 5, Default_tag);
+	Field(accu, 0) =  (value)typlbl; Field(accu, 1) = (value)swlbl; 
+	Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; 
+	Field(accu, 4) = coq_env;
+	sp++;sp[0] = accu;
+	/* On cree l'atome */
+	Alloc_small(accu, 2, ATOM_SWITCH_TAG);
+	Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
+	sp++;sp[0] = accu;
+	/* On cree l'accumulateur */
+	Alloc_small(accu, 2, Accu_tag);
+	Code_val(accu) = accumulate; 
+	Field(accu,1) = *sp++;
+	Next;
+      }
+
+      /* Stack checks */
+      
+    check_stacks:
+      print_instr("check_stacks");
+      if (sp < coq_stack_threshold) {
+	coq_sp = sp;
+	realloc_coq_stack(Coq_stack_threshold);
+	sp = coq_sp;
+      }
+      Next;
+      /* Fall through CHECK_SIGNALS */
+
+/* Integer constants */
+
+      Instruct(CONST0){
+	print_instr("CONST0");
+	accu = Val_int(0); Next;}
+      Instruct(CONST1){
+	print_instr("CONST1");
+	accu = Val_int(1); Next;}
+      Instruct(CONST2){
+	print_instr("CONST2");
+	accu = Val_int(2); Next;}
+      Instruct(CONST3){
+	print_instr("CONST3");
+	accu = Val_int(3); Next;}
+      
+      Instruct(PUSHCONST0){
+	print_instr("PUSHCONST0");
+	*--sp = accu; accu = Val_int(0); Next;
+      }
+      Instruct(PUSHCONST1){
+	print_instr("PUSHCONST1");
+	*--sp = accu; accu = Val_int(1); Next;
+      }
+      Instruct(PUSHCONST2){
+	print_instr("PUSHCONST2");
+	*--sp = accu; accu = Val_int(2); Next;
+      }
+      Instruct(PUSHCONST3){
+	print_instr("PUSHCONST3");
+	*--sp = accu; accu = Val_int(3); Next;
+      }
+
+      Instruct(PUSHCONSTINT){
+	print_instr("PUSHCONSTINT");
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(CONSTINT) {
+	print_instr("CONSTINT");
+	accu = Val_int(*pc);
+	pc++;
+	Next;
+      }
+
+/* Debugging and machine control */
+
+      Instruct(STOP){
+	print_instr("STOP");
+	coq_sp = sp;
+	return accu;
+      }
+      
+      Instruct(ACCUMULATECOND) {
+	int i, num;
+	print_instr("ACCUMULATECOND");
+	num = *pc;
+	pc++;
+	if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) {
+	  /*	  printf ("false\n");
+	    printf ("tag = %d", Tag_val(Field(accu,1))); */
+	  num = Wosize_val(coq_env);
+	  for(i = 2; i < num; i++) *--sp = Field(accu,i);
+	  coq_extra_args = coq_extra_args + (num - 2);
+	  coq_env = Field(Field(accu,1),1);
+	  pc = Code_val(coq_env);
+	  accu = coq_env;
+	  /*	  printf ("end\n"); */
+	  Next;
+	};
+	/*	printf ("true\n"); */
+      }
+
+      Instruct(ACCUMULATE) {
+	mlsize_t i, size;
+	print_instr("ACCUMULATE");
+	size = Wosize_val(coq_env);
+	Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+	for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
+	for(i = size; i <= coq_extra_args + size; i++) 
+	  Field(accu, i) = *sp++;
+	pc = (code_t)(sp[0]);
+	coq_env = sp[1];
+	coq_extra_args = Long_val(sp[2]);
+	sp += 3;
+	Next;
+      }  
+            
+      Instruct(MAKEACCU) {
+	int i;
+	print_instr("MAKEACCU");
+	Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+	Code_val(accu) = accumulate;
+	Field(accu,1) = Field(coq_atom_tbl, *pc);
+	for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+	pc = (code_t)(sp[0]);
+	coq_env = sp[1];
+	coq_extra_args = Long_val(sp[2]);
+	sp += 3;
+	Next;
+      }
+     
+      Instruct(MAKEPROD) {
+	print_instr("MAKEPROD");
+	*--sp=accu;
+	Alloc_small(accu,2,0);
+	Field(accu, 0) = sp[0];
+	Field(accu, 1) = sp[1];
+	sp += 2;
+	Next;
+      }
+      
+#ifndef THREADED_CODE
+    default:
+      /*fprintf(stderr, "%d\n", *pc);*/
+      failwith("Coq VM: Fatal error: bad opcode");
+    }
+  }
+#endif
+}
+
+value coq_push_ra(value tcode) { 
+  print_instr("push_ra");
+  coq_sp -= 3;
+  coq_sp[0] = (value) tcode;
+  coq_sp[1] = Val_unit;
+  coq_sp[2] = Val_long(0);
+  return Val_unit;
+}
+
+value coq_push_val(value v) {
+  print_instr("push_val");
+  *--coq_sp = v;
+  return Val_unit;
+}
+
+value coq_push_arguments(value args) {
+  int nargs,i;
+  nargs = Wosize_val(args) - 2;
+  coq_sp -= nargs;
+  print_instr("push_args");print_int(nargs);
+  for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
+  return Val_unit;
+}
+
+value coq_push_vstack(value stk) {
+  int len,i;
+  len = Wosize_val(stk);
+  coq_sp -= len;
+  print_instr("push_vstack");print_int(len);
+   for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i);
+  return Val_unit;
+}
+
+value  coq_interprete_ml(value tcode, value a, value e, value ea) {
+  print_instr("coq_interprete");
+  return coq_interprete((code_t)tcode, a, 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);
+}
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
new file mode 100644
index 00000000..76e68944
--- /dev/null
+++ b/kernel/byterun/coq_interp.h
@@ -0,0 +1,23 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+
+value coq_push_ra(value tcode);
+
+value coq_push_val(value v);
+
+value coq_push_arguments(value args);
+
+value coq_push_vstack(value stk);
+
+value  coq_interprete_ml(value tcode, value a, value e, value ea);
+
+value coq_eval_tcode (value tcode, value e);
+
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
new file mode 100644
index 00000000..db6aacb9
--- /dev/null
+++ b/kernel/byterun/coq_memory.c
@@ -0,0 +1,273 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include <string.h> 
+#include "coq_gc.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+#include "coq_memory.h"
+
+/* stack */
+
+value * coq_stack_low;
+value * coq_stack_high;
+value * coq_stack_threshold;
+asize_t coq_max_stack_size = Coq_max_stack_size;
+/* global_data */
+
+
+value coq_global_data;
+value coq_global_boxed;
+int coq_all_transp;
+value coq_atom_tbl;
+
+int drawinstr;
+/* interp state */
+
+long coq_saved_sp_offset;
+value * coq_sp;
+value forcable;
+/* Some predefined pointer code */ 
+code_t accumulate;
+
+/* functions over global environment */
+
+void coq_stat_free (void * blk)
+{
+  free (blk);
+}
+
+value coq_static_alloc(value size) /* ML */
+{
+  return (value) coq_stat_alloc((asize_t) Long_val(size));
+}
+
+value coq_static_free(value blk)  /* ML */
+{
+  coq_stat_free((void *) blk);
+  return Val_unit;
+}
+
+value accumulate_code(value unit) /* ML */
+{
+  return (value) accumulate;
+}
+
+static void (*coq_prev_scan_roots_hook) (scanning_action);
+
+static void coq_scan_roots(scanning_action action)
+{
+  register value * i;
+  /* Scan the global variables */
+  (*action)(coq_global_data, &coq_global_data);
+  (*action)(coq_global_boxed, &coq_global_boxed);
+  (*action)(coq_atom_tbl, &coq_atom_tbl);
+  /* Scan the stack */
+  for (i = coq_sp; i < coq_stack_high; i++) {
+    (*action) (*i, i);
+  };
+  /* Hook */
+  if (coq_prev_scan_roots_hook != NULL) (*coq_prev_scan_roots_hook)(action);
+
+
+}
+
+void init_coq_stack()
+{
+  coq_stack_low = (value *) coq_stat_alloc(Coq_stack_size);
+  coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
+  coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
+  coq_max_stack_size = Coq_max_stack_size;
+}  
+
+void init_coq_global_data(long requested_size)
+{
+  int i;
+  coq_global_data = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) 
+    Field (coq_global_data, i) = Val_unit;
+}
+
+void init_coq_global_boxed(long requested_size)
+{
+  int i;
+  coq_global_boxed = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) 
+    Field (coq_global_boxed, i) = Val_true;
+}
+
+void init_coq_atom_tbl(long requested_size){
+  int i;
+  coq_atom_tbl = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit;
+}
+
+void init_coq_interpreter()
+{
+  coq_sp = coq_stack_high;
+  coq_interprete(NULL, Val_unit, Val_unit, 0);
+}
+
+static int coq_vm_initialized = 0;
+
+value init_coq_vm(value unit) /* ML */
+{
+  int i;
+  if (coq_vm_initialized == 1) {
+    fprintf(stderr,"already open \n");fflush(stderr);}
+  else {
+    drawinstr=0;
+#ifdef THREADED_CODE   
+    init_arity();
+#endif /* THREADED_CODE */
+    /* Allocate the table of global and the stack */
+    init_coq_stack();
+    init_coq_global_data(Coq_global_data_Size);
+    init_coq_global_boxed(40);
+    init_coq_atom_tbl(40);
+    /* Initialing the interpreter */
+    coq_all_transp = 0;
+    forcable = Val_false;
+    init_coq_interpreter();
+    
+    /* Some predefined pointer code */
+    accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
+    *accumulate = VALINSTR(ACCUMULATE);
+
+  /* Initialize GC */
+    if (coq_prev_scan_roots_hook == NULL)
+      coq_prev_scan_roots_hook = scan_roots_hook;
+    scan_roots_hook = coq_scan_roots;
+    coq_vm_initialized = 1;
+  } 
+  return Val_unit;;
+}
+
+void realloc_coq_stack(asize_t required_space)
+{
+  asize_t size;
+  value * new_low, * new_high, * new_sp;
+  value * p;
+  size = coq_stack_high - coq_stack_low;
+  do {
+    size *= 2;
+  } while (size < coq_stack_high - coq_sp + required_space);
+  new_low = (value *) coq_stat_alloc(size * sizeof(value));
+  new_high = new_low + size;
+
+#define shift(ptr) \
+    ((char *) new_high - ((char *) coq_stack_high - (char *) (ptr)))
+
+  new_sp = (value *) shift(coq_sp);
+  memmove((char *) new_sp,
+        (char *) coq_sp,
+        (coq_stack_high - coq_sp) * sizeof(value));
+  coq_stat_free(coq_stack_low);
+  coq_stack_low = new_low;
+  coq_stack_high = new_high;
+  coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
+  coq_sp = new_sp;
+#undef shift
+}
+
+value get_coq_global_data(value unit)                /* ML */
+{
+  return coq_global_data;
+}
+
+value get_coq_atom_tbl(value unit)                  /* ML */
+{
+  return coq_atom_tbl;
+}
+
+value get_coq_global_boxed(value unit)        /* ML */
+{
+  return coq_global_boxed;
+}
+
+value realloc_coq_global_data(value size)           /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_global_data;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_global_data);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_global_data = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_global_data, i), Field(coq_global_data, i));
+    for (i = actual_size; i < requested_size; i++){
+      Field (new_global_data, i) = Val_long (0);
+    }
+    coq_global_data = new_global_data;
+  }
+  return Val_unit;
+}
+
+value realloc_coq_global_boxed(value size)           /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_global_boxed;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_global_boxed);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_global_boxed = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_global_boxed, i), Field(coq_global_boxed, i));
+    for (i = actual_size; i < requested_size; i++)
+      Field (new_global_boxed, i) = Val_long (0);
+    coq_global_boxed = new_global_boxed;
+  }
+  return Val_unit;
+}
+
+value realloc_coq_atom_tbl(value size)            /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_atom_tbl;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_atom_tbl);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_atom_tbl = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i));
+    for (i = actual_size; i < requested_size; i++)
+      Field (new_atom_tbl, i) = Val_long (0);
+    coq_atom_tbl = new_atom_tbl;
+  }
+  return Val_unit;
+}
+
+
+value coq_set_transp_value(value transp)
+{
+  coq_all_transp = (transp == Val_true);
+  return Val_unit;
+}
+
+value get_coq_transp_value(value unit)
+{
+  return Val_bool(coq_all_transp);
+}
+
+value coq_set_drawinstr(value unit)
+{
+  drawinstr = 1;
+  return Val_unit;
+}
+
+value coq_set_forcable (value unit)
+{
+  forcable = Val_true;
+  return Val_unit;
+}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
new file mode 100644
index 00000000..7c96e684
--- /dev/null
+++ b/kernel/byterun/coq_memory.h
@@ -0,0 +1,70 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_MEMORY_
+#define _COQ_MEMORY_
+
+#include "config.h"
+#include "fail.h"
+#include "misc.h"
+#include "memory.h"
+#include "mlvalues.h"
+
+
+#define Coq_stack_size (4096 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_global_data_Size (4096 * sizeof(value))
+#define Coq_max_stack_size (256 * 1024)
+
+#define TRANSP 0
+#define BOXED 1
+
+/* stack */
+
+extern value * coq_stack_low;
+extern value * coq_stack_high;
+extern value * coq_stack_threshold;
+
+/* global_data */
+
+extern value coq_global_data;
+extern value coq_global_boxed;
+extern int coq_all_transp;
+extern value coq_atom_tbl;
+
+extern int drawinstr;
+/* interp state */
+
+extern value * coq_sp;
+extern value forcable;
+/* Some predefined pointer code */ 
+extern code_t accumulate;
+
+/* functions over global environment */
+
+value coq_static_alloc(value size);  /* ML */
+value coq_static_free(value string); /* ML */
+
+value init_coq_vm(value unit); /* ML */
+value re_init_coq_vm(value unit); /* ML */
+
+void  realloc_coq_stack(asize_t required_space); 
+value get_coq_global_data(value unit); /* ML */
+value realloc_coq_global_data(value size); /* ML */
+value get_coq_global_boxed(value unit);
+value realloc_coq_global_boxed(value size); /* ML */
+value get_coq_atom_tbl(value unit); /* ML */
+value realloc_coq_atom_tbl(value size); /* ML */
+value coq_set_transp_value(value transp); /* ML */
+value get_coq_transp_value(value unit); /* ML */
+#endif /* _COQ_MEMORY_ */
+
+
+value coq_set_drawinstr(value unit);
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
new file mode 100644
index 00000000..baf3ab09
--- /dev/null
+++ b/kernel/byterun/coq_values.c
@@ -0,0 +1,69 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include "coq_fix_code.h"
+#include "coq_instruct.h"
+#include "coq_memory.h"
+#include "coq_values.h"
+#include "memory.h"
+/* KIND OF VALUES */
+
+#define Setup_for_gc
+#define Restore_after_gc
+
+value coq_kind_of_closure(value v) {
+  opcode_t * c;
+  int res;
+  int is_app = 0;
+  c = Code_val(v);
+  if (Is_instruction(c, GRAB)) return Val_int(0);
+  if (Is_instruction(c, RESTART)) {is_app = 1; c++;}
+  if (Is_instruction(c, GRABREC)) return Val_int(1+is_app);
+  if (Is_instruction(c, COGRAB)) return Val_int(3+is_app);
+  if (Is_instruction(c, MAKEACCU)) return Val_int(5);
+  return Val_int(0);
+}
+
+
+/* DESTRUCT ACCU */
+
+value coq_closure_arity(value clos) {
+  opcode_t * c = Code_val(clos);
+  if (Is_instruction(c,RESTART)) {
+    c++;
+    if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
+    else { 
+      if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+      return Val_int(1);
+    }
+  }
+  if (Is_instruction(c,GRAB)) return Val_int(1 + c[1]);
+  return Val_int(1);
+}
+
+/* Fonction sur les  fix */
+
+value coq_offset(value v) {
+  if (Tag_val(v) == Closure_tag) return Val_int(0);
+  else return Val_long(-Wsize_bsize(Infix_offset_val(v)));
+}
+
+value coq_offset_closure(value v, value offset){
+  return (value)&Field(v, Int_val(offset));
+}
+
+value coq_offset_tcode(value code,value offset){
+  return((value)((code_t)code + Int_val(offset)));
+}
+
+value coq_int_tcode(value code, value offset) {
+  return Val_int(*((code_t) code + Int_val(offset)));
+}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
new file mode 100644
index 00000000..a186d62a
--- /dev/null
+++ b/kernel/byterun/coq_values.h
@@ -0,0 +1,28 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_VALUES_
+#define _COQ_VALUES_
+
+#include "alloc.h"
+#include "mlvalues.h"
+
+#define ATOM_FIX_TAG 3
+#define ATOM_SWITCH_TAG 4
+
+#define Accu_tag 0
+#define Default_tag 0
+
+/* Les blocs accumulate */
+#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
+
+#endif /* _COQ_VALUES_ */
+
+