added orrible hack to make the current uri visible in the parser so that named univer...

[helm.git] / helm / ocaml / cic / cicUniv.ml

diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml
index 44bccc62b281715cbb7c35d882747dd8f25f157a..c986ae866e03ad8759126c054f3707772c245967 100644 (file)
--- 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)
@@ -929,4 +941,25 @@ let recons_graph graph =
       MAL.add (recons_univ universe) (recons_entry entry) map)
     graph MAL.empty
 
+let assert_univs_have_uri graph =
+  let assert_univ u =
+    match u with 
+    | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
+    | _ -> ()
+  in
+  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 *)