]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicUniv.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic / cicUniv.ml
index 7f8266876ddbcaf891d03c8e8bc0bc8086eba685..3d92f33358f1b76929027eb0366da95bea03d7ec 100644 (file)
@@ -38,7 +38,7 @@
 (** switch implementation                                                   **)
 (*****************************************************************************)
 
-let fast_implementation = ref false ;;
+let fast_implementation = ref true ;;
 
 (*****************************************************************************)
 (** open                                                                    **)
@@ -98,28 +98,7 @@ let are_entry_eq v1 v2 =
   (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
   (are_set_eq v1.one_s_eq v2.one_s_eq )
 
-
-(* ocaml 3.07 doesn't have MAP.equal, 3.08 has it! *)
-(*
-  let are_ugraph_eq308 g h =
-    MAL.equal are_entry_eq g h
-*)
-let are_ugraph_eq307 g h = 
-  try
-    MAL.fold (
-      fun k v b -> 
-       if not b then 
-         raise (Failure "Different") 
-       else
-          try
-            let k_h = MAL.find k h in
-            are_entry_eq v k_h
-          with Not_found -> true
-        ) g true
-    with 
-      Failure "Different" -> false
-
-let are_ugraph_eq = are_ugraph_eq307
+let are_ugraph_eq = MAL.equal are_entry_eq
 
 (*****************************************************************************)
 (** Pretty printings                                                        **)
@@ -128,8 +107,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,13 +121,13 @@ 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
   MAL.iter (fun k v ->  
     rc := !rc ^ sprintf "%s --> %s" (string_of_universe k) 
-             (string_of_node v)) m;
+              (string_of_node v)) m;
   !rc
 
 let string_of_bag b = 
@@ -178,7 +157,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 ()
 ;;
 
@@ -241,7 +220,7 @@ and closure_gt_fast ru m =
       
 and print_rec_status u ru =
   print_endline ("Aggiusto " ^ (string_of_universe u) ^ 
-                "e ottengo questa chiusura\n " ^ (string_of_node ru))
+                 "e ottengo questa chiusura\n " ^ (string_of_node ru))
 
 and adjust_fast u m =
   let ru = repr u m in
@@ -257,26 +236,26 @@ and adjust_fast u m =
       m
     else
       begin
-       let ru' = {
-         eq_closure = eq_c;
-         ge_closure = ge_c;
-         gt_closure = gt_c;
-         in_gegt_of = ru.in_gegt_of;
-         one_s_eq = ru.one_s_eq;
-         one_s_ge = ru.one_s_ge;
-         one_s_gt = ru.one_s_gt}
-       in
-       let m = MAL.add u ru' m in
-       let m =
+        let ru' = {
+          eq_closure = eq_c;
+          ge_closure = ge_c;
+          gt_closure = gt_c;
+          in_gegt_of = ru.in_gegt_of;
+          one_s_eq = ru.one_s_eq;
+          one_s_ge = ru.one_s_ge;
+          one_s_gt = ru.one_s_gt}
+        in
+        let m = MAL.add u ru' m in
+        let m =
             SOF.fold (fun x m -> adjust_fast  x m) 
               (SOF.union ru'.eq_closure ru'.in_gegt_of) m
               (* TESI: 
                    ru'.in_gegt_of m 
               *)
         in
-         m (*adjust_fast  u m*)
+          m (*adjust_fast  u m*)
       end
-       
+        
 and add_gt_arc_fast u v m =
   let ru = repr u m in
   let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
@@ -293,7 +272,7 @@ and add_ge_arc_fast u v m =
   let rv = repr v m' in
   let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
   let m'' = MAL.add v rv' m' in
-    adjust_fast u m''
+  adjust_fast u m''
 
 and add_eq_arc_fast u v m =
   let ru = repr u m in
@@ -318,7 +297,7 @@ let closure_of u m =
     let j = ru.one_s_eq in
     let _Uj = merge_closures (fun x -> x.eq_closure) j m in
     let one_step_eq = ru.one_s_eq in
-           (SOF.union one_step_eq _Uj)
+            (SOF.union one_step_eq _Uj)
   in
   let ge_c = 
     let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
@@ -419,26 +398,29 @@ 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)
 
 
-let fill_empty_nodes_with_uri g uri =
+let fill_empty_nodes_with_uri g uri =
   let fill_empty_universe u =
     match u with
