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 7f8266876ddbcaf891d03c8e8bc0bc8086eba685..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)