aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/inductive.ml6
-rw-r--r--checker/reduction.ml2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/inductive.ml14
-rw-r--r--kernel/reduction.ml19
-rw-r--r--kernel/univ.ml36
-rw-r--r--kernel/univ.mli10
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/termops.ml2
9 files changed, 44 insertions, 51 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index febe312f27..05ab5a846b 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -127,7 +127,7 @@ Remark: Set (predicative) is encoded as Type(0)
let sort_as_univ = function
| Type u -> u
-| Prop Null -> lower_univ
+| Prop Null -> type0m_univ
| Prop Pos -> type0_univ
let cons_subst u su subst =
@@ -182,7 +182,7 @@ let instantiate_universes env ctx ar argsorts =
let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
let level = subst_large_constraints subst ar.poly_level in
ctx,
- if is_lower_univ level then Prop Null
+ if is_type0m_univ level then Prop Null
else if is_type0_univ level then Prop Pos
else Type level
@@ -208,7 +208,7 @@ let cumulate_constructor_univ u = function
| Type u' -> sup u u'
let max_inductive_sort =
- Array.fold_left cumulate_constructor_univ lower_univ
+ Array.fold_left cumulate_constructor_univ type0m_univ
(************************************************************************)
(* Type of a constructor *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 503a1b29aa..45a376873a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -145,7 +145,7 @@ type conv_pb =
let sort_cmp univ pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
+ | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible
| (Prop c1, Type u) ->
(match pb with
CUMUL -> ()
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 764dfcc7b9..e9f8f89adf 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -262,7 +262,7 @@ let typecheck_inductive env mie =
Inl (info,full_arity,s), enforce_geq u lev cst
| Prop Pos when engagement env <> Some ImpredicativeSet ->
(* Predicative set: check that the content is indeed predicative *)
- if not (is_lower_univ lev) & not (is_type0_univ lev) then
+ if not (is_type0m_univ lev) & not (is_type0_univ lev) then
error "Large non-propositional inductive types must be in Type";
Inl (info,full_arity,s), cst
| Prop _ ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2059a1a409..3b64a2c09c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -124,7 +124,7 @@ Remark: Set (predicative) is encoded as Type(0)
let sort_as_univ = function
| Type u -> u
-| Prop Null -> lower_univ
+| Prop Null -> type0m_univ
| Prop Pos -> type0_univ
let cons_subst u su subst =
@@ -179,10 +179,12 @@ let instantiate_universes env ctx ar argsorts =
let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
let level = subst_large_constraints subst ar.poly_level in
ctx,
- if is_type0_univ level then set_sort else Type level
- (* Note: for singleton types, we keep a representative in Type so that
- predicativity and subtyping in Set applies, even if the resulting type
- is semantically equivalent to Prop (and indeed convertible to it) *)
+ (* Singleton type not containing types are interpretable in Prop *)
+ if is_type0m_univ level then prop_sort
+ (* Non singleton type not containing types are interpretable in Set *)
+ else if is_type0_univ level then set_sort
+ (* This is a Type with constraints *)
+ else Type level
let type_of_inductive_knowing_parameters env mip paramtyps =
match mip.mind_arity with
@@ -206,7 +208,7 @@ let cumulate_constructor_univ u = function
| Type u' -> sup u u'
let max_inductive_sort =
- Array.fold_left cumulate_constructor_univ lower_univ
+ Array.fold_left cumulate_constructor_univ type0m_univ
(************************************************************************)
(* Type of a constructor *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ee93ec2911..7a7a12b08f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -153,21 +153,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
(* The sort cumulativity is
- Prop, Set <= Type 1 <= ... <= Type i <= ...
+ Prop <= Set <= Type 1 <= ... <= Type i <= ...
and this holds whatever Set is predicative or impredicative
-
- In addition, there are the following internal sorts:
- - Type (-1) is semantically equivalent to Prop but with the
- following syntactic restrictions:
- Type (-1) is syntactically predicative and subtype of all Type i
- Prop is syntactically impredicative and subtype of Type i only for i>=1
- - Type 0 is semantically equivalent to predicative Set
- Both Type (-1) and Type 0 can only occur as types of polymorphic
- inductive types (in practice Type 0 is systematically converted to Set and
- we do not see it outside the computation of polymorphic inductive but
- Type (-1) is kept to avoid setting Prop <= predicative Set in the syntax;
- this means that (*1*) below can happen).
*)
type conv_pb =
@@ -176,14 +164,15 @@ type conv_pb =
let sort_cmp pb s0 s1 cuniv =
match (s0,s1) with
- | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible
+ | (Prop c1, Prop c2) ->
+ if c1 = Null or c2 = Pos then cuniv (* Prop <= Set *)
+ else raise NotConvertible
| (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
| (Type u1, Type u2) ->
assert (is_univ_variable u2);
(match pb with
| CONV -> enforce_eq u1 u2 cuniv
| CUMUL -> enforce_geq u2 u1 cuniv)
- | (Type u, Prop _) when u = lower_univ & pb = CUMUL -> cuniv (*1*)
| (_, _) -> raise NotConvertible
diff --git a/kernel/univ.ml b/kernel/univ.ml
index aa12f0a8bd..89b4a21124 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -40,8 +40,8 @@ open Util
*)
type universe_level =
- | PredicativeSet
- | PredicativeLevel of Names.dir_path * int
+ | Set
+ | Level of Names.dir_path * int
type universe =
| Atom of universe_level
@@ -53,10 +53,10 @@ module UniverseOrdered = struct
end
let string_of_univ_level = function
- | PredicativeSet -> "0"
- | PredicativeLevel (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
+ | Set -> "0"
+ | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
-let make_univ (m,n) = Atom (PredicativeLevel (m,n))
+let make_univ (m,n) = Atom (Level (m,n))
let pr_uni_level u = str (string_of_univ_level u)
@@ -78,8 +78,6 @@ let pr_uni = function
let super = function
| Atom u ->
Max ([],[u])
- | Max ([],[]) -> (* Used for polym. inductive types at the lower level *)
- Max ([],[PredicativeSet])
| Max _ ->
anomaly ("Cannot take the successor of a non variable universe:\n"^
"(maybe a bugged tactic)")
@@ -128,28 +126,28 @@ let declare_univ u g =
(* The lower predicative level of the hierarchy that contains (impredicative)
Prop and singleton inductive types *)
-let lower_univ = Max ([],[])
+let type0m_univ = Max ([],[])
-let is_lower_univ = function
+let is_type0m_univ = function
| Max ([],[]) -> true
| _ -> false
(* The level of predicative Set *)
-let type0_univ = Atom PredicativeSet
+let type0_univ = Atom Set
let is_type0_univ = function
- | Atom PredicativeSet -> true
- | Max ([PredicativeSet],[]) -> warning "Non canonical Set"; true
+ | Atom Set -> true
+ | Max ([Set],[]) -> warning "Non canonical Set"; true
| u -> false
let is_univ_variable = function
- | Atom a when a<>PredicativeSet -> true
+ | Atom a when a<>Set -> true
| _ -> false
(* When typing [Prop] and [Set], there is no constraint on the level,
hence the definition of [type1_univ], the type of [Prop] *)
-let type1_univ = Max ([],[PredicativeSet])
+let type1_univ = Max ([],[Set])
let initial_universes = UniverseMap.empty
@@ -297,7 +295,7 @@ let check_eq g u v =
let compare_greater g strict u v =
let g = declare_univ u g in
let g = declare_univ v g in
- if not strict && compare_eq g v PredicativeSet then true else
+ if not strict && compare_eq g v Set then true else
match compare g v u with
| (EQ|LE) -> not strict
| LT -> true
@@ -461,7 +459,7 @@ type constraint_function =
universe -> universe -> constraints -> constraints
let constraint_add_leq v u c =
- if v = PredicativeSet then c else Constraint.add (v,Leq,u) c
+ if v = Set then c else Constraint.add (v,Leq,u) c
let enforce_geq u v c =
match u, v with
@@ -485,7 +483,7 @@ let merge_constraints c g =
(* Temporary inductive type levels *)
let fresh_level =
- let n = ref 0 in fun () -> incr n; PredicativeLevel (Names.make_dirpath [],!n)
+ let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n)
let fresh_local_univ () = Atom (fresh_level ())
@@ -612,8 +610,8 @@ module Huniv =
type t = universe
type u = Names.dir_path -> Names.dir_path
let hash_aux hdir = function
- | PredicativeSet -> PredicativeSet
- | PredicativeLevel (d,n) -> PredicativeLevel (hdir d,n)
+ | Set -> Set
+ | Level (d,n) -> Level (hdir d,n)
let hash_sub hdir = function
| Atom u -> Atom (hash_aux hdir u)
| Max (gel,gtl) ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ce25afb26d..e2594e217a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,13 +12,17 @@
type universe
-val type0_univ : universe (* predicative Set seen as a universe *)
+(* The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... *)
+(* Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
+
+val type0m_univ : universe (* image of Prop in the universes hierarchy *)
+val type0_univ : universe (* image of Set in the universes hierarchy *)
val type1_univ : universe (* the universe of the type of Prop/Set *)
-val lower_univ : universe (* image of Prop in the predicative hierarchy *)
+
val make_univ : Names.dir_path * int -> universe
val is_type0_univ : universe -> bool
-val is_lower_univ : universe -> bool
+val is_type0m_univ : universe -> bool
val is_univ_variable : universe -> bool
(* The type of a universe *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d6bc6eb717..55b82e2148 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -615,10 +615,10 @@ let sort_cmp = sort_cmp
let base_sort_cmp pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) -> c1 = c2
+ | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *)
| (Prop c1, Type u) -> pb = CUMUL
| (Type u1, Type u2) -> true
- | (Type u, Prop _) -> u = lower_univ & pb = CUMUL
+ | _ -> false
let test_conversion f env sigma x y =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 227a4f9ed0..cb6146338c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -163,7 +163,7 @@ let new_Type_sort () = Type (new_univ ())
let refresh_universes_gen strict t =
let modified = ref false in
let rec refresh t = match kind_of_term t with
- | Sort (Type u) when strict or u <> Univ.lower_univ ->
+ | Sort (Type u) when strict or u <> Univ.type0m_univ ->
modified := true; new_Type ()
| Prod (na,u,v) -> mkProd (na,u,refresh v)
| _ -> t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:32:37 +0000