]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/uriManager.ml.implementazione_semplice
Initial revision
[helm.git] / helm / interface / uriManager.ml.implementazione_semplice
diff --git a/helm/interface/uriManager.ml.implementazione_semplice b/helm/interface/uriManager.ml.implementazione_semplice
new file mode 100644 (file)
index 0000000..8b8921b
--- /dev/null
@@ -0,0 +1,39 @@
+type uri = string;;
+
+let eq uri1 uri2 =
+ uri1 == uri2
+;;
+
+let string_of_uri uri = uri;;
+
+let name_of_uri uri =
+ let l = Str.split (Str.regexp "/") uri in
+  let name_suf = List.nth l (List.length l - 1) in
+   List.hd (Str.split (Str.regexp "\.") name_suf)
+;;
+
+let depth_of_uri uri =
+ List.length (Str.split (Str.regexp "/") uri) - 2
+;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module SetOfStrings = Map.Make(OrderedStrings);;
+
+(* Invariant: the map is the identity function,      *)
+(*  i.e. (SetOfStrings.find str !set_of_uri) == str  *)
+let set_of_uri = ref SetOfStrings.empty;;
+
+let uri_of_string str =
+ try
+  SetOfStrings.find str !set_of_uri
+ with
+  Not_found ->
+   set_of_uri := SetOfStrings.add str str !set_of_uri ;
+   str
+;;