From 7002b3daca6da29eadf80019847630b8583c3daf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 3 Aug 2014 20:02:49 +0200
Subject: Move to a representation of universe polymorphic constants using
 indices for variables. Simplifies instantiation of constants/inductives,
 requiring less allocation and Map.find's. Abstraction by variables is handled
 mostly inside the kernel but could be moved outside.

---
 kernel/cooking.ml      | 40 ++++++++++++++++------
 kernel/declareops.ml   | 20 +++++++++--
 kernel/declareops.mli  |  1 +
 kernel/environ.ml      | 32 +++++++----------
 kernel/fast_typeops.ml |  3 +-
 kernel/indtypes.ml     | 15 ++++++--
 kernel/inductive.ml    | 84 +++++++++++----------------------------------
 kernel/inductive.mli   |  5 +--
 kernel/opaqueproof.ml  |  2 +-
 kernel/opaqueproof.mli |  2 +-
 kernel/safe_typing.ml  |  9 -----
 kernel/term_typing.ml  | 59 +++++++++++++++++++-------------
 kernel/typeops.ml      |  7 ++--
 kernel/univ.ml         | 93 ++++++++++++++++++++++++++++++++++++++++++--------
 kernel/univ.mli        | 25 +++++++++-----
 kernel/vars.ml         | 41 ++++++++++++++++++++++
 kernel/vars.mli        |  4 +++
 17 files changed, 272 insertions(+), 170 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5fa01e5db2..589a261342 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -165,18 +165,37 @@ let constr_of_def = function
   | Def cs -> Mod_subst.force_constr cs
   | OpaqueDef lc -> Opaqueproof.force_proof lc
 
+let expmod_constr_subst cache modlist subst c =
+  let c = expmod_constr cache modlist c in
+    Vars.subst_univs_level_constr subst c
 
 let cook_constr { Opaqueproof.modlist ; abstract } c =
   let cache = RefTable.create 13 in
-  let hyps = Context.map_named_context (expmod_constr cache modlist) (fst abstract) in
-  abstract_constant_body (expmod_constr cache modlist c) hyps
+  let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
+  let hyps = Context.map_named_context expmod (pi1 abstract) in
+  abstract_constant_body (expmod c) hyps
+
+let lift_univs cb subst =
+  if cb.const_polymorphic then
+    let inst = Univ.UContext.instance cb.const_universes in
+    let cstrs = Univ.UContext.constraints cb.const_universes in
+    let len = Univ.LMap.cardinal subst in
+    let subst = 
+      Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
+	subst (Univ.Instance.to_array inst)
+    in
+    let cstrs' = Univ.subst_univs_level_constraints subst cstrs in
+      subst, Univ.UContext.make (inst,cstrs')
+  else subst, cb.const_universes
 
 let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
   let cache = RefTable.create 13 in
-  let abstract, abs_ctx = abstract in 
-  let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
-  let body = on_body modlist (hyps, abs_ctx)
-    (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps)
+  let abstract, usubst, abs_ctx = abstract in
+  let usubst, univs = lift_univs cb usubst in
+  let expmod = expmod_constr_subst cache modlist usubst in
+  let hyps = Context.map_named_context expmod abstract in
+  let body = on_body modlist (hyps, usubst, abs_ctx)
+    (fun c -> abstract_constant_body (expmod c) hyps)
     cb.const_body
   in
   let const_hyps =
@@ -186,17 +205,16 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
   let typ = match cb.const_type with
     | RegularArity t ->
   	let typ =
-          abstract_constant_type (expmod_constr cache modlist t) hyps in
+          abstract_constant_type (expmod t) hyps in
   	RegularArity typ
     | TemplateArity (ctx,s) ->
   	let t = mkArity (ctx,Type s.template_level) in
-  	let typ =
-          abstract_constant_type (expmod_constr cache modlist t) hyps in
+  	let typ = abstract_constant_type (expmod t) hyps in
   	let j = make_judge (constr_of_def body) typ in
   	Typeops.make_polymorphic_if_constant_for_ind env j
   in
   let projection pb =
-    let c' = abstract_constant_body (expmod_constr cache modlist pb.proj_body) hyps in
+    let c' = abstract_constant_body (expmod pb.proj_body) hyps in
     let ((mind, _), _), n' =
       try 
 	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
@@ -213,7 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs = UContext.union abs_ctx cb.const_universes in
+  let univs = UContext.union abs_ctx univs in
     (body, typ, Option.map projection cb.const_proj, 
      cb.const_polymorphic, univs, cb.const_inline_code, 
      Some const_hyps)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 4524b55bb1..f583bff64d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -37,10 +37,22 @@ let hcons_template_arity ar =
 
 (** {6 Constants } *)
 
+let instantiate cb c =
+  if cb.const_polymorphic then 
+    Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
+  else c
+
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
-  | Def c -> Some (force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof o)
+  | Def c -> Some (instantiate cb (force_constr c))
+  | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof o))
+
+let type_of_constant cb =
+  match cb.const_type with
+  | RegularArity t as x -> 
+    let t' = instantiate cb t in
+      if t' == t then x else RegularArity t'
+  | TemplateArity _ as x -> x
 
 let constraints_of_constant cb = Univ.Constraint.union 
   (Univ.UContext.constraints cb.const_universes)
