Refine Gregory Malecha's patch on VM and universe polymorphism.

- Universes are now represented in the VM by a structured constant containing the
  global levels. This constant is applied to local level variables if any.
- When reading back a universe, we perform the union of these levels and return
  a [Vsort].
- Fixed a bug: structured constants could contain local universe variables in
  constructor arguments, which has to be prevented.
  Was showing up for instance when evaluating [cons _ list (nil _)] with
  a polymorphic [list] type.
- Fixed a bug: polymorphic inductive types can have an empty stack.
  Was showing up when evaluating [bool] with a polymorphic [bool] type.
- Made a few cosmetic changes.

Patch written with Benjamin Grégoire.

7 files changed, 124 insertions, 143 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index b13b0607b..0a24a75d6 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -19,6 +19,7 @@ type tag = int
 
 let accu_tag = 0
 
+let type_atom_tag = 2
 let max_atom_tag = 2
 let proj_tag = 3
 let fix_app_tag = 4
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index c35ef6920..03ae6b9cd 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -15,6 +15,7 @@ type tag = int
 
 val accu_tag : tag
 
+val type_atom_tag : tag
 val max_atom_tag : tag
 val proj_tag : tag
 val fix_app_tag : tag
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index f9f72efdb..1f7cc3c7a 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -91,6 +91,7 @@ open Pre_env
 (* In Cfxe_t accumulators, we need to store [fcofixi] for testing         *)
 (* conversion of cofixpoints (which is intentional).                      *)
 
+type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
 
 let empty_fv = { size= 0;  fv_rev = [] }
 
@@ -218,21 +219,6 @@ let pos_rel i r sz =
 	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
 	Kenvacc(r.offset + pos)
 
-(*
-let pos_poly_inst idu r =
-  let env = !(r.in_env) in
-  let f = function
-    | FVpoly_inst i -> Univ.eq_puniverses Names.Constant.equal idu i
-    | _ -> false
-  in
-  try  Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
-  with Not_found ->
-    let pos = env.size in
-    let db = FVpoly_inst idu in
-    r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
-    Kenvacc(r.offset + pos)
-*)
-
 let pos_universe_var i r sz =
   if i < r.nb_uni_stack then
     Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
@@ -494,9 +480,9 @@ let rec str_const c =
               end
 	| _ -> Bconstr c
       end
-  | Ind (ind,_) ->
+  | Ind (ind,u) when Univ.Instance.is_empty u ->
     Bstrconst (Const_ind ind)
-  | Construct (((kn,j),i),u) ->  
+  | Construct (((kn,j),i),_) ->
       begin
       (* spiwack: tries first to apply the run-time compilation
            behavior of the constructor, as in 2/ above *)
@@ -571,10 +557,6 @@ let rec get_alias env kn =
 	| BCalias kn' -> get_alias env kn'
 	| _ -> kn)
 
-(* Compiling expressions *)
-
-type ('a,'b) sum = Inl of 'a | Inr of 'b
-
 (* sz is the size of the local stack *)
 let rec compile_constr reloc c sz cont =
   match kind_of_term c with
@@ -592,39 +574,43 @@ let rec compile_constr reloc c sz cont =
   | Rel i -> pos_rel i reloc sz :: cont
   | Var id -> pos_named id reloc :: cont
   | Const (kn,u) -> compile_const reloc kn u [||] sz cont
-  | Ind (i,u) ->
+  | Ind (ind,u) ->
+     let bcst = Bstrconst (Const_ind ind) in
     if Univ.Instance.is_empty u then
-      compile_str_cst reloc (str_const c) sz cont
+      compile_str_cst reloc bcst sz cont
     else
       comp_app compile_str_cst compile_universe reloc
-	   (str_const c)
+	   bcst
 	   (Univ.Instance.to_array u)
 	   sz
 	   cont
   | Sort (Prop _) | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
   | Sort (Type u) ->
