]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/uriManager.ml.implementazione_semplice
Initial revision
[helm.git] / helm / interface / uriManager.ml.implementazione_semplice
1 type uri = string;;
2
3 let eq uri1 uri2 =
4  uri1 == uri2
5 ;;
6
7 let string_of_uri uri = uri;;
8
9 let name_of_uri uri =
10  let l = Str.split (Str.regexp "/") uri in
11   let name_suf = List.nth l (List.length l - 1) in
12    List.hd (Str.split (Str.regexp "\.") name_suf)
13 ;;
14
15 let depth_of_uri uri =
16  List.length (Str.split (Str.regexp "/") uri) - 2
17 ;;
18
19 module OrderedStrings =
20  struct
21   type t = string
22   let compare (s1 : t) (s2 : t) = compare s1 s2
23  end
24 ;;
25
26 module SetOfStrings = Map.Make(OrderedStrings);;
27
28 (* Invariant: the map is the identity function,      *)
29 (*  i.e. (SetOfStrings.find str !set_of_uri) == str  *)
30 let set_of_uri = ref SetOfStrings.empty;;
31
32 let uri_of_string str =
33  try
34   SetOfStrings.find str !set_of_uri
35  with
36   Not_found ->
37    set_of_uri := SetOfStrings.add str str !set_of_uri ;
38    str
39 ;;