X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;h=0697fb73b9a32a50d8961ba48a2237201cac2c5b;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=cd7f9a119ba38409f121604473f06400bafc4756;hpb=17b586f742e5c58501d62c81b6c517f5ba039f1d;p=helm.git

diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml
index cd7f9a119..0697fb73b 100644
--- a/helm/ocaml/urimanager/uriManager.ml
+++ b/helm/ocaml/urimanager/uriManager.ml
@@ -33,7 +33,7 @@
 type uri = string array;;
 
 let eq uri1 uri2 =
- uri1 == uri2
+  uri1 == uri2 
 ;;
 
 let string_of_uri uri =
@@ -43,6 +43,7 @@ let string_of_uri uri =
   | _ -> 
       String.concat "#" 
         [ uri.(Array.length uri - 3); uri.(Array.length uri - 1) ]
+
 let name_of_uri uri = uri.(Array.length uri - 2);;
 let buri_of_uri uri = uri.(Array.length uri - 4);;
 let depth_of_uri uri = Array.length uri - 3;;
@@ -62,6 +63,24 @@ module SetOfStrings = Map.Make(OrderedStrings);;
 let set_of_uri = ref SetOfStrings.empty;;
 let set_of_prefixes = ref SetOfStrings.empty;;
 
+  
+(* hash conses an uri *)
+let add_to_uriset ?suri uri =
+  let lookup_suri suri =
+    try
+      SetOfStrings.find suri !set_of_uri
+    with Not_found -> assert false
+  in
+  let suri = 
+    match suri with 
+    | None -> string_of_uri uri
+    | Some suri -> suri 
+  in
+  if not(SetOfStrings.mem suri !set_of_uri) then
+    set_of_uri := SetOfStrings.add suri uri !set_of_uri;
+  lookup_suri suri  
+    
+
 (* similar to uri_of_string, but used for prefixes of uris *)
 let normalize prefix =
  try
@@ -113,10 +132,16 @@ let uri_of_string str =
    with
     Not_found ->
       let uri = Array.of_list (mk_prefixes base xpointer) in
-      set_of_uri := SetOfStrings.add str uri !set_of_uri ;
-      uri
+      add_to_uriset ~suri:str uri
 ;;
 
+let strip_xpointer uri =
+  let stripped_uri = Array.copy uri in
+  stripped_uri.(Array.length uri - 1) <- "";  (* reset xpointer field *)
+  let suri = string_of_uri stripped_uri in
+  add_to_uriset ~suri stripped_uri
+
+  
 let cicuri_of_uri uri =
  let completeuri = string_of_uri uri in
   let newcompleteuri = 
@@ -128,7 +153,7 @@ let cicuri_of_uri uri =
    else
     let newuri = Array.copy uri in
      newuri.(Array.length uri - 3) <- newcompleteuri ;
-     newuri
+     add_to_uriset newuri
 ;;
 
 let annuri_of_uri uri =
@@ -138,7 +163,7 @@ let annuri_of_uri uri =
   else
    let newuri = Array.copy uri in
     newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ;
-    newuri
+    add_to_uriset newuri
 ;;
 
 let uri_is_annuri uri =
@@ -150,7 +175,7 @@ let bodyuri_of_uri uri =
   if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then
    let newuri = Array.copy uri in
     newuri.(Array.length uri - 3) <- struri ^ ".body" ;
-    Some newuri
+    Some (add_to_uriset newuri)
   else
    None
 ;;
@@ -159,7 +184,7 @@ let innertypesuri_of_uri uri =
  let cicuri = cicuri_of_uri uri in
   let newuri = Array.copy cicuri in
    newuri.(Array.length cicuri - 3) <- (string_of_uri cicuri) ^ ".types" ;
-   newuri
+   add_to_uriset newuri
 ;;
 
 type uriref = uri * (int list)
@@ -172,3 +197,16 @@ let string_of_uriref (uri, fi) =
       | [t]         -> str ^ xp t ^ ")" 
       | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" 
 
+let compare u1 u2 =
+  let su1 = string_of_uri u1 in
+  let su2 = string_of_uri u2 in
+  Pervasives.compare su1 su2
+
+module OrderedUri =
+struct
+  type t = uri
+  let compare = compare (* the one above, not Pervasives.compare *)
+end
+
+module UriSet = Set.Make (OrderedUri)
+