diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/checker/values.ml b/checker/values.ml index 1ac8d7ce..e1b5a949 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,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 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli +MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli *) @@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0, [|[|v_dp|]; [|v_uid|]; [|v_mp;v_id|]|]) -let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|] +let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;Int|] let v_cons = v_tuple "constructor" [|v_ind;Int|] @@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] @@ -135,7 +135,9 @@ 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 v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|] +let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|] let rec v_constr = Sum ("constr",0,[| @@ -173,7 +175,7 @@ let v_section_ctxt = v_enum "emptylist" 1 (** kernel/mod_subst *) let v_delta_hint = - v_sum "delta_hint" 0 [|[|Int; Opt v_constr|];[|v_kn|]|] + v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|] let v_resolver = v_tuple "delta_resolver" @@ -223,14 +225,8 @@ let v_cst_def = v_sum "constant_def" 0 [|[|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|] - let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] @@ -240,7 +236,6 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; - Opt v_projbody; v_bool; v_typing_flags|] @@ -277,8 +272,10 @@ let v_one_ind = v_tuple "one_inductive_body" Any|] 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_record_info = + v_sum "record_info" 2 + [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |] let v_ind_pack_univs = v_sum "abstract_inductive_universes" 0 @@ -286,7 +283,7 @@ let v_ind_pack_univs = let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; - v_mind_record; + v_record_info; v_finite; Int; v_section_ctxt; |