Initial revision

[helm.git] / helm / interface / getter.ml

diff --git a/helm/interface/getter.ml b/helm/interface/getter.ml
new file mode 100644 (file)
index 0000000..21c1901
--- /dev/null
+++ b/helm/interface/getter.ml
@@ -0,0 +1,143 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 24/01/2000                                 *)
+(*                                                                            *)
+(******************************************************************************)
+
+exception ErrorGetting of string;;
+
+module OrderedStrings =
+ struct
+  type t = string
+  let compare (s1 : t) (s2 : t) = compare s1 s2
+ end
+;;
+
+module MapOfStrings = Map.Make(OrderedStrings);;
+
+let read_index url =
+ let module C = Configuration in
+  if Sys.command ("wget -c -P " ^ C.tmpdir ^ " " ^ url ^ "/\"" ^
+   C.indexname ^ "\"") <> 0
+  then
+   raise (ErrorGetting url) ;
+  let tmpfilename = C.tmpdir ^ "/" ^ C.indexname in
+   let fd = open_in tmpfilename in
+   let uris = ref [] in
+    try
+     while true do
+      uris := (input_line fd) :: !uris
+     done ;
+     [] (* only to make the compiler happy *)
+    with
+     End_of_file ->
+      Sys.remove tmpfilename ;
+      !uris
+;;
+
+(* mk_urls_of_uris list_of_servers_base_urls *)
+let rec mk_urls_of_uris =
+ function
+    [] -> MapOfStrings.empty
+  | he::tl ->
+     let map = mk_urls_of_uris tl in
+      let uris = read_index he in
+       let url_of_uri uri =
+        let url = uri  ^ ".xml" in
+         let url' = Str.replace_first (Str.regexp "cic:") he url in
+         let url'' = Str.replace_first (Str.regexp "theory:") he url' in
+          url''
+       in
+        List.fold_right
+         (fun uri m -> MapOfStrings.add uri (url_of_uri uri) m)
+         uris map
+;;
+
+let update () =
+ let module C = Configuration in
+  let fd = open_in C.servers_file in
+  let servers = ref [] in
+   try
+    while true do
+     servers := (input_line fd) :: !servers
+    done
+   with
+    End_of_file ->
+     let urls_of_uris = mk_urls_of_uris (List.rev !servers) in
+      (try Sys.remove (C.uris_dbm ^ ".db") with _ -> ()) ;
+      let dbm =
+       Dbm.opendbm C.uris_dbm [Dbm.Dbm_wronly ; Dbm.Dbm_create] 0o660
+      in
+       MapOfStrings.iter (fun uri url -> Dbm.add dbm uri url) urls_of_uris ;
+       Dbm.close dbm
+;;
+
+(* url_of_uri : uri -> url *)
+let url_of_uri uri =
+ let dbm = Dbm.opendbm Configuration.uris_dbm [Dbm.Dbm_rdonly] 0o660 in
+  let url = Dbm.find dbm (UriManager.string_of_uri uri) in
+   Dbm.close dbm ;
+   url
+;;
+
+let filedir_of_uri uri =
+ let fn = UriManager.buri_of_uri uri in
+  let fn' = Str.replace_first (Str.regexp ".*:") Configuration.dest fn in
+   fn'
+;;
+
+let name_and_ext_of_uri uri =
+ let str = UriManager.string_of_uri uri in
+  Str.replace_first (Str.regexp ".*/") "" str
+;;
+
+(* get_file : uri -> filename *)
+let get_file uri =
+ let dir = filedir_of_uri uri in
+  let fn = dir ^ "/" ^ name_and_ext_of_uri uri ^ ".xml" in
+   if not (Sys.file_exists fn) then
+    begin
+     let url = url_of_uri uri in
+      (*CSC: use -q for quiet mode *)
+      if Sys.command ("wget -c -P " ^ dir ^ " \"" ^ url ^"\"") <> 0
+      then
+       raise (ErrorGetting url) ;
+    end ;
+   fn
+;;
+
+(* get : uri -> filename *)
+(* If uri is the URI of an annotation, the annotated object is processed *)
+let get uri =
+ let module U = UriManager in
+  get_file
+   (U.uri_of_string
+    (Str.replace_first (Str.regexp "\.ann$") ""
+     (Str.replace_first (Str.regexp "\.types$") "" (U.string_of_uri uri))))
+;;
+
+(* get_ann : uri -> filename *)
+(* If uri is the URI of an annotation, the annotation file is processed *)
+let get_ann = get_file;;
+
+(* get_ann_file_name_and_uri : uri -> filename * annuri *)
+(* If given an URI, it returns the name of the corresponding *)
+(* annotation file and the annotation uri                    *)
+let get_ann_file_name_and_uri uri = 
+ let module U = UriManager in
+  let uri = U.string_of_uri uri in
+   let annuri =
+    U.uri_of_string (
+     if Str.string_match (Str.regexp ".*\.ann$") uri 0 then
+      uri
+     else
+      uri ^ ".ann"
+    )
+   in
+    let dir = filedir_of_uri annuri in
+     let fn = dir ^ "/" ^ name_and_ext_of_uri annuri ^ ".xml" in
+      (fn, annuri)
+;;