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.

7 files changed, 48 insertions, 43 deletions

diff --git a/library/declare.ml b/library/declare.ml
index bacd9e2c1..b80ceb6e6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -158,9 +158,9 @@ let discharge_constant ((sp, kn), obj) =
 
   let from = Global.lookup_constant con in
   let modlist = replacement_context () in
-  let hyps,uctx = section_segment_of_constant con in
+  let hyps,subst,uctx = section_segment_of_constant con in
   let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
-  let abstract = (named_of_variable_context hyps, uctx) in
+  let abstract = (named_of_variable_context hyps, subst, uctx) in
   let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in
   Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
 
@@ -227,7 +227,14 @@ let declare_sideff env fix_exn se =
     | Declarations.TemplateArity _ -> None in
   let cst_of cb =
     let pt, opaque = pt_opaque_of cb in
-    let ty = ty_of cb in
+    let univs, subst = 
+      if cb.const_polymorphic then
+	let univs = Univ.instantiate_univ_context cb.const_universes in
+	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
+      else cb.const_universes, fun x -> x
+    in
+    let pt = (subst (fst pt), snd pt) in
+    let ty = Option.map subst (ty_of cb) in
     { cst_decl = ConstantEntry (DefinitionEntry {
         const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
         const_entry_secctx = Some cb.Declarations.const_hyps;
@@ -236,7 +243,7 @@ let declare_sideff env fix_exn se =
         const_entry_inline_code = false;
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = cb.const_universes;
+	const_entry_universes = univs;
 	const_entry_proj = false;
     });
     cst_hyps = [] ;
@@ -352,7 +359,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
   let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps,uctx = section_segment_of_mutual_inductive mind in
+  let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
         Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie)
 
diff --git a/library/global.ml b/library/global.ml
index c3c309c39..65e895dfd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -198,10 +198,10 @@ let universes_of_global env r =
 	Declareops.universes_of_constant cb
     | IndRef ind ->
       let (mib, oib) = Inductive.lookup_mind_specif env ind in
-	mib.mind_universes 
+	Univ.instantiate_univ_context mib.mind_universes 
     | ConstructRef cstr ->
       let (mib,oib) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
-	mib.mind_universes 
+	Univ.instantiate_univ_context mib.mind_universes 
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
diff --git a/library/impargs.ml b/library/impargs.ml
index 0126c4ad7..55e21b2c8 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -525,10 +525,10 @@ let impls_of_context ctx =
   List.rev_map map (List.filter is_set ctx)
 
 let section_segment_of_reference = function
-  | ConstRef con -> section_segment_of_constant con
+  | ConstRef con -> pi1 (section_segment_of_constant con)
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.UContext.empty
+    pi1 (section_segment_of_mutual_inductive kn)
+  | _ -> []
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
@@ -543,7 +543,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) ->
     (try
-      let vars,_ = section_segment_of_reference ref in
+      let vars = section_segment_of_reference ref in
       (* let isproj =  *)
       (* 	 match ref with *)
       (* 	 | ConstRef cst -> is_projection cst (Global.env ()) *)
@@ -560,7 +560,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplConstant (con,flags) ->
     (try
       let con' = pop_con con in
-      let vars,_ = section_segment_of_constant con in
+      let vars,_,_ = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
       let newimpls = 
 	(* if is_projection con (Global.env()) then (snd (List.hd l)) *)
@@ -572,7 +572,7 @@ let discharge_implicits (_,(req,l)) =
   | ImplMutualInductive (kn,flags) ->
     (try
       let l' = List.map (fun (gr, l) ->
-	let vars,_ = section_segment_of_reference gr in
+	let vars = section_segment_of_reference gr in
 	let extra_impls = impls_of_context vars in
 	((if isVarRef gr then gr else pop_global_reference gr),
 	 List.map (add_section_impls vars extra_impls) l)) l
diff --git a/library/lib.ml b/library/lib.ml
index 92bace745..1ee3ca57b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -382,8 +382,9 @@ let find_opening_node id =
 type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
 
 type variable_context = variable_info list
-type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t *
-  variable_context Univ.in_universe_context Names.Mindmap.t
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
+		  
+type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 let sectab =
   Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * 
@@ -427,8 +428,9 @@ let add_section_replacement f g hyps =
   | (vars,exps,abs)::sl ->
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
+    let subst, ctx = Univ.abstract_universes true ctx in
     let args = instance_from_variable_context (List.rev sechyps) in
-    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,ctx) abs)::sl
+    sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl
 
 let add_section_kn kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
