]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cicUniv.ml
New syntax.
[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 open Printf
38
39 (******************************************************************************)
40 (** Types and default values                                                 **)
41 (******************************************************************************)
42
43 type universe = int
44
45 module UniverseType = struct
46   type t = universe
47   let compare = Pervasives.compare
48 end
49
50 module SOF = Set.Make(UniverseType)
51
52 type entry = {
53         eq_closure : SOF.t;
54         ge_closure : SOF.t;
55         gt_closure : SOF.t;
56         in_eq_of   : SOF.t;
57         in_ge_of   : SOF.t;
58         in_gt_of   : SOF.t;
59         one_s_eq   : SOF.t;
60         one_s_ge   : SOF.t;
61         one_s_gt   : SOF.t;
62 }
63
64 module MAL = Map.Make(UniverseType)
65
66 type arc_type = GE | GT | EQ
67
68 type arc = arc_type * universe * universe
69
70 type bag = entry MAL.t * (arc list)
71
72 let empty_entry = {
73         eq_closure=SOF.empty;
74         ge_closure=SOF.empty;
75         gt_closure=SOF.empty;
76         in_eq_of=SOF.empty;
77         in_ge_of=SOF.empty;
78         in_gt_of=SOF.empty;
79         one_s_eq=SOF.empty;
80         one_s_ge=SOF.empty;
81         one_s_gt=SOF.empty;
82 }
83
84 let empty_bag = (MAL.empty, [])
85
86 let env_bag = ref empty_bag
87
88 (******************************************************************************)
89 (** Pretty printings                                                         **)
90 (******************************************************************************)
91
92 let string_of_universe u = string_of_int u
93
94 let string_of_arc_type u =
95   match u with
96     EQ -> "EQ" 
97   | GT -> "GT"
98   | GE -> "EQ"
99
100 let string_of_arc u = 
101   let atype,a,b = u in
102   (string_of_arc_type atype) ^ " " ^ 
103    (string_of_universe a) ^ " " ^ (string_of_universe b) ^ "; "
104 ;;
105
106 let string_of_universe_set l = 
107   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
108
109 let string_of_arc_list l = 
110   List.fold_left (fun s x -> s ^ (string_of_arc x) ^ " ") "" l
111
112 let string_of_node n =
113   "{"^
114   "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^ 
115   "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^ 
116   "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^ 
117   "i_eq: " ^ (string_of_universe_set n.in_eq_of) ^ "; " ^ 
118   "i_ge: " ^ (string_of_universe_set n.in_ge_of) ^ "; " ^ 
119   "i_gt: " ^ (string_of_universe_set n.in_gt_of) ^ "}\n"
120   
121 let string_of_mal m =
122   let rc = ref "" in
123   MAL.iter (fun k v -> rc := !rc ^ sprintf "%d --> %s" k (string_of_node v)) m;
124   !rc
125
126 let string_of_bag b = 
127   let (m,l) = b in
128   let s_m = string_of_mal m in
129   let s_l = string_of_arc_list l in
130    s_m ^"["^s_l^"]"
131
132 (******************************************************************************)
133 (** Helpers                                                                  **)
134 (******************************************************************************)
135
136 (*
137     we need to merge the 2 graphs... here the code 
138 *)
139 let repr u m =
140   try 
141     MAL.find u m
142   with
143     Not_found -> 
144       try 
145         let m',_ = !env_bag in
146         MAL.find u m'
147       with
148         Not_found -> empty_entry
149     
150 (*
151     FIXME: May be faster if we make it by hand
152 *)
153 let merge_closures f nodes m =  
154   SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
155
156 (******************************************************************************)
157 (** Real stuff GT                                                            **)
158 (******************************************************************************)
159
160 (* 
161     todo is the SOF of nodes that needs to be recomputed, 
162     m is the MAL map, s is the already touched nodes 
163 *)
164 let rec redo_gt_closure todo m s =
165   if SOF.is_empty todo then m
166   else
167     begin
168     (* we choose the node to recompute *)
169     let u = SOF.choose todo in
170     if not (SOF.mem u s) then
171       let ru = repr u m in
172       let ru' = {ru with gt_closure = 
173        (* the new gt closure is the gt-closures + ge-closures + eq-closures 
174           of the one step gt-connected nodes *)
175        SOF.union ru.one_s_gt (merge_closures 
176         (fun x -> SOF.union x.eq_closure 
177          (SOF.union x.gt_closure x.ge_closure)) ru.one_s_gt m) } in
178       let m' = MAL.add u ru' m in
179       let s' = SOF.add u s in
180       redo_gt_closure (SOF.union (SOF.remove u todo) ru'.in_gt_of) m' s'
181     else
182       (* if already done go next. FIXME: think if it is right
183          maybe we should check if we changed something or not *)
184       redo_gt_closure (SOF.remove u todo) m s
185     end
186
187 (*
188     calculates the closures of u and adjusts the in_*_of of v, then
189     starts redo_*_closure to adjust the colure of nodew thet have 
190     (clusure u) in theyr closures
191 *)
192 let add_gt_arc u v m =
193   let ru = repr u m in
194   let rv = repr v m in 
195   let ru' = {
196     (* new node: we add the v gt-closure and v to our gt-closure *)
197     eq_closure = ru.eq_closure;
198     ge_closure = ru.ge_closure;
199     gt_closure = SOF.add v 
200      (SOF.union ru.gt_closure 
201       (SOF.union rv.ge_closure 
202        (SOF.union rv.eq_closure rv.gt_closure)));
203     in_eq_of = ru.in_eq_of;
204     in_ge_of = ru.in_ge_of;
205     in_gt_of = ru.in_gt_of;
206     one_s_eq = ru.one_s_eq;
207     one_s_ge = ru.one_s_ge;
208     one_s_gt = SOF.add v ru.one_s_gt;
209   } in
210   (* may add the sanity check *)
211   let rv' = { rv with in_gt_of = SOF.add u rv.in_gt_of } in
212   let m' = MAL.add u ru' m in
213   let m'' = MAL.add v rv' m' in
214   redo_gt_closure ru'.in_gt_of m'' SOF.empty
215
216 (*                                                                            
217     given the 2 nodes plus the current bag, adds the arc, recomputes the 
218     closures and returns the new map
219 *)                                                                            
220 let add_gt u v b =
221   let m,l = b in
222   let m' = add_gt_arc u v m in
223   let l' = (GT,u,v)::l in
224   (m',l')
225
226 (******************************************************************************)
227 (** Real stuff GE                                                            **)
228 (******************************************************************************)
229
230 (* 
231     todo is the SOF of nodes that needs to be recomputed, 
232     m is the MAL map, s is the already touched nodes 
233 *)
234 let rec redo_ge_closure todo m s =
235   if SOF.is_empty todo then m,s
236   else
237     begin
238     let u = SOF.choose todo in
239     if not (SOF.mem u s) then
240       begin
241         let ru = repr u m in
242         (* the ge-closure is recomputed as the ge-closures of  
243            ge connected nodes plus theys eq-closure *)
244         let ru' = {ru with ge_closure = merge_closures 
245           (fun x -> SOF.union x.eq_closure x.ge_closure) ru.one_s_ge m } in
246         let m' = MAL.add u ru' m in
247         let s' = SOF.add u s in
248         redo_ge_closure (SOF.union (SOF.remove u todo) ru'.in_ge_of) m' s'
249       end
250     else
251       redo_ge_closure (SOF.remove u todo) m s
252     end
253
254 (*
255     calculates the closures of u and adjusts the in_*_of of v, then
256     starts redo_*_closure to adjust the colure of nodew thet have 
257     (clusure u) in theyr closures
258 *)
259 let add_ge_arc u v m =
260   let ru = repr u m in
261    let rv = repr v m in 
262   let ru' = {
263     eq_closure = ru.eq_closure;
264     ge_closure = SOF.add v 
265      (SOF.union ru.ge_closure 
266       (SOF.union rv.eq_closure rv.ge_closure));
267     gt_closure = ru.gt_closure;
268     in_eq_of = ru.in_eq_of;
269     in_ge_of = ru.in_ge_of;
270     in_gt_of = ru.in_gt_of;
271     one_s_eq = ru.one_s_eq;
272     one_s_ge = SOF.add v ru.one_s_ge;
273     one_s_gt = ru.one_s_gt;
274   } in
275   let rv' = { rv with in_gt_of = SOF.add u rv.in_ge_of } in
276   let m' = MAL.add u ru' m in
277   let m'' = MAL.add v rv' m' in
278   let m''',td = redo_ge_closure ru'.in_ge_of m'' SOF.empty in
279   (* closing ge may provoke aome changes in gt-closures *)
280   redo_gt_closure (SOF.union ru'.in_gt_of 
281    (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_gt_of)) 
282     td SOF.empty )) m''' SOF.empty
283
284 (*                                                                            
285     given the 2 nodes plus the current bag, adds the arc, recomputes the 
286     closures and returns the new map
287 *) 
288 let add_ge u v b =
289   let m,l = b in
290   let m' = add_ge_arc u v m in
291   let l' = (GE,u,v)::l in
292   (m',l')
293   
294 (******************************************************************************)
295 (** Real stuff EQ                                                            **)
296 (******************************************************************************)
297
298 let rec redo_eq_closure todo m s =
299   if SOF.is_empty todo then m,s
300   else begin
301     let u = SOF.choose todo in
302     if not (SOF.mem  u s) then
303       begin
304         let ru = repr u m in
305         let eq_closure = merge_closures 
306           (fun x -> x.eq_closure) ru.one_s_eq m in
307         let ru' = {ru with eq_closure = eq_closure
308         ; in_eq_of = eq_closure ; one_s_eq = eq_closure } in
309         let m' = MAL.add u ru' m in
310         let s' = SOF.add u s in
311         redo_eq_closure (SOF.union (SOF.remove u todo) ru'.in_eq_of) m' s'
312       end
313     else
314       redo_eq_closure (SOF.remove u todo) m s
315   end
316
317 (*
318     calculates the closures of u and adjusts the in_*_of of v, then
319     starts redo_*_closure to adjust the colure of nodew thet have 
320     (clusure u) in theyr closures
321 *)
322 let add_eq_arc u v m =
323   let ru = repr u m in
324   let rv = repr v m in 
325   (* since eq is symmetric we have to chage more *)
326   let eq_closure = SOF.add u (SOF.add v 
327      (SOF.union ru.eq_closure rv.eq_closure)) in
328   let ru' = {
329     eq_closure = eq_closure;
330     ge_closure = SOF.union ru.ge_closure rv.ge_closure;
331     gt_closure = SOF.union ru.gt_closure rv.gt_closure;
332     in_eq_of = eq_closure;
333     in_ge_of = SOF.union ru.in_ge_of rv.in_ge_of;
334     in_gt_of = SOF.union ru.in_gt_of rv.in_gt_of;
335     one_s_eq = eq_closure;
336     one_s_ge = SOF.union ru.one_s_ge rv.one_s_ge;
337     one_s_gt = SOF.union ru.one_s_gt rv.one_s_gt;
338   } in
339   (* this is a collapse *)
340   let rv' = ru' in
341   let m' = MAL.add u ru' m in
342   let m'' = MAL.add v rv' m' in
343   let m''',td = redo_eq_closure ru'.in_eq_of m'' SOF.empty in
344   (* redoing a eq may change some ge and some gt *)
345   let m'''',td' = redo_ge_closure 
346    (SOF.union ru'.in_ge_of 
347     (SOF.fold (fun u s -> SOF.union s ((repr u m''').in_ge_of)) 
348     td SOF.empty)) m''' SOF.empty in
349   redo_gt_closure (SOF.union ru'.in_gt_of 
350    (SOF.fold (fun u s -> SOF.union s ((repr u m'''').in_gt_of)) 
351     td' SOF.empty)) m'''' SOF.empty
352
353 (*                                                                            
354     given the 2 nodes plus the current bag, adds the arc, recomputes the 
355     closures and returns the new map
356 *) 
357 let add_eq u v b =
358   let m,l = b in
359   let m' = add_eq_arc u v m in
360   let l' = (EQ,u,v)::l in
361   (m',l')
362
363 (******************************************************************************)
364 (** Oyther real code                                                         **)
365 (******************************************************************************)
366
367 exception UniverseInconsistency of string 
368
369 let error arc node1 closure_type node2 closure =
370   let s = "  ===== Universe Inconsistency detected =====\n\n" ^
371    "\tUnable to add ("^ (string_of_arc arc) ^ ") cause " ^ 
372    (string_of_universe node1) ^ " is in the " ^
373    (string_of_arc_type closure_type) ^ " closure {" ^
374    (string_of_universe_set closure) ^ "} of " ^ 
375    (string_of_universe node2) ^ "\n\n" ^
376    "  ===== Universe Inconsistency detected =====\n" in
377   prerr_endline s;
378   raise (UniverseInconsistency s)
379
380 (*  
381     we merge the env_bag with b
382 *)
383 let qed b = 
384   let m,l = b in
385   let m',l' = !env_bag in
386   let m'' = ref m' in
387   MAL.iter (fun k v -> m'':= MAL.add k v !m'') m;
388   let l'' = l @ l' in
389   env_bag := (!m'',l'')
390   
391 let add_eq u v b =
392   (* should we check to no add twice the same?? *)
393   let m,_ = b in
394   let ru = repr u m in
395   if SOF.mem v ru.gt_closure then
396     error (EQ,u,v) v GT u ru.gt_closure
397   else
398     begin
399     let rv = repr v m in
400     if SOF.mem u rv.gt_closure then
401       error (EQ,u,v) u GT v rv.gt_closure
402     else
403       add_eq u v b
404     end
405
406 let add_ge u v b =
407   (* should we check to no add twice the same?? *)
408   let m,_ = b in
409   let rv = repr v m in
410   if SOF.mem u rv.gt_closure then
411     error (GE,u,v) u GT v rv.gt_closure
412   else
413     add_ge u v b
414   
415 let add_gt u v b =
416   (* should we check to no add twice the same?? *)
417   let m,_ = b in
418   let rv = repr v m in
419   if SOF.mem u rv.gt_closure then
420     error (GT,u,v) u GT v rv.gt_closure
421   else
422     begin
423       if SOF.mem u rv.ge_closure then
424         error (GT,u,v) u GE v rv.ge_closure
425       else
426         begin
427           if SOF.mem u rv.eq_closure then
428             error (GT,u,v) u EQ v rv.eq_closure
429           else
430             add_gt u v b
431         end
432     end
433   
434   
435
436 (******************************************************************************)
437 (** World interface                                                          **)
438 (******************************************************************************)
439
440 type universe_graph = bag
441
442 let work_bag = ref empty_bag
443 let current_index = ref (-1)
444
445 let get_working () = !work_bag
446 let get_global  () = !env_bag 
447 let set_working b = work_bag := b
448
449 let fresh () =
450   current_index := !current_index + 1;
451   !current_index
452
453 let qed () = 
454   qed !work_bag
455
456 let print_global_graph () =
457   let s = string_of_bag !env_bag in
458   prerr_endline s
459
460 let print_working_graph () =
461   let s = string_of_bag !work_bag in
462   prerr_endline s
463
464 type history_ticket = int
465
466 let get_history_ticket b =
467   let m,l = b in
468   List.length l
469
470 let redo_history t b b'=
471   let rec get_history l n =
472     if n == 0 then
473       []
474     else
475       begin
476       match l with 
477         [] -> failwith "erroer, lista piu' corta della history"
478       | h::tl -> h::(get_history tl (n - 1))
479       end
480   in
481   let rec redo_commands l b =
482     match l with
483       [] -> b
484     | (GE,u,v)::tl -> redo_commands tl (add_ge u v b)
485     | (GT,u,v)::tl -> redo_commands tl (add_gt u v b)
486     | (EQ,u,v)::tl -> redo_commands tl (add_eq u v b)
487   in
488   let (m,l) = b in
489   let todo = List.rev (get_history l ((List.length l) - t)) in
490   try 
491     redo_commands todo b'
492   with 
493     UniverseInconsistency s -> failwith s
494   (*| _ -> failwith "Unexpected exception"*)
495
496 let add_gt u v =
497   try 
498     work_bag := add_gt u v !work_bag; true
499   with
500     UniverseInconsistency s -> false
501   (*| _ -> failwith "Unexpected exception"*)
502
503 let add_ge u v = 
504   try 
505     work_bag := add_ge u v !work_bag;true
506   with
507     UniverseInconsistency s -> false
508   (*| _ -> failwith "Unexpected exception"*)
509
510 let add_eq u v =
511   try 
512     work_bag := add_eq u v !work_bag;true
513   with
514     UniverseInconsistency s -> false
515   (*| _ -> failwith "Unexpected exception"*)
516
517 let saved_data = ref (empty_bag,0)
518
519 let directly_to_env_begin () =
520   saved_data := (!work_bag, get_history_ticket !env_bag);
521   work_bag := empty_bag
522   
523 let directly_to_env_end () = 
524   qed ();
525   let (b,t) = !saved_data in
526   work_bag := redo_history t !env_bag b
527  
528 let reset_working () = work_bag := empty_bag
529
530 (******************************************************************************)
531 (** Fake implementatoin                                                      **)
532 (******************************************************************************)
533
534 let reset_working = function _ -> ()
535 let directly_to_env_end = function _ -> ()
536 let directly_to_env_begin = function _ -> ()
537 let add_eq = fun _ _ -> true
538 let add_ge = fun _ _ -> true
539 let add_gt = fun _ _ -> true
540 let get_working = function a -> empty_bag
541 let set_working = function a -> ()