diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.mli | 5 | ||||
| -rw-r--r-- | kernel/environ.ml | 17 | ||||
| -rw-r--r-- | kernel/environ.mli | 7 | ||||
| -rw-r--r-- | kernel/fast_typeops.ml | 6 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 6 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 26 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 5 | ||||
| -rw-r--r-- | kernel/typeops.ml | 6 |
10 files changed, 38 insertions, 45 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c1c19a757c..561c66b422 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -14,7 +14,10 @@ open Context declarations. This includes global constants/axioms, mutual inductive definitions, modules and module types *) -type engagement = ImpredicativeSet +type set_predicativity = ImpredicativeSet | PredicativeSet +type type_hierarchy = TypeInType | StratifiedType + +type engagement = set_predicativity * type_hierarchy (** {6 Representation of constants (Definition/Axiom) } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index a79abbb7e8..30b28177c9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -46,11 +46,14 @@ let empty_env = empty_env let engagement env = env.env_stratification.env_engagement -let type_in_type env = env.env_stratification.env_type_in_type - let is_impredicative_set env = - match engagement env with - | Some ImpredicativeSet -> true + match fst (engagement env) with + | ImpredicativeSet -> true + | _ -> false + +let type_in_type env = + match snd (engagement env) with + | TypeInType -> true | _ -> false let universes env = env.env_stratification.env_universes @@ -191,11 +194,7 @@ let check_constraints c env = let set_engagement c env = (* Unsafe *) { env with env_stratification = - { env.env_stratification with env_engagement = Some c } } - -let set_type_in_type env = - { env with env_stratification = - { env.env_stratification with env_type_in_type = true } } + { env.env_stratification with env_engagement = c } } let push_constraints_to_env (_,univs) env = add_constraints univs env diff --git a/kernel/environ.mli b/kernel/environ.mli index ede356e699..4ad0327fc7 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab val set_opaque_tables : env -> Opaqueproof.opaquetab -> env -val engagement : env -> engagement option +val engagement : env -> engagement val is_impredicative_set : env -> bool - -val type_in_type : env -> bool +val type_in_type : env -> bool (** is the local context empty *) val empty_context : env -> bool @@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env -val set_type_in_type : env -> env - (** {6 Sets of referred section variables } [global_vars_set env c] returns the list of [id]'s occurring either directly as [Var id] in [c] or indirectly as a section variable diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 86fb1b64c6..d22abff10c 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - begin match engagement env with - | Some ImpredicativeSet -> + if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort - | _ -> + else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) - end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 31c0e83c84..9c79009dba 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign = sign (Universe.type0m,env)) let is_impredicative env u = - is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet) + is_type0m_univ u || (is_type0_univ u && is_impredicative_set env) (* Returns the list [x_1, ..., x_n] of levels contributing to template polymorphism. The elements x_k is None if the k-th parameter (starting diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 557ed3d7da..5f3f559a2c 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -46,8 +46,7 @@ type globals = { type stratification = { env_universes : universes; - env_engagement : engagement option; - env_type_in_type : bool + env_engagement : engagement } type val_kind = @@ -95,8 +94,7 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = initial_universes; - env_engagement = None; - env_type_in_type = false}; + env_engagement = (PredicativeSet,StratifiedType) }; env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge; indirect_pterms = Opaqueproof.empty_opaquetab } diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 03ac41b45e..0ce0bed235 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -33,8 +33,7 @@ type globals = { type stratification = { env_universes : universes; - env_engagement : engagement option; - env_type_in_type : bool + env_engagement : engagement } type lazy_val diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d8473183ab..907ad2a1d4 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -184,16 +184,20 @@ let set_engagement c senv = (** Check that the engagement [c] expected by a library matches the current (initial) one *) -let check_engagement env c = - match Environ.engagement env, c with - | None, Some ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." - | _ -> () - -let set_type_in_type senv = - { senv with - env = Environ.set_type_in_type senv.env; - type_in_type = true } +let check_engagement env (expected_impredicative_set,expected_type_in_type) = + let impredicative_set,type_in_type = Environ.engagement env in + begin + match impredicative_set, expected_impredicative_set with + | PredicativeSet, ImpredicativeSet -> + Errors.error "Needs option -impredicative-set." + | _ -> () + end; + begin + match type_in_type, expected_type_in_type with + | StratifiedType, TypeInType -> + Errors.error "Needs option -type-in-type." + | _ -> () + end (** {6 Stm machinery } *) @@ -734,7 +738,7 @@ type compiled_library = { comp_name : DirPath.t; comp_mod : module_body; comp_deps : library_info array; - comp_enga : engagement option; + comp_enga : engagement; comp_natsymbs : Nativecode.symbols } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1e9cdbda0e..2b4324b96f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -99,12 +99,9 @@ val add_constraints : (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) -(** Setting the strongly constructive or classical logical engagement *) +(** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 -(** Collapsing the type hierarchy *) -val set_type_in_type : safe_transformer0 - (** {6 Interactive module functions } *) val start_module : Label.t -> module_path safe_transformer diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 48dbacf1a4..fe82d85d5d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - begin match engagement env with - | Some ImpredicativeSet -> + if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort - | _ -> + else (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) - end (* Product rule (Prop,Type_i,Type_i) *) | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) |