Adds support for the virtual machine to perform reduction of universe polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.

1 files changed, 21 insertions, 10 deletions

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03d638305..c35ef6920 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -22,14 +22,18 @@ 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
 
@@ -64,9 +68,11 @@ 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             (** accu = coq_global_data[c] *)
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *)
+  | 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 *)
@@ -120,7 +126,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
 
@@ -129,26 +138,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_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 *)
-                                 (** recursives =  nbr                      *)
+                                 (** (= 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 dump_bytecode : 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 =