X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicUniv.ml;h=abb50a196482da30fee62ecdaf33e53c967c9d1a;hb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;hp=7e6bde44ebcb2b29000171317e69efadf7c80909;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 7e6bde44e..abb50a196 100644
--- a/helm/ocaml/cic/cicUniv.ml
+++ b/helm/ocaml/cic/cicUniv.ml
@@ -128,8 +128,8 @@ let are_ugraph_eq = are_ugraph_eq307
 let string_of_universe (i,u) = 
   match u with
       Some u ->
-	((string_of_int i) ^ " " ^ (UriManager.string_of_uri u))
-    | None -> (string_of_int i)
+	"(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
+    | None -> "(" ^ (string_of_int i) ^ ",None)"
 
 let string_of_universe_set l = 
   SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
@@ -142,7 +142,7 @@ let string_of_node n =
   "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
 
 let string_of_arc (a,u,v) = 
-  "(" ^ (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v) ^ ")"
+  (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
   
 let string_of_mal m =
   let rc = ref "" in
@@ -178,7 +178,7 @@ let partial = ref 0.0 ;;
 let reset_spent_time () = time_spent := 0.0;;
 let get_spent_time () = !time_spent ;;
 let begin_spending () =
-  assert (!partial = 0.0);
+  (*assert (!partial = 0.0);*)
   partial := Unix.gettimeofday ()
 ;;
 
@@ -419,11 +419,14 @@ exception UniverseInconsistency of string
 
 let error arc node1 closure_type node2 closure =
   let s = "\n  ===== Universe Inconsistency detected =====\n\n" ^
-   "\tUnable to add "^ (string_of_arc arc) ^ " cause " ^ 
-   (string_of_universe node1) ^ " is in the " ^
-   closure_type ^ " closure {" ^
-   (string_of_universe_set closure) ^ "} of " ^ 
-   (string_of_universe node2) ^ "\n\n" ^
+   "   Unable to add\n" ^ 
+   "\t" ^ (string_of_arc arc) ^ "\n" ^
+   "   cause\n" ^ 
+   "\t" ^ (string_of_universe node1) ^ "\n" ^
+   "   is in the " ^ closure_type ^ " closure\n" ^
+   "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^ 
+   "   of\n" ^ 
+   "\t" ^ (string_of_universe node2) ^ "\n\n" ^
    "  ===== Universe Inconsistency detected =====\n" in
   prerr_endline s;
   raise (UniverseInconsistency s)
@@ -463,13 +466,22 @@ type universe_graph = bag
 
 let empty_ugraph = empty_bag
 
-let current_index = ref (-1)
+let current_index_anon = ref (-1)
+let current_index_named = ref (-1)
 
-let restart_numbering () = current_index := (-1) 
+let restart_numbering () = current_index_named := (-1) 
 
-let fresh () =
-  current_index := !current_index + 1;
-  (!current_index,None)
+let fresh ?uri () =
+  let i =
+    match uri with
+    | None -> 
+        current_index_anon := !current_index_anon + 1;
+        !current_index_anon
+    | Some _ -> 
+        current_index_named := !current_index_named + 1;
+        !current_index_named
+  in
+  (i,uri)
 
 let print_ugraph g = 
   prerr_endline (string_of_bag g)
@@ -903,4 +915,51 @@ let _ =
 
  *)
 
+let recons_univ u =
+  match u with
+  | i, None -> u
+  | i, Some uri ->
+      i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
+
+let recons_entry entry =
+  let recons_set set =
+    SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
+  in
+  {
+    eq_closure = recons_set entry.eq_closure;
+    ge_closure = recons_set entry.ge_closure;
+    gt_closure = recons_set entry.gt_closure;
+    in_gegt_of = recons_set entry.in_gegt_of;
+    one_s_eq = recons_set entry.one_s_eq;
+    one_s_ge = recons_set entry.one_s_ge;
+    one_s_gt = recons_set entry.one_s_gt;
+  }
+
+let recons_graph graph =
+  MAL.fold
+    (fun universe entry map ->
+      MAL.add (recons_univ universe) (recons_entry entry) map)
+    graph MAL.empty
+
+let assert_univ u =
+    match u with 
+    | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+    | _ -> ()
+    
+let assert_univs_have_uri graph =
+  let assert_set s =
+    SOF.iter (fun u -> assert_univ u) s
+  in
+  let assert_entry e =
+    assert_set e.eq_closure;
+    assert_set e.ge_closure;
+    assert_set e.gt_closure;
+    assert_set e.in_gegt_of;
+    assert_set e.one_s_eq;
+    assert_set e.one_s_ge;
+    assert_set e.one_s_gt;
+  in
+  MAL.iter (fun k v -> assert_univ k; assert_entry v)graph 
+  
+    
 (* EOF *)