helm/ocaml/urimanager/uriManager.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* "cic:/a/b/c.con" => [| "cic:/a" ; "cic:/a/b" ; "cic:/a/b/c.con" ; "c" |] *)
  27 type uri = string array;;
  28
  29 let eq uri1 uri2 =
  30  uri1 == uri2
  31 ;;
  32
  33 let string_of_uri uri = uri.(Array.length uri - 2);;
  34 let name_of_uri uri = uri.(Array.length uri - 1);;
  35 let buri_of_uri uri = uri.(Array.length uri - 3);;
  36 let depth_of_uri uri = Array.length uri - 2;;
  37
  38 module OrderedStrings =
  39  struct
  40   type t = string
  41   let compare (s1 : t) (s2 : t) = compare s1 s2
  42  end
  43 ;;
  44
  45 module SetOfStrings = Map.Make(OrderedStrings);;
  46
  47 (*CSC: commento obsoleto ed errato *)
  48 (* Invariant: the map is the identity function,      *)
  49 (*  i.e. (SetOfStrings.find str !set_of_uri) == str  *)
  50 let set_of_uri = ref SetOfStrings.empty;;
  51 let set_of_prefixes = ref SetOfStrings.empty;;
  52
  53 (* similar to uri_of_string, but used for prefixes of uris *)
  54 let normalize prefix =
  55  try
  56   SetOfStrings.find prefix !set_of_prefixes
  57  with
  58   Not_found ->
  59    set_of_prefixes := SetOfStrings.add prefix prefix !set_of_prefixes ;
  60    prefix
  61 ;;
  62
  63 exception IllFormedUri of string;;
  64
  65 let mk_prefixes str =
  66  let rec aux curi =
  67   function
  68      [he] ->
  69       let prefix_uri = curi ^ "/" ^ he
  70       and name = List.hd (Str.split (Str.regexp "\.") he) in
  71        [ normalize prefix_uri ; name ]
  72    | he::tl ->
  73       let prefix_uri = curi ^ "/" ^ he in
  74        (normalize prefix_uri)::(aux prefix_uri tl)
  75    | _ -> raise (IllFormedUri str)
  76  in
  77   let tokens = (Str.split (Str.regexp "/") str) in
  78    (* ty = "cic:" *)
  79    let (ty, sp) =
  80     (try (List.hd tokens, List.tl tokens)
  81      with Failure "hd" | Failure "tl" ->
  82       raise (IllFormedUri str))
  83     in
  84     aux ty sp
  85 ;;
  86
  87 let uri_of_string str =
  88  try
  89   SetOfStrings.find str !set_of_uri
  90  with
  91   Not_found ->
  92    let uri = Array.of_list (mk_prefixes str) in
  93     set_of_uri := SetOfStrings.add str uri !set_of_uri ;
  94     uri
  95 ;;
  96
  97 let cicuri_of_uri uri =
  98  let completeuri = string_of_uri uri in
  99   let newcompleteuri =
 100    (Str.replace_first (Str.regexp "\.types$") ""
 101     (Str.replace_first (Str.regexp "\.ann$") "" completeuri))
 102   in
 103    if completeuri = newcompleteuri then
 104     uri
 105    else
 106     let newuri = Array.copy uri in
 107      newuri.(Array.length uri - 2) <- newcompleteuri ;
 108      newuri
 109 ;;
 110
 111 let annuri_of_uri uri =
 112  let completeuri = string_of_uri uri in
 113   if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then
 114    uri
 115   else
 116    let newuri = Array.copy uri in
 117     newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ;
 118     newuri
 119 ;;
 120
 121 let uri_is_annuri uri =
 122  Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0
 123 ;;
 124
 125 let bodyuri_of_uri uri =
 126  let struri = string_of_uri uri in
 127   if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then
 128    let newuri = Array.copy uri in
 129     newuri.(Array.length uri - 2) <- struri ^ ".body" ;
 130     Some newuri
 131   else
 132    None
 133 ;;
 134
 135 let innertypesuri_of_uri uri =
 136  let cicuri = cicuri_of_uri uri in
 137   let newuri = Array.copy cicuri in
 138    newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ;
 139    newuri
 140 ;;