compatibility with POWERPC

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 237 insertions, 263 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 446c76498..4616580df 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -18,6 +18,45 @@
 #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);
@@ -25,16 +64,11 @@ void * coq_stat_alloc (asize_t sz)
   return result;
 }
 
-#ifdef THREADED_CODE
-
-char ** coq_instr_table;
-char * coq_instr_base;
-
 value coq_makeaccu (value i) {
   code_t q;
   code_t res = coq_stat_alloc(8);
   q = res;
-  *q++ = (opcode_t)(coq_instr_table[MAKEACCU] - coq_instr_base);
+  *q++ = VALINSTR(MAKEACCU);
   *q = (opcode_t)Int_val(i);
   return (value)res;
 }
@@ -43,178 +77,90 @@ value coq_accucond (value i) {
   code_t q;
   code_t res = coq_stat_alloc(8);
   q = res;
-  *q++ = (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base);
+  *q++ = VALINSTR(ACCUMULATECOND);
   *q = (opcode_t)Int_val(i);
   return (value)res;
 }
 
-value coq_is_accumulate_code(value code){
-  code_t q;
-  int res;
-  q = (code_t)code;
-  res = 
-    (*q == (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base))
-    || 
-    (*q == (opcode_t)(coq_instr_table[ACCUMULATE] - coq_instr_base));
-  return Val_bool(res);
-}
-
 value coq_pushpop (value i) {
   code_t res;
   int n;
   n = Int_val(i);
   if (n == 0) {
     res = coq_stat_alloc(4);
-    *res = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+    *res = VALINSTR(STOP);
     return (value)res;
   }
   else {
     code_t q;
     res = coq_stat_alloc(12);
     q = res;
-    *q++ = (opcode_t)(coq_instr_table[POP] - coq_instr_base);
+    *q++ = VALINSTR(POP);
     *q++ = (opcode_t)n;
-    *q = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+    *q = VALINSTR(STOP);
     return (value)res;
   }
 }
-  
-code_t coq_thread_code (code_t code, asize_t len){
-  opcode_t instr;
-  code_t p, q;
-  code_t res = coq_stat_alloc(len);
-  int i;
-  q = res;
-  len /= sizeof(opcode_t);
-  for (p=code; p < code + len; /*nothing*/) {
-    instr = *p++;
-    *q++ = (opcode_t)(coq_instr_table[instr] - coq_instr_base);
-    switch(instr){
-      /* instruction with zero operand */
-    case ACC0: case ACC1: case ACC2: case ACC3: case ACC4: case ACC5:
-    case ACC6: case ACC7: case PUSH: case PUSHACC0: case PUSHACC1:
-    case PUSHACC2: case PUSHACC3: case PUSHACC4: case PUSHACC5: case PUSHACC6:
-    case PUSHACC7: case ENVACC1: case ENVACC2: case ENVACC3: case ENVACC4:
-    case PUSHENVACC1: case PUSHENVACC2: case PUSHENVACC3: case PUSHENVACC4:
-    case APPLY1: case APPLY2: case APPLY3: case RESTART: case OFFSETCLOSUREM2:
-    case OFFSETCLOSURE0: case OFFSETCLOSURE2: case PUSHOFFSETCLOSUREM2:
-    case PUSHOFFSETCLOSURE0: case PUSHOFFSETCLOSURE2:
-    case CONST0: case CONST1: case CONST2: case CONST3:
-    case PUSHCONST0: case PUSHCONST1: case PUSHCONST2: case PUSHCONST3:
-    case ACCUMULATE: case STOP: case FORCE: case MAKEPROD: 
-    break;
-    
-    /* instruction with one operand */
-    case ACC: case PUSHACC: case  POP: case ENVACC: case PUSHENVACC: 
-    case PUSH_RETADDR:
-    case APPLY: case APPTERM1: case APPTERM2: case APPTERM3: case RETURN:
-    case GRAB: case COGRAB: 
-    case OFFSETCLOSURE: case PUSHOFFSETCLOSURE: 
-    case GETGLOBAL: case PUSHGETGLOBAL: 
-      /*    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: */
-    case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU:
-    case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD:
-    case ACCUMULATECOND:
-    *q++ = *p++;
-    break;
-    
-    /* instruction with two operands */
-    case APPTERM: case MAKEBLOCK: case CLOSURE:
-      *q++ = *p++; *q++ = *p++;
-      break;
-    
-    /* instruction with four operands */ 
-    case MAKESWITCHBLOCK:
-      *q++ = *p++; *q++ = *p++; *q++ = *p++; *q++ = *p++;
-    break;
-    
-    /* instruction with arbitrary operands */
-    case CLOSUREREC: {
-      int i; 
-      uint32 n = 2*(*p) + 3; /* ndefs, nvars, start, typlbls,lbls*/
-      for(i=0; i < n; i++) *q++ = *p++;
-    }
-    break; 
-
-    case SWITCH: {
-      int i;
-      uint32 sizes = *p;
-      uint32 const_size = sizes & 0xFFFF;
-      uint32 block_size = sizes >> 16;
-      sizes = const_size + block_size + 1 ;/* sizes */
-      for(i=0; i < sizes; i++) *q++ = *p++;
-    }  
-    break;
-    
-    default: 
-       invalid_argument("Fatal error in coq_thread_code : bad opcode");
-    break;
-    }
-  }
-  if (p != code + len) fprintf(stderr, "error thread code\n");
-  return res;
-}
-
-value coq_tcode_of_code(value code, value len){
-  return (value)coq_thread_code((code_t)code,(asize_t) Long_val(len));
-}
-#else
-
-value coq_makeaccu (value i) {
-  code_t q;
-  code_t res = coq_stat_alloc(8);
-  q = res;
-  *q++ = (opcode_t)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++ = (opcode_t)ACCUMULATECOND;
-  *q = (opcode_t)Int_val(i);
-  return (value)res;
-}
 
 value coq_is_accumulate_code(value code){
   code_t q;
   int res;
   q = (code_t)code;
-  res = 
-    (*q == ACCUMULATECOND) || 
-    (*q == ACCUMULATE);
+  res = Is_instruction(q,ACCUMULATECOND) || Is_instruction(q,ACCUMULATE);
   return Val_bool(res);
 }
 
