Less footguns in universe handling: remove subst_instance_context.

This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.

5 files changed, 44 insertions, 56 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd204c7d5..ca2c8e135 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -230,8 +230,7 @@ let add_constant kn cb env =
 let constraints_of cb u =
   match cb.const_universes with
   | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
-    Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
 let map_regular_arity f = function
   | RegularArity a as ar -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be..1eaba49aa 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx = 
-    Univ.UContext.constraints (Univ.subst_instance_context u auctx)
-  in
+  let process auctx =  Univ.AUContext.instantiate u auctx in
   match mib.mind_universes with
   | Monomorphic_ind _ -> Univ.Constraint.empty
   | Polymorphic_ind auctx -> process auctx
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 423e0d934..2bf9f43a5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -689,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints 
-            (Univ.subst_instance_context comp_subst ind_subtypctx) 
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
         in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
@@ -775,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.UContext.constraints
-        (Univ.subst_instance_context comp_subst ind_subtypctx)
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
         let comp_cst' = 
           let comp_subst = (Univ.Instance.append u' u) in
-          Univ.UContext.constraints
-            (Univ.subst_instance_context comp_subst ind_subtypctx) in
+          Univ.AUContext.instantiate comp_subst ind_subtypctx
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1c887e2a9..cb19761b3 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -988,6 +988,31 @@ let enforce_eq_instances x y =
 		 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
+let subst_instance_level s l =
+  match l.Level.data with
+  | Level.Var n -> s.(n) 
+  | _ -> l
+
+let subst_instance_instance s i = 
+  Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+  let u' = Universe.smartmap f u in
+    if u == u' then u
+    else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+  let u' = subst_instance_level s u in
+  let v' = subst_instance_level s v in
+    if u' == u && v' == v then c
+    else (u',d,v')
+
+let subst_instance_constraints s csts =
+  Constraint.fold 
+    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+    csts Constraint.empty 
+
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
@@ -1031,7 +1056,15 @@ end
 type universe_context = UContext.t
 let hcons_universe_context = UContext.hcons
 
-module AUContext = UContext
+module AUContext =
+struct
+  include UContext
+
+  let instantiate inst (u, cst) =
+    assert (Array.length u = Array.length inst);
+    subst_instance_constraints inst cst
+
+end
 
 type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
@@ -1256,31 +1289,6 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
-let subst_instance_level s l =
-  match l.Level.data with
-  | Level.Var n -> s.(n) 
-  | _ -> l
-
-let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
-  let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
-  let u' = Universe.smartmap f u in
-    if u == u' then u
-    else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
-  let u' = subst_instance_level s u in
-  let v' = subst_instance_level s v in
-    if u' == u && v' == v then c
-    else (u',d,v')
-
-let subst_instance_constraints s csts =
-  Constraint.fold 
-    (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
-
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context (ctx, csts) = 
   (ctx, subst_instance_constraints ctx csts)
@@ -1378,19 +1386,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 let compare_levels = Level.compare
 let eq_levels = Level.equal
 let equal_universes = Universe.equal
-
-
-let subst_instance_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_constraints
-  else subst_instance_constraints
-
-let subst_instance_context = 
-  let subst_instance_context_body inst (inner_inst, inner_constr) =
-    (inner_inst, subst_instance_constraints inst inner_constr)
-  in
-  if Flags.profile then 
-    let key = Profile.declare_profile "subst_instance_constraints" in
-      Profile.profile2 key subst_instance_context_body
-  else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index dc6fb85a0..3d0d2234d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -329,6 +329,9 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
+  val instantiate : Instance.t -> t -> Constraint.t
+  (** Generate the set of instantiated constraints **)
+
 end
 
 type abstract_universe_context = AUContext.t
@@ -443,7 +446,6 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
 (** Substitution of instances *)
 val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
 val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
 
 val make_instance_subst : universe_instance -> universe_level_subst
 val make_inverse_instance_subst : universe_instance -> universe_level_subst