1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 The strings contains an unreadable message
30 exception UniverseInconsistency of string
38 Opaque data structure you will use to store constraints
43 returns a fresh universe
46 ?uri:UriManager.uri ->
52 really useful at the begin and in all the functions that don't care
55 val empty_ugraph: universe_graph
58 These are the real functions to add eq/ge/gt constraints
59 to the passed graph, returning an updated graph or raising
63 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
65 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
67 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
70 debug function to print the graph to standard error
73 universe_graph -> unit
76 does what expected, but I don't remember why this was exported
78 val string_of_universe:
82 given the list of visible universes (see universes_of_obj) returns a
83 cleaned graph (cleaned from the not visible nodes)
86 universe_graph -> universe list -> universe_graph
89 Since fresh() can't add the right uri to each node, you
90 must fill empty nodes with the uri before you serialize the graph to xml
92 these empty nodes are also filled in the universe list
94 val fill_empty_nodes_with_uri:
95 universe_graph -> universe list -> UriManager.uri ->
96 universe_graph * universe list
101 - remember already merged uri so that we completely skip already merged
102 graphs, this may include a dependecy graph (not merge a subpart of an
103 already merged graph)
106 universe_graph -> universe_graph -> universe_graph
109 ugraph to xml file and viceversa
111 val write_xml_of_ugraph:
112 string -> universe_graph -> universe list -> unit
115 given a filename parses the xml and returns the data structure
117 val ugraph_and_univlist_of_xml:
118 string -> universe_graph * universe list
119 val restart_numbering:
123 returns the universe number (used to save it do xml)
125 val univno: universe -> int
127 (** re-hash-cons URIs contained in the given universe so that phisicaly
128 * equality could be enforced. Mainly used by
129 * CicEnvironment.restore_from_channel *)
130 val recons_graph: universe_graph -> universe_graph
132 (** re-hash-cons a single universe *)
133 val recons_univ: universe -> universe
135 (** consistency chek that should be done before committin the graph to the
137 val assert_univs_have_uri: universe_graph -> universe list-> unit
139 (** asserts the universe is named *)
140 val assert_univ: universe -> unit
142 val compare: universe -> universe -> int
143 val eq: universe -> universe -> bool
148 val get_spent_time: unit -> float
149 val reset_spent_time: unit -> unit