From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 11 Oct 2017 19:41:23 +0200 Subject: Remove Sorts.contents --- kernel/cbytecodes.ml | 4 ++-- kernel/cbytegen.ml | 2 +- kernel/constr.ml | 10 ++++----- kernel/inductive.ml | 11 +++------ kernel/nativevalues.ml | 2 +- kernel/reduction.ml | 61 ++++++++++++++++++++++---------------------------- kernel/sorts.ml | 57 +++++++++++++++++++++------------------------- kernel/sorts.mli | 7 +++--- kernel/term.ml | 5 +---- kernel/term.mli | 5 +---- kernel/typeops.ml | 16 +++++-------- kernel/typeops.mli | 1 - 12 files changed, 75 insertions(+), 106 deletions(-) (limited to 'kernel') 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. } *) -- cgit v1.2.3