@@ -57,7 +69,9 @@ let universes_of_constant cb =
       (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
 
 let universes_of_polymorphic_constant cb = 
-  if cb.const_polymorphic then universes_of_constant cb
+  if cb.const_polymorphic then 
+    let univs = universes_of_constant cb in
+      Univ.instantiate_univ_context univs
   else Univ.UContext.empty
 
 let constant_has_body cb = match cb.const_body with
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 6c43bffa9e..04a067aff0 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -29,6 +29,7 @@ val constant_has_body : constant_body -> bool
     Only use this function if you know what you're doing. *)
 
 val body_of_constant : constant_body -> Term.constr option
+val type_of_constant : constant_body -> constant_type
 val constraints_of_constant : constant_body -> Univ.constraints
 val universes_of_constant : constant_body -> Univ.universe_context
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 48a7964c3e..2a4f3a9485 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -212,13 +212,9 @@ let add_constant_key kn cb linkinfo env =
 let add_constant kn cb env =
   add_constant_key kn cb (no_link_info ()) env
 
-let universes_of cb = 
-  cb.const_universes
-
-let universes_and_subst_of cb u =
-  let univs = universes_of cb in
-  let subst = Univ.make_universe_subst u univs in
-    subst, Univ.instantiate_univ_context subst univs
+let constraints_of cb u =
+  let univs = cb.const_universes in
+    Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
@@ -230,8 +226,8 @@ let map_regular_arity f = function
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst, csts = universes_and_subst_of cb u in
-	(map_regular_arity (subst_univs_level_constr subst) cb.const_type, csts)
+      let csts = constraints_of cb u in
+	(map_regular_arity (subst_instance_constr u) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
 let constant_context env kn =
@@ -249,8 +245,8 @@ let constant_value env (kn,u) =
       match cb.const_body with
       | Def l_body -> 
 	if cb.const_polymorphic then
-	  let subst, csts = universes_and_subst_of cb u in
-	    (subst_univs_level_constr subst (Mod_subst.force_constr l_body), csts)
+	  let csts = constraints_of cb u in
+	    (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
 	else Mod_subst.force_constr l_body, Univ.Constraint.empty
       | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
       | Undef _ -> raise (NotEvaluableConst NoBody)
@@ -263,13 +259,13 @@ let constant_opt_value env cst =
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst, cst = universes_and_subst_of cb u in
+      let cst = constraints_of cb u in
       let b' = match cb.const_body with
-	| Def l_body -> Some (subst_univs_level_constr subst (Mod_subst.force_constr l_body))
+	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_univs_level_constr subst) cb.const_type, cst
+	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -285,8 +281,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then
-      let subst = Univ.make_universe_subst u cb.const_universes in
-	map_regular_arity (subst_univs_level_constr subst) cb.const_type
+      map_regular_arity (subst_instance_constr u) cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -294,10 +289,7 @@ let constant_value_in env (kn,u) =
   match cb.const_body with
     | Def l_body -> 
       let b = Mod_subst.force_constr l_body in
-	if cb.const_polymorphic then
-	  let subst = Univ.make_universe_subst u cb.const_universes in
-	    subst_univs_level_constr subst b
-	else b
+	subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 83f1e74baf..a88302e047 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -302,8 +302,7 @@ let judge_of_projection env p c ct =
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
     assert(eq_mind pb.proj_ind (fst ind));
-    let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
+    let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
       substl (c :: List.rev args) ty
       
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 89d2d7b671..ff5ce284e7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -683,12 +683,20 @@ let compute_expansion ((kn, _ as ind), u) params ctx =
 let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
-  let hyps =  used_section_variables env inds in
+  let hyps = used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
   let nparamdecls = rel_context_length params in
+  let subst, ctx = Univ.abstract_universes p ctx in
+  let params = Vars.subst_univs_level_context subst params in
+  let env_ar = 
+    let ctx = Environ.rel_context env_ar in 
+    let ctx' = Vars.subst_univs_level_context subst ctx in
+      Environ.push_rel_context ctx' env
+  in
   (* Check one inductive *)
   let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
+    let lc = Array.map (Vars.subst_univs_level_constr subst) lc in
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let consnrealdecls =
@@ -707,7 +715,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	let s = sort_of_univ defs in
 	let kelim = allowed_sorts info s in
 	let ar = RegularArity 
-	  { mind_user_arity = ar; mind_sort = s; } in
+	  { mind_user_arity = Vars.subst_univs_level_constr subst ar; 
+	    mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in
 	  ar, kelim in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
@@ -726,7 +735,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       (* Build the inductive packet *)
       { mind_typename = id;
 	mind_arity = arkind;
-	mind_arity_ctxt = ar_sign;
+	mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
 	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 163bc3a42a..dfed980714 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -50,28 +50,22 @@ let find_coinductive env c =
 
 let inductive_params (mib,_) = mib.mind_nparams
 
-let make_inductive_subst mib u =
-  if mib.mind_polymorphic then 
-    make_universe_subst u mib.mind_universes
-  else Univ.empty_level_subst
-
 let inductive_paramdecls (mib,u) = 
-  let subst = make_inductive_subst mib u in
-    Vars.subst_univs_level_context subst mib.mind_params_ctxt
+  Vars.subst_instance_context u mib.mind_params_ctxt
 
 let inductive_instance mib =
-  if mib.mind_polymorphic then 
+  if mib.mind_polymorphic then
     UContext.instance mib.mind_universes
   else Instance.empty
 
 let inductive_context mib =
   if mib.mind_polymorphic then 
-    mib.mind_universes 
+    instantiate_univ_context mib.mind_universes 
   else UContext.empty
 
-let instantiate_inductive_constraints mib subst =
+let instantiate_inductive_constraints mib u =
   if mib.mind_polymorphic then
-    instantiate_univ_context subst mib.mind_universes
+    subst_instance_constraints u (UContext.constraints mib.mind_universes)
   else Constraint.empty
 
 (************************************************************************)
@@ -84,9 +78,9 @@ let ind_subst mind mib u =
   List.init ntypes make_Ik
 
 (* Instantiate inductives in constructor type *)
-let constructor_instantiate mind u subst mib c =
+let constructor_instantiate mind u mib c =
   let s = ind_subst mind mib u in
-    substl s (subst_univs_level_constr subst c)
+    substl s (subst_instance_constr u c)
 
 let instantiate_params full t args sign =
   let fail () =
@@ -108,13 +102,11 @@ let instantiate_params full t args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = prop_sort in
   let t = mkArity (sign,dummy) in
-  let subst = make_inductive_subst mib u in
   let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    Vars.subst_univs_level_context subst ar
+    Vars.subst_instance_context u ar
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let subst = make_inductive_subst mib u in
-  let inst_ind = constructor_instantiate mind u subst mib in
+  let inst_ind = constructor_instantiate mind u mib in
   (fun t ->
     instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
 
@@ -204,30 +196,9 @@ let instantiate_universes env ctx ar argsorts =
 
 (* Type of an inductive type *)
 
-let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps =
-  match mip.mind_arity with
-  | RegularArity a ->
-    if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty)
-    else 
-      let subst = make_inductive_subst mib u in
-	(subst_univs_level_constr subst a.mind_user_arity, subst)
-  | TemplateArity ar ->
-    let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes env ctx ar paramtyps in
-      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
-         the situation where a non-Prop singleton inductive becomes Prop
-         when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
-      then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s), Univ.LMap.empty
-
 let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
-  | RegularArity a ->
-    if not mib.mind_polymorphic then a.mind_user_arity
-    else 
-      let subst = make_inductive_subst mib u in
-	(subst_univs_level_constr subst a.mind_user_arity)
+  | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
@@ -242,13 +213,13 @@ let type_of_inductive env pind =
   type_of_inductive_gen env pind [||]
 
 let constrained_type_of_inductive env ((mib,mip),u as pind) =
-  let ty, subst = type_of_inductive_subst env pind [||] in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_inductive env pind in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
-  let ty, subst = type_of_inductive_subst env pind args in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_inductive_gen env pind args in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
@@ -267,44 +238,29 @@ let max_inductive_sort =
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor_subst cstr u subst (mib,mip) =
+let type_of_constructor (cstr, u) (mib,mip) =
   let ind = inductive_of_constructor cstr in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
   if i > nconstr then error "Not enough constructors in the type.";
-  let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in
-    c
-
-let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
-  let subst = make_inductive_subst mib u in
-    type_of_constructor_subst cstr u subst mspec, subst
-
-let type_of_constructor cstru mspec = 
-  fst (type_of_constructor_gen cstru mspec)
-
-let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
-  let u = UContext.instance mib.mind_universes in
-  let c = type_of_constructor_gen (cstr, u) mspec in
-    (fst c, mib.mind_universes)
+  constructor_instantiate (fst ind) u mib specif.(i-1)
 
 let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
-  let ty, subst = type_of_constructor_gen cstru ind in
-  let cst = instantiate_inductive_constraints mib subst in
+  let ty = type_of_constructor cstru ind in
+  let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
-  let subst = make_inductive_subst mib u in
-    Array.map (constructor_instantiate kn u subst mib) specif
+    Array.map (constructor_instantiate kn u mib) specif
 
 let arities_of_constructors ind specif =
   arities_of_specif (fst (fst ind), snd ind) specif
 
 let type_of_constructors (ind,u) (mib,mip) =
   let specif = mip.mind_user_lc in
-  let subst = make_inductive_subst mib u in
-  Array.map (constructor_instantiate (fst ind) u subst mib) specif
+    Array.map (constructor_instantiate (fst ind) u mib) specif
 
 (************************************************************************)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8bd1a56058..9140d171d0 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -35,14 +35,12 @@ val lookup_mind_specif : env -> inductive -> mind_specif
 (** {6 Functions to build standard types related to inductive } *)
 val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list
 
-val make_inductive_subst : mutual_inductive_body -> universe_instance -> universe_level_subst
-
 val inductive_instance : mutual_inductive_body -> universe_instance
 val inductive_context : mutual_inductive_body -> universe_context
 val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context
 
 val instantiate_inductive_constraints : 
-  mutual_inductive_body -> universe_level_subst -> constraints
+  mutual_inductive_body -> universe_instance -> constraints
 
 val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained
 val constrained_type_of_inductive_knowing_parameters : 
@@ -59,7 +57,6 @@ val elim_sorts : mind_specif -> sorts_family list
 
 val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
 val type_of_constructor : pconstructor -> mind_specif -> types
-val type_of_constructor_in_ctx : constructor -> mind_specif -> types in_universe_context
 
 (** Return constructor types in normal form *)
 val arities_of_constructors : pinductive -> mind_specif -> types array
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 7aed4bf501..a5def3dc8f 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.named_context in_universe_context } 
+  abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } 
 type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3e45f65b42..092f0aeb17 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -43,7 +43,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.named_context Univ.in_universe_context } 
