diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 81 |
1 files changed, 39 insertions, 42 deletions
diff --git a/checker/values.ml b/checker/values.ml index c175aed6..1ac8d7ce 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Abstract representations of values in a vo *) @@ -13,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 6466d8cc443b5896cb905776df0cc49e checker/cic.mli +MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli *) @@ -54,6 +56,7 @@ let v_enum name n = Sum(name,n,[||]) let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 +let v_unit = v_enum "unit" 1 let v_ref v = v_tuple "ref" [|v|] let v_set v = @@ -69,6 +72,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", @@ -98,7 +103,7 @@ let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] let v_expr = v_tuple "levelexpr" [|v_level;Int|] -let rec v_univ = Sum ("universe", 1, [| [|v_expr; Int; v_univ|] |]) +let v_univ = List v_expr let v_cstrs = Annot @@ -107,8 +112,12 @@ let v_cstrs = (v_tuple "univ_constraint" [|v_level;v_enum "order_request" 3;v_level|])) +let v_variance = v_enum "variance" 3 + let v_instance = Annot ("instance", Array v_level) let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] +let v_abs_context = v_context (* only for clarity *) +let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) @@ -196,12 +205,20 @@ 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|] -let v_cst_type = - v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|] - let v_cst_def = v_sum "constant_def" 0 [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] @@ -213,15 +230,16 @@ 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|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; - v_cst_type; + v_constr; Any; - v_bool; - v_context; + v_const_univs; Opt v_projbody; v_bool; v_typing_flags|] @@ -262,6 +280,10 @@ let v_finite = v_enum "recursivity_kind" 3 let v_mind_record = Annot ("mind_record", Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]))) +let v_ind_pack_univs = + v_sum "abstract_inductive_universes" 0 + [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] + let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; v_mind_record; @@ -271,21 +293,15 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; Int; v_rctxt; - v_bool; - v_context; + v_ind_pack_univs; (* universes *) Opt v_bool; v_typing_flags|] -let v_with = - Sum ("with_declaration_body",0, - [|[|List v_id;v_mp|]; - [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|]) - let rec v_mae = Sum ("module_alg_expr",0, [|[|v_mp|]; (* SEBident *) [|v_mae;v_mp|]; (* SEBapply *) - [|v_mae;v_with|] (* SEBwith *) + [|v_mae; Any|] (* SEBwith *) |]) let rec v_sfb = @@ -308,13 +324,13 @@ and v_impl = Sum ("module_impl",2, (* Abstract, FullStruct *) [|[|v_mexpr|]; (* Algebraic *) [|v_sign|]|]) (* Struct *) -and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) +and v_noimpl = v_unit and v_module = Tuple ("module_body", [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) (** kernel/safe_typing *) @@ -368,22 +384,3 @@ let v_lib = let v_opaques = Array (v_computation v_constr) let v_univopaques = Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) - -(** Registering dynamic values *) - -module IntOrd = -struct - type t = int - let compare (x : t) (y : t) = compare x y -end - -module IntMap = Map.Make(IntOrd) - -let dyn_table : value IntMap.t ref = ref IntMap.empty - -let register_dyn name t = - dyn_table := IntMap.add name t !dyn_table - -let find_dyn name = - try IntMap.find name !dyn_table - with Not_found -> Any |