-value coq_pushpop (value i) {
-  code_t res;
-  int n;
-  n = Int_val(i);
-  if (n == 0) {
-    res = coq_stat_alloc(4);
-    *res = (opcode_t)STOP;
-    return (value)res;
-  }
-  else {
-    res = coq_stat_alloc(12);
-    q = res;
-    *q++ = (opcode_t)POP;
-    *q++ = (opcode_t)n;
-    *q = (opcode_t)STOP;
-    return (value)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 s, value size) 
-{
-  void * new_s = coq_stat_alloc(Int_val(size));
-  memmove(new_s, &Byte(s, 0), Int_val(size));
-  return (value)new_s;
+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;
 }
-
-#endif /* THREADED_CODE */
-
-
-
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index e3296c0da..035d5b9b1 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,11 +18,13 @@ void * coq_stat_alloc (asize_t sz);
 #ifdef THREADED_CODE
 extern char ** coq_instr_table;
 extern char * coq_instr_base;
-#define Is_instruction(i1,i2) \
-       (*i1 == (opcode_t)(coq_instr_table[i2] - coq_instr_base))
-#else 
-#define Is_instruction(i1,i2) (*i1 == i2)
-#endif
+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);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 692baa7e7..48d91e4dc 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -55,11 +55,11 @@ sp is a local copy of the global variable extern_sp. */
 #  define Next break
 #endif 
 
-/*#define _COQ_DEBUG_*/
+/*#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)
+#   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) 
@@ -164,7 +164,9 @@ value coq_interprete
 #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;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index f94d2fb9e..db6aacb92 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -124,9 +124,11 @@ value init_coq_vm(value unit) /* ML */
   if (coq_vm_initialized == 1) {
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
-
-    /* Allocate the table of global and the stack */
     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);
@@ -138,9 +140,7 @@ value init_coq_vm(value unit) /* ML */
     
     /* Some predefined pointer code */
     accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