-       (i,None) -> (i,Some uri)
+        (i,None) -> (i,Some uri)
       | (i,Some _) as u -> u
   in
   let fill_empty_set s =
     SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty 
   in
-  let fill_empty_entry e = {
+  let fill_empty_entry e = { e with
     eq_closure = (fill_empty_set e.eq_closure) ;
     ge_closure = (fill_empty_set e.ge_closure) ;
     gt_closure = (fill_empty_set e.gt_closure) ;
@@ -452,7 +434,8 @@ let fill_empty_nodes_with_uri g uri =
     fun k v m -> 
       MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
   in
-    m'
+  let l' = List.map fill_empty_universe l in
+    m',l'
 
 
 (*****************************************************************************)
@@ -463,14 +446,30 @@ type universe_graph = bag
 
 let empty_ugraph = empty_bag
 
-let current_index = ref (-1)
-
-let restart_numbering () = current_index := (-1) 
-
-let fresh () =
-  current_index := !current_index + 1;
-  (!current_index,None)
+let current_index_anon = ref (-1)
+let current_index_named = ref (-1)
+
+let restart_numbering () = current_index_named := (-1) 
+
+let fresh ?uri ?id () =
+  let i =
+    match uri,id with
+    | None,None -> 
+        current_index_anon := !current_index_anon + 1;
+        !current_index_anon
+    | None, Some _ -> assert false
+    | Some _, None -> 
+        current_index_named := !current_index_named + 1;
+        !current_index_named
+    | Some _, Some id -> id
+  in
+  (i,uri)
 
+let name_universe u uri =
+  match u with
+  | (i, None) -> (i, Some uri)
+  | _ -> u
+  
 let print_ugraph g = 
   prerr_endline (string_of_bag g)
 
@@ -521,9 +520,9 @@ let add_gt ?(fast=(!fast_implementation)) u v b =
 (*        begin
           if SOF.mem u rv.eq_closure then
             error ("GT",u,v) u "EQ" v rv.eq_closure
-         else*)
-           add_gt fast u v b
-(*     end
+          else*)
+            add_gt fast u v b
+(*        end
     end*)
 
 (*****************************************************************************)
@@ -560,37 +559,41 @@ let merge_ugraphs u v =
     else
       let m1 = u in 
       let m2 = v in 
-       MAL.fold (
-         fun k v x -> 
-           (SOF.fold (
-              fun u x -> 
-                let m = add_gt k u x in m) v.one_s_gt 
+        MAL.fold (
+          fun k v x -> 
+            (SOF.fold (
+               fun u x -> 
+                 let m = add_gt k u x in m) 
+                  (SOF.union v.one_s_gt v.gt_closure)
                (SOF.fold (
-                 fun u x -> 
-                   let m = add_ge k u x in m) v.one_s_ge
-                 (SOF.fold (
-                    fun u x -> 
-                      let m = add_eq k u x in m) v.one_s_eq x)))
-       ) m1 m2
+                  fun u x -> 
+                    let m = add_ge k u x in m) 
+                      (SOF.union v.one_s_ge v.ge_closure)
+                  (SOF.fold (
+                     fun u x ->
+                       let m = add_eq k u x in m) 
+                        (SOF.union v.one_s_eq v.eq_closure) x)))
+        ) m1 m2
   in
-    merge_brutal u v
+  merge_brutal u v
 
 
 (*****************************************************************************)
 (** Xml sesialization and parsing                                           **)
 (*****************************************************************************)
 
+let xml_of_universe name u = 
+  match u with
+  | (i,Some u) -> 
+      Xml.xml_empty name [
+        None,"id",(string_of_int i) ;
+        None,"uri",(UriManager.string_of_uri u)]
+  | (_,None) -> 
+      raise (Failure "we can serialize only universes with uri")
+
 let xml_of_set s =
   let l = 
-    List.map (
-      function 
-         (i,Some u) -> 
-           Xml.xml_empty "node" [
-             None,"id",(string_of_int i) ;
-             None,"uri",(UriManager.string_of_uri u)]
-       | (_,None) -> 
-           raise (Failure "we can serialize only universes with uri")
-    ) (SOF.elements s) 
+    List.map (xml_of_universe "node") (SOF.elements s) 
   in
     List.fold_left (fun s x -> [< s ; x >] ) [<>] l
       
