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, 72 insertions, 24 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 46af784dd..b9c1a5a1c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -93,19 +93,6 @@ let construct_of_constr_const env tag typ =
 
 let construct_of_constr_block = construct_of_constr false
 
-let constr_type_of_idkey env idkey =
-  match idkey with
-  | ConstKey cst ->
-    let const_type = Typeops.type_of_constant_in env cst in
-      mkConstU cst, const_type
-  | VarKey id ->
-      let (_,_,ty) = lookup_named id env in
-      mkVar id, ty
-  | RelKey i ->
-      let n = (nb_rel env - i) in
-      let (_,_,ty) = lookup_rel n env in
-      mkRel n, lift n ty
-
 let type_of_ind env (ind, u) =
   type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
 
@@ -164,9 +151,11 @@ and nf_whd env whd typ =
       let t = ta.(i) in
       let _, args = nf_args env vargs t in
       mkApp(cfd,args)
-  | Vconstr_const n -> construct_of_constr_const env n typ
+  | Vconstr_const n ->
+    construct_of_constr_const env n typ
   | Vconstr_block b ->
       let tag = btag b in
+      let x = tag in
       let (tag,ofs) =
         if tag = Cbytecodes.last_variant_tag then
 	  match whd_val (bfield b 0) with
@@ -177,22 +166,80 @@ and nf_whd env whd typ =
       let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
-      let c,typ = constr_type_of_idkey env idkey in
-      nf_stk env c typ stk
-  | Vatom_stk(Aind ind, stk) ->
-      nf_stk env (mkIndU ind) (type_of_ind env ind) stk
+      constr_type_of_idkey env idkey stk nf_stk
+(*let c,typ = constr_type_of_idkey env idkey in
+      nf_stk env c typ stk *)
+  | Vatom_stk(Aind ((mi,i) as ind), stk) ->
+      if Environ.polymorphic_ind ind env then
+	let mib = Environ.lookup_mind mi env in
+	let ulen = Univ.UContext.size mib.mind_universes in
+	match stk with
+	| Zapp args :: stk' ->
+	  assert (ulen <= nargs args) ;
+	  let inst =
+	    Array.init ulen (fun i -> Vm.uni_lvl_val (arg args i))
+	  in
+	  let pind = (ind, Univ.Instance.of_array inst) in
+	  nf_stk ~from:ulen env (mkIndU pind) (type_of_ind env pind) stk
+	| _ -> assert false
+      else
+	let pind = (ind, Univ.Instance.empty) in
+	nf_stk env (mkIndU pind) (type_of_ind env pind) stk
+  | Vatom_stk(Atype u, stk) ->
+    mkSort (Type (Vm.instantiate_universe u stk))
+  | Vuniv_level lvl ->
+    assert false
+
+and constr_type_of_idkey env (idkey : Vars.id_key) stk cont =
+  match idkey with
+  | ConstKey cst ->
+    if Environ.polymorphic_constant cst env then
+      let cbody = Environ.lookup_constant cst env in
+      match stk with
+      | Zapp vargs :: stk' ->
+        let uargs = Univ.UContext.size cbody.const_universes in
+        assert (Vm.nargs vargs >= uargs) ;
+        let uary = Array.init uargs (fun i -> Vm.uni_lvl_val (Vm.arg vargs i)) in
+        let ui = Univ.Instance.of_array uary in
+	let ucst = (cst, ui) in
+	let const_type = Typeops.type_of_constant_in env ucst in
+        if uargs < Vm.nargs vargs then
+	  let t, args = nf_args env vargs ~from:uargs const_type in
+          cont env (mkApp (mkConstU ucst, args)) t stk'
+        else
+          cont env (mkConstU ucst) const_type stk'
+      | _ -> assert false
+    else
+      begin
+	let ucst = (cst, Univ.Instance.empty) in
+	let const_type = Typeops.type_of_constant_in env ucst in
+        cont env (mkConstU ucst) const_type stk
+      end
+  | VarKey id ->
+      let (_,_,ty) = lookup_named id env in
+      cont env (mkVar id) ty stk
+  | RelKey i ->
+      let n = (nb_rel env - i) in
+      let (_,_,ty) = lookup_rel n env in
+      cont env (mkRel n) (lift n ty) stk
 
-and nf_stk env c t stk  =
+and nf_stk ?from:(from=0) env c t stk  =
   match stk with
   | [] -> c
   | Zapp vargs :: stk ->
-      let t, args = nf_args env vargs t in
-      nf_stk env (mkApp(c,args)) t stk
+      if nargs vargs >= from then
+	let t, args = nf_args ~from:from env vargs t in
+	nf_stk env (mkApp(c,args)) t stk
+      else
+	let rest = from - nargs vargs in
+	nf_stk ~from:rest env c t stk
   | Zfix (f,vargs) :: stk ->
+      assert (from = 0) ;
       let fa, typ = nf_fix_app env f vargs in
       let _,_,codom = decompose_prod env typ in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
+      assert (from = 0) ;
       let ((mind,_ as ind), u), allargs = find_rectype_a env t in
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
@@ -215,6 +262,7 @@ and nf_stk env c t stk  =
       let ci = case_info sw in
       nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
   | Zproj p :: stk ->
+     assert (from = 0) ;
      let p' = Projection.make p true in
      let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
      nf_stk env (mkProj(p',c)) ty stk
@@ -240,14 +288,14 @@ and nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
 
-and nf_args env vargs t =
+and nf_args env vargs ?from:(f=0) t =
   let t = ref t in
-  let len = nargs vargs in
+  let len = nargs vargs - f in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (arg vargs i) dom in
+	let c = nf_val env (arg vargs (f+i)) dom in
 	t := subst1 c codom; c) in
   !t,args