-    *accumulate = ACCUMULATE;
-    accumulate = 
-      (code_t) coq_tcode_of_code((value)accumulate, Val_int(sizeof(opcode_t))); 
+    *accumulate = VALINSTR(ACCUMULATE);
 
   /* Initialize GC */
     if (coq_prev_scan_roots_hook == NULL)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 108dadbb7..40965d2f5 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -466,29 +466,27 @@ let compile env c =
   let reloc = empty () in
   let init_code = compile_constr reloc c 0 [Kstop] in
   let fv = List.rev (!(reloc.in_env).fv_rev) in
-  if Options.print_bytecodes() then 
-    (draw_instr init_code; draw_instr !fun_code);
   init_code,!fun_code, Array.of_list fv
 
-
 let compile_constant_body env body opaque boxed =
   if opaque then BCconstant
   else match body with
   | None -> BCconstant
   | Some sb ->
       let body = Declarations.force sb in
-      match kind_of_term body with
-      | Const kn' -> BCallias (get_allias env kn')
-      | Construct _ ->
-	  let res = compile env body in
-	  let to_patch = to_memory res in
-	  BCdefined (false,to_patch)
-
-      | _ -> 
-	  let res = compile env body in
-	  let to_patch = to_memory res in
-	  (*if Options.print_bytecodes() then 
-	    (let init,fun_code,_= res in
-	    draw_instr init; draw_instr fun_code);*)
-	  BCdefined (boxed && Options.boxed_definitions (),to_patch)
+      if boxed then
+	let res = compile env body in
+	let to_patch = to_memory res in
+	BCdefined(true, to_patch)
+      else
+	match kind_of_term body with
+	| Const kn' -> BCallias (get_allias env kn')
+	| Construct _ ->
+	    let res = compile env body in
+	    let to_patch = to_memory res in
+	    BCdefined (false, to_patch)
+	| _ -> 
+	    let res = compile env body in
+	    let to_patch = to_memory res in
+	    BCdefined (false, to_patch)
 
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 0e7434e53..135afb1e2 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -12,5 +12,6 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
 
 val compile_constant_body : 
     env -> constr_substituted option -> bool -> bool -> body_code
-                                  (* opaque *) (* boxed *)
+                                 (* opaque *) (* boxed *)
+
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index f9f03e348..73e10df65 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -8,6 +8,9 @@ open Environ
 open Cbytegen
 open Cemitcodes
 
+
+open Format 
+
 external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external free_tcode : tcode -> unit = "coq_static_free"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
@@ -95,6 +98,8 @@ let slot_for_annot key =
     Hashtbl.add annot_tbl key n;
     n
 
+open Format
+
 let rec slot_for_getglobal env kn =
   let ck = lookup_constant_key kn env in
   try constant_key_pos ck
@@ -159,7 +164,9 @@ and eval_to_patch env (buff,pl,fv) =
   eval_tcode tc vm_env
 
 and val_of_constr env c = 
-  let (_,fun_code,_ as ccfv) = compile env c in
+  let (_,fun_code,_ as ccfv) = 
+    try compile env c 
+    with e -> print_string "can not compile \n";print_flush();raise e in
   eval_to_patch env (to_memory ccfv)
  
 let set_transparent_const kn =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a6d7ff65b..6d16632cd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -149,7 +149,6 @@ let lookup_named id env =
   Sign.lookup_named id env.env_named_context
     
 
-    
 (* A local const is evaluable if it is defined  *)
 let evaluable_named id env =
   try 
@@ -165,6 +164,7 @@ let push_named d env =
     match body with
     | None -> ref (VKaxiom id)
     | Some c -> ref (VKdef(c,env))
