Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.

9 files changed, 41 insertions, 153 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 3d688011c..802b0f9d8 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,6 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind((sp,i),_) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829ab..416e5e532 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 
 
 value coq_global_data;
-int coq_all_transp;
 value coq_atom_tbl;
 
 int drawinstr;
@@ -117,7 +116,6 @@ value init_coq_vm(value unit) /* ML */
     init_coq_global_data(Coq_global_data_Size);
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
-    coq_all_transp = 0;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -207,18 +205,6 @@ value realloc_coq_atom_tbl(value size)            /* ML */
   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;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1590a2141..80100da71 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -20,13 +20,12 @@
 
 
 #define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_PROJ_TAG 3
-#define ATOM_FIX_TAG 4
-#define ATOM_SWITCH_TAG 5
-#define ATOM_COFIX_TAG 6
-#define ATOM_COFIXEVALUATED_TAG 7
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_PROJ_TAG 2
+#define ATOM_FIX_TAG 3
+#define ATOM_SWITCH_TAG 4
+#define ATOM_COFIX_TAG 5
+#define ATOM_COFIXEVALUATED_TAG 6
 
 
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index a03a67db8..8af2efc58 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -76,11 +76,7 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
-      conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
-  | _, Vatom_stk(Aiddef(_,v),stk) ->
-      conv_whd env pb k whd1 (force_whd v stk) cu
-  | Vatom_stk(Aiddef(_,v),stk), _ ->
-      conv_whd env pb k (force_whd v stk) whd2 cu
+      conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
   | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
@@ -97,22 +93,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
       if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
-  | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
-      begin
-	try
-	  if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
-	    conv_stack env k stk1 stk2 cu
-	  else raise NotConvertible
-	with NotConvertible ->
-	  if oracle_order Univ.out_punivs (oracle_of_infos !infos) 
-	    false ik1 ik2 then
-            conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
-          else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
-      end
-  | Aiddef(ik1,v1), _ ->
-      conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
-  | _, Aiddef(ik2,v2) ->
-      conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
   | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env k stk1 stk2 cu =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index a822f92eb..4607ad716 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -20,6 +20,12 @@ external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset : Obj.t -> int = "coq_offset"
 
 let accu_tag = 0
+let max_atom_tag = 1
+let proj_tag = 2
+let fix_app_tag = 3
+let switch_tag = 4
+let cofix_tag = 5
+let cofix_evaluated_tag = 6
 
 (*******************************************)
 (* Initalization of the abstract machine ***)
@@ -29,9 +35,6 @@ external init_vm : unit -> unit = "init_coq_vm"
 
 let _ = init_vm ()
 
-external transp_values : unit -> bool = "get_coq_transp_value"
-external set_transp_values : bool -> unit = "coq_set_transp_value"
-
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
@@ -141,7 +144,6 @@ type vswitch = {
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (* Zippers *)
@@ -176,20 +178,20 @@ let rec whd_accu a stk =
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
-  | i when i <= 2 ->
+  | i when i <= max_atom_tag ->
       Vatom_stk(Obj.magic at, stk)
-  | 3 (* proj tag *) ->
+  | i when Int.equal i proj_tag ->
      let zproj = Zproj (Obj.obj (Obj.field at 0)) in
      whd_accu (Obj.field at 1) (zproj :: stk)
-  | 4 (* fix_app tag *) ->
+  | i when Int.equal i fix_app_tag ->
       let fa = Obj.field at 1 in
       let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
-  | 5 (* switch tag  *) ->
+  | i when Int.equal i switch_tag ->
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
-  | 6 (* cofix_tag *) ->
+  | i when Int.equal i cofix_tag ->
       let vcfx = Obj.obj (Obj.field at 0) in
       let to_up = Obj.obj a in
       begin match stk with
@@ -197,7 +199,7 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
-  | 7 (* cofix_evaluated_tag *) ->
+  | i when Int.equal i cofix_evaluated_tag ->
       let vcofix = Obj.obj (Obj.field at 0) in
       let res = Obj.obj a in
       begin match stk with
@@ -258,6 +260,7 @@ let arg args i =
 		("Vm.arg size = "^(string_of_int (nargs args))^
 		 " acces "^(string_of_int i))
 
+(* Apply a value to arguments contained in [vargs] *)
 let apply_arguments vf vargs =
   let n = nargs vargs in
   if Int.equal n 0 then vf
@@ -268,13 +271,14 @@ let apply_arguments vf vargs =
      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
    end
 
-let apply_vstack vf vstk =
-  let n = Array.length vstk in
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+  let n = Array.length varray in
   if Int.equal n 0 then vf
   else
     begin
       push_ra stop;
-      push_vstack vstk;
+      push_vstack varray;
       interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
     end
 
@@ -360,14 +364,14 @@ external closure_arity : vfun -> int = "coq_closure_arity"
 
 let body_of_vfun k vf =
   let vargs = mkrel_vstack k 1 in
-  apply_vstack (Obj.magic vf) vargs
+  apply_varray (Obj.magic vf) vargs
 
 let decompose_vfun2 k vf1 vf2 =
   let arity = min (closure_arity vf1) (closure_arity vf2) in
   assert (0 < arity && arity < Sys.max_array_length);
   let vargs = mkrel_vstack k arity in
-  let v1 = apply_vstack (Obj.magic vf1) vargs in
-  let v2 = apply_vstack (Obj.magic vf2) vargs in
+  let v1 = apply_varray (Obj.magic vf1) vargs in
+  let v2 = apply_varray (Obj.magic vf2) vargs in
   arity, v1, v2
 
 (* Functions over fixpoint *)
@@ -497,7 +501,7 @@ let reduce_cofix k vcf =
     let self = Obj.new_block accu_tag 2 in
     Obj.set_field self 0 (Obj.repr accumulate);
     Obj.set_field self 1 (Obj.repr atom);
-    apply_vstack (Obj.obj e) [|Obj.obj self|] in
+    apply_varray (Obj.obj e) [|Obj.obj self|] in
   (Array.init ndef cofix_body, ftyp)
 
 
@@ -550,62 +554,12 @@ let branch_of_switch k sw =
   in
   Array.map eval_branch sw.sw_annot.rtbl
 
-
-
-(* Evaluation *)
-
-let rec whd_stack v stk =
-  match stk with
-  | [] -> whd_val v
-  | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
-  | Zfix (f,args) :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	whd_accu (Obj.repr v) stk
-      else
-	let v', stkt =
-	  match stkt with
-	  | Zapp args' :: stkt ->
-	      push_ra stop;
-	      push_arguments args';
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args+ nargs args') in
-	      v', stkt
-	  | _ ->
-	      push_ra stop;
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args) in
-	      v', stkt
-	in
-	whd_stack v' stkt
-  | Zswitch sw :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
-	else
-	  let to_up =
-	    match whd_accu (Obj.repr v) [] with
-	    | Vcofix (_, to_up, _) -> to_up
-	    | _ -> assert false in
-	  whd_stack (apply_switch sw to_up) stkt
-      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
-
-
-let rec eta_stack a stk v =
+(* Apply the term represented by a under stack stk to argument v *)
+(* t = a stk --> t v *)
+let rec apply_stack a stk v =
   match stk with
