Merge PR #7863: Remove Sorts.contents

12 files changed, 75 insertions, 106 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 521f540d2..487385a78 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -235,8 +235,8 @@ open Util
 let pp_sort s =
   let open Sorts in
   match s with
-  | Prop Null -> str "Prop"
-  | Prop Pos -> str "Set"
+  | Prop -> str "Prop"
+  | Set -> str "Set"
   | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
 
 let rec pp_struct_const = function
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 7a27a3d20..881bfae19 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -498,7 +498,7 @@ let rec compile_lam env cenv lam sz cont =
     else comp_app compile_structured_constant compile_universe cenv
         (Const_ind ind) (Univ.Instance.to_array u) sz cont
 
-  | Lsort (Sorts.Prop _ as s) ->
+  | Lsort (Sorts.Prop | Sorts.Set as s) ->
     compile_structured_constant cenv (Const_sort s) sz cont
   | Lsort (Sorts.Type u) ->
     (* We represent universes as a global constant with local universes
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e68f906ec..45812b5a1 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -130,8 +130,8 @@ let mkProp   = Sort Sorts.prop
 let mkSet    = Sort Sorts.set
 let mkType u = Sort (Sorts.Type u)
 let mkSort   = function
-  | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *)
-  | Sorts.Prop Sorts.Pos -> mkSet
+  | Sorts.Prop -> mkProp (* Easy sharing *)
+  | Sorts.Set -> mkSet
   | s -> Sort s
 
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
@@ -260,17 +260,17 @@ let isSort c = match kind c with
   | _ -> false
 
 let rec isprop c = match kind c with
-  | Sort (Sorts.Prop _) -> true
+  | Sort (Sorts.Prop | Sorts.Set) -> true
   | Cast (c,_,_) -> isprop c
   | _ -> false
 
 let rec is_Prop c = match kind c with
-  | Sort (Sorts.Prop Sorts.Null) -> true
+  | Sort Sorts.Prop -> true
   | Cast (c,_,_) -> is_Prop c
   | _ -> false
 
 let rec is_Set c = match kind c with
