Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.

1 files changed, 37 insertions, 10 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index e281751be1..1e4e4e00b4 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -10,13 +10,15 @@
 
 open Univ
 
-type family = InProp | InSet | InType
+type family = InSProp | InProp | InSet | InType
 
 type t =
+  | SProp
   | Prop
   | Set
   | Type of Universe.t
 
+let sprop = SProp
 let prop = Prop
 let set = Set
 let type1 = Type type1_univ
@@ -25,15 +27,20 @@ let univ_of_sort = function
   | Type u -> u
   | Set -> Universe.type0
   | Prop -> Universe.type0m
+  | SProp -> Universe.sprop
 
 let sort_of_univ u =
-  if is_type0m_univ u then prop
+  if Universe.is_sprop u then sprop
+  else if is_type0m_univ u then prop
   else if is_type0_univ u then set
   else Type u
 
 let compare s1 s2 =
   if s1 == s2 then 0 else
     match s1, s2 with
+    | SProp, SProp -> 0
+    | SProp, _ -> -1
+    | _, SProp -> 1
     | Prop, Prop -> 0
     | Prop, _ -> -1
     | Set, Prop -> 1
@@ -45,33 +52,51 @@ let compare s1 s2 =
 let equal s1 s2 = Int.equal (compare s1 s2) 0
 
 let super = function
-  | Prop | Set -> Type (Universe.type1)
+  | SProp | Prop | Set -> Type (Universe.type1)
   | Type u -> Type (Universe.super u)
 
+let is_sprop = function
+  | SProp -> true
+  | Prop | Set | Type _ -> false
+
 let is_prop = function
   | Prop -> true
-  | Set | Type _ -> false
+  | SProp | Set | Type _ -> false
 
 let is_set = function
   | Set -> true
-  | Prop | Type _ -> false
+  | SProp | Prop | Type _ -> false
 
 let is_small = function
-  | Prop | Set -> true
+  | SProp | Prop | Set -> true
   | Type _ -> false
 
 let family = function
+  | SProp -> InSProp
   | Prop -> InProp
   | Set -> InSet
   | Type _ -> InType
 
+let family_compare a b = match a,b with
+  | InSProp, InSProp -> 0
+  | InSProp, _ -> -1
+  | _, InSProp -> 1
+  | InProp, InProp -> 0
+  | InProp, _ -> -1
+  | _, InProp -> 1
+  | InSet, InSet -> 0
+  | InSet, _ -> -1
+  | _, InSet -> 1
+  | InType, InType -> 0
+
 let family_equal = (==)
 
 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
   | Type u ->
     let h = Univ.Universe.hash u in
     combinesmall 2 h
@@ -104,11 +129,13 @@ module Hsorts =
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
 
 let debug_print = function
-  | Set -> Pp.(str "Set")
+  | SProp -> Pp.(str "SProp")
   | Prop -> Pp.(str "Prop")
+  | Set -> Pp.(str "Set")
   | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")")
 
 let pr_sort_family = function
-  | InSet -> Pp.(str "Set")
+  | InSProp -> Pp.(str "SProp")
   | InProp -> Pp.(str "Prop")
+  | InSet -> Pp.(str "Set")
   | InType -> Pp.(str "Type")