Merge PR #6425: Cleanup universes in the kernel

10 files changed, 47 insertions, 120 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7b921d35be..23a578d993 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -168,38 +168,47 @@ let on_body ml hy f = function
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
 let expmod_constr_subst cache modlist subst c =
+  let subst = Univ.make_instance_subst subst in
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
 
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
   let cache = RefTable.create 13 in
-  let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
-  let hyps = Context.Named.map expmod (pi1 abstract) in
+  let expmod = expmod_constr_subst cache modlist subst in
+  let hyps = Context.Named.map expmod vars in
   abstract_constant_body (expmod c) hyps
 
-let lift_univs cb subst =
+let lift_univs cb subst auctx0 =
   match cb.const_universes with
-  | Monomorphic_const ctx -> subst, (Monomorphic_const ctx)
-  | Polymorphic_const auctx ->  
-    if (Univ.LMap.is_empty subst) then
-      subst, (Polymorphic_const auctx)
+  | Monomorphic_const ctx ->
+    assert (AUContext.is_empty auctx0);
+    subst, (Monomorphic_const ctx)
+  | Polymorphic_const auctx ->
+    (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract
+        context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
+        and another abstract context relative to the former context
+        [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}],
+        construct the lifted abstract universe context
+        [0 ... n - 1 n ... n + m - 1 |=
+          C{0, ... n - 1} ∪
+          C'{0, ..., n - 1, n, ..., n + m - 1} ]
+        together with the instance
+        [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)].
+    *)
+    if (Univ.Instance.is_empty subst) then
+      (** Still need to take the union for the constraints between globals *)
+      subst, (Polymorphic_const (AUContext.union auctx0 auctx))
     else
-      let len = Univ.LMap.cardinal subst in
-      let rec gen_subst i acc =
-        if i < 0 then acc
-        else
-          let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
-          gen_subst (pred i) acc
-      in
-      let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
-      let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
-      subst, (Polymorphic_const auctx')
+      let ainst = Univ.make_abstract_instance auctx in
+      let subst = Instance.append subst ainst in
+      let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
+      subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
 
 let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  let usubst, univs = lift_univs cb usubst in
+  let usubst, univs = lift_univs cb usubst abs_ctx in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
   let map c =
@@ -234,13 +243,6 @@ let cook_constant ~hcons env { from = cb; info } =
 	proj_eta = etab, etat;
 	proj_type = ty'; proj_body = c' }
   in
-  let univs =
-    match univs with
-    | Monomorphic_const ctx -> 
-      assert (AUContext.is_empty abs_ctx); univs
-    | Polymorphic_const auctx -> 
-      Polymorphic_const (AUContext.union abs_ctx auctx)
-  in
   {
     cook_body = body;
     cook_type = typ;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1f2ae0b6cc..b117f8714b 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -879,9 +879,13 @@ let abstract_inductive_universes iu =
   match iu with
   | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
   | Polymorphic_ind_entry ctx -> 
-    let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx)
+    let (inst, auctx) = Univ.abstract_universes ctx in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Polymorphic_ind auctx)
   | Cumulative_ind_entry cumi -> 
-    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+    let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+    let inst = Univ.make_instance_subst inst in
+    (inst, Cumulative_ind acumi)
 
 let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7e755f005..b7eb481ee3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
           let ctx = Univ.ContextSet.of_context ctx in
           c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
         | Polymorphic_const uctx ->
-          let subst, ctx = Univ.abstract_universes ctx in
-          let c = Vars.subst_univs_level_constr subst c in
+          let inst, ctx = Univ.abstract_universes ctx in
+          let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
           let () =
             if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
               error_incorrect_with_constraint lab
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 45a62d55a1..c2fcfbfd6a 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
+  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
 type proofterm = (constr * Univ.ContextSet.t) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 20d76ce238..c8339e6eb3 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
 
 type cooking_info = { 
   modlist : work_list; 
-  abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } 
+  abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
 
 (* The type has two caveats:
    1) cook_constr is defined after
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2e4426d621..cbc4ee2ec4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -232,6 +232,7 @@ let abstract_constant_universes = function
     Univ.empty_level_subst, Monomorphic_const uctx
   | Polymorphic_const_entry uctx ->
     let sbst, auctx = Univ.abstract_universes uctx in
+    let sbst = Univ.make_instance_subst sbst in
     sbst, Polymorphic_const auctx
 
 let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8cf9028fb1..f72f6f26a9 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -686,12 +686,6 @@ let enforce_leq u v c =
 let enforce_leq_level u v c =
   if Level.equal u v then c else Constraint.add (u,Le,v) 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
-
 (* Miscellaneous functions to remove or test local univ assumed to
    occur in a universe *)
 
@@ -718,14 +712,6 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-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
-     
 module Instance : sig 
     type t = Level.t array
 
@@ -1128,24 +1114,6 @@ let subst_univs_universe fn ul =
 	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
 	  substs nosubst
 
-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 cstrs -> subst_univs_constraint subst c cstrs)
-    csts Constraint.empty 
-
 let make_instance_subst i = 
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
@@ -1168,7 +1136,7 @@ let abstract_universes ctx =
       (UContext.constraints ctx)
   in
   let ctx = UContext.make (instance, cstrs) in
-  subst, ctx
+  instance, ctx
 
 let abstract_cumulativity_info (univcst, substcst) = 
   let instance, univcst = abstract_universes univcst in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 4593944395..63bef1b81b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,8 +238,6 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
 (** {6 Universe instances} *)
 
 module Instance :
@@ -461,18 +459,21 @@ val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
 val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t
-val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t
+(** Only user in the kernel is template polymorphism. Ideally we get rid of
+    this code if it goes away. *)
 
 (** Substitution of instances *)
 val subst_instance_instance : Instance.t -> Instance.t -> Instance.t
 val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
 
 val make_instance_subst : Instance.t -> universe_level_subst
-val make_inverse_instance_subst : Instance.t -> universe_level_subst
+(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *)
 
-val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
+val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
+val abstract_universes : UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+(** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index eae917b5a2..b3b3eff628 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -235,49 +235,6 @@ let subst_vars subst c = substn_vars 1 subst c
 (** Universe substitutions *)
 open Constr
 
-let subst_univs_fn_puniverses fn =
-  let f = Univ.Instance.subst_fn fn in
-    fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u')
-
-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 (Univ.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_level_constr subst c =
   if Univ.is_empty_level_subst subst then c
   else 
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 964de4e958..b74d25260f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr
 
 open Univ
 
-val subst_univs_fn_constr : universe_subst_fn -> constr -> constr
-val subst_univs_fn_puniverses : universe_level_subst_fn -> 
-  'a puniverses -> 'a puniverses
-
-val subst_univs_constr : universe_subst -> constr -> constr
-
 (** Level substitutions for polymorphism. *)
 
 val subst_univs_level_constr : universe_level_subst -> constr -> constr