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 ""
"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
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 ()
;;
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)
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)
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 *)