@@ -616,9 +619,9 @@ let xml_of_entry u e =
   let (i,u') = u in
   let u'' = 
     match u' with 
-       Some x -> x 
+        Some x -> x 
       | None -> 
-         raise (Failure "we can serialize only universes (entry) with uri")
+          raise (Failure "we can serialize only universes (entry) with uri")
   in
   let ent = Xml.xml_nempty "entry" [
     None,"id",(string_of_int i) ; 
@@ -626,15 +629,19 @@ let xml_of_entry u e =
   let content = xml_of_entry_content e in
   ent content
 
-let write_xml_of_ugraph filename m =
-    let o = open_out filename in
-    output_string o "<?xml version=\"1.0\" encoding=\"iso-8859-1\" ?>\n";
-    Xml.pp_to_outchan (
-      Xml.xml_nempty "ugraph" [] (
-      MAL.fold (
-        fun k v s -> [< s ; (xml_of_entry k v) >])
-      m [<>])) o;
-    close_out o
+let write_xml_of_ugraph filename m l =
+    let tokens = 
+      [< 
+        Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+        Xml.xml_nempty "ugraph" [] 
+          ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ; 
+           (List.fold_left 
+             (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>]
+    in
+    Xml.pp ~gzip:true tokens (Some filename)
+
+let univno = fst
+
  
 let rec clean_ugraph m f =
   let m' = 
@@ -651,18 +658,20 @@ let rec clean_ugraph m f =
     } in 
     MAL.add k v' x ) m' MAL.empty in
   let e_l = 
-    MAL.fold (fun k v l -> if v = empty_entry then k::l else l) m'' []
+    MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
+      begin
+      k::l end else l) m'' []
   in
     if e_l != [] then
       clean_ugraph m'' (fun u -> (f u) && not (List.mem u e_l))
     else
-      m''
+      MAL.fold 
+        (fun k v x -> if v <> empty_entry then MAL.add k v x else x) 
+      m'' MAL.empty
 
 let clean_ugraph g l =
   clean_ugraph g (fun u -> List.mem u l)
 
-open Pxp_types ;;
-
 let assigner_of = 
   function
     "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
@@ -675,83 +684,50 @@ let assigner_of =
   | s -> raise (Failure ("unsupported tag " ^ s))
 ;;
 
-let cb_factory m = 
+let cb_factory m l = 
+  let module XPP = XmlPushParser in
   let current_node = ref (0,None) in
   let current_entry = ref empty_entry in
-  let current_assign = ref (assigner_of "in_ge_of") in
-    function 
-      | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
-      | E_start_tag ("entry",attlist,_,_) -> 
-         let id = List.assoc "id" attlist in      
-         let uri = List.assoc "uri" attlist in
-           current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
-      | E_start_tag ("node",attlist,_,_) -> 
-         let id = int_of_string (List.assoc "id" attlist) in
-         let uri = List.assoc "uri" attlist in 
-           current_entry := !current_assign !current_entry 
-             (id,Some (UriManager.uri_of_string uri))
-      | E_start_tag (s,_,_,_) -> 
-         current_assign := assigner_of s
-      | E_end_tag ("entry",_) -> 
-         m := MAL.add !current_node !current_entry !m;
-         current_entry := empty_entry
+  let current_assign = ref (assigner_of "in_gegt_of") in
+  { XPP.default_callbacks with
+    XPP.end_element = Some( fun name ->
+      match name with
+      | "entry" -> 
+          m := MAL.add !current_node !current_entry !m;
+          current_entry := empty_entry
       | _ -> ()
+    );
+    XPP.start_element = Some( fun name attlist ->
+      match name with
+      | "ugraph" -> ()
+      | "entry" -> 
+          let id = List.assoc "id" attlist in      
+          let uri = List.assoc "uri" attlist in
+          current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
+      | "node" -> 
+          let id = int_of_string (List.assoc "id" attlist) in
+          let uri = List.assoc "uri" attlist in        
+            current_entry := !current_assign !current_entry 
+              (id,Some (UriManager.uri_of_string uri))
+      | "owned_node" -> 
+          let id = int_of_string (List.assoc "id" attlist) in
+          let uri = List.assoc "uri" attlist in        
+          l := (id,Some (UriManager.uri_of_string uri)) :: !l
+      | s -> current_assign := assigner_of s
+    )
+  }
 ;; 
 
-(* alternative implementation *)
-let mapl = [
-  ("ge_closure",0);("gt_closure",1);("eq_closure",2);
-  ("in_gegt_of",  3);
-  ("one_s_ge",  4);("one_s_gt",  5);("one_s_eq",  6)]
-;;
-
-let assigner_of' s = List.assoc s mapl ;;
-
-let entry_of_array a = { 
-  ge_closure = a.(0); gt_closure = a.(1); eq_closure = a.(2);
-  in_gegt_of   = a.(3); 
-  one_s_ge   = a.(4); one_s_gt   = a.(5); one_s_eq   = a.(6)}
-;;
-
-let cb_factory' m = 
-  let current_node = ref (0,None) in
-  let current_entry = Array.create 7 SOF.empty in
-  let current_assign = ref 0 in
-    function 
-      | E_error exn -> raise (Failure (Pxp_types.string_of_exn exn))
-      | E_start_tag ("entry",attlist,_,_) -> 
-          let id = List.assoc "id" attlist in      
-          let uri = List.assoc "uri" attlist in
-            current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
-      | E_start_tag ("node",attlist,_,_) -> 
-         let id = int_of_string (List.assoc "id" attlist) in
-         let uri = List.assoc "uri" attlist in 
-           current_entry.(!current_assign) <- 
-           SOF.add (id,Some (UriManager.uri_of_string uri)) 
-             current_entry.(!current_assign) 
-      | E_start_tag (s,_,_,_) -> 
-         current_assign := assigner_of' s
-      | E_end_tag ("entry",_) -> 
-         m := MAL.add !current_node (entry_of_array current_entry) !m;
-         Array.fill current_entry 0 7 SOF.empty 
-      | _ -> ()
-;;
-
-     
-let ugraph_of_xml filename =
-  let module PX = Pxp_ev_parser in
-  let module NE = Netconversion in 
-  let config = default_config in
-  let entry = `Entry_document [] in
-  let encoding = `Enc_iso88591 in
-  let source = from_file ~system_encoding:encoding filename in
-  let entity_manager = 
-    PX.create_entity_manager ~is_document:true config source in
-  let result = ref MAL.empty in
-  let cb = cb_factory result in
-(*let cb = cb_factory' result in*)
-  PX.process_entity config entry entity_manager cb;
-  !result
+let ugraph_and_univlist_of_xml filename =
+  let module XPP = XmlPushParser in
+  let result_map = ref MAL.empty in
+  let result_list = ref [] in
+  let cb = cb_factory result_map result_list in
+  let xml_parser = XPP.create_parser cb in
+  let xml_source = `Gzip_file filename in
+  (try XPP.parse xml_parser xml_source
+   with (XPP.Parse_error err) as exn -> raise exn);
+  !result_map, !result_list
 
 \f
 (*****************************************************************************)
@@ -770,18 +746,18 @@ let randomize_actionlist n m =
     let node2 = Random.int m in
     let op = 
       let r = Random.float 1.0 in
-       if r < ge_percent then 
-         Ge 
-       else (if r < (ge_percent +. gt_percent) then 
-         Gt 
-       else 
-         Eq) 
+        if r < ge_percent then 
+          Ge 
+        else (if r < (ge_percent +. gt_percent) then 
+          Gt 
+        else 
+          Eq) 
     in
       op,node1,node2      
   in
   let rec aux n =
     match n with 
-       0 -> []
+        0 -> []
       | n -> (random_step ())::(aux (n-1))
   in
     aux n
@@ -789,16 +765,16 @@ let randomize_actionlist n m =
 let print_action_list l =
   let string_of_step (op,node1,node2) =
     (match op with
-        Ge -> "Ge"
+         Ge -> "Ge"
        | Gt -> "Gt"
        | Eq -> "Eq") ^ 
     "," ^ (string_of_int node1) ^ ","   ^ (string_of_int node2) 
   in
   let rec aux l =
     match l with 
-       [] -> "]"
+        [] -> "]"
       | a::tl ->
-         ";" ^ (string_of_step a) ^ (aux tl)
+          ";" ^ (string_of_step a) ^ (aux tl)
   in
   let body = aux l in
   let l_body = (String.length body) - 1 in
@@ -823,18 +799,18 @@ let _ =
   let prform_step ?(fast=false) (t,u,v) g =
     let f,str = 
       match t with
-         Ge -> add_ge,">="
-       | Gt -> add_gt,">"
-       | Eq -> add_eq,"="
+          Ge -> add_ge,">="
+        | Gt -> add_gt,">"
+        | Eq -> add_eq,"="
     in
       d_print_endline (
-       "Aggiungo " ^ 
-       (string_of_int u) ^
-       " " ^ str ^ " " ^ 
-       (string_of_int v));
+        "Aggiungo " ^ 
+        (string_of_int u) ^
+        " " ^ str ^ " " ^ 
+        (string_of_int v));
       let g' = f ~fast (u,None) (v,None) g in
-       (*print_ugraph g' ;*)
-       g'
+        (*print_ugraph g' ;*)
+        g'
   in
   let fail = ref false in
   let time1 = Unix.gettimeofday () in
@@ -843,12 +819,12 @@ let _ =
     try 
       d_print_endline "SAFE";
       List.fold_left (
-       fun g e -> 
-         n_safe := !n_safe + 1;
-         prform_step e g
+        fun g e -> 
+          n_safe := !n_safe + 1;
+          prform_step e g
       ) empty_ugraph action_list
     with
-       UniverseInconsistency s -> fail:=true;empty_bag
+        UniverseInconsistency s -> fail:=true;empty_bag
   in
   let time2 = Unix.gettimeofday () in
   d_print_ugraph g_safe;
@@ -858,8 +834,8 @@ let _ =
     try
       d_print_endline "FAST";
       List.fold_left (
-       fun g e ->
-         n_test := !n_test + 1;
+        fun g e ->
+          n_test := !n_test + 1;
           prform_step ~fast:true e g
       ) empty_ugraph action_list
     with
@@ -869,35 +845,35 @@ let _ =
   d_print_ugraph g_test;
     if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
       begin
-       let num_eq = 
-         List.fold_left (
-           fun s (e,_,_) -> 
-             if e = Eq then s+1 else s 
-         ) 0 action_list 
-       in
-       let num_gt = 
-         List.fold_left (
+        let num_eq = 
+          List.fold_left (
+            fun s (e,_,_) -> 
+              if e = Eq then s+1 else s 
+          ) 0 action_list 
+        in
+        let num_gt = 
+          List.fold_left (
             fun s (e,_,_) ->
               if e = Gt then s+1 else s
           ) 0 action_list
         in
-       let num_ge = max_edges - num_gt - num_eq in
-       let time_fast = (time4 -. time3) in
-       let time_safe = (time2 -. time1) in
-       let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
-       let fail = if !fail then 1 else 0 in
-         print_endline 
-           (sprintf 
-              "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
-              fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
-         exit 0
+        let num_ge = max_edges - num_gt - num_eq in
+        let time_fast = (time4 -. time3) in
+        let time_safe = (time2 -. time1) in
+        let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
+        let fail = if !fail then 1 else 0 in
+          print_endline 
+            (sprintf 
+               "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d" 
+               fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
+          exit 0
       end
     else
       begin
-       print_endline "FAIL";
+        print_endline "FAIL";
         print_ugraph g_safe;
         print_ugraph g_test;
-       exit 1
+        exit 1
       end
 ;;
 
@@ -929,12 +905,12 @@ 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 =
+let assert_univ u =
     match u with 
     | (_,None) -> raise (UniverseInconsistency "This universe graph has a hole")
     | _ -> ()
-  in
+    
+let assert_univs_have_uri graph univlist =
   let assert_set s =
     SOF.iter (fun u -> assert_univ u) s
   in
@@ -947,7 +923,25 @@ let assert_univs_have_uri graph =
     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 
+  MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
+  List.iter assert_univ univlist
+  
+let eq u1 u2 = 
+  match u1,u2 with
+  | (id1, Some uri1),(id2, Some uri2) -> 
+      id1 = id2 && UriManager.eq uri1 uri2
+  | (id1, None),(id2, None) -> id1 = id2
+  | _ -> false
+  
+let compare (id1, uri1) (id2, uri2) = 
+  let cmp = id1 - id2 in
+  if cmp = 0 then
+    match uri1,uri2 with
+    | None, None -> 0 
+    | Some _, None -> 1
+    | None, Some _ -> ~-1
+    | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
+  else
+    cmp
   
-    
 (* EOF *)