From 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Dec 2018 10:33:47 +0100
Subject: Fix race condition triggered by fresh universe generation

Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
---
 kernel/indtypes.ml  |  2 +-
 kernel/inductive.ml |  2 +-
 kernel/uGraph.ml    |  2 +-
 kernel/univ.ml      | 50 +++++++++++++++++++++++++++++++++++++++-----------
 kernel/univ.mli     | 31 ++++++++++++++++++++++++++++---
 5 files changed, 70 insertions(+), 17 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a4a02791b4..8efda16d64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,7 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
     let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+    let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
     let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
         LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
     in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bbcf07f7e..30d96a22e0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -594,7 +594,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      | _ -> assert false
 
 let lambda_implicit_lift n a =
-  let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
+  let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in
   let implicit_sort = mkType (Universe.make level) in
   let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index afdc8f1511..064fffe98e 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
   let types = Array.init (max_lvl + 1) (function
     | 0 -> Level.prop
     | 1 -> Level.set
-    | n -> Level.make mp (n-2))
+    | n -> Level.make2 mp (Level.Id.make (n-2)))
   in
   let g = Array.fold_left (fun g u ->
     let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..57a5dce8a4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,10 +36,35 @@ open Util
 module RawLevel =
 struct
   open Names
+
+  module Id = struct
+    type t = int
+
+    let make i = i
+    let to_string i = string_of_int i
+
+  end
+
+  module Qualid = struct
+    type t = DirPath.t * Id.t
+
+    let make dp i = (dp,i)
+    let repr x = x
+
+    let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+
+    let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+
+    let compare (d, i) (d', i') =
+      let c = Int.compare i i' in
+      if Int.equal c 0 then DirPath.compare d d'
+      else c
+  end
+
   type t =
     | Prop
     | Set
-    | Level of int * DirPath.t
+    | Level of Qualid.t
     | Var of int
 
   (* Hash-consing *)
@@ -49,7 +74,7 @@ struct
       match x, y with
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
+      | Level (d,n), Level (d',n') ->
         Int.equal n n' && DirPath.equal d d'
       | Var n, Var n' -> Int.equal n n'
       | _ -> false
@@ -62,7 +87,7 @@ struct
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (i1, dp1), Level (i2, dp2) ->
+    | Level (dp1, i1), Level (dp2, i2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
       else DirPath.compare dp1 dp2
@@ -83,9 +108,9 @@ struct
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
-    | Level (n,d) as x -> 
+    | Level (d,n) as x ->
       let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (n,d')
+        if d' == d then x else Level (d',n)
     | Var _n as x -> x
 
   open Hashset.Combine
@@ -94,18 +119,20 @@ struct
     | Prop -> combinesmall 1 0
     | Set -> combinesmall 1 1
     | Var n -> combinesmall 2 n
-    | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+    | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 
 end
 
 module Level = struct
 
-  open Names
+  module Id = RawLevel.Id
+
+  module Qualid = RawLevel.Qualid
 
   type raw_level = RawLevel.t =
   | Prop
   | Set
-  | Level of int * DirPath.t
+  | Level of Qualid.t
   | Var of int
 
   (** Embed levels with their hash value *)
@@ -166,7 +193,7 @@ module Level = struct
     match data x with
     | Prop -> "Prop"
     | Set -> "Set"
-    | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
     | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
@@ -185,11 +212,12 @@ module Level = struct
     match data u with
     | Var n -> Some n | _ -> None
 
-  let make m n = make (Level (n, Names.DirPath.hcons m))
+  let make2 m n = make (Level (Names.DirPath.hcons m, n))
+  let make qid = make (Level qid)
 
   let name u =
     match data u with
-    | Level (n, d) -> Some (d, n)
+    | Level (d, n) -> Some (d, n)
     | _ -> None
 end
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index de7b334ae4..69aecac4f3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,9 +11,32 @@
 (** Universes. *)
 module Level :
 sig
+
+  module Id : sig
+    type t
+
+    val make : int -> t
+    val to_string : t -> string
+
+  end
+  (** Non-qualified global universe level *)
+
+  module Qualid : sig
+    type t
+
+    val make : Names.DirPath.t -> Id.t -> t
+    val repr : t -> Names.DirPath.t * Id.t
+    val equal : t -> t -> bool
+    val hash : t -> int
+    val compare : t -> t -> int
+
+  end
+  (** Qualified global universe level *)
+
   type t
   (** Type of universe levels. A universe level is essentially a unique name
-      that will be associated to constraints later on. *)
+      that will be associated to constraints later on. A level can be local to a
+      definition or global. *)
 
   val set : t
   val prop : t
@@ -34,7 +57,9 @@ sig
 
   val hash : t -> int
 
-  val make : Names.DirPath.t -> int -> t
+  val make : Qualid.t -> t
+
+  val make2 : Names.DirPath.t -> Id.t -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
@@ -48,7 +73,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> (Names.DirPath.t * int) option
+  val name : t -> Qualid.t option
 end
 
 (** Sets of universe levels *)
-- 
cgit v1.2.3


From cff3c5a7148afc722852bd01658fe49ffec1d967 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Dec 2018 15:52:37 +0100
Subject: Revise API for global universes.

Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.

Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).

Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)

