Merge PR #6425: Cleanup universes in the kernel

1 files changed, 28 insertions, 26 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;