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.

9 files changed, 38 insertions, 50 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index be22030ced..3c7d4f75b9 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -41,12 +41,12 @@ let section_segment_of_reference = function
   | ConstRef con -> Lib.section_segment_of_constant con
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
       Lib.section_segment_of_mutual_inductive kn
-  | _ -> [], Univ.UContext.empty
+  | _ -> [], Univ.LMap.empty, Univ.UContext.empty
 
 let discharge_rename_args = function
   | _, (ReqGlobal (c, names), _ as req) ->
      (try 
-       let vars,_ = section_segment_of_reference c in
+       let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
        let names' = List.map (fun l -> var_names @ l) names in
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index a12fe6b67c..81b5c9ad83 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -59,10 +59,7 @@ let check_privacy_block mib =
 (* Christine Paulin, 1996 *)
 
 let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
-  let usubst = Inductive.make_inductive_subst mib u in
-  let lnamespar = Vars.subst_univs_level_context usubst
-    mib.mind_params_ctxt
-  in
+  let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
   let () = check_privacy_block mib in
   let () = 
     if not (Sorts.List.mem kind (elim_sorts specif)) then
@@ -282,9 +279,8 @@ let mis_make_indrec env sigma listdepkind mib u =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let evdref = ref sigma in
-  let usubst = Inductive.make_inductive_subst mib u in
   let lnonparrec,lnamesparrec =
-    context_chop (nparams-nparrec) (Vars.subst_univs_level_context usubst mib.mind_params_ctxt) in
+    context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in
   let nrec = List.length listdepkind in
   let depPvec =
     Array.make mib.mind_ntypes (None : (bool * constr) option) in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dee22cb173..f6ca611a33 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -35,11 +35,6 @@ let type_of_constructor env (cstr,u) =
  Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps;
  Inductive.type_of_constructor (cstr,u) specif
 
-let type_of_constructor_in_ctx env cstr =
- let specif =
-  Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Inductive.type_of_constructor_in_ctx cstr specif
-
 (* Return constructor types in user form *)
 let type_of_constructors env (ind,u as indu) =
  let specif = Inductive.lookup_mind_specif env ind in
@@ -101,8 +96,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
   if j > nconstr then error "Not enough constructors in the type.";
-  let univsubst = make_inductive_subst mib u in
-    substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1))
+    substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
 
 (* Number of constructors *)
 
@@ -248,13 +242,11 @@ let inductive_paramdecls_env env (ind,u) =
 
 let inductive_alldecls (ind,u) =
   let (mib,mip) = Global.lookup_inductive ind in
-  let subst = Inductive.make_inductive_subst mib u in
-    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
+    Vars.subst_instance_context u mip.mind_arity_ctxt
 
 let inductive_alldecls_env env (ind,u) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let subst = Inductive.make_inductive_subst mib u in
-    Vars.subst_univs_level_context subst mip.mind_arity_ctxt
+    Vars.subst_instance_context u mip.mind_arity_ctxt
 
 let constructor_has_local_defs (indsp,j) =
   let (mib,mip) = Global.lookup_inductive indsp in