+	  
   in
   { env with  
     env_named_context = Sign.add_named_decl d env.env_named_context;
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 85d668f7a..156e3a44a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -341,19 +341,19 @@ let conv_leq_vecti env v1 v2 =
     v2
 
 (* option for conversion *)
-let use_vm = ref true
-let vm_fconv = ref (fun _ _ _ _ -> error "VM not installed")
+
+let vm_fconv = ref fconv 
+
+let set_default_vm_conv _ = vm_fconv := fconv
 let set_vm_conv_cmp f = vm_fconv := f
 
-let vm_conv cv_pb env t1 t2 =
-  if eq_constr t1 t2 then 
-    Constraint.empty
-  else if !use_vm then
-    try !vm_fconv cv_pb env t1 t2
-    with Not_found | Invalid_argument _ ->
+let vm_conv cv_pb env t1 t2 = 
+  try 
+    !vm_fconv cv_pb env t1 t2
+  with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
       clos_fconv cv_pb env t1 t2
-  else clos_fconv cv_pb env t1 t2
+  
 
 let vm_conv_leq_vecti env v1 v2 =
   array_fold_left2_i 
@@ -366,6 +366,7 @@ let vm_conv_leq_vecti env v1 v2 =
     v1
     v2
 
+let vm_conv_leq = vm_conv CUMUL
 (*
 let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ca4ab8c94..5d383e61e 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -44,10 +44,12 @@ val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
 (* option for conversion *)
-val use_vm : bool ref
+
+val set_default_vm_conv : unit -> unit
 val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
 val vm_conv_leq_vecti : types array conversion_function
+val vm_conv_leq          : types conversion_function
 
 (************************************************************************)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 57c1710ff..360d3d94c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -29,7 +29,7 @@ let constrain_type env j cst1 = function
   | Some t -> 
       let (tj,cst2) = infer_type env t in
       let cst3 =
-	try conv_leq env j.uj_type tj.utj_val
+	try vm_conv_leq env j.uj_type tj.utj_val
 	with NotConvertible -> error_actual_type env j tj.utj_val in
       let typ = 
         if t = tj.utj_val then t else
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 841bed98f..8105bcae4 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -12,6 +12,7 @@ open Univ
 open Cbytecodes
 
 
+
 (* Test la structure des piles *)
 
 let compare_zipper z1 z2 =
@@ -40,31 +41,33 @@ let conv_vect fconv vect1 vect2 cu =
     !rcu
   else raise NotConvertible
 
-let rec conv_val infos pb k v1 v2 cu =
-  if v1 == v2 then cu else conv_whd infos pb k (whd_val v1) (whd_val v2) cu 
+let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
+
+let rec conv_val pb k v1 v2 cu =
+  if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu 
     
-and conv_whd infos pb k whd1 whd2 cu =
+and conv_whd pb k whd1 whd2 cu =  
   match whd1, whd2 with
   | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu 
   | Vprod p1, Vprod p2 ->
-      let cu = conv_val infos CONV k (dom p1) (dom p2) cu in
-      conv_fun infos pb k (codom p1) (codom p2) cu
-  | Vfun f1, Vfun f2 -> conv_fun infos CONV k f1 f2 cu
-  | Vfix f1, Vfix f2 -> conv_fix infos k f1 f2 cu
+      let cu = conv_val CONV k (dom p1) (dom p2) cu in
+      conv_fun pb k (codom p1) (codom p2) cu
+  | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu
+  | Vfix f1, Vfix f2 -> conv_fix k f1 f2 cu
   | Vfix_app fa1, Vfix_app fa2 ->
       let f1 = fix fa1 in
       let args1 = args_of_fix fa1 in
       let f2 = fix fa2 in
       let args2 = args_of_fix fa2 in
-      conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu)
+      conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
   | Vcofix cf1, Vcofix cf2 -> 
-      conv_cofix infos k cf1 cf2 cu
+      conv_cofix k cf1 cf2 cu
   | Vcofix_app cfa1, Vcofix_app cfa2 ->	
       let cf1 = cofix cfa1 in
       let args1 = args_of_cofix cfa1 in
       let cf2 = cofix cfa2 in
       let args2 = args_of_cofix cfa2 in
-      conv_arguments infos k args1 args2 (conv_cofix infos k cf1 cf2 cu)
+      conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 -> 
       if i1 = i2 then cu else raise NotConvertible 
   | Vconstr_block b1, Vconstr_block b2 ->
@@ -72,113 +75,111 @@ and conv_whd infos pb k whd1 whd2 cu =
       if btag b1 = btag b2 && sz = bsize b2 then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
-	  rcu := conv_val infos CONV k (bfield b1 i) (bfield b2 i) !rcu
+	  rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu
 	done;
 	!rcu
       else raise NotConvertible
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> 
-      conv_atom infos pb k a1 stk1 a2 stk2 cu
-  | _, Vatom_stk(Aiddef(_,v),stk) -> 
-      conv_whd infos pb k whd1 (whd_stack v stk) cu
-  | Vatom_stk(Aiddef(_,v),stk), _ -> 
-      conv_whd infos pb k (whd_stack v stk) whd2 cu
+      conv_atom pb k a1 stk1 a2 stk2 cu
+  | _, Vatom_stk(Aiddef(_,v) as a2,stk) -> 
+      conv_whd pb k whd1 (force_whd v stk) cu
+  | Vatom_stk(Aiddef(_,v) as a1,stk), _ -> 
+      conv_whd pb k (force_whd v stk) whd2 cu
   | _, _ -> raise NotConvertible
 
-and conv_atom infos pb k a1 stk1 a2 stk2 cu =
+and conv_atom pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind (kn1,i1), Aind(kn2,i2) ->
-      if i1 = i2 && mind_equiv infos kn1 kn2 then
-	conv_stack infos k stk1 stk2 cu
+      if i1 = i2 && mind_equiv !infos kn1 kn2 && compare_stack stk1 stk2 then
+	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 -> 
-      if ik1 = ik2 then conv_stack infos k stk1 stk2 cu 
+      if ik1 = ik2 && compare_stack stk1 stk2 then 
+	conv_stack k stk1 stk2 cu 
       else raise NotConvertible
   | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
       begin
 	try
-	  if ik1 = ik2 then conv_stack infos k stk1 stk2 cu 
+	  if ik1 = ik2 && compare_stack stk1 stk2 then
+	    conv_stack k stk1 stk2 cu 
 	  else raise NotConvertible
 	with NotConvertible ->
 	  if oracle_order ik1 ik2 then             
-            conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
-          else conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+            conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+          else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
   | Aiddef(ik1,v1), _ ->
-      conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+      conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
-      conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+      conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
   | Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ -> 
       Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work"
   | _, _ -> raise NotConvertible 
+	
+and conv_stack k stk1 stk2 cu =
+  match stk1, stk2 with
+  | [], [] -> cu
+  | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
+      conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) 
+  | Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
+      let f1 = fix fa1 in
+      let args1 = args_of_fix fa1 in
+      let f2 = fix fa2 in
+      let args2 = args_of_fix fa2 in
+      conv_stack k stk1 stk2 
+	(conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
+  | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
+      if eq_tbl sw1 sw2 then
+	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
+	let rcu = ref (conv_val CONV k vt1 vt2 cu) in
+	let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
+	for i = 0 to Array.length b1 - 1 do
+	  rcu := 
+	    conv_val CONV (k + fst b1.(i)) 
+	      (snd b1.(i)) (snd b2.(i)) !rcu
+	done;
+	conv_stack k stk1 stk2 !rcu
+      else raise NotConvertible
+  | _, _ -> raise NotConvertible
 
-and conv_stack infos k stk1 stk2 cu =
-  if compare_stack stk1 stk2 then
-    let rec conv_rec stk1 stk2 cu =
-      match stk1, stk2 with
-      |	[], [] -> cu
-      |	Zapp args1 :: stk1, Zapp args2 :: stk2 ->
-	  conv_rec stk1 stk2 (conv_arguments infos k args1 args2 cu) 
-      |	Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
-	  let f1 = fix fa1 in
-	  let args1 = args_of_fix fa1 in
-	  let f2 = fix fa2 in
-	  let args2 = args_of_fix fa2 in
-	  conv_rec stk1 stk2 
-	    (conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu))
-      |	Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
-	  if eq_tbl sw1 sw2 then
-	    let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
-	    let rcu = ref (conv_val infos CONV k vt1 vt2 cu) in
-	    let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
-	    for i = 0 to Array.length b1 - 1 do
-	      rcu := 
-		conv_val infos CONV (k + fst b1.(i)) 
-		  (snd b1.(i)) (snd b2.(i)) !rcu
-	    done;
-	    conv_rec stk1 stk2 !rcu
-	  else raise NotConvertible
-      |	_, _ -> raise NotConvertible
-    in conv_rec stk1 stk2 cu
-  else raise NotConvertible
-
-and conv_fun infos pb k f1 f2 cu =
+and conv_fun pb k f1 f2 cu =
   if f1 == f2 then cu
   else
     let arity,b1,b2 = decompose_vfun2 k f1 f2 in
