Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 53 insertions, 42 deletions

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index f4dc0b14..c5d483ac 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: cbytecodes.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+
 open Names
 open Term
 
@@ -38,42 +48,43 @@ type instruction =
   | Kpush
   | Kpop of int
   | Kpush_retaddr of Label.t
-  | Kapply of int                       (*  number of arguments *)
-  | Kappterm of int * int               (* number of arguments, slot size *)
-  | Kreturn of int                      (* slot size *)
+  | Kapply of int                       (**  number of arguments *)
+  | Kappterm of int * int               (** number of arguments, slot size *)
+  | Kreturn of int                      (** slot size *)
   | Kjump
   | Krestart
-  | Kgrab of int                        (* number of arguments *)
-  | Kgrabrec of int                     (* rec arg *)
-  | Kclosure of Label.t * int           (* label, number of free variables *)
+  | Kgrab of int                        (** number of arguments *)
+  | Kgrabrec of int                     (** rec arg *)
+  | Kclosure of Label.t * int           (** label, number of free variables *)
   | Kclosurerec of int * int * Label.t array * Label.t array
-                   (* nb fv, init, lbl types, lbl bodies *)
+                   (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
-                   (* nb fv, init, lbl types, lbl bodies *)
+                   (** nb fv, init, lbl types, lbl bodies *)
   | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of int * tag             (* size, tag *)
+  | Kmakeblock of int * tag             (** size, tag *)
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+  | Kswitch of Label.t array * Label.t array (** consts,blocks *)
   | Kpushfields of int
   | Kfield of int
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
-(* spiwack: instructions concerning integers *)
-  | Kbranch of Label.t                  (* jump to label, is it needed ? *)
-  | Kaddint31                           (* adds the int31 in the accu
+
+(** spiwack: instructions concerning integers *)
+  | Kbranch of Label.t                  (** jump to label, is it needed ? *)
+  | Kaddint31                           (** adds the int31 in the accu
                                            and the one ontop of the stack *)
-  | Kaddcint31                          (* makes the sum and keeps the carry *)
-  | Kaddcarrycint31                     (* sum +1, keeps the carry *)
-  | Ksubint31                           (* subtraction modulo *)
-  | Ksubcint31                          (* subtraction, keeps the carry *)
-  | Ksubcarrycint31                     (* subtraction -1, keeps the carry *)
-  | Kmulint31                           (* multiplication modulo *)
-  | Kmulcint31                          (* multiplication, result in two
+  | Kaddcint31                          (** makes the sum and keeps the carry *)
+  | Kaddcarrycint31                     (** sum +1, keeps the carry *)
+  | Ksubint31                           (** subtraction modulo *)
+  | Ksubcint31                          (** subtraction, keeps the carry *)
+  | Ksubcarrycint31                     (** subtraction -1, keeps the carry *)
+  | Kmulint31                           (** multiplication modulo *)
+  | Kmulcint31                          (** multiplication, result in two
 					   int31, for exact computation *)
-  | Kdiv21int31                         (* divides a double size integer
+  | Kdiv21int31                         (** divides a double size integer
                                            (represented by an int31 in the
 					   accumulator and one on the top of
 					   the stack) by an int31. The result
@@ -81,23 +92,23 @@ type instruction =
 					   rest.
 					   If the divisor is 0, it returns
 					   0. *)
-  | Kdivint31                           (* euclidian division (returns a pair
+  | Kdivint31                           (** euclidian division (returns a pair
 					   quotient,rest) *)
-  | Kaddmuldivint31                     (* generic operation for shifting and
+  | Kaddmuldivint31                     (** generic operation for shifting and
 					   cycling. Takes 3 int31 i j and s,
 					   and returns x*2^s+y/(2^(31-s) *)
-  | Kcompareint31                        (* unsigned comparison of int31
+  | Kcompareint31                        (** unsigned comparison of int31
 					   cf COMPAREINT31 in
 					   kernel/byterun/coq_interp.c
 					   for more info *)
-  | Khead0int31                         (* Give the numbers of 0 in head of a in31*)
-  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31
+  | Khead0int31                         (** Give the numbers of 0 in head of a in31*)
+  | Ktail0int31                         (** Give the numbers of 0 in tail of a in31
                                            ie low bits *)
-  | Kisconst of Label.t                 (* conditional jump *)
-  | Kareconst of int*Label.t            (* conditional jump *)
-  | Kcompint31                          (* dynamic compilation of int31 *)
-  | Kdecompint31                        (* dynamix decompilation of int31 *)
-(* /spiwack *)
+  | Kisconst of Label.t                 (** conditional jump *)
+  | Kareconst of int*Label.t            (** conditional jump *)
+  | Kcompint31                          (** dynamic compilation of int31 *)
+  | Kdecompint31                        (** dynamix decompilation of int31 
+   /spiwack *)
 
 
 and bytecodes = instruction list
@@ -107,25 +118,25 @@ type fv_elem = FVnamed of identifier | FVrel of int
 type fv = fv_elem array
 
 
-(* spiwack: this exception is expected to be raised by function expecting
+(** spiwack: this exception is expected to be raised by function expecting
             closed terms. *)
 exception NotClosed
 
 (*spiwack: both type have been moved from Cbytegen because I needed then
   for the retroknowledge *)
 type vm_env = {
-    size : int;              (* longueur de la liste [n] *)
-    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+    size : int;              (** longueur de la liste [n] *)
+    fv_rev : fv_elem list    (** [fvn; ... ;fv1] *)
   }
 
 
 type comp_env = {
-    nb_stack : int;              (* nbre de variables sur la pile          *)
-    in_stack : int list;         (* position dans la pile                  *)
-    nb_rec : int;                (* nbre de fonctions mutuellement         *)
-                                 (* recursives =  nbr                      *)
-    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
-                                 (*  de point fix ou de cofix              *)
+    nb_stack : int;              (** nbre de variables sur la pile          *)
+    in_stack : int list;         (** position dans la pile                  *)
+    nb_rec : int;                (** nbre de fonctions mutuellement         *)
+                                 (** recursives =  nbr                      *)
+    pos_rec  : instruction list; (** instruction d'acces pour les variables *)
+                                 (**  de point fix ou de cofix              *)
     offset : int;
     in_env : vm_env ref
   }
@@ -140,7 +151,7 @@ type block =
   | Bstrconst of structured_constant
   | Bmakeblock of int * block array
   | Bconstruct_app of int * int * int * block array
-                  (* tag , nparams, arity *)
+                  (** tag , nparams, arity *)
   | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
-                (* compilation function (see get_vm_constant_dynamic_info in
+                (** compilation function (see get_vm_constant_dynamic_info in
                    retroknowledge.mli for more info) , argument array  *)