- Fix substitution of universes which needlessly hashconsed existing universes.

- More cleanup. remove unneeded functions in universes

6 files changed, 30 insertions, 65 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e038f46e72..5eea9561b9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1984,10 +1984,6 @@ type universe_subst_fn = universe_level -> universe
 
 let make_subst subst = fun l -> LMap.find l subst
 
-let subst_univs_level fn l = 
-  try fn l
-  with Not_found -> make l
-
 let subst_univs_expr_opt fn (l,n) =
   Universe.addn n (fn l)
 
@@ -2007,14 +2003,22 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u))
 	  substs nosubst
 
-let subst_univs_constraint fn (u,d,v) =
-  let u' = subst_univs_level fn u and v' = subst_univs_level fn v in
-    if d != Lt && Universe.equal u' v' then None
-    else Some (u',d,v')
+let subst_univs_level fn l = 
+  try Some (fn l)
+  with Not_found -> None
+
+let subst_univs_constraint fn (u,d,v as c) cstrs =
+  let u' = subst_univs_level fn u in
+  let v' = subst_univs_level fn v in
+  match u', v' with
+  | None, None -> Constraint.add c cstrs
+  | Some u, None -> enforce_univ_constraint (u,d,make v) cstrs
+  | None, Some v -> enforce_univ_constraint (make u,d,v) cstrs
+  | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs
 
 let subst_univs_constraints subst csts =
   Constraint.fold 
