Reuse universe level substitutions for template polymorphism, fixing …

…performance

problem with hashconsing at the same time. This fixes bug# 3302.

kernel/declarations.mli

@@ -27,7 +27,7 @@ type engagement = ImpredicativeSet
 *)
 
 type template_arity = {
-  template_param_levels : Univ.universe option list;
+  template_param_levels : Univ.universe_level option list;
   template_level : Univ.universe;
 }
 

kernel/declareops.ml

@@ -31,8 +31,8 @@ let map_decl_arity f g = function
   | TemplateArity a -> TemplateArity (g a)
 
 let hcons_template_arity ar =
-  { template_param_levels =
-      List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels;
+  { template_param_levels = ar.template_param_levels;
+      (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *)
     template_level = Univ.hcons_univ ar.template_level }
 
 (** {6 Constants } *)

kernel/indtypes.ml

@@ -195,11 +195,11 @@ let is_impredicative env u =
 
 let param_ccls params =
   let has_some_univ u = function
-    | Some v when Universe.equal u v -> true
+    | Some v when Univ.Level.equal u v -> true
     | _ -> false
   in
   let remove_some_univ u = function
-    | Some v when Universe.equal u v -> None
+    | Some v when Univ.Level.equal u v -> None
     | x -> x
   in
   let fold l (_, b, p) = match b with
@@ -210,10 +210,13 @@ let param_ccls params =
     (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
     begin match kind_of_term c with
     | Sort (Type u) ->
-      if List.exists (has_some_univ u) l then
-        None :: List.map (remove_some_univ u) l
-      else
-        Some u :: l
+      (match Univ.Universe.level u with
+      | Some u ->
+	if List.exists (has_some_univ u) l then
+          None :: List.map (remove_some_univ u) l
+	else
+          Some u :: l
+      | None -> None :: l)
     | _ ->
       None :: l
     end

kernel/inductive.ml

@@ -155,10 +155,7 @@ let sort_as_univ = function
 (* Template polymorphism *)
 
 let cons_subst u su subst =
-  try
-    (u, sup su (List.assoc_f Universe.equal u subst)) ::
-      List.remove_assoc_f Universe.equal u subst
-  with Not_found -> (u, su) :: subst
+  Univ.LMap.add u su subst
 
 let actualize_decl_level env lev t =
   let sign,s = dest_arity env t in
@@ -192,7 +189,7 @@ let rec make_subst env = function
 	d::ctx, subst
   | sign, [], _ ->
       (* Uniform parameters are exhausted *)
-      sign,[]
+      sign, Univ.LMap.empty
   | [], _, _ ->
       assert false
 
@@ -201,7 +198,7 @@ exception SingletonInductiveBecomesProp of Id.t
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
   let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
-  let level = subst_large_constraints subst ar.template_level in
+  let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
     if is_type0m_univ level then prop_sort

kernel/typeops.ml

@@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign =
 
 let extract_level env p =
   let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
 
 let extract_context_levels env l =
   let fold l (_, b, p) = match b with

plugins/extraction/extraction.ml

@@ -207,7 +207,7 @@ let oib_equal o1 o2 =
       | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
 	eq_constr c1 c2 && Sorts.equal s1 s2
       | TemplateArity p1, TemplateArity p2 ->
-	let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in
+	let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in
 	  List.equal eq p1.template_param_levels p2.template_param_levels &&
 	    Univ.Universe.equal p1.template_level p2.template_level
       | _, _ -> false

pretyping/evarutil.ml

@@ -830,7 +830,7 @@ let get_template_constructor_type evdref (ind, i) n =
     | Some u :: l, Prod (na, t, t') ->
       let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in
 	(* evdref := set_leq_sort !evdref u'l (Type u); *)
-	let s = Univ.LMap.add (Option.get (Univ.Universe.level u))
+	let s = Univ.LMap.add u
 	  (Option.get (Univ.Universe.level u')) Univ.LMap.empty in
 	let dom = subst_univs_level_constr s t in
 	(* let codom = subst_univs_level_constr s t' in *)

pretyping/evarutil.mli

@@ -221,7 +221,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b ->
 
 (* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *)
 val get_template_constructor_type : evar_map ref -> constructor -> int -> 
-  (Univ.universe option list * types)
+  (Univ.universe_level option list * types)
 
 val get_template_inductive_type : evar_map ref -> inductive -> int -> 
-  (Univ.universe option list * types)
+  (Univ.universe_level option list * types)

pretyping/inductiveops.ml

@@ -465,7 +465,7 @@ let rec instantiate_universes env evdref scl is = function
       let s =
 	(* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
-        if univ_depends u is then
+        if univ_depends (Univ.Universe.make u) is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstriained sort: replace by fresh universe *)