helm/software/components/ng_kernel/nUri.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 type uri = int * string (* shareno, URI *)
  15
  16 let string_of_uri (_, uri) = uri;;
  17
  18 let name_of_uri (_, uri) =
  19   let name = Filename.basename uri in
  20   Filename.chop_extension name
  21 ;;
  22
  23 module OrderedStrings =
  24  struct
  25   type t = string
  26   let compare (s1 : t) (s2 : t) = compare s1 s2
  27  end
  28 ;;
  29
  30 module MapStringsToUri = Map.Make(OrderedStrings);;
  31
  32 let set_of_uri = ref MapStringsToUri.empty;;
  33
  34 let uri_of_string =
  35   let counter = ref 0 in
  36   let c () = incr counter; !counter in
  37 fun s ->
  38   try MapStringsToUri.find s !set_of_uri
  39   with Not_found ->
  40     let new_uri = c(), s in
  41     set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
  42     new_uri
  43 ;;
  44
  45 let eq = (==);;
  46 let compare (n1,_) (n2,_) = n2 - n1;;
  47
  48 module HT = struct
  49         type t = uri
  50         let equal = eq
  51         let compare = compare
  52         let hash (n,_) = n;;
  53 end;;
  54
  55 module UriHash = Hashtbl.Make(HT);;