-    (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c))
+    (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
 (** Pretty-printing *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e43b19d305..a5d66eecb7 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -412,7 +412,6 @@ val empty_subst : universe_subst
 val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
-val subst_univs_level : universe_subst_fn -> universe_level -> universe
 val subst_univs_universe : universe_subst_fn -> universe -> universe
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 
diff --git a/library/universes.ml b/library/universes.ml
index 11ab849c52..9c8d8a512a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -462,13 +462,6 @@ let new_global_univ () =
 
 module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
 
-let remove_trivial_constraints cst =
-  Constraint.fold (fun (l,d,r as cstr) nontriv ->
-    if d != Lt && Univ.Level.equal l r then nontriv
-    else if d == Le && is_type0m_univ (Univ.Universe.make l) then nontriv
-    else Constraint.add cstr nontriv)
-    cst Constraint.empty
-
 let add_list_map u t map = 
   let l, d, r = LMap.split u map in
   let d' = match d with None -> [t] | Some l -> t :: l in
@@ -593,7 +586,7 @@ let normalize_univ_variable ~find ~update =
     let b' = subst_univs_universe aux b in
       if Universe.equal b' b then b
       else update cur b'
-  in fun b -> try aux b with Not_found -> Universe.make b
+  in aux
 
 let normalize_univ_variable_opt_subst ectx =
   let find l = 
@@ -621,6 +614,15 @@ let normalize_universe_subst subst =
   let normlevel = normalize_univ_variable_subst subst in
     subst_univs_universe normlevel
 
+let normalize_opt_subst ctx = 
+  let ectx = ref ctx in
+  let normalize = normalize_univ_variable_opt_subst ectx in
+  let () =
+    Univ.LMap.iter (fun u v ->
+      if Option.is_empty v then ()
+      else try ignore(normalize u) with Not_found -> assert(false)) ctx 
+  in !ectx
+
 type universe_opt_subst = universe option universe_map
 	  
 let make_opt_subst s = 
@@ -633,17 +635,16 @@ let subst_opt_univs_constr s =
   let f = make_opt_subst s in
     Vars.subst_univs_fn_constr f
 
+
 let normalize_univ_variables ctx = 
-  let ectx = ref ctx in
-  let normalize = normalize_univ_variable_opt_subst ectx in
-  let _ = Univ.LMap.iter (fun u _ -> ignore(normalize u)) ctx in
-  let undef, def, subst = 
+  let ctx = normalize_opt_subst ctx in
+  let undef, def, subst =
     Univ.LMap.fold (fun u v (undef, def, subst) -> 
       match v with
       | None -> (Univ.LSet.add u undef, def, subst)
       | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
-    !ectx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
-  in !ectx, undef, def, subst
+    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
+  in ctx, undef, def, subst
 
 let pr_universe_body = function
   | None -> mt ()
@@ -871,10 +872,8 @@ let normalize_context_set ctx us algs =
   let ctx', us, algs, inst, noneqs = 
     minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
   in
-  let us = ref us in
-  let norm = normalize_univ_variable_opt_subst us in
-  let _normalize_subst = LMap.iter (fun u v -> ignore(norm u)) !us in
-    (!us, algs), (ctx', Constraint.union noneqs eqs)
+  let us = normalize_opt_subst us in
+    (us, algs), (ctx', Constraint.union noneqs eqs)
 
 (* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
 (* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
@@ -890,18 +889,6 @@ let universes_of_constr c =
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
-let shrink_universe_context (univs,csts) s =
-  let univs' = LSet.inter univs s in
-    Constraint.fold (fun (l,d,r as c) (univs',csts) ->
-      if LSet.mem l univs' then
-	let univs' = if LSet.mem r univs then LSet.add r univs' else univs' in
-	  (univs', Constraint.add c csts)
-      else if LSet.mem r univs' then
-	let univs' = if LSet.mem l univs then LSet.add l univs' else univs' in
-	  (univs', Constraint.add c csts)
-      else (univs', csts))
-      csts (univs',Constraint.empty)
-
 let restrict_universe_context (univs,csts) s =
   (* Universes that are not necessary to typecheck the term.
      E.g. univs introduced by tactics and not used in the proof term. *)
@@ -971,10 +958,3 @@ let refresh_constraints univs (ctx, cstrs) =
       else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
-
-let remove_trivial_constraints (ctx, cstrs) =
-  let cstrs' = 
-    Univ.Constraint.fold (fun c acc ->
-      if is_prop_leq c then Univ.Constraint.remove c acc
-      else acc) cstrs cstrs
-  in (ctx, cstrs')
diff --git a/library/universes.mli b/library/universes.mli
index 4cc92543b2..691f404aa2 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -194,15 +194,12 @@ val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
 (** Shrink a universe context to a restricted set of variables *)
 
 val universes_of_constr : constr -> universe_set
-val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set
 val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set
 val simplify_universe_context : universe_context_set -> 
   universe_context_set * universe_level_subst
 
 val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
 
-val remove_trivial_constraints : universe_context_set -> universe_context_set
-
 (** Pretty-printing *)
 
 val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index adcc7bf381..8173e7b972 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1181,25 +1181,11 @@ let subst_univs_context_with_def def usubst (ctx, cst) =
 let subst_univs_context usubst ctx =
   subst_univs_context_with_def (Univ.LMap.universes usubst) (Univ.make_subst usubst) ctx
 
-let subst_univs_universes s g = 
-  Univ.LMap.fold (fun u v g ->
-    (* Problem here: we might have instantiated an algebraic universe... *)
-    Univ.enforce_constraint (u, Univ.Eq, Option.get (Univ.Universe.level v)) g) s g
-
-let subst_univs_opt_universes s g = 
-  Univ.LMap.fold (fun u v g ->
-    (* Problem here: we might have instantiated an algebraic universe... *)
-    match v with
-    | Some l ->
-      Univ.enforce_constraint (u, Univ.Eq, Option.get (Univ.Universe.level l)) g
-    | None -> g) s g
-
 let normalize_evar_universe_context_variables uctx =
   let normalized_variables, undef, def, subst = 
     Universes.normalize_univ_variables uctx.uctx_univ_variables 
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
-  (* let univs = subst_univs_universes subst uctx.uctx_universes in *)
   let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
     subst, { uctx with uctx_local = ctx_local';
       uctx_univ_variables = normalized_variables;
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 99c3e977c0..56f9cb5647 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -339,7 +339,6 @@ let context l =
   in
   let uctx = Evd.universe_context_set !evars in
   let fn status (id, b, t) =
-    (* let uctx = Universes.shrink_universe_context uctx (Universes.universes_of_constr t) in *)
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let uctx = Univ.ContextSet.to_context uctx in	
       let decl = (ParameterEntry (None,false,(t,uctx),None), IsAssumption Logical) in