Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 89 insertions, 87 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
index 4ed0592d..33893625 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vm.ml 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id$ *)
 
 open Names
 open Term
@@ -39,11 +39,11 @@ external set_transp_values : bool -> unit = "coq_set_transp_value"
 (* Le code machine  ************************)
 (*******************************************)
 
-type tcode 
+type tcode
 let tcode_of_obj v = ((Obj.obj v):tcode)
-let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) 
+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"
@@ -57,21 +57,21 @@ let accumulate = accumulate ()
 
 external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
 
-let popstop_tbl =  ref (Array.init 30 mkPopStopCode) 
+let popstop_tbl =  ref (Array.init 30 mkPopStopCode)
 
 let popstop_code i =
   let len = Array.length !popstop_tbl in
-  if i < len then !popstop_tbl.(i) 
+  if i < len then !popstop_tbl.(i)
   else
     begin
       popstop_tbl :=
 	Array.init (i+10)
 	  (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
-      !popstop_tbl.(i) 
+      !popstop_tbl.(i)
     end
 
 let stop = popstop_code 0
- 
+
 (******************************************************)
 (* Types de donnees abstraites et fonctions associees *)
 (******************************************************)
@@ -81,23 +81,23 @@ let val_of_obj v = ((Obj.obj v):values)
 let crasy_val = (val_of_obj (Obj.repr 0))
 
 (* Abstract data *)
-type vprod 
+type vprod
 type vfun
 type vfix
 type vcofix
 type vblock
 type arguments
 
-type vm_env      
+type vm_env
 type vstack = values array
 
 type vswitch = {
-    sw_type_code : tcode; 
-    sw_code : tcode; 
+    sw_type_code : tcode;
+    sw_code : tcode;
     sw_annot : annot_switch;
     sw_stk : vstack;
     sw_env : vm_env
-  } 
+  }
 
 (* Representation des types abstraits:                                    *)
 (* + Les produits :                                                       *)
