X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Furimanager%2FuriManager.ml;fp=helm%2Focaml%2Furimanager%2FuriManager.ml;h=0000000000000000000000000000000000000000;hp=6dad8ddef6c4095e4764497f21150d53c4e649e2;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml deleted file mode 100644 index 6dad8ddef..000000000 --- a/helm/ocaml/urimanager/uriManager.ml +++ /dev/null @@ -1,140 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(* "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;; - -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) = - (try (List.hd tokens, List.tl tokens) - with Failure "hd" | Failure "tl" -> - raise (IllFormedUri str)) - 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 -;; - -let cicuri_of_uri uri = - let completeuri = string_of_uri uri in - let newcompleteuri = - (Str.replace_first (Str.regexp "\.types$") "" - (Str.replace_first (Str.regexp "\.ann$") "" completeuri)) - in - if completeuri = newcompleteuri then - uri - else - let newuri = Array.copy uri in - newuri.(Array.length uri - 2) <- newcompleteuri ; - newuri -;; - -let annuri_of_uri uri = - let completeuri = string_of_uri uri in - if Str.string_match (Str.regexp ".*\.ann$") completeuri 0 then - uri - else - let newuri = Array.copy uri in - newuri.(Array.length uri - 2) <- completeuri ^ ".ann" ; - newuri -;; - -let uri_is_annuri uri = - Str.string_match (Str.regexp ".*\.ann$") (string_of_uri uri) 0 -;; - -let bodyuri_of_uri uri = - let struri = string_of_uri uri in - if Str.string_match (Str.regexp ".*\.con$") (string_of_uri uri) 0 then - let newuri = Array.copy uri in - newuri.(Array.length uri - 2) <- struri ^ ".body" ; - Some newuri - else - None -;; - -let innertypesuri_of_uri uri = - let cicuri = cicuri_of_uri uri in - let newuri = Array.copy cicuri in - newuri.(Array.length cicuri - 2) <- (string_of_uri cicuri) ^ ".types" ; - newuri -;;