returns a fresh universe
*)
val fresh:
- unit -> universe
-
+ ?uri:UriManager.uri ->
+ ?id:int ->
+ unit ->
+ universe
+
+ (* names a universe if unnamed *)
+val name_universe: universe -> UriManager.uri -> universe
+
(*
really useful at the begin and in all the functions that don't care
of universes
(*
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.
already merged graph)
*)
val merge_ugraphs:
- universe_graph -> universe_graph -> universe_graph
+ base_ugraph:universe_graph ->
+ increment:(universe_graph * UriManager.uri) -> universe_graph
(*
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 *)
val recons_graph: universe_graph -> universe_graph
+ (** re-hash-cons a single universe *)
+val recons_univ: universe -> universe
+
+ (** consistency chek that should be done before committin the graph to the
+ * cache *)
+val assert_univs_have_uri: universe_graph -> universe list-> unit
+
+ (** asserts the universe is named *)
+val assert_univ: universe -> unit
+
+val compare: universe -> universe -> int
+val eq: universe -> universe -> bool
+
(*
Benchmarking stuff
*)
val get_spent_time: unit -> float
val reset_spent_time: unit -> unit
+