diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 43 |
1 files changed, 35 insertions, 8 deletions
diff --git a/checker/values.ml b/checker/values.ml index 3ca44b7d..cf93466b 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 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli +MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli *) @@ -270,7 +270,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" let v_with = Sum ("with_declaration_body",0, [|[|List v_id;v_mp|]; - [|List v_id;v_constr|]|]) + [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|]) let rec v_mae = Sum ("module_alg_expr",0, @@ -321,6 +321,33 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) +(** STM objects *) + +let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|]) +let v_states = v_pair Any v_frozen +let v_state = Tuple ("state", [|v_states; Any; v_bool|]) + +let v_vcs = + let data = Opt Any in + let vcs = + Tuple ("vcs", + [|Any; Any; + Tuple ("dag", + [|Any; Any; v_map Any (Tuple ("state_info", + [|Any; Any; Opt v_state; v_pair data Any|])) + |]) + |]) + in + let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in + vcs + +let v_uuid = Any +let v_request id doc = + Tuple ("request", [|Any; Any; doc; Any; id; String|]) +let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool) +let v_counters = Any +let v_stm_seg = v_pair v_tasks v_counters + (** Toplevel structures in a vo (see Cic.mli) *) let v_lib = @@ -332,19 +359,19 @@ let v_univopaques = (** Registering dynamic values *) -module StringOrd = +module IntOrd = struct - type t = string + type t = int let compare (x : t) (y : t) = compare x y end -module StringMap = Map.Make(StringOrd) +module IntMap = Map.Make(IntOrd) -let dyn_table : value StringMap.t ref = ref StringMap.empty +let dyn_table : value IntMap.t ref = ref IntMap.empty let register_dyn name t = - dyn_table := StringMap.add name t !dyn_table + dyn_table := IntMap.add name t !dyn_table let find_dyn name = - try StringMap.find name !dyn_table + try IntMap.find name !dyn_table with Not_found -> Any |