Reuse universe level substitutions for template polymorphism, fixing performance

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

5 files changed, 16 insertions, 16 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index b8dfe63d3..85dac4bfc 100644
--- a/kernel/declarations.mli
+++ b/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;
 }
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 55868097f..dd906bab2 100644
--- a/kernel/declareops.ml
+++ b/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 } *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0f9c7421f..85d04e5e2 100644
--- a/kernel/indtypes.ml
+++ b/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
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8d6f757b6..3f1c4e75f 100644
--- a/kernel/inductive.ml
+++ b/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
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c6355b3ea..49f883628 100644
--- a/kernel/typeops.ml
+++ b/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