diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 37 |
1 files changed, 26 insertions, 11 deletions
diff --git a/checker/values.ml b/checker/values.ml index 1afe764ca4..66467fa8f5 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -34,6 +34,7 @@ type value = | Dyn | Proxy of value ref + | Uint63 let fix (f : value -> value) : value = let self = ref Any in @@ -111,7 +112,6 @@ let v_variance = v_enum "variance" 3 let v_instance = Annot ("instance", Array v_level) let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|] -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 *) @@ -151,7 +151,8 @@ let rec v_constr = [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) - [|v_proj;v_constr|] (* Proj *) + [|v_proj;v_constr|]; (* Proj *) + [|Uint63|] (* Int *) |]) and v_prec = Tuple ("prec_declaration", @@ -214,21 +215,24 @@ let v_oracle = let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] +let v_primitive = + v_enum "primitive" 25 + let v_cst_def = v_sum "constant_def" 0 - [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] + [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] +let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; v_constr; Any; - v_const_univs; + v_univs; Opt v_context_set; v_bool; v_typing_flags|] @@ -271,10 +275,6 @@ 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 - [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] - let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; v_record_info; @@ -284,10 +284,25 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; Int; v_rctxt; - v_ind_pack_univs; (* universes *) + v_univs; (* universes *) + Opt (Array v_variance); Opt v_bool; v_typing_flags|] +let v_prim_ind = v_enum "prim_ind" 4 + +let v_prim_type = v_enum "prim_type" 1 + +let v_retro_action = + v_sum "retro_action" 0 [| + [|v_prim_ind; v_ind|]; + [|v_prim_type; v_cst|]; + [|v_cst|]; + |] + +let v_retroknowledge = + v_sum "module_retroknowledge" 1 [|[|List v_retro_action|]|] + let rec v_mae = Sum ("module_alg_expr",0, [|[|v_mp|]; (* SEBident *) @@ -318,7 +333,7 @@ and v_impl = 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|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|]) and v_modtype = Tuple ("module_type_body", [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|]) |