]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/urimanager/uriManager.ml
many strings that are supposed to be URIs are now UriManager.uri
[helm.git] / helm / ocaml / urimanager / uriManager.ml
index 0697fb73b9a32a50d8961ba48a2237201cac2c5b..4eae6799d2e21d11c64974793e93bee723c4f104 100644 (file)
 * "cic:/a/b/c.ind#xpointer(1/1/1)" =>
 *   [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c"; "#xpointer(1/1/1)" |]
 *)
-type uri = string array;;
+
+let fresh_id =
+ let id = ref 0 in
+  function () ->
+    incr id;
+    !id
+
+type uri = string array * int;;
 
 let eq uri1 uri2 =
   uri1 == uri2 
 ;;
 
-let string_of_uri uri =
+let string_of_uri (uri,_) =
   match  uri.(Array.length uri - 1) with
   | "" -> 
       uri.(Array.length uri - 3)
@@ -44,9 +51,9 @@ 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;;
+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;;
 
 module OrderedStrings =
  struct
@@ -63,7 +70,7 @@ 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 =
@@ -131,15 +138,16 @@ let uri_of_string str =
     SetOfStrings.find str !set_of_uri
    with
     Not_found ->
-      let uri = Array.of_list (mk_prefixes base xpointer) in
+      let uri = Array.of_list (mk_prefixes base xpointer), fresh_id () in
       add_to_uriset ~suri:str uri
 ;;
 
-let strip_xpointer 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 new_uri = stripped_uri,fresh_id () in
+  let suri = string_of_uri new_uri in
+  add_to_uriset ~suri new_uri
 
   
 let cicuri_of_uri uri =
@@ -151,9 +159,10 @@ let cicuri_of_uri uri =
    if completeuri = newcompleteuri then
     uri
    else
+    let uri = fst uri in
     let newuri = Array.copy uri in
      newuri.(Array.length uri - 3) <- newcompleteuri ;
-     add_to_uriset newuri
+     add_to_uriset (newuri,fresh_id ())
 ;;
 
 let annuri_of_uri uri =
@@ -161,9 +170,10 @@ let annuri_of_uri uri =
   if Str.string_match (Str.regexp ".*\\.ann$") completeuri 0 then
    uri
   else
+   let uri = fst uri in
    let newuri = Array.copy uri in
     newuri.(Array.length uri - 3) <- completeuri ^ ".ann" ;
-    add_to_uriset newuri
+    add_to_uriset (newuri,fresh_id ())
 ;;
 
 let uri_is_annuri uri =
@@ -173,18 +183,19 @@ let uri_is_annuri uri =
 let bodyuri_of_uri uri =
  let struri = string_of_uri uri in
   if Str.string_match (Str.regexp ".*\\.con$") (string_of_uri uri) 0 then
+   let uri = fst uri in
    let newuri = Array.copy uri in
     newuri.(Array.length uri - 3) <- struri ^ ".body" ;
-    Some (add_to_uriset newuri)
+    Some (add_to_uriset (newuri,fresh_id ()))
   else
    None
 ;;
 
 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" ;
-   add_to_uriset newuri
+  let newuri = Array.copy (fst cicuri) in
+   newuri.(Array.length (fst cicuri) - 3) <- (string_of_uri cicuri) ^ ".types" ;
+   add_to_uriset (newuri,fresh_id ())
 ;;
 
 type uriref = uri * (int list)
@@ -197,10 +208,7 @@ 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
+let compare (_,id1) (_,id2) = id1 - id2
 
 module OrderedUri =
 struct