@@ -105,10 +105,10 @@ type vswitch = {
 (*             dom : values, codom : vfun                                 *)
 (*                                                                        *)
 (* + Les fonctions ont deux representations possibles :                   *)
-(*   - fonction non applique :  vf = Ct_[ C | fv1 | ... | fvn]            *) 
+(*   - fonction non applique :  vf = Ct_[ C | fv1 | ... | fvn]            *)
 (*                                       C:tcode, fvi : values            *)
 (*     Remarque : il n'y a pas de difference entre la fct et son          *)
-(*                environnement.                                          *) 
+(*                environnement.                                          *)
 (*   - Application partielle  : Ct_[Restart:C| vf | arg1 | ... argn]      *)
 (*                                                                        *)
 (* + Les points fixes :                                                   *)
@@ -138,7 +138,7 @@ type vswitch = {
 (*     -- 4_[accu|vswitch] : un case bloque par un accu                   *)
 (*     -- 5_[fcofix]       : une fonction de cofix                        *)
 (*     -- 6_[fcofix|val]   : une fonction de cofix, val represente        *)
-(*        la valeur de la reduction de la fct applique a arg1 ... argn    *) 
+(*        la valeur de la reduction de la fct applique a arg1 ... argn    *)
 (* Le type [arguments] est utiliser de maniere abstraite comme un         *)
 (* tableau, il represente la structure de donnee suivante :               *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
@@ -146,7 +146,7 @@ type vswitch = {
 
 (* Ne pas changer ce type sans modifier le code C, *)
 (* en particulier le fichier "coq_values.h"        *)
-type atom = 
+type atom =
   | Aid of id_key
   | Aiddef of id_key * values
   | Aind of inductive
@@ -164,7 +164,7 @@ type to_up = values
 
 type whd =
   | Vsort of sorts
-  | Vprod of vprod 
+  | Vprod of vprod
   | Vfun of vfun
   | Vfix of vfix * arguments option
   | Vcofix of vcofix * to_up * arguments option
@@ -177,16 +177,16 @@ type whd =
 (*************************************************)
 
 let rec whd_accu a stk =
-  let stk = 
+  let stk =
     if Obj.size a = 2 then 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 <= 2 ->
       Vatom_stk(Obj.magic at, stk)
   | 3 (* fix_app tag *) ->
       let fa = Obj.field at 1 in
-      let zfix  = 
+      let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
   | 4 (* switch tag  *) ->
@@ -194,7 +194,7 @@ let rec whd_accu a stk =
       whd_accu (Obj.field at 0) (zswitch :: stk)
   | 5 (* cofix_tag *) ->
       begin match stk with
-      | [] -> 
+      | [] ->
 	  let vcfx = Obj.obj (Obj.field at 0) in
 	  let to_up = Obj.obj a in
 	  Vcofix(vcfx, to_up, None)
@@ -210,7 +210,7 @@ let rec whd_accu a stk =
 	  let vcofix = Obj.obj (Obj.field at 0) in
 	  let res = Obj.obj a in
 	  Vcofix(vcofix, res, None)
-      | [Zapp args] -> 
+      | [Zapp args] ->
 	  let vcofix = Obj.obj (Obj.field at 0) in
 	  let res = Obj.obj a in
 	  Vcofix(vcofix, res, Some args)
@@ -221,18 +221,18 @@ let rec whd_accu a stk =
 external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
 
 let whd_val : values -> whd =
-  fun v -> 
-    let o = Obj.repr v in 
+  fun v ->
+    let o = Obj.repr v in
     if Obj.is_int o then Vconstr_const (Obj.obj o)
-    else 
+    else
       let tag = Obj.tag o in
       if tag = accu_tag then
 	(
 	if Obj.size o = 1 then Obj.obj o (* sort *)
-	else 
+	else
 	  if is_accumulate (fun_code o) then whd_accu o []
 	  else (Vprod(Obj.obj o)))
-      else 
+      else
 	if tag = Obj.closure_tag || tag = Obj.infix_tag then
 	  (	   match kind_of_closure o with
 	   | 0 -> Vfun(Obj.obj o)
@@ -241,7 +241,7 @@ let whd_val : values -> whd =
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
 	   | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work")
 	else Vconstr_block(Obj.obj o)
-	
+
 
 
 (************************************************)
@@ -263,16 +263,16 @@ external interprete : tcode -> values -> vm_env -> int -> values =
 
 (* Functions over arguments *)
 let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i = 
-  if  0 <= i && i < (nargs args) then 
+let arg args i =
+  if  0 <= i && i < (nargs args) then
     val_of_obj (Obj.field (Obj.repr args) (i+2))
-  else raise (Invalid_argument 
+  else raise (Invalid_argument
 		("Vm.arg size = "^(string_of_int (nargs args))^
 		 " acces "^(string_of_int i)))
 
 let apply_arguments vf vargs =
   let n = nargs vargs in
-  if n = 0 then vf 
+  if n = 0 then vf
   else
    begin
      push_ra stop;
@@ -283,7 +283,7 @@ let apply_arguments vf vargs =
 let apply_vstack vf vstk =
   let n = Array.length vstk in
   if n = 0 then vf
-  else 
+  else
     begin
       push_ra stop;
       push_vstack vstk;
@@ -295,23 +295,23 @@ let apply_vstack vf vstk =
 (**********************************************)
 
 let obj_of_atom : atom -> Obj.t =
-  fun a -> 
+  fun a ->
     let res = Obj.new_block accu_tag 2 in
     Obj.set_field res 0 (Obj.repr accumulate);
     Obj.set_field res 1 (Obj.repr a);
-    res 
+    res
 
 (* obj_of_str_const : structured_constant -> Obj.t *)
 let rec obj_of_str_const str =
-  match str with 
+  match str with
   | Const_sorts s -> Obj.repr (Vsort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
       let res = Obj.new_block tag len in
-      for i = 0 to len - 1 do 
-	Obj.set_field res i (obj_of_str_const args.(i)) 
+      for i = 0 to len - 1 do
+	Obj.set_field res i (obj_of_str_const args.(i))
       done;
       res
 
@@ -324,8 +324,8 @@ let val_of_atom a = val_of_obj (obj_of_atom a)
 let idkey_tbl = Hashtbl.create 31
 
 let val_of_idkey key =
-  try Hashtbl.find idkey_tbl key 
-  with Not_found -> 
+  try Hashtbl.find idkey_tbl key
+  with Not_found ->
     let v = val_of_atom (Aid key) in
     Hashtbl.add idkey_tbl key v;
     v
@@ -335,14 +335,16 @@ 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 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"
+
 let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
@@ -354,7 +356,7 @@ let mkrel_vstack k arity =
 
 (* Functions over products *)
 
-let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) 
+let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
 let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1))
 
 (* Functions over vfun *)
@@ -383,7 +385,7 @@ let current_fix vf = - (offset (Obj.repr vf) / 2)
 let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
 
 let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
-  
+
 let rec_args vf =
   let fb = first (Obj.repr vf) in
   let size = Obj.size (last fb) in
@@ -391,7 +393,7 @@ let rec_args vf =
 
 exception FALSE
 
-let check_fix f1 f2 = 
+let check_fix f1 f2 =
   let i1, i2 = current_fix f1, current_fix f2 in
   (* Verification du point de depart *)
   if i1 = i2 then
@@ -407,22 +409,22 @@ let check_fix f1 f2 =
 	done;
 	true
       with FALSE -> false
-    else false 
+    else false
   else false
 
 (* Functions over vfix *)
 external atom_rel : unit -> atom array = "get_coq_atom_tbl"
 external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
 
-let relaccu_tbl =  
+let relaccu_tbl =
   let atom_rel = atom_rel() in
   let len = Array.length atom_rel in
   for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
-  ref (Array.init len mkAccuCode) 
+  ref (Array.init len mkAccuCode)
 
 let relaccu_code i =
   let len = Array.length !relaccu_tbl in
-  if i < len then !relaccu_tbl.(i) 
+  if i < len then !relaccu_tbl.(i)
   else
     begin
       realloc_atom_rel i;
@@ -432,7 +434,7 @@ let relaccu_code i =
       relaccu_tbl :=
 	Array.init nl
 	  (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
-      !relaccu_tbl.(i) 
+      !relaccu_tbl.(i)
     end
 
 let reduce_fix k vf =
@@ -441,8 +443,8 @@ let reduce_fix k vf =
   let fc_typ = ((Obj.obj (last fb)) : tcode array) in
   let ndef = Array.length fc_typ in
   let et = offset_closure fb (2*(ndef - 1)) in
-  let ftyp =  
-    Array.map 
+  let ftyp =
+    Array.map
       (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in
   (* Construction de l' environnement des corps des points fixes *)
   let e = Obj.dup fb in
@@ -455,12 +457,12 @@ let reduce_fix k vf =
     let res = Obj.new_block Obj.closure_tag 2 in
     Obj.set_field res 0 (Obj.repr c);
     Obj.set_field res 1 (offset_closure e (2*i));
-    ((Obj.obj res) : vfun)  in 
+    ((Obj.obj res) : vfun)  in
   (Array.init ndef fix_body, ftyp)
- 
+
 (* Functions over vcofix *)
 
-let get_fcofix vcf i = 
+let get_fcofix vcf i =
   match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
   | Vcofix(vcfi, _, _) -> vcfi
   | _ -> assert false
@@ -482,29 +484,29 @@ let check_cofix vcf1 vcf2 =
 let reduce_cofix k vcf =
   let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
   let ndef = Array.length fc_typ in
-  let ftyp =  
+  let ftyp =
     Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
   (* Construction de l'environnement des corps des cofix *)
 
-  let e = Obj.dup (Obj.repr vcf) in 
+  let e = Obj.dup (Obj.repr vcf) in
   for i = 0 to ndef - 1 do
-    Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) 
+    Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
   done;
-   
+
   let cofix_body i =
     let vcfi = get_fcofix vcf i in
     let c = Obj.field (Obj.repr vcfi) 0 in
-    Obj.set_field e 0 c; 
+    Obj.set_field e 0 c;
     let atom = Obj.new_block cofix_tag 1 in
     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_vstack (Obj.obj e) [|Obj.obj self|] in
   (Array.init ndef cofix_body, ftyp)
 
 
 (* Functions over vblock *)
-  
+
 let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b)
 let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b)
 let bfield b i =
@@ -514,15 +516,15 @@ let bfield b i =
 
 (* Functions over vswitch *)
 
-let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl 
-    
+let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl
+
 let case_info sw = sw.sw_annot.ci
-    
-let type_of_switch sw = 
+
+let type_of_switch sw =
   push_vstack sw.sw_stk;
-  interprete sw.sw_type_code crasy_val sw.sw_env 0 
-    
-let branch_arg k (tag,arity) = 
+  interprete sw.sw_type_code crasy_val sw.sw_env 0
+
+let branch_arg k (tag,arity) =
   if arity = 0 then  ((Obj.magic tag):values)
   else
     let b = Obj.new_block tag arity in
@@ -533,38 +535,38 @@ let branch_arg k (tag,arity) =
 
 let apply_switch sw arg =
   let tc = sw.sw_annot.tailcall in
-  if tc then 
+  if tc then
     (push_ra stop;push_vstack sw.sw_stk)
-  else 
+  else
     (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk)));
   interprete sw.sw_code arg sw.sw_env 0
-        
+
 let branch_of_switch k sw =
   let eval_branch (_,arity as ta) =
     let arg = branch_arg k ta in
     let v = apply_switch sw arg in
     (arity, v)
-  in 
+  in
   Array.map eval_branch sw.sw_annot.rtbl
-	
+
 
 (* Evaluation *)
 
 
-let is_accu v = 
+let is_accu v =
   let o = Obj.repr v in
-  Obj.is_block o && Obj.tag o = accu_tag && 
-  fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag 
+  Obj.is_block o && Obj.tag o = accu_tag &&
+  fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag
 
-let rec whd_stack v stk =  
+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 -> 
+  | 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 
+      else
 	let v', stkt =
 	  match stkt with
 	  | Zapp args' :: stkt ->
@@ -573,30 +575,30 @@ let rec whd_stack v stk =
 	      push_val v;
 	      push_arguments args;
 	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f) 
+		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) 
+		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
 		  (nargs args) in
 	      v', stkt
 	in
 	whd_stack v' stkt
-  | Zswitch sw :: 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 = 
+	  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 
+      else whd_stack (apply_switch sw v) stkt
 
 let rec force_whd v stk =
   match whd_stack v stk with