From 6e49d0bee79cd68495955deb115b495fb01f01fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 11:52:19 +0100
Subject: Hardening universe abstraction in Cooking.

---
 kernel/cooking.ml | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7b921d35be..31988ac1c1 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -177,12 +177,14 @@ let cook_constr { Opaqueproof.modlist ; abstract } c =
   let hyps = Context.Named.map expmod (pi1 abstract) 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 ->  
+  | Monomorphic_const ctx ->
+    assert (AUContext.is_empty auctx0);
+    subst, (Monomorphic_const ctx)
+  | Polymorphic_const auctx ->
     if (Univ.LMap.is_empty subst) then
-      subst, (Polymorphic_const auctx)
+      subst, (Polymorphic_const (AUContext.union auctx0 auctx))
     else
       let len = Univ.LMap.cardinal subst in
       let rec gen_subst i acc =
@@ -193,13 +195,13 @@ let lift_univs cb subst =
       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')
+      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 +236,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;
-- 
cgit v1.2.3


From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 13:57:10 +0100
Subject: Returning instance instead of substitution in universe context
 abstraction.

This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
---
 kernel/cooking.ml      | 22 +++++++++-------------
 kernel/indtypes.ml     |  8 ++++++--
 kernel/mod_typing.ml   |  4 ++--
 kernel/opaqueproof.ml  |  2 +-
 kernel/opaqueproof.mli |  2 +-
 kernel/term_typing.ml  |  1 +
 kernel/univ.ml         |  2 +-
 kernel/univ.mli        |  4 ++--
 8 files changed, 23 insertions(+), 22 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31988ac1c1..1f407fc298 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -168,13 +168,14 @@ 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 auctx0 =
@@ -183,18 +184,13 @@ let lift_univs cb subst auctx0 =
     assert (AUContext.is_empty auctx0);
     subst, (Monomorphic_const ctx)
   | Polymorphic_const auctx ->
-    if (Univ.LMap.is_empty subst) then
+    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
+      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 } =
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..fee431ff43 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1168,7 +1168,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..324167890a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -470,9 +470,9 @@ 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
 
-val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
+val abstract_universes : UContext.t -> Instance.t * AUContext.t
 
-val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
+val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 
 val make_abstract_instance : AUContext.t -> Instance.t
 
-- 
cgit v1.2.3


From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 17:33:04 +0100
Subject: 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.
---
 kernel/univ.ml  | 32 --------------------------------
 kernel/univ.mli |  9 +++++----
 kernel/vars.ml  | 43 -------------------------------------------
 kernel/vars.mli |  6 ------
 4 files changed, 5 insertions(+), 85 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fee431ff43..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 ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 324167890a..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
+(** Creates [u(0) ↦ 0; ...; u(n-1) ↦ n - 1] out of [u(0); ...; u(n - 1)] *)
+
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
 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
-- 
cgit v1.2.3


From 4131f060ac42f121685817fcc9546c3899c09ab7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 31 Dec 2017 21:05:16 +0100
Subject: Add a comment about universe lifting in sections in the kernel.

---
 kernel/cooking.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1f407fc298..23a578d993 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -184,6 +184,17 @@ let lift_univs cb subst auctx0 =
     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))
-- 
cgit v1.2.3