aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-27 13:28:44 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-27 13:28:44 +0200
commit04e0f9fde8789a28b66f24000ac8c831ff0815af (patch)
treeb9e3d026e192e7b5b0409594b11fb95ed138b6cb /kernel
parentd9e6bed640083fce067343f24183382cc8e6ca7b (diff)
parent8d89102e84d41956fb1359089d573cc64d7838ca (diff)
Merge PR #7863: Remove Sorts.contents
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml4
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/constr.ml10
-rw-r--r--kernel/inductive.ml11
-rw-r--r--kernel/nativevalues.ml2
-rw-r--r--kernel/reduction.ml61
-rw-r--r--kernel/sorts.ml57
-rw-r--r--kernel/sorts.mli7
-rw-r--r--kernel/term.ml5
-rw-r--r--kernel/term.mli5
-rw-r--r--kernel/typeops.ml16
-rw-r--r--kernel/typeops.mli1
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. } *)