diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 40 |
1 files changed, 18 insertions, 22 deletions
diff --git a/checker/values.ml b/checker/values.ml index 5a371164c6..55e1cdb6f7 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", @@ -108,10 +110,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; v_context|] +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 *) @@ -199,6 +203,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 +228,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|]|] @@ -372,22 +387,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 |