]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/uriManager.ml
Initial revision
[helm.git] / helm / interface / uriManager.ml
diff --git a/helm/interface/uriManager.ml b/helm/interface/uriManager.ml
new file mode 100644 (file)
index 0000000..d03d997
--- /dev/null
@@ -0,0 +1,86 @@
+(* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
+type uri = string array;;
+
+let eq uri1 uri2 =
+ uri1 == uri2
+;;
+
+let string_of_uri uri = uri.(Array.length uri - 2);;
+let name_of_uri uri = uri.(Array.length uri - 1);;
+let buri_of_uri uri = uri.(Array.length uri - 3);;
+let depth_of_uri uri = Array.length uri - 2;;
+
+(*CSC: ora e' diventato poco efficiente, migliorare *)
+let relative_depth curi uri cookingsno =
+ let rec length_of_current_prefix l1 l2 =
+  match (l1, l2) with
+     (he1::tl1, he2::tl2) when he1 == he2 ->
+       1 + length_of_current_prefix tl1 tl2
+   | (_,_) -> 0
+ in
+  depth_of_uri uri -
+   length_of_current_prefix
+    (Array.to_list (Array.sub curi 0 (Array.length curi - (2 + cookingsno))))
+    (Array.to_list (Array.sub uri 0 (Array.length uri - 2)))
+  (*CSC: vecchio codice da eliminare
+  if eq curi uri then 0
+  else
+   depth_of_uri uri -
+    length_of_current_prefix (Array.to_list curi) (Array.to_list uri)
+  *)
+;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module SetOfStrings = Map.Make(OrderedStrings);;
+
+(*CSC: commento obsoleto ed errato *)
+(* Invariant: the map is the identity function,      *)
+(*  i.e. (SetOfStrings.find str !set_of_uri) == str  *)
+let set_of_uri = ref SetOfStrings.empty;;
+let set_of_prefixes = ref SetOfStrings.empty;;
+
+(* similar to uri_of_string, but used for prefixes of uris *)
+let normalize prefix =
+ try
+  SetOfStrings.find prefix !set_of_prefixes
+ with
+  Not_found ->
+   set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ;
+   prefix
+;;
+
+exception IllFormedUri of string;;
+
+let mk_prefixes str =
+ let rec aux curi =
+  function
+     [he] ->
+      let prefix_uri = curi ^ "/" ^ he
+      and name = List.hd (Str.split (Str.regexp "\.") he) in
+       [ normalize prefix_uri ; name ]
+   | he::tl ->
+      let prefix_uri = curi ^ "/" ^ he in
+       (normalize prefix_uri)::(aux prefix_uri tl)
+   | _ -> raise (IllFormedUri str)
+ in
+  let tokens = (Str.split (Str.regexp "/") str) in
+   (* ty = "cic:" *)
+   let (ty, sp) = (List.hd tokens, List.tl tokens) in
+    aux ty sp
+;;
+
+let uri_of_string str =
+ try
+  SetOfStrings.find str !set_of_uri
+ with
+  Not_found ->
+   let uri = Array.of_list (mk_prefixes str) in
+    set_of_uri := SetOfStrings.add str uri !set_of_uri ;
+    uri
+;;