]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicUniv.mli
incomplete proof completed
[helm.git] / helm / ocaml / cic / cicUniv.mli
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26
27 (*
28   The strings contains an unreadable message
29 *)
30 exception UniverseInconsistency of string
31
32 (*
33   Cic.Type of universe 
34 *)
35 type universe
36
37 (*
38   Opaque data structure you will use to store constraints
39 *)
40 type universe_graph
41
42 (*
43   returns a fresh universe
44 *)
45 val fresh: 
46   ?uri:UriManager.uri ->
47   unit -> 
48     universe
49
50 (*
51   really useful at the begin and in all the functions that don't care 
52   of universes
53 *)
54 val empty_ugraph: universe_graph
55
56 (*
57   These are the real functions to add eq/ge/gt constraints 
58   to the passed graph, returning an updated graph or raising
59   UniverseInconsistency
60 *)
61 val add_eq: 
62   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
63 val add_ge: 
64   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
65 val add_gt: 
66   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
67
68 (*
69   debug function to print the graph to standard error
70 *)
71 val print_ugraph: 
72   universe_graph -> unit
73
74 (*
75   does what expected, but I don't remember why this was exported
76 *)
77 val string_of_universe: 
78   universe -> string
79
80 (*
81   given the list of visible universes (see universes_of_obj) returns a
82   cleaned graph (cleaned from the not visible nodes) 
83 *)
84 val clean_ugraph: 
85   universe_graph -> universe list -> universe_graph
86
87 (*
88   Since fresh() can't add the right uri to each node, you
89   must fill empty nodes with the uri before you serialize the graph to xml
90 *)
91 val fill_empty_nodes_with_uri:
92   universe_graph -> UriManager.uri -> universe_graph
93
94 (*
95   makes a union.
96   TODO:
97   - remember already merged uri so that we completely skip already merged
98     graphs, this may include a dependecy graph (not merge a subpart of an
99     already merged graph)
100 *)
101 val merge_ugraphs:
102   universe_graph -> universe_graph -> universe_graph
103
104 (*
105   ugraph to xml file and viceversa
106 *)
107 val write_xml_of_ugraph: 
108   string -> universe_graph -> unit
109
110 (*
111   given a filename parses the xml and returns the data structure
112 *)
113 val ugraph_of_xml:
114   string -> universe_graph
115 val restart_numbering:
116   unit -> unit
117
118   (** re-hash-cons URIs contained in the given universe so that phisicaly
119    * equality could be enforced. Mainly used by
120    * CicEnvironment.restore_from_channel *)
121 val recons_graph: universe_graph -> universe_graph
122
123   (** re-hash-cons a single universe *)
124 val recons_univ: universe -> universe
125
126   (** consistency chek that should be done before committin the graph to the
127    * cache *)
128 val assert_univs_have_uri: universe_graph -> unit
129
130   (** asserts the univers is named *)
131 val assert_univ: universe -> unit
132
133 (*
134   Benchmarking stuff
135 *)
136 val get_spent_time: unit -> float
137 val reset_spent_time: unit -> unit