diff options
40 files changed, 182 insertions, 225 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index a890f2cef..4846a9af8 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -33,11 +33,10 @@ open Names (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type sorts = - | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) + | Prop + | Set + | Type of Univ.universe (** {6 The sorts family of CCI. } *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 916934a81..bcb71fe55 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t = (* Prop and Set are small *) let is_small_sort = function - | Prop _ -> true + | Prop | Set -> true | _ -> false let is_logic_sort = function -| Prop Null -> true +| Prop -> true | _ -> false (* [infos] is a sequence of pair [islogic,issmall] for each type in @@ -186,10 +186,10 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, ImpredicativeSet -> () - | Prop Pos, _ -> + | Set, ImpredicativeSet -> () + | Set, _ -> if not small then failwith "impredicative Set inductive type" - | Prop Null,_ -> () + | Prop,_ -> () let sort_of_ind = function diff --git a/checker/inductive.ml b/checker/inductive.ml index e1c6b135d..b1edec556 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -101,7 +101,7 @@ let instantiate_params full t u args sign = substl subs ty let full_inductive_instantiate mib u params sign = - let dummy = Prop Null in + let dummy = Prop in let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) @@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> Univ.type0m_univ -| Prop Pos -> Univ.type0_univ +| Prop -> Univ.type0m_univ +| Set -> Univ.type0_univ (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) (* in the domain or add [u |-> sup x su] if [u] is already mapped *) @@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts = let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) - if Univ.is_type0m_univ level then Prop Null + if Univ.is_type0m_univ level then Prop (* Non singleton type not containing types are interpretable in Set *) - else if Univ.is_type0_univ level then Prop Pos + else if Univ.is_type0_univ level then Set (* This is a Type with constraints *) else Type level in @@ -226,8 +226,8 @@ let type_of_inductive env mip = (* The max of an array of universes *) let cumulate_constructor_univ u = function - | Prop Null -> u - | Prop Pos -> Univ.sup Univ.type0_univ u + | Prop -> u + | Set -> Univ.sup Univ.type0_univ u | Type u' -> Univ.sup u u' let max_inductive_sort = diff --git a/checker/print.ml b/checker/print.ml index fc9cd687e..247c811f8 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -57,8 +57,8 @@ let print_pure_constr fmt csr = fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c and pp_sort fmt = function - | Prop(Pos) -> pp_print_string fmt "Set" - | Prop(Null) -> pp_print_string fmt "Prop" + | Set -> pp_print_string fmt "Set" + | Prop -> pp_print_string fmt "Prop" | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) and pp_name fmt = function diff --git a/checker/reduction.ml b/checker/reduction.ml index 4e508dc77..16c701213 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -210,29 +210,26 @@ let convert_constructors let sort_cmp env univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible - | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible - | (Prop c1, Type u) -> + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) | Set, Type _ -> + if not (pb = CUMUL) then raise NotConvertible + | Type u1, Type u2 -> + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with - CUMUL -> () - | _ -> raise NotConvertible) - | (Type u1, Type u2) -> - (** FIXME: handle type-in-type option here *) - if (* snd (engagement env) == StratifiedType && *) - not - (match pb with - | CONV -> Univ.check_eq univ u1 u2 - | CUMUL -> Univ.check_leq univ u1 u2) - then begin - if !Flags.debug then begin - let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( - str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ) - end; - raise NotConvertible - end - | (_, _) -> raise NotConvertible + | CONV -> Univ.check_eq univ u1 u2 + | CUMUL -> Univ.check_leq univ u1 u2) + then begin + if !Flags.debug then begin + let op = match pb with CONV -> "=" | CUMUL -> "<=" in + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) + end; + raise NotConvertible + end + | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible let rec no_arg_available = function | [] -> true diff --git a/checker/term.ml b/checker/term.ml index 509634bdb..d84491b38 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -20,15 +20,15 @@ open Cic (* Sorts. *) let family_of_sort = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type _ -> InType let family_equal = (==) let sort_of_univ u = - if Univ.is_type0m_univ u then Prop Null - else if Univ.is_type0_univ u then Prop Pos + if Univ.is_type0m_univ u then Prop + else if Univ.is_type0_univ u then Set else Type u (********************************************************************) @@ -356,15 +356,11 @@ let rec isArity c = (* alpha conversion : ignore print names and casts *) let compare_sorts s1 s2 = match s1, s2 with -| Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> true - | Pos, Null -> false - | Null, Pos -> false - end +| Prop, Prop | Set, Set -> true | Type u1, Type u2 -> Univ.Universe.equal u1 u2 -| Prop _, Type _ -> false -| Type _, Prop _ -> false +| Prop, Set | Set, Prop -> false +| (Prop | Set), Type _ -> false +| Type _, (Prop | Set) -> false let eq_puniverses f (c1,u1) (c2,u2) = Univ.Instance.equal u1 u2 && f c1 c2 diff --git a/checker/typeops.ml b/checker/typeops.ml index 345ee5b8f..19ede4b9a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv = 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 engagement env = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Univ.sup u1 Univ.type0_univ) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2) + | Set, Type u2 -> Type (Univ.sup Univ.type0_univ 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 (Univ.sup u1 u2) + | Type u1, Type u2 -> Type (Univ.sup u1 u2) (* Type of a type cast *) @@ -239,7 +239,7 @@ let type_fixpoint env lna lar lbody vdefj = let rec execute env cstr = match cstr with (* Atomic terms *) - | Sort (Prop _) -> judge_of_prop + | Sort (Prop | Set) -> judge_of_prop | Sort (Type u) -> judge_of_type u diff --git a/checker/values.ml b/checker/values.ml index 4f28d6e44..88cdb644d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli +MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli *) @@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] diff --git a/dev/ci/user-overlays/07863-rm-sorts-contents.sh b/dev/ci/user-overlays/07863-rm-sorts-contents.sh new file mode 100644 index 000000000..374a61484 --- /dev/null +++ b/dev/ci/user-overlays/07863-rm-sorts-contents.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7863" ] || [ "$CI_BRANCH" = "rm-sorts-contents" ]; then + Elpi_CI_BRANCH=fix-sorts-contents + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 844ad9188..811abd67f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -301,8 +301,8 @@ let constr_display csr = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ()) and sort_display = function - | Prop(Pos) -> "Prop(Pos)" - | Prop(Null) -> "Prop(Null)" + | Set -> "Set" + | Prop -> "Prop" | Type u -> univ_display u; "Type("^(string_of_int !cnt)^")" @@ -423,8 +423,8 @@ let print_pure_constr csr = Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u) and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> open_hbox(); print_string "Type("; pp (pr_uni u); print_string ")"; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 7589e5348..c8385da61 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -26,8 +26,8 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> print_string "Type" diff --git a/engine/evd.ml b/engine/evd.ml index 945cba58f..761ae7983 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -855,7 +855,7 @@ let normalize_universe_instance evd l = let normalize_sort evars s = match s with - | Prop _ -> s + | Prop | Set -> s | Type u -> let u' = normalize_universe evars u in if u' == u then s else Type u' diff --git a/engine/namegen.ml b/engine/namegen.ml index 23c691139..978f33b68 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -137,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *) s ^ Unicode.lowercase_first_char s' let sort_hdchar = function - | Prop(_) -> "P" - | Type(_) -> "T" + | Prop -> "P" + | Set -> "S" + | Type _ -> "T" let hdchar env sigma c = let rec hdrec k c = diff --git a/engine/termops.ml b/engine/termops.ml index 2db2e07bf..2b179c43b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -25,8 +25,8 @@ module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) let print_sort = function - | Prop Pos -> (str "Set") - | Prop Null -> (str "Prop") + | Set -> (str "Set") + | Prop -> (str "Prop") | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function @@ -1162,15 +1162,14 @@ let is_template_polymorphic env sigma f = let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb == Reduction.CUMUL - | (Type u1, Type u2) -> true - | _ -> false + | Prop, Prop | Set, Set | Type _, Type _ -> true + | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL + | Set, Prop | Type _, Prop | Type _, Set -> false let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Null -> true + | Prop -> true | _ -> false end | Cast (c,_,_) -> is_Prop sigma c @@ -1179,7 +1178,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with let rec is_Set sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Pos -> true + | Set -> true | _ -> false end | Cast (c,_,_) -> is_Set sigma c 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. } *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4c6156a38..4a691e442 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -130,8 +130,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index cc9c2046d..84baea964 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,11 +199,12 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bf9e37aa7..5c4cbefad 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) match (EConstr.kind !evdref x, EConstr.kind !evdref y) with | Sort s, Sort s' -> (match ESorts.kind !evdref s, ESorts.kind !evdref s' with - | Prop x, Prop y when x == y -> None - | Prop _, Type _ -> None + | Prop, Prop | Set, Set -> None + | (Prop | Set), Type _ -> None | Type x, Type y when Univ.Universe.equal x y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2bc603a90..d7118efd7 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels let open Glob_term in begin match ps, ESorts.kind sigma s with - | GProp, Prop Null -> subst - | GSet, Prop Pos -> subst + | GProp, Prop -> subst + | GSet, Set -> subst | GType _, Type _ -> subst | _ -> raise PatternMatchingFailure end diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 23a985dc3..d0de2f8c0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -597,8 +597,8 @@ let detype_universe sigma u = Univ.Universe.map fn u let detype_sort sigma = function - | Prop Null -> GProp - | Prop Pos -> GSet + | Prop -> GProp + | Set -> GSet | Type u -> GType (if !print_universes diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 8afb9b942..3f5d186d4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) - | Prop Pos when refreshset && not direction -> + | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 622a8e982..685aa400b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -150,8 +150,8 @@ let pattern_of_constr env sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop Null) -> PSort GProp - | Sort (Prop Pos) -> PSort GSet + | Sort Prop -> PSort GProp + | Sort Set -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 746a68b21..7e43c5e41 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> Sorts.type1 + | Prop | Set -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with - | _, (Prop Null as s) -> s - | Prop _, (Prop Pos as s) -> s - | Type _, (Prop Pos as s) when is_impredicative_set env -> s - | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ) - | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) - | Prop Null, (Type _ as s) -> s - | Type u1, Type u2 -> Type (Univ.sup u1 u2)) + let dom = sort_of env t in + let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in + Typeops.sort_of_product env dom rang | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cf34ac016..a66ecaaac 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -241,10 +241,6 @@ let judge_of_set = { uj_val = EConstr.mkSet; uj_type = EConstr.mkSort Sorts.type1 } -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_type u = let uu = Univ.Universe.super u in { uj_val = EConstr.mkType u; @@ -333,10 +329,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with - | Prop c -> - sigma, judge_of_prop_contents c - | Type u -> - sigma, judge_of_type u + | Prop -> sigma, judge_of_prop + | Set -> sigma, judge_of_set + | Type u -> sigma, judge_of_type u end | Proj (p, c) -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 773fc1520..9c5fdcd1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -477,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index 91c577405..0e3921570 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -942,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the diff --git a/tactics/inv.ml b/tactics/inv.ml index 755494c2d..e467eacd9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 6057c05f5..0387b32ba 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly = else sigma let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) + u = Prop || (is_impredicative_set env && u = Set) let interp_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in @@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds = let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> - if a = Prop Null then None + if a = Prop then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = @@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds = (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du + Evd.set_leq_sort env evd Set du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du + Evd.set_eq_sort env evd Prop du else evd else Evd.set_eq_sort env evd (Type cu) du in diff --git a/vernac/record.ml b/vernac/record.ml index 202c9b92f..2d7800827 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -164,8 +164,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in let sigma = Evd.minimize_universes sigma in |