Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 43 insertions, 13 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 09bf695915..8263c68bf5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -53,6 +53,7 @@ struct
   end
 
   type t =
+    | SProp
     | Prop
     | Set
     | Level of UGlobal.t
@@ -63,6 +64,7 @@ struct
   let equal x y =
     x == y ||
       match x, y with
+      | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
       | Level l, Level l' -> UGlobal.equal l l'
@@ -71,6 +73,9 @@ struct
 
   let compare u v =
     match u, v with
+    | SProp, SProp -> 0
+    | SProp, _ -> -1
+    | _, SProp -> 1
     | Prop,Prop -> 0
     | Prop, _ -> -1
     | _, Prop -> 1
@@ -88,6 +93,7 @@ struct
   let hequal x y =
     x == y ||
       match x, y with
+      | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
       | Level (n,d), Level (n',d') ->
@@ -96,6 +102,7 @@ struct
       | _ -> false
 
   let hcons = function
+    | SProp as x -> x
     | Prop as x -> x
     | Set as x -> x
     | Level (d,n) as x ->
@@ -106,8 +113,9 @@ struct
   open Hashset.Combine
 
   let hash = function
-    | Prop -> combinesmall 1 0
-    | Set -> combinesmall 1 1
+    | SProp -> combinesmall 1 0
+    | Prop -> combinesmall 1 1
+    | Set -> combinesmall 1 2
     | Var n -> combinesmall 2 n
     | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
 
@@ -118,6 +126,7 @@ module Level = struct
   module UGlobal = RawLevel.UGlobal
 
   type raw_level = RawLevel.t =
+  | SProp
   | Prop
   | Set
   | Level of UGlobal.t
@@ -155,11 +164,13 @@ module Level = struct
 
   let set = make Set
   let prop = make Prop
+  let sprop = make SProp
 
   let is_small x = 
     match data x with
     | Level _ -> false
     | Var _ -> false
+    | SProp -> true
     | Prop -> true
     | Set -> true
  
@@ -173,12 +184,18 @@ module Level = struct
     | Set -> true
     | _ -> false
 
+  let is_sprop x =
+    match data x with
+    | SProp -> true
+    | _ -> false
+
   let compare u v =
     if u == v then 0
     else RawLevel.compare (data u) (data v)
 	    
   let to_string x = 
     match data x with
+    | SProp -> "SProp"
     | Prop -> "Prop"
     | Set -> "Set"
     | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
@@ -188,6 +205,7 @@ module Level = struct
 
   let apart u v =
     match data u, data v with
+    | SProp, _ | _, SProp
     | Prop, Set | Set, Prop -> true
     | _ -> false
 
@@ -308,6 +326,7 @@ struct
 	  if Int.equal n n' then Level.compare x x'
 	  else n - n'
 
+    let sprop = hcons (Level.sprop, 0)
     let prop = hcons (Level.prop, 0)
     let set = hcons (Level.set, 0)
     let type1 = hcons (Level.set, 1)
@@ -326,16 +345,16 @@ struct
       let cmp = Level.compare u v in
 	if Int.equal cmp 0 then n <= n'
 	else if n <= n' then 
-	  (Level.is_prop u && Level.is_small v)
+          (Level.is_prop u && not (Level.is_sprop v))
 	else false
 
     let successor (u,n) =
-      if Level.is_prop u then type1
+      if Level.is_small u then type1
       else (u, n + 1)
 
     let addn k (u,n as x) = 
       if k = 0 then x 
-      else if Level.is_prop u then
+      else if Level.is_small u then
 	(Level.set,n+k)
       else (u,n+k)
 
@@ -353,13 +372,16 @@ struct
        left expression is "smaller" than the right one in both cases. *)
     let super (u,n) (v,n') =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then SuperSame (n < n')
+        if Int.equal cmp 0 then SuperSame (n < n')
 	else
           let open RawLevel in
           match Level.data u, n, Level.data v, n' with
-          | Prop, _, Prop, _ -> SuperSame (n < n')
-          | Prop, 0, _, _ -> SuperSame true
-          | _, _, Prop, 0 -> SuperSame false
+          | SProp, _, SProp, _ | Prop, _, Prop, _ -> SuperSame (n < n')
+          | SProp, 0, Prop, 0 -> SuperSame true
+          | Prop, 0, SProp, 0 -> SuperSame false
+          | (SProp | Prop), 0, _, _ -> SuperSame true
+          | _, _, (SProp | Prop), 0 -> SuperSame false
+
           | _, _, _, _ -> SuperDiff cmp
 
     let to_string (v, n) =
@@ -445,6 +467,8 @@ struct
     | [l] -> Expr.is_small l
     | _ -> false
 
+  let sprop = tip Expr.sprop
+
   (* The lower predicative level of the hierarchy that contains (impredicative)
      Prop and singleton inductive types *)
   let type0m = tip Expr.prop
@@ -454,8 +478,9 @@ struct
 
   (* When typing [Prop] and [Set], there is no constraint on the level,
      hence the definition of [type1_univ], the type of [Prop] *)    
-  let type1 = tip (Expr.successor Expr.set)
+  let type1 = tip Expr.type1
 
+  let is_sprop x = equal sprop x
   let is_type0m x = equal type0m x
   let is_type0 x = equal type0 x
 
@@ -656,7 +681,7 @@ let enforce_eq u v c =
 let constraint_add_leq v u c =
   (* We just discard trivial constraints like u<=u *)
   if Expr.equal v u then c
-  else 
+  else
     match v, u with
     | (x,n), (y,m) -> 
     let j = m - n in
@@ -679,7 +704,12 @@ let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
-  List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
+  match is_sprop u, is_sprop v with
+  | true, true -> c
+  | true, false | false, true ->
+    raise (UniverseInconsistency (Le, u, v, None))
+  | false, false ->
+    List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
@@ -845,7 +875,7 @@ struct
     else Array.append x y
 
   let of_array a =
-    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    assert(Array.for_all (fun x -> not (Level.is_prop x || Level.is_sprop x)) a);
     a
 
   let to_array a = a