-    conv_val infos pb (k+arity) b1 b2 cu
+    conv_val pb (k+arity) b1 b2 cu
 
-and conv_fix infos k f1 f2 cu =
+and conv_fix k f1 f2 cu =
   if f1 == f2 then cu 
   else
     if check_fix f1 f2 then
       let tf1 = types_of_fix f1 in
       let tf2 = types_of_fix f2 in
-      let cu = conv_vect (conv_val infos CONV k) tf1 tf2 cu in
+      let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in
       let bf1 = bodies_of_fix k f1 in
       let bf2 = bodies_of_fix k f2 in
-      conv_vect (conv_fun infos CONV (k + (fix_ndef f1))) bf1 bf2 cu
+      conv_vect (conv_fun CONV (k + (fix_ndef f1))) bf1 bf2 cu
     else raise NotConvertible
 
-and conv_cofix infos k cf1 cf2 cu =
+and conv_cofix k cf1 cf2 cu =
   if cf1 == cf2 then cu
   else
     if check_cofix cf1 cf2 then
       let tcf1 = types_of_cofix cf1 in
       let tcf2 = types_of_cofix cf2 in
-      let cu = conv_vect (conv_val infos CONV k) tcf1 tcf2 cu in
+      let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in
       let bcf1 = bodies_of_cofix k cf1 in
       let bcf2 = bodies_of_cofix k cf2 in
