Imported Upstream version 8.5~beta3+dfsg

1 files changed, 43 insertions, 28 deletions

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index fbb40ffd..03ae6b9c 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -13,20 +13,28 @@ open Term
 
 type tag = int
 
-val id_tag : tag
-val iddef_tag : tag
-val ind_tag : tag
-val fix_tag : tag
+val accu_tag : tag
+
+val type_atom_tag : tag
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
-val last_variant_tag : tag 
+
+val last_variant_tag : tag
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of pinductive
+  | Const_ind of inductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
+  | Const_univ_level of Univ.universe_level
+  | Const_type of Univ.universe
+
+val pp_struct_const : structured_constant -> Pp.std_ppcmds
 
 type reloc_table = (tag * int) array
 
@@ -43,13 +51,13 @@ module Label :
 
 type instruction =
   | Klabel of Label.t
-  | Kacc of int
-  | Kenvacc of int
-  | Koffsetclosure of int
-  | Kpush
-  | Kpop of int
-  | Kpush_retaddr of Label.t
-  | Kapply of int                       (**  number of arguments *)
+  | Kacc of int                         (** accu = sp[n] *)
+  | Kenvacc of int                      (** accu = coq_env[n] *)
+  | Koffsetclosure of int               (** accu = &coq_env[n] *)
+  | Kpush                               (** sp = accu :: sp *)
+  | Kpop of int                         (** sp = skipn n sp *)
+  | Kpush_retaddr of Label.t            (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+  | Kapply of int                       (** number of arguments (arguments on top of stack) *)
   | Kappterm of int * int               (** number of arguments, slot size *)
   | Kreturn of int                      (** slot size *)
   | Kjump
@@ -61,17 +69,21 @@ type instruction =
                    (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of pconstant
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of int * tag             (** size, tag *)
+  | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
+                                         ** is accu, all others are popped from
+					 ** the top of the stack  *)
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array (** consts,blocks *)
   | Kpushfields of int
-  | Kfield of int
-  | Ksetfield of int
+  | Kfield of int                       (** accu = accu[n] *)
+  | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (** index of the projected argument,
+                                            name of projection *)
 
 (** spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (** jump to label, is it needed ? *)
@@ -115,7 +127,10 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+  FVnamed of Id.t
+| FVrel of int
+| FVuniv_var of int
 
 type fv = fv_elem array
 
@@ -124,28 +139,28 @@ type fv = fv_elem array
             closed terms. *)
 exception NotClosed
 
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Cbytegen because I needed them
   for the retroknowledge *)
 type vm_env = {
-    size : int;              (** longueur de la liste [n] *)
+    size : int;              (** length of the list [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                      *)
+    nb_uni_stack : int ;         (** number of universes on the stack       *)
+    nb_stack : int;              (** number of variables on the stack       *)
+    in_stack : int list;         (** position in the stack                  *)
+    nb_rec : int;                (** number of mutually recursive functions *)
+                                 (** (= nbr)                                *)
     pos_rec  : instruction list; (** instruction d'acces pour les variables *)
                                  (**  de point fix ou de cofix              *)
     offset : int;
-    in_env : vm_env ref
+    in_env : vm_env ref          (** the variables that are accessed        *)
   }
 
-val draw_instr : bytecodes -> unit
-
-
+val pp_bytecodes : bytecodes -> Pp.std_ppcmds
+val pp_fv_elem : fv_elem -> Pp.std_ppcmds
 
 (*spiwack: moved this here because I needed it for retroknowledge *)
 type block =