raise (UniverseInconsistency s)
-let fill_empty_nodes_with_uri g uri =
+let fill_empty_nodes_with_uri g l uri =
let fill_empty_universe u =
match u with
(i,None) -> (i,Some uri)
fun k v m ->
MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
in
- m'
+ let l' = List.map fill_empty_universe l in
+ m',l'
(*****************************************************************************)
let restart_numbering () = current_index_named := (-1)
-let fresh ?uri () =
+let fresh ?uri ?id () =
let i =
- match uri with
- | None ->
+ match uri,id with
+ | None,None ->
current_index_anon := !current_index_anon + 1;
!current_index_anon
- | Some _ ->
+ | None, Some _ -> assert false
+ | Some _, None ->
current_index_named := !current_index_named + 1;
!current_index_named
+ | Some _, Some id -> id
in
(i,uri)
(** Xml sesialization and parsing **)
(*****************************************************************************)
+let xml_of_universe name u =
+ match u with
+ | (i,Some u) ->
+ Xml.xml_empty name [
+ None,"id",(string_of_int i) ;
+ None,"uri",(UriManager.string_of_uri u)]
+ | (_,None) ->
+ raise (Failure "we can serialize only universes with uri")
+
let xml_of_set s =
let l =
- List.map (
- function
- (i,Some u) ->
- Xml.xml_empty "node" [
- None,"id",(string_of_int i) ;
- None,"uri",(UriManager.string_of_uri u)]
- | (_,None) ->
- raise (Failure "we can serialize only universes with uri")
- ) (SOF.elements s)
+ List.map (xml_of_universe "node") (SOF.elements s)
in
List.fold_left (fun s x -> [< s ; x >] ) [<>] l
let content = xml_of_entry_content e in
ent content
-let write_xml_of_ugraph filename m =
- let o = open_out filename in
- output_string o "<?xml version=\"1.0\" encoding=\"iso-8859-1\" ?>\n";
- Xml.pp_to_outchan (
- Xml.xml_nempty "ugraph" [] (
- MAL.fold (
- fun k v s -> [< s ; (xml_of_entry k v) >])
- m [<>])) o;
- close_out o
+let write_xml_of_ugraph filename m l =
+ let tokens =
+ [<
+ Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+ Xml.xml_nempty "ugraph" []
+ ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ;
+ (List.fold_left
+ (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>]
+ in
+ Xml.pp ~gzip:true tokens (Some filename)
+
+let univno = fst
+
let rec clean_ugraph m f =
let m' =
| s -> raise (Failure ("unsupported tag " ^ s))
;;
-let cb_factory m =
+let cb_factory m l =
let module XPP = XmlPushParser in
let current_node = ref (0,None) in
let current_entry = ref empty_entry in
- let current_assign = ref (assigner_of "in_ge_of") in
+ let current_assign = ref (assigner_of "in_gegt_of") in
{ XPP.default_callbacks with
XPP.end_element = Some( fun name ->
match name with
);
XPP.start_element = Some( fun name attlist ->
match name with
+ | "ugraph" -> ()
| "entry" ->
let id = List.assoc "id" attlist in
let uri = List.assoc "uri" attlist in
let uri = List.assoc "uri" attlist in
current_entry := !current_assign !current_entry
(id,Some (UriManager.uri_of_string uri))
+ | "owned_node" ->
+ let id = int_of_string (List.assoc "id" attlist) in
+ let uri = List.assoc "uri" attlist in
+ l := (id,Some (UriManager.uri_of_string uri)) :: !l
| s -> current_assign := assigner_of s
)
}
;;
-(* alternative implementation *)
-let mapl = [
- ("ge_closure",0);("gt_closure",1);("eq_closure",2);
- ("in_gegt_of", 3);
- ("one_s_ge", 4);("one_s_gt", 5);("one_s_eq", 6)]
-;;
-
-let assigner_of' s = List.assoc s mapl ;;
-
-let entry_of_array a = {
- ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
- in_gegt_of = a.(3);
- one_s_ge = a.(4); one_s_gt = a.(5); one_s_eq = a.(6)}
-;;
-
-let cb_factory' m =
- let module XPP = XmlPushParser in
- let current_node = ref (0,None) in
- let current_entry = Array.create 7 SOF.empty in
- let current_assign = ref 0 in
- { XPP.default_callbacks with
- XPP.start_element = Some( fun name attlist ->
- match name with
- | "entry" ->
- let id = List.assoc "id" attlist in
- let uri = List.assoc "uri" attlist in
- current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
- | "node" ->
- let id = int_of_string (List.assoc "id" attlist) in
- let uri = List.assoc "uri" attlist in
- current_entry.(!current_assign) <-
- SOF.add (id,Some (UriManager.uri_of_string uri))
- current_entry.(!current_assign)
- | s -> current_assign := assigner_of' s
- );
- XPP.end_element = Some( fun name ->
- match name with
- | "entry" ->
- m := MAL.add !current_node (entry_of_array current_entry) !m;
- Array.fill current_entry 0 7 SOF.empty
- | _ -> ()
- );
- }
-;;
-
-
-let ugraph_of_xml filename =
+let ugraph_and_univlist_of_xml filename =
let module XPP = XmlPushParser in
- let result = ref MAL.empty in
- let cb = cb_factory result in
-(*let cb = cb_factory' result in*)
+ let result_map = ref MAL.empty in
+ let result_list = ref [] in
+ let cb = cb_factory result_map result_list in
let xml_parser = XPP.create_parser cb in
let xml_source = `Gzip_file filename in
(try XPP.parse xml_parser xml_source
with (XPP.Parse_error err) as exn -> raise exn);
- !result
+ !result_map, !result_list
\f
(*****************************************************************************)
| (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
| _ -> ()
-let assert_univs_have_uri graph =
+let assert_univs_have_uri graph univlist =
let assert_set s =
SOF.iter (fun u -> assert_univ u) s
in
assert_set e.one_s_ge;
assert_set e.one_s_gt;
in
- MAL.iter (fun k v -> assert_univ k; assert_entry v)graph
+ MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
+ List.iter assert_univ univlist
+
+let eq u1 u2 =
+ match u1,u2 with
+ | (id1, Some uri1),(id2, Some uri2) ->
+ id1 = id2 && UriManager.eq uri1 uri2
+ | (id1, None),(id2, None) -> id1 = id2
+ | _ -> false
+
+let compare (id1, uri1) (id2, uri2) =
+ let cmp = id1 - id2 in
+ if cmp = 0 then
+ match uri1,uri2 with
+ | None, None -> 0
+ | Some _, None -> 1
+ | None, Some _ -> ~-1
+ | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+ else
+ cmp
-
(* EOF *)
*)
val fresh:
?uri:UriManager.uri ->
+ ?id:int ->
unit ->
universe
(*
Since fresh() can't add the right uri to each node, you
must fill empty nodes with the uri before you serialize the graph to xml
+
+ these empty nodes are also filled in the universe list
*)
val fill_empty_nodes_with_uri:
- universe_graph -> UriManager.uri -> universe_graph
+ universe_graph -> universe list -> UriManager.uri ->
+ universe_graph * universe list
(*
makes a union.
ugraph to xml file and viceversa
*)
val write_xml_of_ugraph:
- string -> universe_graph -> unit
+ string -> universe_graph -> universe list -> unit
(*
given a filename parses the xml and returns the data structure
*)
-val ugraph_of_xml:
- string -> universe_graph
+val ugraph_and_univlist_of_xml:
+ string -> universe_graph * universe list
val restart_numbering:
unit -> unit
+(*
+ returns the universe number (used to save it do xml)
+*)
+val univno: universe -> int
+
(** re-hash-cons URIs contained in the given universe so that phisicaly
* equality could be enforced. Mainly used by
* CicEnvironment.restore_from_channel *)
(** consistency chek that should be done before committin the graph to the
* cache *)
-val assert_univs_have_uri: universe_graph -> unit
+val assert_univs_have_uri: universe_graph -> universe list-> unit
- (** asserts the univers is named *)
+ (** asserts the universe is named *)
val assert_univ: universe -> unit
+val compare: universe -> universe -> int
+val eq: universe -> universe -> bool
+
(*
Benchmarking stuff
*)
projects / helm.git / commitdiff