matita/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 let baseuri_of_uri (_,uri) =
  24  Filename.dirname uri
  25 ;;
  26
  27 module OrderedStrings =
  28  struct
  29   type t = string
  30   let compare (s1 : t) (s2 : t) = compare s1 s2
  31  end
  32 ;;
  33
  34 module MapStringsToUri = Map.Make(OrderedStrings);;
  35
  36 let set_of_uri = ref MapStringsToUri.empty;;
  37
  38 let uri_of_string =
  39   let counter = ref 0 in
  40   let c () = incr counter; !counter in
  41 fun s ->
  42   try MapStringsToUri.find s !set_of_uri
  43   with Not_found ->
  44     let new_uri = c(), s in
  45     set_of_uri := MapStringsToUri.add s new_uri !set_of_uri;
  46     new_uri
  47 ;;
  48
  49 let eq = (==);;
  50 let compare (n1,_) (n2,_) = n2 - n1;;
  51
  52 module HT = struct
  53         type t = uri
  54         let equal = eq
  55         let compare = compare
  56         let hash (n,_) = n;;
  57 end;;
  58
  59 module UriHash = Hashtbl.Make(HT);;
  60 module UriMap = Map.Make(HT);;