This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~

Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.

UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.

NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
---
 kernel/indtypes.ml  |  4 +++-
 kernel/inductive.ml |  6 +++---
 kernel/uGraph.ml    |  2 +-
 kernel/univ.ml      | 27 +++++++--------------------
 kernel/univ.mli     | 22 ++++------------------
 5 files changed, 18 insertions(+), 43 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8efda16d64..68d44f8782 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
 let check_subtyping cumi paramsctxt env_ar inds = 
     let numparams = Context.Rel.nhyps paramsctxt in
     let uctx = CumulativityInfo.univ_context cumi in
-    let new_levels = Array.init (UContext.size uctx) (fun i -> Level.make2 DirPath.empty (Level.Id.make i)) in
+    let new_levels = Array.init (UContext.size uctx)
+        (fun i -> Level.make (Level.UGlobal.make DirPath.empty i))
+    in
     let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
         LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
     in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 30d96a22e0..05c5c0e821 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      ienv_decompose_prod ienv' (n-1) b
      | _ -> assert false
 
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_implicit_sort = mkType (Universe.make dummy_univ)
 let lambda_implicit_lift n a =
-  let level = Level.make2 (DirPath.make [Id.of_string "implicit"]) (Level.Id.make 0) in
-  let implicit_sort = mkType (Universe.make level) in
-  let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
+  let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
 
 (* This removes global parameters of the inductive types in lc (for
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 064fffe98e..5fc8d0297f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
   let types = Array.init (max_lvl + 1) (function
     | 0 -> Level.prop
     | 1 -> Level.set
-    | n -> Level.make2 mp (Level.Id.make (n-2)))
+    | n -> Level.make (Level.UGlobal.make  mp (n-2)))
   in
   let g = Array.fold_left (fun g u ->
     let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 57a5dce8a4..7b5ed05bda 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -37,19 +37,10 @@ module RawLevel =
 struct
   open Names
 
-  module Id = struct
-    type t = int
+  module UGlobal = struct
+    type t = DirPath.t * int
 
-    let make i = i
-    let to_string i = string_of_int i
-
-  end
-
-  module Qualid = struct
-    type t = DirPath.t * Id.t
-
-    let make dp i = (dp,i)
-    let repr x = x
+    let make dp i = (DirPath.hcons dp,i)
 
     let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
 
@@ -64,7 +55,7 @@ struct
   type t =
     | Prop
     | Set
-    | Level of Qualid.t
+    | Level of UGlobal.t
     | Var of int
 
   (* Hash-consing *)
@@ -74,8 +65,7 @@ struct
       match x, y with
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (d,n), Level (d',n') ->
-        Int.equal n n' && DirPath.equal d d'
+      | Level l, Level l' -> UGlobal.equal l l'
       | Var n, Var n' -> Int.equal n n'
       | _ -> false
 
@@ -125,14 +115,12 @@ end
 
 module Level = struct
 
-  module Id = RawLevel.Id
-
-  module Qualid = RawLevel.Qualid
+  module UGlobal = RawLevel.UGlobal
 
   type raw_level = RawLevel.t =
   | Prop
   | Set
-  | Level of Qualid.t
+  | Level of UGlobal.t
   | Var of int
 
   (** Embed levels with their hash value *)
@@ -212,7 +200,6 @@ module Level = struct
     match data u with
     | Var n -> Some n | _ -> None
 
-  let make2 m n = make (Level (Names.DirPath.hcons m, n))
   let make qid = make (Level qid)
 
   let name u =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 69aecac4f3..512f38cedd 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,20 +12,10 @@
 module Level :
 sig
 
-  module Id : sig
+  module UGlobal : sig
     type t
 
-    val make : int -> t
-    val to_string : t -> string
-
-  end
-  (** Non-qualified global universe level *)
-
-  module Qualid : sig
-    type t
-
-    val make : Names.DirPath.t -> Id.t -> t
-    val repr : t -> Names.DirPath.t * Id.t
+    val make : Names.DirPath.t -> int -> t
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
@@ -57,11 +47,7 @@ sig
 
   val hash : t -> int
 
-  val make : Qualid.t -> t
-
-  val make2 : Names.DirPath.t -> Id.t -> t
-  (** Create a new universe level from a unique identifier and an associated
-      module path. *)
+  val make : UGlobal.t -> t
 
   val pr : t -> Pp.t
   (** Pretty-printing *)
@@ -73,7 +59,7 @@ sig
 
   val var_index : t -> int option
 
-  val name : t -> Qualid.t option
+  val name : t -> UGlobal.t option
 end
 
 (** Sets of universe levels *)
-- 
cgit v1.2.3