-  | Sort (Sorts.Prop Sorts.Pos) -> true
+  | Sort Sorts.Set -> true
   | Cast (c,_,_) -> is_Set c
   | _ -> false
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9130b8778..584c1af03 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -130,11 +130,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let sort_as_univ = let open Sorts in function
-| Type u -> u
-| Prop Null -> Universe.type0m
-| Prop Pos -> Universe.type0
-
 (* Template polymorphism *)
 
 (* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
@@ -168,7 +163,7 @@ let make_subst env =
         (* arity is a global level which, at typing time, will be enforce *)
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
-        let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+        let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in
           make (cons_subst u s subst) (sign, exp, args)
     | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
@@ -236,8 +231,8 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
 (* The max of an array of universes *)
 
 let cumulate_constructor_univ u = let open Sorts in function
-  | Prop Null -> u
-  | Prop Pos -> Universe.sup Universe.type0 u
+  | Prop -> u
+  | Set -> Universe.sup Universe.type0 u
   | Type u' -> Universe.sup u u'
 
 let max_inductive_sort =
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index da4413a0a..3901cb9ce 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -116,7 +116,7 @@ let mk_ind_accu ind u =
 let mk_sort_accu s u =
   let open Sorts in
   match s with
-  | Prop _ -> mk_accu (Asort s)
+  | Prop | Set -> mk_accu (Asort s)
   | Type s ->
      let u = Univ.Instance.of_array u in
      let s = Univ.subst_instance_universe u s in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2c61b7a01..3228a155f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -649,23 +649,19 @@ let check_leq univs u u' =
 let check_sort_cmp_universes env pb s0 s1 univs =
   let open Sorts in
   if not (type_in_type env) then
+    let check_pb u0 u1 =
+      match pb with
+      | CUMUL -> check_leq univs u0 u1
+      | CONV -> check_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | Null, _ | _, Pos -> () (* Prop <= Set *)
-        | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
-    | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
-      (match pb with
-       | CUMUL -> check_leq univs u0 u
-       | CONV -> check_eq univs u0 u)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) ->
-      (match pb with
-       | CUMUL -> check_leq univs u1 u2
-       | CONV -> check_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> ()
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> check_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> check_pb u Univ.type0_univ
+    | Type u0, Type u1 -> check_pb u0 u1
 
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
@@ -697,26 +693,23 @@ let infer_leq (univs, cstrs as cuniv) u u' =
       univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
-  let open Sorts in
-  if type_in_type env then univs
+  if type_in_type env
+  then univs
   else
+    let open Sorts in
+    let infer_pb u0 u1 =
+      match pb with
+      | CUMUL -> infer_leq univs u0 u1
+      | CONV -> infer_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | Null, _ | _, Pos -> univs (* Prop <= Set *)
-        | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
-    | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
-      (match pb with
-       | CUMUL -> infer_leq univs u0 u
-       | CONV -> infer_eq univs u0 u)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) ->
-      (match pb with
-       | CUMUL -> infer_leq univs u1 u2
-       | CONV -> infer_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> univs
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> infer_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> infer_pb u Univ.type0_univ
+    | Type u0, Type u1 -> infer_pb u0 u1
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   let cstrs' =
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index daeb90be7..a7bb08f5b 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -10,22 +10,21 @@
 
 open Univ
 
-type contents = Pos | Null
-
 type family = InProp | InSet | InType
 
 type t =
-  | Prop of contents                      (* proposition types *)
+  | Prop
+  | Set
   | Type of Universe.t
 
-let prop = Prop Null
-let set = Prop Pos
+let prop = Prop
+let set = Set
 let type1 = Type type1_univ
 
 let univ_of_sort = function
   | Type u -> u
-  | Prop Pos -> Universe.type0
-  | Prop Null -> Universe.type0m
+  | Set -> Universe.type0
+  | Prop -> Universe.type0m
 
 let sort_of_univ u =
   if is_type0m_univ u then prop
@@ -34,36 +33,34 @@ let sort_of_univ u =
 
 let compare s1 s2 =
   if s1 == s2 then 0 else
-  match s1, s2 with
-  | Prop c1, Prop c2 ->
-    begin match c1, c2 with
-    | Pos, Pos | Null, Null -> 0
-    | Pos, Null -> -1
-    | Null, Pos -> 1
-    end
-  | Type u1, Type u2 -> Universe.compare u1 u2
-  | Prop _, Type _ -> -1
-  | Type _, Prop _ -> 1
+    match s1, s2 with
+    | Prop, Prop -> 0
+    | Prop, _ -> -1
+    | Set, Prop -> 1
+    | Set, Set -> 0
+    | Set, _ -> -1
+    | Type u1, Type u2 -> Universe.compare u1 u2
+    | Type _, _ -> -1
 
 let equal s1 s2 = Int.equal (compare s1 s2) 0
 
 let is_prop = function
-  | Prop Null -> true
+  | Prop -> true
   | Type u when Universe.equal Universe.type0m u -> true
   | _ -> false
 
 let is_set = function
-  | Prop Pos -> true
+  | Set -> true
   | Type u when Universe.equal Universe.type0 u -> true
   | _ -> false
 
 let is_small = function
-  | Prop _ -> true
+  | Prop | Set -> true
   | Type u -> is_small_univ u
 
 let family = function
-  | Prop Null -> InProp
-  | Prop Pos -> InSet
+  | Prop -> InProp
+  | Set -> InSet
   | Type u when is_type0m_univ u -> InProp
   | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
@@ -73,15 +70,11 @@ let family_equal = (==)
 open Hashset.Combine
 
 let hash = function
-| Prop p ->
-  let h = match p with
-  | Pos -> 0
-  | Null -> 1
-  in
-  combinesmall 1 h
-| Type u ->
- let h = Univ.Universe.hash u in
-  combinesmall 2 h
+  | Prop -> combinesmall 1 0
+  | Set -> combinesmall 1 1
+  | Type u ->
+    let h = Univ.Universe.hash u in
+    combinesmall 2 h
 
 module List = struct
   let mem = List.memq
@@ -101,7 +94,7 @@ module Hsorts =
 	    if u' == u then c else Type u'
         | s -> s
       let eq s1 s2 = match (s1,s2) with
-        | (Prop c1, Prop c2) -> c1 == c2
+        | Prop, Prop | Set, Set -> true
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
 
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 1bbde2608..cac6229b9 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -10,13 +10,12 @@
 
 (** {6 The sorts of CCI. } *)
 
-type contents = Pos | Null
-
 type family = InProp | InSet | InType
 
 type t =
-| Prop of contents       (** Prop and Set *)
-| Type of Univ.Universe.t  (** Type *)
+  | Prop
+  | Set
+  | Type of Univ.Universe.t
 
 val set  : t
 val prop : t
diff --git a/kernel/term.ml b/kernel/term.ml
index b44e038e9..81e344e73 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -16,14 +16,11 @@ open Vars
 open Constr
 
 (* Deprecated *)
-type contents = Sorts.contents = Pos | Null
-[@@ocaml.deprecated "Alias for Sorts.contents"]
-
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
 type sorts = Sorts.t =
-  | Prop of Sorts.contents   (** Prop and Set *)
+  | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
 
diff --git a/kernel/term.mli b/kernel/term.mli
index f651d1a58..4d340399d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -190,13 +190,10 @@ type ('constr, 'types) kind_of_type =
 val kind_of_type : types -> (constr, types) kind_of_type
 
 (* Deprecated *)
-type contents = Sorts.contents = Pos | Null
-[@@ocaml.deprecated "Alias for Sorts.contents"]
-
 type sorts_family = Sorts.family = InProp | InSet | InType
 [@@ocaml.deprecated "Alias for Sorts.family"]
 
 type sorts = Sorts.t =
-  | Prop of Sorts.contents   (** Prop and Set *)
+  | Prop | Set
   | Type of Univ.Universe.t  (** Type *)
 [@@ocaml.deprecated "Alias for Sorts.t"]
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 34ed2afb2..7c0057696 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -69,7 +69,7 @@ let type_of_type u =
     mkType uu
 
 let type_of_sort = function
-  | Prop c -> type1
+  | Prop | Set -> type1
   | Type u -> type_of_type u
 
 (*s Type of a de Bruijn index. *)
@@ -178,11 +178,11 @@ let type_of_apply env func funt argsv argstv =
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
     (* Product rule (s,Prop,Prop) *)
-    | (_,       Prop Null)  -> rangsort
+    | (_,       Prop)  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
-    | (Prop _,  Prop Pos) -> rangsort
+    | ((Prop | Set),  Set) -> rangsort
     (* Product rule (Type,Set,?) *)
-    | (Type u1, Prop Pos) ->
+    | (Type u1, Set) ->
         if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
@@ -190,9 +190,9 @@ let sort_of_product env domsort rangsort =
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
+    | (Set,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Null, Type _)  -> rangsort
+    | (Prop, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
     | (Type u1, Type u2) -> Type (Universe.sup u1 u2)
 
@@ -481,10 +481,6 @@ let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1
 let judge_of_type u = make_judge (mkType u) (type_of_type u)
 
-let judge_of_prop_contents = function
-  | Null -> judge_of_prop
-  | Pos -> judge_of_set
-
 let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
 
 let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 546f2d2b4..3b2abc777 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -43,7 +43,6 @@ val type1 : types
 val type_of_sort : Sorts.t -> types
 val judge_of_prop : unsafe_judgment
 val judge_of_set  : unsafe_judgment
-val judge_of_prop_contents  : Sorts.contents -> unsafe_judgment
 val judge_of_type           : Universe.t -> unsafe_judgment
 
 (** {6 Type of a bound variable. } *)