+  abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t } 
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0578d35fc9..71a6b7a399 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -363,15 +363,6 @@ let constraints_of_sfb sfb =
   | SFBmodtype mtb -> [Now mtb.typ_constraints]
   | SFBmodule mb -> [Now mb.mod_constraints]
 
-(* let add_constraints cst senv = *)
-(*   { senv with *)
-(*     env = Environ.add_constraints cst senv.env; *)
-(*     univ = Univ.Constraint.union cst senv.univ } *)
-
-(* let next_universe senv = *)
-(*   let univ = senv.max_univ in *)
-(*     univ + 1, { senv with max_univ = univ + 1 } *)
-
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 9f30b7da38..c44adad5cb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,21 +24,21 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type env j poly = function
+let constrain_type env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
-    else RegularArity j.uj_type
+    else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
       let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
-	RegularArity t
+	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
       let tj = infer_type env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
-	RegularArity t
+	RegularArity (Vars.subst_univs_level_constr subst t)
 
 let map_option_typ = function None -> `None | Some x -> `Some x
 
@@ -65,11 +65,12 @@ let handle_side_effects env body side_eff =
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
     let rec sub_body c u b i x = match kind_of_term x with
       | Const (c',u') when eq_constant c c' -> 
-	let subst = 
-	  Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst)
-	    Univ.LMap.empty (Instance.to_array u) (Instance.to_array u')
-	in 
-	  Vars.subst_univs_level_constr subst b
+	(* let subst =  *)
+	(*   Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) *)
+	(*     Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') *)
+	(* in  *)
+	(*   Vars.subst_univs_level_constr subst b *)
+	Vars.subst_instance_constr u' b
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
     let fix_body (c,cb) t =
       match cb.const_body with
@@ -107,7 +108,7 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
-let check_projection env kn inst body =
+let check_projection env kn usubst body =
   let cannot_recognize () = error ("Cannot recognize a projection") in
   let ctx, m = decompose_lam_assum body in
   let () = if not (isCase m) then cannot_recognize () in
@@ -136,19 +137,27 @@ let check_projection env kn inst body =
   let pb = { proj_ind = fst ci.ci_ind;
 	     proj_npars = n;
 	     proj_arg = arg;
-	     proj_type = ty;
-	     proj_body = body }
+	     proj_type = Vars.subst_univs_level_constr usubst ty;
+	     proj_body = Vars.subst_univs_level_constr usubst body }
   in pb
   
