diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-14 01:14:27 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-14 01:59:25 +0100 |
commit | 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 (patch) | |
tree | 2a699f00ea98b91f518597b3dc05c83c79e98670 | |
parent | 8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (diff) |
Store the conversion oracle in constant and inductive definitions.
We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
-rw-r--r-- | checker/cic.mli | 12 | ||||
-rw-r--r-- | checker/values.ml | 17 | ||||
-rw-r--r-- | kernel/declarations.ml | 1 | ||||
-rw-r--r-- | kernel/declareops.ml | 3 | ||||
-rw-r--r-- | kernel/declareops.mli | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 6 | ||||
-rw-r--r-- | kernel/pre_env.ml | 4 | ||||
-rw-r--r-- | kernel/pre_env.mli | 1 |
8 files changed, 36 insertions, 10 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 4a0e706aa..95dd18f5f 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet type engagement = set_predicativity +(** {6 Conversion oracle} *) + +type level = Expand | Level of int | Opaque + +type oracle = { + var_opacity : level Id.Map.t; + cst_opacity : level Cmap.t; + var_trstate : Id.Pred.t; + cst_trstate : Cpred.t; +} + (** {6 Representation of constants (Definition/Axiom) } *) @@ -219,6 +230,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : oracle; (** Unfolding strategies for conversion *) } type constant_body = { diff --git a/checker/values.ml b/checker/values.ml index 4698227ff..313067cb6 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli +MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli *) @@ -70,6 +70,8 @@ let v_map vk vd = let v_hset v = v_map Int (v_set v) let v_hmap vk vd = v_map Int (v_map vk vd) +let v_pred v = v_pair v_bool (v_set v) + (* lib/future *) let v_computation f = Annot ("Future.computation", @@ -199,6 +201,17 @@ let v_lazy_constr = let v_impredicative_set = v_enum "impr-set" 2 let v_engagement = v_impredicative_set +let v_conv_level = + v_sum "conv_level" 2 [|[|Int|]|] + +let v_oracle = + v_tuple "oracle" [| + v_map v_id v_conv_level; + v_hmap v_cst v_conv_level; + v_pred v_id; + v_pred v_cst; + |] + let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -213,7 +226,7 @@ let v_projbody = v_constr|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7f4b85fd0..5b9e1a141 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -74,6 +74,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d8768a0fc..9eed9efcb 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -15,9 +15,10 @@ module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) -let safe_flags = { +let safe_flags oracle = { check_guarded = true; check_universes = true; + conv_oracle = oracle; } (** {6 Arities } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 198831848..0eed11f49 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -67,7 +67,7 @@ val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) -val safe_flags : typing_flags +val safe_flags : Conv_oracle.oracle -> typing_flags (** {6 Hash-consing} *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 1afab453a..3c86129fe 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -37,8 +37,10 @@ type env = Pre_env.env let pre_env env = env let env_of_pre_env env = env -let oracle env = env.env_conv_oracle -let set_oracle env o = { env with env_conv_oracle = o } +let oracle env = env.env_typing_flags.conv_oracle +let set_oracle env o = + let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in + { env with env_typing_flags } let empty_named_context_val = empty_named_context_val diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index c5254b453..4ef89f8c0 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -75,7 +75,6 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; - env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } @@ -98,8 +97,7 @@ let empty_env = { env_stratification = { env_universes = UGraph.initial_universes; env_engagement = PredicativeSet }; - env_typing_flags = Declareops.safe_flags; - env_conv_oracle = Conv_oracle.empty; + env_typing_flags = Declareops.safe_flags 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 054ae1743..fef530c87 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -53,7 +53,6 @@ type env = { env_nb_rel : int; env_stratification : stratification; env_typing_flags : typing_flags; - env_conv_oracle : Conv_oracle.oracle; retroknowledge : Retroknowledge.retroknowledge; indirect_pterms : Opaqueproof.opaquetab; } |