@@ -353,7 +345,6 @@ let instantiate_context sign args =
 
 let get_arity env ((ind,u),params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let univsubst = make_inductive_subst mib u in
   let parsign =
     (* Dynamically detect if called with an instance of recursively
        uniform parameter only or also of non recursively uniform
@@ -364,11 +355,11 @@ let get_arity env ((ind,u),params) =
       snd (List.chop nnonrecparams mib.mind_params_ctxt)
     else
       parsign in
-  let parsign = Vars.subst_univs_level_context univsubst parsign in
+  let parsign = Vars.subst_instance_context u parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
   let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
   let subst = instantiate_context parsign params in
-  let arsign = Vars.subst_univs_level_context univsubst arsign in
+  let arsign = Vars.subst_instance_context u arsign in
   (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
 (* Functions to build standard types related to inductive *)
@@ -583,9 +574,7 @@ let rec instantiate_universes env evdref scl is = function
 
 let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
-  | RegularArity s ->
-    let subst = Inductive.make_inductive_subst mib u in
-      sigma, subst_univs_level_constr subst s.mind_user_arity
+  | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
   | TemplateArity ar ->
     let _,scl = Reduction.dest_arity env conclty in
     let ctx = List.rev mip.mind_arity_ctxt in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cefd5bd9da..5583eff4d8 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -20,7 +20,6 @@ val type_of_inductive    : env -> pinductive -> types
 
 (** Return type as quoted by the user *)
 val type_of_constructor  : env -> pconstructor -> types
-val type_of_constructor_in_ctx  : env -> constructor -> types Univ.in_universe_context
 val type_of_constructors : env -> pinductive -> types array
 
 (** Return constructor types in normal form *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e5023e8582..fe9646b9d8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -532,8 +532,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	      (mk_tycon (applist (mkIndU ind, args))) in
 	    j', (ind, args))
     in
-    let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in
-    let ty = Vars.subst_univs_level_constr usubst ty in
+    let ty = Vars.subst_instance_constr u ty in
     let ty = substl (recty.uj_val :: List.rev pars) ty in
     let j = {uj_val = mkProj (cst,recty.uj_val); uj_type = ty} in
       inh_conv_coerce_to_tycon loc env evdref j tycon
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e6844673ce..1f3e7b5717 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -61,7 +61,7 @@ module ReductionBehaviour = struct
   let discharge = function
     | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
        let c' = pop_con c in
-       let vars, _ctx = Lib.section_segment_of_constant c in
+       let vars, _subst, _ctx = Lib.section_segment_of_constant c in
        let extra = List.length vars in
        let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
        let recargs' = List.map ((+) extra) b.b_recargs in
@@ -654,23 +654,23 @@ let reducible_mind_case c = match kind_of_term c with
 *)
 let magicaly_constant_of_fixbody env bd = function
   | Name.Anonymous -> bd
-  | Name.Name id ->
-    try
-      let cst = Nametab.locate_constant
-	(Libnames.make_qualid DirPath.empty id) in
-      let (cst, u), ctx = Universes.fresh_constant_instance env cst in
-      match constant_opt_value env (cst,u) with
-      | None -> bd
-      | Some (t,cstrs) -> 
-        let b, csts = Universes.eq_constr_universes t bd in
-	let subst = Universes.Constraints.fold (fun (l,d,r) acc -> 
-	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
-	  csts Univ.LMap.empty
-	in
-	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          if b then mkConstU (cst,inst) else bd
-    with
-    | Not_found -> bd
+  | Name.Name id -> bd
+    (* try *)
+    (*   let cst = Nametab.locate_constant *)
+    (* 	(Libnames.make_qualid DirPath.empty id) in *)
+    (*   let (cst, u), ctx = Universes.fresh_constant_instance env cst in *)
+    (*   match constant_opt_value_in env (cst,u) with *)
+    (*   | None -> bd *)
+    (*   | Some t ->  *)
+    (*     let b, csts = Universes.eq_constr_universes t bd in *)
+    (* 	let subst = Universes.Constraints.fold (fun (l,d,r) acc ->  *)
+    (* 	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) *)
+    (* 	  csts Univ.LMap.empty *)
+    (* 	in *)
+    (* 	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in *)
+    (*       if b then mkConstU (cst,inst) else bd *)
+    (* with *)
+    (* | Not_found -> bd *)
 
 let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fad8623b0f..f2a0b6fd18 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -896,6 +896,12 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
   in app_stack (redrec (c, empty_stack))
 *)
 
+let whd_simpl_stack = 
+  if Flags.profile then 
+    let key = Profile.declare_profile "whd_simpl_stack" in
+      Profile.profile3 key whd_simpl_stack
+  else whd_simpl_stack
+
 (* Same as [whd_simpl] but also reduces constants that do not hide a
    reducible fix, but does this reduction of constants only until it
    immediately hides a non reducible fix or a cofix *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index dd09d5b29a..67189e22d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -210,7 +210,7 @@ let discharge_class (_,cl) =
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
-    let ctx, uctx = abs_context cl in
+    let ctx, usubst, uctx = abs_context cl in
     let ctx, subst = rel_of_variable_context ctx in
     let context = discharge_context ctx subst cl.cl_context in
     let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
@@ -379,7 +379,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance pri local glob =
-  let ty = Global.type_of_global_unsafe (*FIXME*) glob in
+  let ty = Global.type_of_global_unsafe glob in
     match class_of_constr ty with
     | Some (rels, ((tc,_), args) as _cl) ->
       add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b21f4e383c..758686aa94 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -58,8 +58,7 @@ let find_rectype_a env c =
 let type_constructor mind mib u typ params =
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
-  let usubst = make_inductive_subst mib u in
-  let ctyp = subst_univs_level_constr usubst ctyp in
+  let ctyp = subst_instance_constr u ctyp in
   let nparams = Array.length params in
   if Int.equal nparams 0 then ctyp
   else