diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 26 |
1 files changed, 17 insertions, 9 deletions
diff --git a/checker/values.ml b/checker/values.ml index cf93466b..34de511c 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 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli +MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli *) @@ -126,6 +126,7 @@ let v_caseinfo = v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 4 +let v_proj = v_tuple "projection" [|v_cst; v_bool|] let rec v_constr = Sum ("constr",0,[| @@ -145,7 +146,7 @@ let rec v_constr = [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) - [|v_cst;v_constr|] (* Proj *) + [|v_proj;v_constr|] (* Proj *) |]) and v_prec = Tuple ("prec_declaration", @@ -192,7 +193,9 @@ let v_lazy_constr = (** kernel/declarations *) -let v_engagement = v_enum "eng" 1 +let v_impredicative_set = v_enum "impr-set" 2 +let v_type_in_type = v_enum "type-in-type" 2 +let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|] let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -205,8 +208,10 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_projbody = - v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|]; - v_constr|] + v_tuple "projection_body" + [|v_cst;Int;Int;v_constr; + v_tuple "proj_eta" [|v_constr;v_constr|]; + v_constr|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -302,17 +307,17 @@ and v_impl = and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|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_cstrs;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) (** kernel/safe_typing *) let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |]) let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|]) let v_compiled_lib = - v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|] + v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|] (** Library objects *) @@ -350,8 +355,11 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) +let v_libsum = + Tuple ("summary", [|v_dp;Array v_dp;v_deps|]) + let v_lib = - Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) + Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) let v_opaques = Array (v_computation v_constr) let v_univopaques = |