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.

3 files changed, 20 insertions, 8 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index bd5218eff..971ae70d8 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -77,12 +77,23 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
 
 let process_inductive (sechyps,abs_ctx) modlist mib =
   let nparams = mib.mind_nparams in
+  let subst, univs = 
+    if mib.mind_polymorphic then 
+      let inst = Univ.UContext.instance mib.mind_universes in
+      let cstrs = Univ.UContext.constraints mib.mind_universes in
+	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
+    else Univ.Instance.empty, mib.mind_universes
+  in
   let inds =
     Array.map_to_list
       (fun mip ->
 	let ty = refresh_polymorphic_type_of_inductive (mib,mip) in
 	let arity = expmod_constr modlist ty in
-	let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
+	let arity = Vars.subst_instance_constr subst arity in
+	let lc = Array.map 
+	  (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c))
+	  mip.mind_user_lc 
+	in
 	  (mip.mind_typename,
 	   arity,
 	   Array.to_list mip.mind_consnames,
@@ -90,7 +101,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
-  let univs = Univ.UContext.union abs_ctx mib.mind_universes in
+  let univs = Univ.UContext.union abs_ctx univs in
   let record = match mib.mind_record with
     | None -> None
     | Some (_, a) -> Some (Array.length a > 0)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 896cc41c7..302fe6280 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -209,9 +209,9 @@ let instantiate_possibly_recursive_type indu paramdecls fields =
 let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let paramdecls = mib.mind_params_ctxt in
-  let poly = mib.mind_polymorphic and ctx = mib.mind_universes in
   let u = Inductive.inductive_instance mib in
+  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
+  let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 016b9f22b..e2a4ad25c 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -43,9 +43,9 @@ module SearchBlacklist =
    of the object, the assumptions that will make it possible to print its type,
    and the constr term that represent its type. *)
 
-let iter_constructors indsp fn env nconstr =
+let iter_constructors indsp u fn env nconstr =
   for i = 1 to nconstr do
-    let typ, _ = Inductiveops.type_of_constructor_in_ctx env (indsp, i) in
+    let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
     fn (ConstructRef (indsp, i)) env typ
   done
 
@@ -68,11 +68,12 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let i = (ind, Inductive.inductive_instance mib) in
+      let u = Inductive.inductive_instance mib in
+      let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in
       let len = Array.length mip.mind_user_lc in
-      iter_constructors ind fn env len
+      iter_constructors ind u fn env len
     in
     Array.iteri iter_packet mib.mind_packets
   | _ -> ()