-    begin
-      let levels = Univ.Universe.levels u in
-      if Univ.LSet.exists (fun x -> Univ.Level.var_index x <> None) levels
-      then
-        (** TODO(gmalecha): Fix this **)
-        (** NOTE: This relies on the order of iteration to be consistent
-         **)
-	let level_vars =
-	  List.map_filter (fun x -> Univ.Level.var_index x)
-	    (Univ.LSet.elements levels)
-	in
-        let compile_get_univ reloc idx sz cont =
+     (* We separate global and local universes in [u]. The former will be part
+        of the structured constant, while the later (if any) will be applied as
+        arguments. *)
+     let open Univ in begin
+      let levels = Universe.levels u in
+      let global_levels =
+	LSet.filter (fun x -> Level.var_index x = None) levels
+      in
+      let local_levels =
+	List.map_filter (fun x -> Level.var_index x)
+	  (LSet.elements levels)
+      in
+      (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
+      let uglob =
+	LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
+      in
+      if local_levels = [] then
+	compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont
+      else
+	let compile_get_univ reloc idx sz cont =
 	  compile_fv_elem reloc (FVuniv_var idx) sz cont
 	in
         comp_app compile_str_cst compile_get_univ reloc
-	   (Bstrconst (Const_type u))
-	   (Array.of_list level_vars)
-	   sz
-	   cont
-      else
-	compile_str_cst reloc (str_const c) sz cont
+	  (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
     end
   | LetIn(_,xb,_,body) ->
       compile_constr reloc xb sz
@@ -831,8 +817,7 @@ and compile_universe reloc uni sz cont =
   | None -> Kconst (Const_univ_level uni) :: cont
   | Some idx -> pos_universe_var idx reloc sz :: cont
 
-and compile_const =
-  fun reloc-> fun  kn u -> fun args -> fun sz -> fun cont ->
+and compile_const reloc kn u args sz cont =
   let nargs = Array.length args in
   (* spiwack: checks if there is a specific way to compile the constant
               if there is not, Not_found is raised, and the function
@@ -850,18 +835,19 @@ and compile_const =
             compile_get_global reloc (kn,u) sz cont)
           compile_constr reloc () args sz cont
       else
-        let compile_either reloc constr_or_uni sz cont =
+        let compile_arg reloc constr_or_uni sz cont =
           match constr_or_uni with
-          | Inl cst -> compile_constr reloc cst sz cont
-          | Inr uni -> compile_universe reloc uni sz cont
-        in
-        (** TODO(gmalecha): This can be more efficient **)
-        let all =
-          Array.of_list (List.map (fun x -> Inr x) (Array.to_list (Univ.Instance.to_array u)) @
-                         List.map (fun x -> Inl x) (Array.to_list args))
+          | ArgConstr cst -> compile_constr reloc cst sz cont
+          | ArgUniv uni -> compile_universe reloc uni sz cont
         in
+	let u = Univ.Instance.to_array u in
+	let lu = Array.length u in
+	let all =
+	  Array.init (lu + Array.length args) 
+	    (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu))
+	in
         comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
-          compile_either reloc () all sz cont
+          compile_arg reloc () all sz cont
 
 let is_univ_copy max u =
   let u = Univ.Instance.to_array u in
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2a70d0b1b..ef0c9af4f 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -307,7 +307,7 @@ type to_patch = emitcodes * (patch list) * fv
 (* Substitution *)
 let rec subst_strcst s sc =
   match sc with
-  | Const_sorts _ | Const_b0 _ -> sc
+  | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> 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 -> let kn,i = ind in Const_ind (subst_mind s kn, i)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2e519789e..4610dbcb0 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -98,6 +98,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
           let mib = Environ.lookup_mind mi env in
 	  let ulen = Univ.UContext.size mib.Declarations.mind_universes in
           match stk1 , stk2 with
+	  | [], [] -> assert (Int.equal ulen 0); cu
 	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
 	     assert (ulen <= nargs args1);
              assert (ulen <= nargs args2);
@@ -108,7 +109,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 	     let cu = convert_instances ~flex:false u1 u2 cu in
              conv_arguments env ~from:ulen k args1 args2
 			    (conv_stack env k stk1' stk2' cu)
-	  | _ -> raise NotConvertible
+	  | _, _ -> assert false (* Should not happen if problem is well typed *)
         else
 	  conv_stack env k stk1 stk2 cu
       else raise NotConvertible
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 858f546c6..64ddc4376 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -162,16 +162,96 @@ type whd =
   | Vatom_stk of atom * stack
   | Vuniv_level of Univ.universe_level
 
+(************************************************)
+(* Abstract machine *****************************)
+(************************************************)
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+  "coq_interprete_ml"
+
+
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i =
+  if  0 <= i && i < (nargs args) then
+    val_of_obj (Obj.field (Obj.repr args) (i+2))
+  else invalid_arg
+		("Vm.arg size = "^(string_of_int (nargs args))^
+		 " acces "^(string_of_int i))
+
+(* Apply a value to arguments contained in [vargs] *)
+let apply_arguments vf vargs =
+  let n = nargs vargs in
+  if Int.equal n 0 then vf
+  else
+   begin
+     push_ra stop;
+     push_arguments vargs;
+     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+   end
+
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+  let n = Array.length varray in
+  if Int.equal n 0 then vf
+  else
+    begin
+      push_ra stop;
+      push_vstack varray;
+      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+    end
+
 (*************************************************)
 (* Destructors ***********************************)
 (*************************************************)
 
+let uni_lvl_val (v : values) : Univ.universe_level =
+    let whd = Obj.magic v in
+    match whd with
+    | Vuniv_level lvl -> lvl
+    | _ ->
+      let pr =
+        let open Pp in
+        match whd with
+        | Vsort _ -> str "Vsort"
+        | Vprod _ -> str "Vprod"
+        | Vfun _ -> str "Vfun"
+        | Vfix _ -> str "Vfix"
+        | Vcofix _ -> str "Vcofix"
+        | Vconstr_const i -> str "Vconstr_const"
+        | Vconstr_block b -> str "Vconstr_block"
+        | Vatom_stk (a,stk) -> str "Vatom_stk"
+        | _ -> assert false
+      in
+      Errors.anomaly
+        Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
+            ++ pr)
+
 let rec whd_accu a stk =
   let stk =
     if Int.equal (Obj.size a) 2 then stk
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
+  | i when Int.equal i type_atom_tag ->
+     begin match stk with
+     | [Zapp args] ->
+	let u = ref (Obj.obj (Obj.field at 0)) in
+	for i = 0 to nargs args - 1 do
+	  u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
+	done;
+	Vsort (Type !u)
+     | _ -> assert false
+     end
   | i when i <= max_atom_tag ->
       Vatom_stk(Obj.magic at, stk)
   | i when Int.equal i proj_tag ->
