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 Lazy.t
38 Opaque data structure you will use to store constraints
43 returns a fresh universe
46 ?uri:UriManager.uri ->
51 (* names a universe if unnamed *)
52 val name_universe: universe -> UriManager.uri -> universe
55 really useful at the begin and in all the functions that don't care
58 val empty_ugraph: universe_graph
60 (* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
61 val oblivion_ugraph: universe_graph
64 These are the real functions to add eq/ge/gt constraints
65 to the passed graph, returning an updated graph or raising
69 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
71 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
73 ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
75 val do_rank: universe_graph -> unit
76 val get_rank: universe -> int
79 debug function to print the graph to standard error
82 universe_graph -> unit
85 does what expected, but I don't remember why this was exported
87 val string_of_universe:
91 given the list of visible universes (see universes_of_obj) returns a
92 cleaned graph (cleaned from the not visible nodes)
95 universe_graph -> universe list -> universe_graph
98 Since fresh() can't add the right uri to each node, you
99 must fill empty nodes with the uri before you serialize the graph to xml
101 these empty nodes are also filled in the universe list
103 val fill_empty_nodes_with_uri:
104 universe_graph -> universe list -> UriManager.uri ->
105 universe_graph * universe list
110 - remember already merged uri so that we completely skip already merged
111 graphs, this may include a dependecy graph (not merge a subpart of an
112 already merged graph)
115 base_ugraph:universe_graph ->
116 increment:(universe_graph * UriManager.uri) -> universe_graph
119 ugraph to xml file and viceversa
121 val write_xml_of_ugraph:
122 string -> universe_graph -> universe list -> unit
125 given a filename parses the xml and returns the data structure
127 val ugraph_and_univlist_of_xml:
128 string -> universe_graph * universe list
129 val restart_numbering:
133 returns the universe number (used to save it do xml)
135 val univno: universe -> int
137 (** re-hash-cons URIs contained in the given universe so that phisicaly
138 * equality could be enforced. Mainly used by
139 * CicEnvironment.restore_from_channel *)
140 val recons_graph: universe_graph -> universe_graph
142 (** re-hash-cons a single universe *)
143 val recons_univ: universe -> universe
145 (** consistency check that should be done before committin the graph to the
147 val assert_univs_have_uri: universe_graph -> universe list-> unit
149 (** asserts the universe is named *)
150 val assert_univ: universe -> unit
152 val compare: universe -> universe -> int
153 val eq: universe -> universe -> bool
158 val get_spent_time: unit -> float
159 val reset_spent_time: unit -> unit
161 val is_anon: universe -> bool