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, 9 insertions, 14 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 9b275cb6c3..2a70d0b1b7 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -19,7 +19,7 @@ open Mod_subst
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of pconstant
+  | Reloc_getglobal of Names.constant
 
 type patch = reloc_info * int
 
@@ -127,11 +127,11 @@ let slot_for_const c =
   enter (Reloc_const c);
   out_int 0
 
-and slot_for_annot a =
+let slot_for_annot a =
   enter (Reloc_annot a);
   out_int 0
 
-and slot_for_getglobal p =
+let slot_for_getglobal p =
   enter (Reloc_getglobal p);
   out_int 0
 
@@ -190,7 +190,7 @@ let emit_instr = function
       Array.iter (out_label_with_orig org) lbl_bodies
   | Kgetglobal q ->
       out opGETGLOBAL; slot_for_getglobal q
-  | Kconst((Const_b0 i)) ->
+  | Kconst (Const_b0 i) ->
       if i >= 0 && i <= 3
           then out (opCONST0 + i)
           else (out opCONSTINT; out_int i)
@@ -310,7 +310,7 @@ let rec subst_strcst s sc =
   | Const_sorts _ | Const_b0 _ -> sc
   | Const_proj p -> Const_proj (subst_constant s p)
   | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
-  | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
+  | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_patch s (ri,pos) =
   match ri with
@@ -319,7 +319,7 @@ let subst_patch s (ri,pos) =
       let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
 
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
@@ -328,12 +328,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of pconstant
+  | BCalias of Names.constant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCalias of pconstant substituted
+| PBCalias of Names.constant substituted
 | PBCconstant
 
 let from_val = function
@@ -343,7 +343,7 @@ let from_val = function
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCalias cu -> BCalias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
@@ -373,8 +373,3 @@ let to_memory (init_code, fun_code, fv) =
     | Label_undefined patchlist ->
 	assert (patchlist = []))) !label_table;
   (code, reloc, fv)
-
-
-
-
-