Moving some universe substitution code out of the kernel.

This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.

4 files changed, 81 insertions, 6 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index e33c851f6..0e9472158 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -855,7 +855,7 @@ let normalize_universe evd =
 
 let normalize_universe_instance evd l =
   let vars = ref (UState.subst evd.universes) in
-  let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
+  let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
 let normalize_sort evars s =
diff --git a/engine/uState.ml b/engine/uState.ml
index 6131f4c03..6f2b3c4b2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -516,7 +516,7 @@ let is_sort_variable uctx s =
   | _ -> None
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+  (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst)
 
 let normalize_variables uctx =
   let normalized_variables, undef, def, subst = 
diff --git a/engine/universes.ml b/engine/universes.ml
index 30490ec56..eaddf98a8 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -181,6 +181,30 @@ let enforce_eq_instances_univs strict x y c =
       (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
       ax ay c
 
+let enforce_univ_constraint (u,d,v) =
+  match d with
+  | Eq -> enforce_eq u v
+  | Le -> enforce_leq u v
+  | Lt -> enforce_leq (super u) 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,Universe.make v) cstrs
+  | None, Some v -> enforce_univ_constraint (Universe.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 cstrs -> subst_univs_constraint subst c cstrs)
+    csts Constraint.empty
+
 let subst_univs_universe_constraint fn (u,d,v) =
   let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
     if Universe.equal u' v' then None
@@ -519,13 +543,60 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_fn_constr f c =
+  let changed = ref false in
+  let fu = Univ.subst_univs_universe f in
+  let fi = Univ.Instance.subst_fn (level_subst_of f) in
+  let rec aux t =
+    match kind t with
+    | Sort (Sorts.Type u) ->
+      let u' = fu u in
+        if u' == u then t else
+          (changed := true; mkSort (Sorts.sort_of_univ u'))
+    | Const (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstU (c, u'))
+    | Ind (i, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkIndU (i, u'))
+    | Construct (c, u) ->
+      let u' = fi u in
+        if u' == u then t
+        else (changed := true; mkConstructU (c, u'))
+    | _ -> map aux t
+  in
+  let c' = aux c in
+    if !changed then c' else c
+
+let subst_univs_constr subst c =
+  if Univ.is_empty_subst subst then c
+  else
+    let f = Univ.make_subst subst in
+      subst_univs_fn_constr f c
+
+let subst_univs_constr =
+  if Flags.profile then
+    let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in
+      CProfile.profile2 subst_univs_constr_key subst_univs_constr
+  else subst_univs_constr
+
 let subst_univs_fn_puniverses lsubst (c, u as cu) =
   let u' = Instance.subst_fn lsubst u in
     if u' == u then cu else (c, u')
 
 let nf_evars_and_universes_opt_subst f subst =
   let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
-  let lsubst = Univ.level_subst_of subst in
+  let lsubst = level_subst_of subst in
   let rec aux c =
     match kind c with
     | Evar (evk, args) ->
@@ -605,7 +676,7 @@ let normalize_opt_subst ctx =
   in !ectx
 
 type universe_opt_subst = Universe.t option universe_map
-	  
+
 let make_opt_subst s = 
   fun x -> 
     (match Univ.LMap.find x s with
@@ -614,8 +685,7 @@ let make_opt_subst s =
 
 let subst_opt_univs_constr s = 
   let f = make_opt_subst s in
-    Vars.subst_univs_fn_constr f
-
+  subst_univs_fn_constr f
 
 let normalize_univ_variables ctx = 
   let ctx = normalize_opt_subst ctx in
diff --git a/engine/universes.mli b/engine/universes.mli
index 1a98d969b..130dcf8bb 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -154,6 +154,11 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t ->
 
 module UF : Unionfind.PartitionSig with type elt = Level.t
 
+val level_subst_of : universe_subst_fn -> universe_level_subst_fn
+val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+
+val subst_univs_constr : universe_subst -> constr -> constr
+
 type universe_opt_subst = Universe.t option universe_map
 
 val make_opt_subst : universe_opt_subst -> universe_subst_fn