]> matita.cs.unibo.it Git - helm.git/blobdiff - components/ng_kernel/nUri.ml
branch for universe
[helm.git] / components / ng_kernel / nUri.ml
diff --git a/components/ng_kernel/nUri.ml b/components/ng_kernel/nUri.ml
new file mode 100644 (file)
index 0000000..7e8cf40
--- /dev/null
@@ -0,0 +1,41 @@
+type uri = int * string (* shareno, URI *)
+
+let string_of_uri (_, uri) = uri;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module MapStringsToUri = Map.Make(OrderedStrings);;
+
+let set_of_uri = ref MapStringsToUri.empty;;
+
+let uri_of_string = 
+  let counter = ref 0 in 
+  let c () = incr counter; !counter in 
+fun s ->
+  try MapStringsToUri.find s !set_of_uri
+  with Not_found ->
+    let new_uri = c(), s in
+    set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
+    new_uri
+;;
+
+let eq = (==);;
+let compare (n1,_) (n2,_) = n2 - n1;;
+
+module HT = struct
+        type t = uri
+        let equal = eq
+        let compare = compare
+        let hash (n,_) = n;;
+end;;
+
+module UriHash = Hashtbl.Make(HT);;
+
+let ouri_of_nuri u = UriManager.uri_of_string (string_of_uri u);;
+let nuri_of_ouri o = uri_of_string (UriManager.string_of_uri o);;
+