-  | [] -> apply_vstack a [|v|]
-  | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v
+  | [] -> apply_varray a [|v|]
+  | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v
   | Zfix(f,args) :: stk ->
       let a,stk = 
 	match stk with
@@ -626,11 +580,11 @@ let rec eta_stack a stk v =
 	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
 		(nargs args) in
 	    a, stk in
-      eta_stack a stk v
+      apply_stack a stk v
   | Zswitch sw :: stk ->
-      eta_stack (apply_switch sw a) stk v
+      apply_stack (apply_switch sw a) stk v
 
-let eta_whd k whd =
+let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
   | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
@@ -649,8 +603,4 @@ let eta_whd k whd =
       push_val v;
       interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
   | Vatom_stk(a,stk) ->
-      eta_stack (val_of_atom a) stk v 
-
-
-      
-      
+      apply_stack (val_of_atom a) stk v 
diff --git a/kernel/vm.mli b/kernel/vm.mli
index d31448ee1..045d02333 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
 open Term
 open Cbytecodes
 
-(** Efficient Virtual Machine *)
+(** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
 (** Machine code *)
 
 type tcode
@@ -25,7 +22,6 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (** Zippers *)
@@ -106,10 +102,6 @@ val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
 
+val apply_whd : int -> whd -> values
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index af640d7f3..f768e4fee 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -179,8 +179,6 @@ and nf_whd env whd typ =
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
       nf_stk env c typ stk
-  | Vatom_stk(Aiddef(idkey,v), stk) ->
-      nf_whd env (whd_stack v stk) typ
   | Vatom_stk(Aind ind, stk) ->
       nf_stk env (mkIndU ind) (type_of_ind env ind) stk
 
@@ -312,10 +310,5 @@ and nf_cofix env cf =
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env c t  =
-  let transp = transp_values () in
-  if not transp then set_transp_values true;
   let v = Vconv.val_of_constr env c in
-  let c = nf_val env v t in
-  if not transp then set_transp_values false;
-  c
-
+  nf_val env v t
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9b5a09de0..8925bbe29 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -235,11 +235,9 @@ let compile_files () =
 
 (*s options for the virtual machine *)
 
-let boxed_val = ref false
 let use_vm = ref false
 
 let set_vm_opt () =
-  Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
 (** Options for proof general *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 820903c41..35730eea0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1375,15 +1375,6 @@ let _ =
       optread  = (fun () -> !Closure.share);
       optwrite = (fun b -> Closure.share := b) }
 
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of boxed values";
-      optkey   = ["Boxed";"Values"];
-      optread  = (fun _ -> not (Vm.transp_values ()));
-      optwrite = (fun b -> Vm.set_transp_values (not b)) }
-
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)