Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

1 files changed, 63 insertions, 75 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
index 35032c6b..ceb8ea9c 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: vm.ml 13363 2010-07-30 16:17:24Z barras $ *)
 
 open Names
 open Term
@@ -16,7 +16,7 @@ open Cbytecodes
 external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 
 (******************************************)
-(* Fonctions en plus du module Obj ********)
+(* Utility Functions about Obj ************)
 (******************************************)
 
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
@@ -25,7 +25,7 @@ external offset : Obj.t -> int = "coq_offset"
 let accu_tag = 0
 
 (*******************************************)
-(* Initalisation de la machine abstraite ***)
+(* Initalization of the abstract machine ***)
 (*******************************************)
 
 external init_vm : unit -> unit = "init_coq_vm"
@@ -36,15 +36,13 @@ external transp_values : unit -> bool = "get_coq_transp_value"
 external set_transp_values : bool -> unit = "coq_set_transp_value"
 
 (*******************************************)
-(* Le code machine  ************************)
+(* Machine code *** ************************)
 (*******************************************)
 
 type tcode
 let tcode_of_obj v = ((Obj.obj v):tcode)
 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"
@@ -73,12 +71,12 @@ let popstop_code i =
 let stop = popstop_code 0
 
 (******************************************************)
-(* Types de donnees abstraites et fonctions associees *)
+(* Abstract data types and utility functions **********)
 (******************************************************)
 
 (* Values of the abstract machine *)
 let val_of_obj v = ((Obj.obj v):values)
-let crasy_val = (val_of_obj (Obj.repr 0))
+let crazy_val = (val_of_obj (Obj.repr 0))
 
 (* Abstract data *)
 type vprod
@@ -99,63 +97,60 @@ type vswitch = {
     sw_env : vm_env
   }
 
-(* Representation des types abstraits:                                    *)
-(* + Les produits :                                                       *)
+(* Representation of values *)
+(* + Products : *)
 (*   -   vprod = 0_[ dom | codom]                                         *)
 (*             dom : values, codom : vfun                                 *)
 (*                                                                        *)
-(* + Les fonctions ont deux representations possibles :                   *)
-(*   - fonction non applique :  vf = Ct_[ C | fv1 | ... | fvn]            *)
+(* + Functions have two representations :                                 *)
+(*   - unapplied fun :  vf = Ct_[ C | fv1 | ... | fvn]                    *)
 (*                                       C:tcode, fvi : values            *)
-(*     Remarque : il n'y a pas de difference entre la fct et son          *)
-(*                environnement.                                          *)
-(*   - Application partielle  : Ct_[Restart:C| vf | arg1 | ... argn]      *)
+(*     Remark : a function and its environment is the same value.         *)
+(*   - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn]       *)
 (*                                                                        *)
-(* + Les points fixes :                                                   *)
+(* + Fixpoints :                                                          *)
 (*   -        Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn]               *)