@@ -230,77 +310,6 @@ let whd_val : values -> whd =
 	else
            Vconstr_block(Obj.obj o)
 
-let uni_lvl_val : values -> Univ.universe_level =
-  fun v ->
-    let whd = Obj.magic v in
-    match whd with
-    | Vuniv_level lvl -> lvl
-    | _ ->
-      let pr =
-        let open Pp in
-        match whd with
-        | Vsort _ -> str "Vsort"
-        | Vprod _ -> str "Vprod"
-        | Vfun _ -> str "Vfun"
-        | Vfix _ -> str "Vfix"
-        | Vcofix _ -> str "Vcofix"
-        | Vconstr_const i -> str "Vconstr_const"
-        | Vconstr_block b -> str "Vconstr_block"
-        | Vatom_stk (a,stk) -> str "Vatom_stk"
-        | _ -> assert false
-      in
-      Errors.anomaly
-        Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
-            ++ pr)
-
-(************************************************)
-(* Abstract machine *****************************)
-(************************************************)
-
-(* gestion de la pile *)
-external push_ra : tcode -> unit = "coq_push_ra"
-external push_val : values -> unit = "coq_push_val"
-external push_arguments : arguments -> unit = "coq_push_arguments"
-external push_vstack : vstack -> unit = "coq_push_vstack"
-
-
-(* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
-  "coq_interprete_ml"
-
-
-
-(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i =
-  if  0 <= i && i < (nargs args) then
-    val_of_obj (Obj.field (Obj.repr args) (i+2))
-  else invalid_arg
-		("Vm.arg size = "^(string_of_int (nargs args))^
-		 " acces "^(string_of_int i))
-
-(* Apply a value to arguments contained in [vargs] *)
-let apply_arguments vf vargs =
-  let n = nargs vargs in
-  if Int.equal n 0 then vf
-  else
-   begin
-     push_ra stop;
-     push_arguments vargs;
-     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
-   end
-
-(* Apply value [vf] to an array of argument values [varray] *)
-let apply_varray vf varray =
-  let n = Array.length varray in
-  if Int.equal n 0 then vf
-  else
-    begin
-      push_ra stop;
-      push_vstack varray;
-      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
-    end
-
 (**********************************************)
 (* Constructors *******************************)
 (**********************************************)
@@ -637,22 +646,6 @@ let apply_whd k whd =
       apply_stack (val_of_atom a) stk v 
   | Vuniv_level lvl -> assert false
 
-let instantiate_universe (u : Univ.universe) (stk : stack) : Univ.universe =
-  match stk with
-  | [] -> u
-  | [Zapp args] ->
-    assert (Univ.LSet.cardinal (Univ.Universe.levels u) = nargs args) ;
-    let _,mp = Univ.LSet.fold (fun key (i,mp) ->
-	let u = uni_lvl_val (arg args i) in
-        (i+1, Univ.LMap.add key (Univ.Universe.make u) mp))
-	(Univ.Universe.levels u)
-        (0,Univ.LMap.empty) in
-    let subst = Univ.make_subst mp in
-    Univ.subst_univs_universe subst u
-  | _ ->
-    Errors.anomaly Pp.(str "ill-formed universe")
-
-
 let rec pr_atom a =
   Pp.(match a with
   | Aid c -> str "Aid(" ++ (match c with
diff --git a/kernel/vm.mli b/kernel/vm.mli
index bc1978663..43a42eb9c 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -64,7 +64,6 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
 
 val whd_val : values -> whd
 val uni_lvl_val : values -> Univ.universe_level
-val instantiate_universe : Univ.universe -> stack -> Univ.universe
 
 (** Arguments *)