+let subst_instance_j s j =
+  { uj_val = Vars.subst_univs_level_constr s j.uj_val;
+    uj_type = Vars.subst_univs_level_constr s j.uj_type }
+
 let infer_declaration env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context uctx env in
       let j = infer env t in
-      let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, RegularArity t, None, poly, uctx, false, ctx
+      let abstract = poly && not (Option.is_empty kn) in
+      let usubst, univs = Univ.abstract_universes abstract uctx in
+      let c = Typeops.assumption_of_judgment env j in
+      let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
+	Undef nl, RegularArity t, None, poly, univs, false, ctx
   | DefinitionEntry ({ const_entry_type = Some typ;
-                       const_entry_opaque = true } as c) ->
+                       const_entry_opaque = true;
+		       const_entry_polymorphic = false} as c) ->
       let env = push_context c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
@@ -158,7 +167,9 @@ let infer_declaration env kn dcl =
 	  let env' = push_context_set ctx env in
           let j = infer env' body in
           let j = hcons_j j in
-          let _typ = constrain_type env' j c.const_entry_polymorphic (`SomeWJ (typ,tyj)) in
+	  let subst = Univ.LMap.empty in
+          let _typ = constrain_type env' j c.const_entry_polymorphic subst
+	    (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
           j.uj_val, ctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
@@ -172,28 +183,28 @@ let infer_declaration env kn dcl =
       let (body, ctx), side_eff = Future.join body in
       assert(Univ.ContextSet.is_empty ctx);
       let body = handle_side_effects env body side_eff in
+      let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
+      let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
       let def, typ, proj = 
 	if c.const_entry_proj then
 	  (** This should be the projection defined as a match. *)
 	  let j = infer env body in
-	  let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in
+	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
 	  (** We check it does indeed have the shape of a projection. *)
-	  let inst = Univ.UContext.instance c.const_entry_universes in
-	  let pb = check_projection env (Option.get kn) inst body in
+	  let pb = check_projection env (Option.get kn) usubst body in
 	  (** We build the eta-expanded form. *)
 	  let context, m = decompose_lam_n_assum (pb.proj_npars + 1) body in 
 	  let body' = mkProj (Option.get kn, mkRel 1) in
 	  let body = it_mkLambda_or_LetIn body' context in
-	    Def (Mod_subst.from_val (hcons_constr body)),
+	    Def (Mod_subst.from_val (hcons_constr (Vars.subst_univs_level_constr usubst body))),
 	    typ, Some pb
 	else
 	  let j = infer env body in
-	  let j = hcons_j j in
-	  let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in
-	  let def = Def (Mod_subst.from_val j.uj_val) in
+	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+	  let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
+	  let def = Def (Mod_subst.from_val def) in
 	    def, typ, None
       in
-      let univs = c.const_entry_universes in
 	feedback_completion_typecheck feedback_id;
 	def, typ, proj, c.const_entry_polymorphic,
         univs, c.const_entry_inline_code, c.const_entry_secctx
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index cd1f2c8564..cb0c429a95 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -189,9 +189,7 @@ let type_of_projection env (cst,u) =
   match cb.const_proj with
   | Some pb -> 
     if cb.const_polymorphic then
-      let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
-      let subst = make_inductive_subst mib u in
-	Vars.subst_univs_level_constr subst pb.proj_type
+      Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
 
@@ -388,8 +386,7 @@ let judge_of_projection env p cj =
     with Not_found -> error_case_not_inductive env cj
   in
     assert(eq_mind pb.proj_ind (fst ind));
-    let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_level_constr usubst pb.Declarations.proj_type in
+    let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
     let ty = substl (cj.uj_val :: List.rev args) ty in
       (* TODO: Universe polymorphism for projections *)
       {uj_val = mkProj (p,cj.uj_val);
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4adc1e6830..2fd94e1a94 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -254,6 +254,7 @@ struct
     | Prop
     | Set
     | Level of int * DirPath.t
+    | Var of int
 
   (* Hash-consing *)
 
@@ -264,6 +265,7 @@ struct
       | Set, Set -> true
       | Level (n,d), Level (n',d') ->
         Int.equal n n' && DirPath.equal d d'
+      | Var n, Var n' -> true
       | _ -> false
 
   let compare u v =
@@ -278,20 +280,26 @@ struct
       if i1 < i2 then -1
       else if i1 > i2 then 1
       else DirPath.compare dp1 dp2
-
+    | Level _, _ -> -1
+    | _, Level _ -> 1
+    | Var n, Var m -> Int.compare n m
+      
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
     | Level (n,d) as x -> 
       let d' = Names.DirPath.hcons d in
         if d' == d then x else Level (n,d')
+    | Var n as x -> x
 
   open Hashset.Combine
 
   let hash = function
     | Prop -> combinesmall 1 0
     | Set -> combinesmall 1 1
-    | Level (n, d) -> combinesmall 2 (combine n (Names.DirPath.hash d))
+    | Var n -> combinesmall 2 n
+    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+
 end
 
 module Level = struct
@@ -302,6 +310,7 @@ module Level = struct
   | Prop
   | Set
   | Level of int * DirPath.t
+  | Var of int
 
   (** Embed levels with their hash value *)
   type t = { 
@@ -365,6 +374,7 @@ module Level = struct
     | Prop -> "Prop"
     | Set -> "Set"
     | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
 
@@ -373,6 +383,10 @@ module Level = struct
     | Prop, Set | Set, Prop -> true
     | _ -> false
 
+  let vars = Array.init 20 (fun i -> make (Var i))
+
+  let var n = 
+    if n < 20 then vars.(n) else make (Var n)
 
   let make m n = make (Level (n, Names.DirPath.hcons m))
 
@@ -1690,7 +1704,7 @@ let level_subst_of f =
     with Not_found -> l
      
 module Instance : sig 
-    type t
+    type t = Level.t array
 
     val empty : t
     val is_empty : t -> bool
@@ -1894,12 +1908,6 @@ type 'a in_universe_context_set = 'a * universe_context_set
 
 (** Substitutions. *)
 
-let make_universe_subst inst (ctx, csts) = 
-  try Array.fold_left2 (fun acc c i -> LMap.add c i acc)
-        LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
-  with Invalid_argument _ -> 
-    anomaly (Pp.str "Mismatched instance and context when building universe substitution")
-
 let empty_subst = LMap.empty
 let is_empty_subst = LMap.is_empty
 
@@ -1930,10 +1938,6 @@ let subst_univs_level_constraints subst csts =
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
     csts Constraint.empty 
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context subst (_, csts) = 
-  subst_univs_level_constraints subst csts
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1976,6 +1980,62 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
+
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
+(** Substitute instance inst for ctx in csts *)
+let instantiate_univ_context (ctx, csts) = 
+  (ctx, subst_instance_constraints ctx csts)
+
+let instantiate_univ_constraints u (_, csts) = 
+  subst_instance_constraints u csts
+
+let make_instance_subst i = 
+  let arr = Instance.to_array i in
+    Array.fold_left_i (fun i acc l ->
+      LMap.add l (Level.var i) acc)
+      LMap.empty arr
+
+let make_inverse_instance_subst i = 
+  let arr = Instance.to_array i in
+    Array.fold_left_i (fun i acc l ->
+      LMap.add (Level.var i) l acc)
+      LMap.empty arr
+
+let abstract_universes poly ctx =
+  let instance = UContext.instance ctx in
+    if poly then
+      let subst = make_instance_subst instance in
+      let cstrs = subst_univs_level_constraints subst 
+	(UContext.constraints ctx)
+      in
+      let ctx = UContext.make (instance, cstrs) in
+	subst, ctx
+    else empty_level_subst, ctx
+
 (** Pretty-printing *)
 
 let pr_arc = function
@@ -2065,7 +2125,11 @@ let eq_levels = Level.equal
 let equal_universes = Universe.equal
 
 
-(*
+let subst_instance_constraints = 
+  if Flags.profile then 
+    let key = Profile.declare_profile "subst_instance_constraints" in
+      Profile.profile2 key subst_instance_constraints
+  else subst_instance_constraints
 
 let merge_constraints = 
   if Flags.profile then 
@@ -2089,4 +2153,3 @@ let check_leq =
     let check_leq_key = Profile.declare_profile "check_leq" in
       Profile.profile3 check_leq_key check_leq
   else check_leq
-*)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8f40bc5f88..655f87bb56 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -27,15 +27,14 @@ sig
   val equal : t -> t -> bool
   (** Equality function *)
 
-  (* val hash : t -> int *)
-  (** Hash function *)
-
   val make : Names.DirPath.t -> int -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
   val pr : t -> Pp.std_ppcmds
   (** Pretty-printing *)
+
+  val var : int -> t
 end
 
 type universe_level = Level.t
@@ -370,11 +369,6 @@ val subst_univs_level_level : universe_level_subst -> universe_level -> universe
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
 val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
-(** Make a universe level substitution: the instances must match. *)
-val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
-(** Get the instantiated graph. *)
-val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
-
 (** Level to universe substitutions. *)
 
 val empty_subst : universe_subst
@@ -384,6 +378,21 @@ val make_subst : universe_subst -> universe_subst_fn
 val subst_univs_universe : universe_subst_fn -> universe -> universe
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 
+(** Substitution of instances *)
+val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
+val subst_instance_universe : universe_instance -> universe -> universe
+val subst_instance_constraints : universe_instance -> constraints -> constraints
+
+val make_instance_subst : universe_instance -> universe_level_subst
+val make_inverse_instance_subst : universe_instance -> universe_level_subst
+
+val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context
+
+(** Get the instantiated graph. *)
+val instantiate_univ_context : universe_context -> universe_context
+
+val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : universes -> Pp.std_ppcmds
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 386a3e8ff2..ee156d8c9a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,3 +295,44 @@ let subst_univs_level_constr subst c =
 
 let subst_univs_level_context s = 
   map_rel_context (subst_univs_level_constr s)
+      
+let subst_instance_constr subst c =
+  if Univ.Instance.is_empty subst then c
+  else
+    let f u = Univ.subst_instance_instance subst u in
+    let changed = ref false in
+    let rec aux t = 
+      match kind t with
+      | Const (c, u) -> 
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkConstU (c, u'))
+      | Ind (i, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+	  let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkIndU (i, u'))
+      | Construct (c, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; mkConstructU (c, u'))
+      | Sort (Sorts.Type u) -> 
+         let u' = Univ.subst_instance_universe subst u in
+	   if u' == u then t else 
+	     (changed := true; mkSort (Sorts.sort_of_univ u'))
+      | _ -> Constr.map aux t
+    in
+    let c' = aux c in
+      if !changed then c' else c
+
+(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
+(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
+
+let subst_instance_context s ctx = 
+  if Univ.Instance.is_empty s then ctx
+  else map_rel_context (fun x -> subst_instance_constr s x) ctx
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 0d5ab07db0..cfa9fcb264 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -83,3 +83,7 @@ val subst_univs_constr : universe_subst -> constr -> constr
 
 val subst_univs_level_constr : universe_level_subst -> constr -> constr
 val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context
+
+(** Instance substitution for polymorphism. *)
+val subst_instance_constr : universe_instance -> constr -> constr
+val subst_instance_context : universe_instance -> rel_context -> rel_context
-- 
cgit v1.2.3