diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 14 | ||||
| -rw-r--r-- | kernel/reduction.ml | 19 | ||||
| -rw-r--r-- | kernel/univ.ml | 36 | ||||
| -rw-r--r-- | kernel/univ.mli | 10 |
5 files changed, 37 insertions, 44 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 764dfcc7b..e9f8f89ad 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 2059a1a40..3b64a2c09 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 ee93ec291..7a7a12b08 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 aa12f0a8b..89b4a2112 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 ce25afb26..e2594e217 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 *) |