Remove some dead code in the vm

 Apparently Cysmtable.set_global_boxed is unused,
 and removing it allows to get rid of a bunch of C code
 concerning "boxed" things (including ACCUMULATECOND
 instruction).

 Still TODO: Csymtable.set_transparent_const and
 Csymtable.set_opaque_const appear to be no-ops.
 Should we remove them ?

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

10 files changed, 5 insertions, 124 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 9a59a773f..3fded6638 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -55,7 +55,7 @@ void init_arity () {
     arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
     arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
     arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
-    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]=
+    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
     arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
@@ -85,15 +85,6 @@ value coq_makeaccu (value 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;
@@ -118,7 +109,7 @@ 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);
+  res = Is_instruction(q,ACCUMULATE);
   return Val_bool(res);
 }
 
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index c1a4e0ae6..5c85389dd 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -29,7 +29,6 @@ void init_arity();
 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_instruct.h b/kernel/byterun/coq_instruct.h
index d1136b2dc..9cbf4077e 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -38,7 +38,7 @@ enum instructions {
   SETFIELD0, SETFIELD1, SETFIELD,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
-  ACCUMULATE, ACCUMULATECOND, 
+  ACCUMULATE,
   MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
 /* spiwack: */
   BRANCH,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 216919ae3..84bc08d2b 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -922,26 +922,6 @@ value coq_interprete
       }
 
       /* Special operations for reduction of open term */
-      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");
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 00f5eb3b0..8d03829ab 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;
-value coq_global_boxed;
 int coq_all_transp;
 value coq_atom_tbl;
 
@@ -62,7 +61,6 @@ 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++) {
@@ -90,14 +88,6 @@ void init_coq_global_data(long requested_size)
     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);
@@ -125,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
     /* 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;
@@ -181,11 +170,6 @@ 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;
@@ -205,24 +189,6 @@ value realloc_coq_global_data(value size)           /* ML */
   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;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 79e4d0fea..cec34f566 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -35,7 +35,6 @@ 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;
 
@@ -56,8 +55,6 @@ 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 */
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 82250badb..f44e85320 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -51,35 +51,6 @@ let set_global v =
   incr num_global;
   n
 
-(* [global_transp],[global_boxed] contiennent les valeurs des
-   definitions gelees. Les deux versions sont maintenues en //.
-   [global_transp] contient la version transparente.
-   [global_boxed] contient la version gelees. *)
-
-external global_boxed : unit -> bool array = "get_coq_global_boxed"
-
-(* [realloc_global_data n] augmente de n la taille de [global_data] *)
-external realloc_global_boxed : int -> unit = "realloc_coq_global_boxed"
-
-let check_global_boxed n =
-  if n >= Array.length (global_boxed()) then realloc_global_boxed n
-
-let num_boxed = ref 0
-
-let boxed_tbl = Hashtbl.create 53
-
-let cst_opaque = ref Cpred.full
-
-let is_opaque kn = Cpred.mem kn !cst_opaque
-
-let set_global_boxed kn v =
-  let n = !num_boxed in
-  check_global_boxed n;
-  (global_boxed()).(n) <- (is_opaque kn);
-  Hashtbl.add boxed_tbl kn n ;
-  incr num_boxed;
-  set_global (val_of_constant_def n kn v)
-
 (* table pour les structured_constant et les annotations des switchs *)
 
 let str_cst_tbl = Hashtbl.create 31
@@ -192,14 +163,7 @@ and val_of_constr env c =
     with e -> print_string "can not compile \n";Format.print_flush();raise e in
   eval_to_patch env (to_memory ccfv)
 
-let set_transparent_const kn =
-  cst_opaque := Cpred.remove kn !cst_opaque;
-  List.iter (fun n -> (global_boxed()).(n) <- false)
-    (Hashtbl.find_all boxed_tbl kn)
-
-let set_opaque_const kn =
-  cst_opaque := Cpred.add kn !cst_opaque;
-  List.iter (fun n -> (global_boxed()).(n) <- true)
-    (Hashtbl.find_all boxed_tbl kn)
+let set_transparent_const kn = () (* !?! *)
+let set_opaque_const kn = () (* !?! *)
 
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 5ba4a9789..8bd0a653c 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -61,8 +61,6 @@ module Umap = struct
   let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
   let find_mp mp map = MPmap.find mp (fst map)
   let find_mbi mbi map = MBImap.find mbi (snd map)
-  let mem_mp mp map = MPmap.mem mp (fst map)
-  let mem_mbi mbi map = MBImap.mem mbi (snd map)
   let iter_mbi f map = MBImap.iter f (snd map)
   let fold fmp fmbi (m1,m2) i =
     MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 656e555fc..d4a86cb49 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -42,7 +42,6 @@ let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
 
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external mkPopStopCode : int -> tcode = "coq_pushpop"
-external mkAccuCond : int -> tcode = "coq_accucond"
 
 external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
 external int_tcode : tcode -> int -> int = "coq_int_tcode"
@@ -315,17 +314,10 @@ let val_of_idkey key =
     v
 
 let val_of_rel k = val_of_idkey (RelKey k)
-let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v))
 
 let val_of_named id = val_of_idkey (VarKey id)
-let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v))
 
 let val_of_constant c = val_of_idkey (ConstKey c)
-let val_of_constant_def n c v =
-  let res = Obj.new_block accu_tag 2 in
-  Obj.set_field res 0 (Obj.repr (mkAccuCond n));
-  Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v)));
-  val_of_obj res
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 58228eb85..4bdc1fbff 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -53,15 +53,9 @@ type whd =
 (** Constructors *)
 
 val val_of_str_const : structured_constant -> values
-
 val val_of_rel : int -> values
-val val_of_rel_def : int -> values -> values
-
 val val_of_named : identifier -> values
-val val_of_named_def : identifier -> values -> values
-
 val val_of_constant : constant -> values
-val val_of_constant_def : int -> constant -> values -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"