-      conv_vect (conv_val infos CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
+      conv_vect (conv_val CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
     else raise NotConvertible
 
-and conv_arguments infos k args1 args2 cu =
+and conv_arguments k args1 args2 cu =
   if args1 == args2 then cu
   else
     let n = nargs args1 in
     if n = nargs args2 then
       let rcu = ref cu in
       for i = 0 to n - 1 do
-	rcu := conv_val infos CONV k (arg args1 i) (arg args2 i) !rcu
+	rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu
       done;
       !rcu
     else raise NotConvertible
@@ -237,14 +238,21 @@ let vconv pb env t1 t2 =
   let cu =
     try conv_eq pb t1 t2 Constraint.empty
     with NotConvertible ->
-      let infos = create_clos_infos betaiotazeta env in
+      infos := create_clos_infos betaiotazeta env;
       let v1 = val_of_constr env t1 in
       let v2 = val_of_constr env t2 in
-      let cu = conv_val infos pb (nb_rel env) v1 v2 Constraint.empty in
+      let cu = conv_val pb (nb_rel env) v1 v2 Constraint.empty in
       cu
   in cu
-
+    
+let use_vm = ref true
 let _ = Reduction.set_vm_conv_cmp vconv
+let set_use_vm b =
+  use_vm := b;
+  if b then Reduction.set_vm_conv_cmp vconv
+  else Reduction.set_default_vm_conv ()
+      
+let use_vm _ = !use_vm
 
 (*******************************************)
 (* Calcul de la forme normal d'un terme    *)
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index ea84a4ea8..fa6026509 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -7,6 +7,8 @@ open Reduction
 
 (***********************************************************************)
 (*s conversion functions *)
+val use_vm : unit -> bool
+val set_use_vm : bool -> unit
 val vconv : conv_pb -> types conversion_function
 
 (***********************************************************************)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 4482696ae..0aa4f1ff4 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -432,6 +432,11 @@ let rec whd_stack v stk =
       if is_accu v then whd_accu (magic v) stk 
       else whd_stack (apply_switch sw v) stkt 
 
+let rec force_whd v stk =
+  match whd_stack v stk with
+  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
+  | res -> res
+
 	  
 
 (* Function *)
diff --git a/kernel/vm.mli b/kernel/vm.mli
index a4651cf7d..b5fd9b9db 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -104,6 +104,6 @@ val arg : arguments -> int -> values
 
 (* Evaluation *)
 val whd_stack : values -> stack -> whd
-
+val force_whd : values -> stack -> whd