]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicUniv.ml
Files control.js graphLinks.js utils.js no longer in use.
[helm.git] / helm / ocaml / cic / cicUniv.ml
1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
24  *)
25
26 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                      Enrico Tassi <tassi@cs.unibo.it>                      *)
31 (*                                 23/04/2004                                 *)
32 (*                                                                            *)
33 (* This module implements the aciclic graph of universes.                     *)
34 (*                                                                            *)
35 (******************************************************************************)
36
37 (* 
38
39    todo:
40      - in add_eq there is probably no need of add_gt, simple @ the gt lists 
41      - the problem of duplicates in the 1steg gt/ge list if two of them are
42        add_eq may be "fixed" in some ways:
43         - lazy, do nothing on add_eq and eventually update the ge list 
44           on closure
45         - add a check_duplicates_after_eq function called by add_eq
46         - do something like rmap, add a list of canonical that point to us
47           so when we collapse we have the list of the canonical we may update
48      - don't use failure but another exception
49      
50 *)
51
52 (* ************************************************************************** *)
53 (*  TYPES                                                                     *)
54 (* ************************************************************************** *)
55 type universe = int 
56
57 type canonical_repr = {
58         mutable ge:universe list; 
59         mutable gt:universe list;
60         (* since we collapse we may need the reverse map *) 
61         mutable eq:universe list; 
62         (* the canonical representer *)
63         u:universe
64 }
65
66 module UniverseType = struct
67   type t = universe
68   let compare = Pervasives.compare
69 end
70
71 module MapUC = Map.Make(UniverseType)
72
73 (* ************************************************************************** *)
74 (*  Globals                                                                   *)
75 (* ************************************************************************** *)
76
77 let map = ref MapUC.empty 
78 let used = ref (-1)
79
80 (* ************************************************************************** *)
81 (*  Helpers                                                                   *)
82 (* ************************************************************************** *)
83
84 (* create a canonical for [u] *)
85 let mk_canonical u =
86   {u = u ; gt = [] ; ge = [] ; eq = [u] }
87
88 (* give a new universe *)
89 let fresh () = 
90   used := !used + 1;
91   map := MapUC.add !used (mk_canonical !used) !map;
92   !used
93   
94 let reset () =
95   map := MapUC.empty;
96   used := -1
97   
98 (* ************************************************************************** *)
99 (*   Pretty printing                                                          *)
100 (* ************************************************************************** *) 
101 (* pp *)
102 let string_of_universe = string_of_int
103
104 (* pp *)
105 let canonical_to_string c = 
106   let s_gt = 
107     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.gt in
108   let s_ge = 
109     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.ge in  
110   let s_eq =
111     List.fold_left (fun s u -> s ^ (string_of_universe u) ^ " ") "" c.eq in
112   let s_u = (string_of_universe c.u) in
113   "{ u:" ^ s_u ^ " ; gt:" ^ s_gt ^ " ; ge:" ^ s_ge ^ " ; eq: " ^ s_eq ^ "}"
114
115 (* print the content of map *)
116 let print_map () =
117   MapUC.iter (fun u c -> 
118    prerr_endline 
119     (" " ^ (string_of_universe u) ^ " -> " ^ (canonical_to_string c))) 
120   !map;
121   prerr_endline ""
122
123 (* ************************************************************************** *)
124 (*  The way we fail                                                           *)
125 (* ************************************************************************** *)   
126 (* we are doing bad *)
127 let error s = 
128   (*prerr_endline " ======= Universe Inconsistency =========";
129   print_map ();*)
130   prerr_endline (" " ^ s ^ "\n");
131   failwith s
132
133 (* ************************************************************************** *)
134 (*  The real code                                                             *)
135 (* ************************************************************************** *) 
136 (* <--------> *)
137
138 (* the canonical representer of the [u] equaliti class *)
139 let repr u = 
140   try 
141     MapUC.find u !map
142   with
143     Not_found -> error ("map inconsistency, unbound " ^ (string_of_universe u))
144
145 (* all the nodes we can ifer in the ge list of u *)
146 let close_ge u =
147   let repr_u = repr u in
148   let rec close_ge_aux tofollow bag = 
149     match tofollow with
150       [] -> bag
151     | v::tl -> let repr_v = repr v in
152                if List.mem repr_v bag then (* avoid loops *)
153                  (close_ge_aux tl bag ) 
154                else
155                  (close_ge_aux (tl @ repr_v.ge) (repr_v::bag))
156                  (* we assume that v==u -> v \notin (repr u).ge *)
157   in
158   close_ge_aux repr_u.ge []
159
160 (* all the nodes we can ifer in the gt list of u,
161    we must follow bot gt and ge arcs, but we must put in bag only 
162    the nodes that have a gt in theys path 
163 *)
164 let close_gt u =
165   let repr_u = repr u in
166   let rec close_gt_aux bag todo inspected =
167     (*print_all bag todo;Unix.sleep 1;*)
168     match todo with
169       [],[] -> bag
170     | [],p::may -> let repr_p = repr p in 
171                    if List.mem repr_p.u inspected then (* avoid loops *)
172                      close_gt_aux bag ([],may) inspected
173                    else 
174                      close_gt_aux bag (repr_p.gt,repr_p.ge @ may) 
175                       (repr_p.u::inspected)
176     | s::secure,may -> let repr_s = repr s in
177                        if List.mem repr_s.u inspected then (* avoid loops *)
178                          if List.mem repr_s bag then
179                            close_gt_aux bag (secure,may) inspected
180                          else
181                            (* even if we ave already inspected the node, now
182                               it is in the secure list so we want it in the bag 
183                            *)
184                            close_gt_aux (repr_s::bag) (secure,may) inspected
185                        else
186                          close_gt_aux ((repr_s)::bag) 
187                           (repr_s.gt @ repr_s.ge,may) (repr_s.u::inspected)
188   in
189   close_gt_aux [] (repr_u.gt,repr_u.ge) []
190   
191 (* when we add an eq we have to change the mapping of u to c*)
192 let remap u c =
193   let repr_u = repr u in
194   List.iter (fun u' -> if u <> u' then map := MapUC.remove u' !map) repr_u.eq;
195   List.iter (fun u' -> map := MapUC.add u' c !map) repr_u.eq
196
197 (* we suspect that u and v are connected by a == implyed by two >= *)
198 let rec collapse u v = 
199   let repr_u = repr u in
200   let repr_v = repr v in
201   let ge_v = close_ge v in
202   let ge_u = close_ge u in
203   if List.mem repr_u ge_v && List.mem repr_v ge_u then
204     add_eq u v
205
206 (* we have to add u == v *)
207 and add_eq u v = 
208   let repr_u = repr u in
209   let repr_v = repr v in
210   (* if we already have u == v then do nothing *)
211   if repr_u = repr_v then
212     () 
213   else
214     (* if we already have v > u then fail *)
215     let gt_v = close_gt v in
216     if List.mem repr_u gt_v then
217       error ("Asking for " ^ (string_of_universe u) ^ " == " ^ 
218             (string_of_universe v) ^ " but " ^ 
219             (string_of_universe v) ^ " > " ^ (string_of_universe u))
220     else 
221       (* if we already have u > v then fail *)
222       let gt_u = close_gt u in
223       if List.mem repr_v gt_u then           
224         error ("Asking for " ^ (string_of_universe u) ^ " == " ^ 
225               (string_of_universe v) ^ " but " ^ 
226               (string_of_universe u) ^ " > " ^ (string_of_universe v))
227       else
228         (* add the inherited > constraints *)
229         List.iter (fun v -> add_gt u v ) (*gt_v*) repr_v.gt;
230         (* add the inherited >= constraints *)
231         (* close_ge assumes that v==u -> v \notin (repr u).ge *)
232         repr_u.ge <- List.filter (fun x -> x <> u && x <> v) 
233          (repr_v.ge @ repr_u.ge);
234         (* mege the eq list, we assume they are disjuncted *)
235         repr_u.eq <- repr_u.eq @ repr_v.eq;
236         (* we have to remap all node represented by repr_v to repr_u *)
237         remap v repr_u;
238         (* FIXME: not sure this is what we have to do 
239                   think more to the list of suspected cicles
240         *)
241         List.iter (fun x -> collapse u x) repr_u.ge 
242     
243 (* we have to add u >= v *)
244 and add_ge u v =
245   let repr_u = repr u in
246   let repr_v = repr v in
247   (* if we already have u == v then do nothing *)
248   if repr_u = repr_v then
249     () 
250   else 
251     (* if we already have v > u then fail *)
252     let gt = close_gt v in
253     if List.memq repr_u gt then
254       error ("Asking for " ^ (string_of_universe u) ^ " >= " ^ 
255             (string_of_universe v) ^ " but " ^ 
256             (string_of_universe v) ^ " > " ^ (string_of_universe u))
257     else
258       (* it is now safe to add u >= v *)
259       repr_u.ge <- v::repr_u.ge;
260       (* but we may have introduced a cicle *)
261       collapse u v (* FIXME: not sure it is from u to v, think more. *)
262       
263 (* we have to add u > v *)        
264 and add_gt u v =
265   let repr_u = repr u in
266   let repr_v = repr v in
267   (* if we already have u == v then fail *)
268   if repr_u = repr_v then
269     error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
270           (string_of_universe v) ^ " but " ^ 
271           (string_of_universe u) ^ " == " ^ (string_of_universe v))
272   else 
273     (* if we already have u > v do nothing *)
274     let gt_u = close_gt u in
275     if List.memq repr_v gt_u then
276       () 
277     else
278       (* if we already have v > u then fail *)
279       let gt = close_gt v in
280       if List.memq repr_u gt then
281         error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
282               (string_of_universe v) ^ " but " ^ 
283               (string_of_universe v) ^ " > " ^ (string_of_universe u))
284       else
285         (* if we already have v >= u then fail *)
286         let ge = close_ge v in
287         if List.memq repr_u ge then
288           error ("Asking for " ^ (string_of_universe u) ^ " > " ^ 
289                 (string_of_universe v) ^ " but " ^ 
290                 (string_of_universe v) ^ " >= " ^ (string_of_universe u))
291         else
292           (* it is safe to add u > v *)
293           repr_u.gt <- v::repr_u.gt
294
295 let add_gt u v =
296   try 
297     add_gt u v; true
298   with
299     exn -> false
300
301 let add_ge u v =
302   try 
303     add_ge u v; true
304   with
305     exn -> false
306
307 let add_eq u v =
308   try 
309     add_eq u v; true
310   with
311     exn -> false
312
313 (* <--------> *)
314
315 (* ************************************************************************** *)
316 (*  To make tests                                                             *)
317 (* ************************************************************************** *)
318
319 (*
320 let check_status_eq l =
321   let s = List.fold_left (fun s u -> s^(string_of_universe u) ^ ";") "" l in
322   let repr_u = repr (List.hd l) in
323   let rec check_status_eq_aux c =
324     match c with
325       [] -> print_endline (" Result check_status_eq["^s^"] = OK");true
326     | u::tl -> if repr u != repr_u then
327                  (print_endline (" Result check_status_eq["^s^"] = FAILED");
328                  print_endline ((string_of_universe u) ^ " != " ^ 
329                   (string_of_universe repr_u.u));
330                  print_map ();false)
331                else
332                  check_status_eq_aux tl
333   in
334   check_status_eq_aux (List.tl l)
335 *)
336
337 (* ************************************************************************** *)
338 (*  Fake implementation                                                       *)
339 (* ************************************************************************** *)
340
341 (* <--------> *
342 let add_ge u v = true
343 let add_gt u v = true
344 let add_eq u v = true
345 * <--------> *)