-(*     Remarque il n'y a qu'un seul block pour representer tout les       *)
-(*     points fixes d'une declaration mutuelle, chaque point fixe         *)
-(*     pointe sur la position de son code dans le block.                  *)
-(*   - L'application partielle d'un point fixe suit le meme schema        *)
-(*     que celui des fonctions                                            *)
-(*     Remarque seul les points fixes qui n'ont pas encore recu leur      *)
-(*     argument recursif sont encode de cette maniere (si l'argument      *)
-(*     recursif etait un constructeur le point fixe se serait reduit      *)
-(*     sinon il est represente par un accumulateur)                       *)
+(*     One single block to represent all of the fixpoints, each fixpoint  *)
+(*     is the pointer to the field holding the pointer to its code, and   *)
+(*     the infix tag is used to know where the block starts.              *)
+(*   - Partial application follows the scheme of partially applied        *)
+(*     functions. Note: only fixpoints not having been applied to its     *)
+(*     recursive argument are coded this way. When the rec. arg. is       *)
+(*     applied, either it's a constructor and the fix reduces, or it's    *)
+(*     and the fix is coded as an accumulator.                            *)
 (*                                                                        *)
-(* + Les cofix sont expliques dans cbytegen.ml                            *)
+(* + Cofixpoints : see cbytegen.ml                                        *)
 (*                                                                        *)
-(* + Les vblock encodent les constructeurs (non constant) de caml,        *)
-(*   la difference est que leur tag commence a 1 (0 est reserve pour les  *)
-(*   accumulateurs : accu_tag)                                            *)
+(* + vblock's encode (non constant) constructors as in Ocaml, but         *)
+(*   starting from 0 up. tag 0 ( = accu_tag) is reserved for              *)
+(*   accumulators.                                                        *)
 (*                                                                        *)
-(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *)
+(* + vm_env is the type of the machine environments (i.e. a function or   *)
+(*   a fixpoint)                                                          *)
 (*                                                                        *)
-(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ]       *)
-(*   - representation des [accu] : tag_[....]                             *)
-(*     -- tag <= 2 : encodage du type atom                                *)
-(*     -- 3_[accu|fix_app] : un point fixe bloque par un accu             *)
-(*     -- 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    *)
-(* Le type [arguments] est utiliser de maniere abstraite comme un         *)
-(* tableau, il represente la structure de donnee suivante :               *)
+(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
+(*   - representation of [accu] : tag_[....]                              *)
+(*     -- tag <= 2 : encoding atom type (sorts, free vars, etc.)          *)
+(*     -- 3_[accu|fix_app] : a fixpoint blocked by an accu                *)
+(*     -- 4_[accu|vswitch] : a match blocked by an accu                   *)
+(*     -- 5_[fcofix]       : a cofix function                             *)
+(*     -- 6_[fcofix|val]   : a cofix function, val represent the value    *)
+(*        of the function applied to arg1 ... argn                        *)
+(* The [arguments] type, which is abstracted as an array, represents :    *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
-(* Generalement le 1er champs est un pointeur de code                     *)
+(* Generally the first field is a code pointer.                           *)
 
-(* Ne pas changer ce type sans modifier le code C, *)
-(* en particulier le fichier "coq_values.h"        *)
+(* Do not edit this type without editing C code, especially "coq_values.h" *)
 type atom =
   | Aid of id_key
   | Aiddef of id_key * values
   | Aind of inductive
 
-(* Les zippers *)
+(* Zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (* Peut-etre vide *)
+  | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -193,28 +188,20 @@ let rec whd_accu a stk =
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
   | 5 (* cofix_tag *) ->
+      let vcfx = Obj.obj (Obj.field at 0) in
+      let to_up = Obj.obj a in
       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)
-      | [Zapp args] ->
-	  let vcfx = Obj.obj (Obj.field at 0) in
-	  let to_up = Obj.obj a in
-	  Vcofix(vcfx, to_up, Some args)
+      | []          -> Vcofix(vcfx, to_up, None)
+      | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
   | 6 (* cofix_evaluated_tag *) ->
+      let vcofix = Obj.obj (Obj.field at 0) in
+      let res = Obj.obj a in
       begin match stk with
-      | [] ->
-	  let vcofix = Obj.obj (Obj.field at 0) in
-	  let res = Obj.obj a in
-	  Vcofix(vcofix, res, None)
-      | [Zapp args] ->
-	  let vcofix = Obj.obj (Obj.field at 0) in
-	  let res = Obj.obj a in
-	  Vcofix(vcofix, res, Some args)
-      | _ -> assert false
+      | []          -> Vcofix(vcofix, res, None)
+      | [Zapp args] -> Vcofix(vcofix, res, Some args)
+      | _           -> assert false
       end
   | _ -> assert false
 
@@ -245,7 +232,7 @@ let whd_val : values -> whd =
 
 
 (************************************************)
-(* La machine abstraite *************************)
+(* Abstrct machine ******************************)
 (************************************************)
 
 (* gestion de la pile *)
@@ -291,7 +278,7 @@ let apply_vstack vf vstk =
     end
 
 (**********************************************)
-(* Constructeurs ******************************)
+(* Constructors *******************************)
 (**********************************************)
 
 let obj_of_atom : atom -> Obj.t =
@@ -349,11 +336,11 @@ let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
 
+
 (*************************************************)
-(** Operations pour la manipulation des donnees **)
+(** Operations manipulating data types ***********)
 (*************************************************)
 
-
 (* Functions over products *)
 
 let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0)
@@ -395,13 +382,13 @@ exception FALSE
 
 let check_fix f1 f2 =
   let i1, i2 = current_fix f1, current_fix f2 in
-  (* Verification du point de depart *)
+  (* Checking starting point *)
   if i1 = i2 then
     let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
     let n = Obj.size (last fb1) in
-    (* Verification du nombre de definition *)
+    (* Checking number of definitions *)
     if n = Obj.size (last fb2) then
-      (* Verification des arguments recursifs *)
+      (* Checking recursive arguments *)
       try
 	for i = 0 to n - 1 do
 	  if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
@@ -439,14 +426,14 @@ let relaccu_code i =
 
 let reduce_fix k vf =
   let fb = first (Obj.repr vf) in
-  (* calcul des types *)
+  (* computing types *)
   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
-      (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in
-  (* Construction de l' environnement des corps des points fixes *)
+      (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in
+  (* Construction of the environment of fix bodies *)
   let e = Obj.dup fb in
   for i = 0 to ndef - 1 do
     Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
@@ -485,9 +472,10 @@ 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 =
-    Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
-  (* Construction de l'environnement des corps des cofix *)
+    (* Evaluate types *)
+    Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in
 
+  (* Construction of the environment of cofix bodies *)
   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)))
@@ -522,7 +510,7 @@ let case_info sw = sw.sw_annot.ci
 
 let type_of_switch sw =
   push_vstack sw.sw_stk;
-  interprete sw.sw_type_code crasy_val sw.sw_env 0
+  interprete sw.sw_type_code crazy_val sw.sw_env 0
 
 let branch_arg k (tag,arity) =
   if arity = 0 then  ((Obj.magic tag):values)