@@ -464,7 +466,7 @@ let full_replacement_context () = List.map pi2 !sectab
 let full_section_segment_of_constant con =
   List.map (fun (vars,_,(x,_)) -> fun hyps ->
     named_of_variable_context
-      (try fst (Names.Cmap.find con x)
+      (try pi1 (Names.Cmap.find con x)
        with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
 
 (*************)
diff --git a/library/lib.mli b/library/lib.mli
index 759a1a135..615a39f9e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -162,12 +162,13 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t
 type variable_info = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
 type variable_context = variable_info list 
+type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t
 
 val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Context.named_context
 
-val section_segment_of_constant : Names.constant -> variable_context Univ.in_universe_context
-val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context Univ.in_universe_context
+val section_segment_of_constant : Names.constant -> abstr_info
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info
 
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
diff --git a/library/universes.ml b/library/universes.ml
index c38d25d75..c5363fd9a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -236,23 +236,19 @@ let fresh_universe_instance ctx =
 
 let fresh_instance_from_context ctx =
   let inst = fresh_universe_instance ctx in
-  let subst = make_universe_subst inst ctx in
-  let constraints = instantiate_univ_context subst ctx in
-    (inst, subst), constraints
+  let constraints = instantiate_univ_constraints inst ctx in
+    inst, constraints
 
 let fresh_instance ctx =
   let ctx' = ref LSet.empty in
-  let s = ref LMap.empty in
   let inst = 
     Instance.subst_fn (fun v -> 
       let u = new_univ_level (Global.current_dirpath ()) in
-	ctx' := LSet.add u !ctx';
-	s := LMap.add v u !s; u) 
+	ctx' := LSet.add u !ctx'; u) 
       (UContext.instance ctx)
-  in !ctx', !s, inst
+  in !ctx', inst
 
 let existing_instance ctx inst = 
-  let s = ref LMap.empty in
   let () = 
     let a1 = Instance.to_array inst 
     and a2 = Instance.to_array (UContext.instance ctx) in
@@ -261,18 +257,18 @@ let existing_instance ctx inst =
 	Errors.errorlabstrm "Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
-      else Array.iter2 (fun u v -> s := LMap.add v u !s) a1 a2
-  in LSet.empty, !s, inst
+      else ()
+  in LSet.empty, inst
 
 let fresh_instance_from ctx inst =
-  let ctx', subst, inst = 
+  let ctx', inst = 
     match inst with 
     | Some inst -> existing_instance ctx inst
     | None -> fresh_instance ctx 
   in
-  let constraints = instantiate_univ_context subst ctx in
-    (inst, subst), (ctx', constraints)
-      
+  let constraints = instantiate_univ_constraints inst ctx in
+    inst, (ctx', constraints)
+
 let unsafe_instance_from ctx =
   (Univ.UContext.instance ctx, ctx)
     
@@ -281,21 +277,21 @@ let unsafe_instance_from ctx =
 let fresh_constant_instance env c inst =
   let cb = lookup_constant c env in
     if cb.Declarations.const_polymorphic then
-      let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
+      let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) inst in
 	((c, inst), ctx)
     else ((c,Instance.empty), ContextSet.empty)
 
 let fresh_inductive_instance env ind inst = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+      let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
 	((ind,inst), ctx)
     else ((ind,Instance.empty), ContextSet.empty)
 
 let fresh_constructor_instance env (ind,i) inst = 
   let mib, mip = Inductive.lookup_mind_specif env ind in
     if mib.Declarations.mind_polymorphic then
-      let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes inst in
+      let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in
 	(((ind,i),inst), ctx)
     else (((ind,i),Instance.empty), ContextSet.empty)
 
@@ -412,15 +408,14 @@ let type_of_reference env r =
      let cb = Environ.lookup_constant c env in
      let ty = Typeops.type_of_constant_type env cb.const_type in
        if cb.const_polymorphic then
-	 let (inst, subst), ctx = 
-	   fresh_instance_from (Declareops.universes_of_constant cb) None in
-	   Vars.subst_univs_level_constr subst ty, ctx
+	 let inst, ctx = fresh_instance_from (Declareops.universes_of_constant cb) None in
+	   Vars.subst_instance_constr inst ty, ctx
        else ty, ContextSet.empty
 
   | IndRef ind ->
      let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
        if mib.mind_polymorphic then
-	 let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in
+	 let inst, ctx = fresh_instance_from mib.mind_universes None in
 	 let ty = Inductive.type_of_inductive env (specif, inst) in
 	   ty, ctx
        else
@@ -429,7 +424,7 @@ let type_of_reference env r =
   | ConstructRef cstr ->
      let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
        if mib.mind_polymorphic then
-	 let (inst, subst), ctx = fresh_instance_from mib.mind_universes None in
+	 let inst, ctx = fresh_instance_from mib.mind_universes None in
 	   Inductive.type_of_constructor (cstr,inst) specif, ctx
        else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
 
diff --git a/library/universes.mli b/library/universes.mli
index 565f9fb0a..6cfee48d2 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -84,10 +84,10 @@ val leq_constr_universes : constr -> constr -> bool universe_constrained
     the instantiated constraints. *)
 
 val fresh_instance_from_context : universe_context -> 
-  (universe_instance * universe_level_subst) constrained
+  universe_instance constrained
 
 val fresh_instance_from : universe_context -> universe_instance option ->
-  (universe_instance * universe_level_subst) in_universe_context_set
+  universe_instance in_universe_context_set
 
 val fresh_sort_in_family : env -> sorts_family -> 
   sorts in_universe_context_set