diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:13:59 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /kernel | |
parent | 591e7e484d544e958595a0fb784336ae050a9c74 (diff) |
Option -type-in-type: added support in checker and making it contaminating
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
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 c1c19a757..561c66b42 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 a79abbb7e..30b28177c 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 ede356e69..4ad0327fc 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 86fb1b64c..d22abff10 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 31c0e83c8..9c79009db 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 557ed3d7d..5f3f559a2 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 03ac41b45..0ce0bed23 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 d8473183a..907ad2a1d 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 1e9cdbda0..2b4324b96 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 48dbacf1a..fe82d85d5 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) *) |