]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/getter/http_getter_cache.ml
coercion application
[helm.git] / helm / ocaml / getter / http_getter_cache.ml
1 (*
2  * Copyright (C) 2003-2004:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
6  *  This file is part of HELM, an Hypertextual, Electronic
7  *  Library of Mathematics, developed at the Computer Science
8  *  Department, University of Bologna, Italy.
9  *
10  *  HELM is free software; you can redistribute it and/or
11  *  modify it under the terms of the GNU General Public License
12  *  as published by the Free Software Foundation; either version 2
13  *  of the License, or (at your option) any later version.
14  *
15  *  HELM is distributed in the hope that it will be useful,
16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18  *  GNU General Public License for more details.
19  *
20  *  You should have received a copy of the GNU General Public License
21  *  along with HELM; if not, write to the Free Software
22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 (* TODO cache expires control!!! *)
30 (* TODO uwobo loop:
31     if two large proof (already in cache) are requested at the same time by two
32     clients, uwobo (java implementation, not yet tested with the OCaml one)
33     starts looping sending output to one of the client *)
34
35 open Http_getter_common
36 open Http_getter_misc
37 open Http_getter_types
38 open Printf
39
40   (* expose ThreadSafe.threadSafe methods *)
41 class threadSafe =
42   object
43     inherit ThreadSafe.threadSafe
44     method virtual doCritical : 'a. 'a lazy_t -> 'a
45     method virtual doReader : 'a. 'a lazy_t -> 'a
46     method virtual doWriter : 'a. 'a lazy_t -> 'a
47   end
48
49 let threadSafe = new threadSafe
50
51 let finally cleanup f =
52   try
53     let res = Lazy.force f in
54     cleanup ();
55     res
56   with e ->
57     cleanup ();
58     raise (Http_getter_types.Cache_failure (Printexc.to_string e))
59
60 let resource_type_of_url = function
61   | url when Pcre.pmatch ~pat:"\\.xml\\.gz$" url -> `Gzipped
62   | url when Pcre.pmatch ~pat:"\\.xml$" url -> `Normal
63   | url -> raise (Invalid_URL url)
64
65 let extension_of_resource_type = function
66   | `Normal -> "xml"
67   | `Gzipped -> "xml.gz"
68
69   (* basename = resource name without trailing ".gz", if any *)
70 let is_in_cache basename =
71   Sys.file_exists
72     (match Lazy.force Http_getter_env.cache_mode with
73     | `Normal -> basename
74     | `Gzipped -> basename ^ ".gz")
75
76 let respond_xml
77   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url ~uri outchan
78   =
79   let resource_type = resource_type_of_url url in
80   let extension = extension_of_resource_type resource_type in
81   let downloadname =
82     match uri_of_string uri with  (* parse uri *)
83     | Cic_uri (Cic baseuri) | Cic_uri (Theory baseuri) ->
84           (* assumption: baseuri starts with "/" *)
85         sprintf "%s%s.%s" (Lazy.force Http_getter_env.cic_dir) baseuri extension
86     | Nuprl_uri baseuri ->
87           (* assumption: baseuri starts with "/" *)
88         sprintf "%s%s.%s" (Lazy.force Http_getter_env.nuprl_dir) baseuri
89           extension
90     | Rdf_uri (prefix, ((Cic baseuri) as qbaseuri))
91     | Rdf_uri (prefix, ((Theory baseuri) as qbaseuri)) ->
92         let escaped_prefix =
93           (Pcre.replace ~pat:"/" ~templ:"_"
94             (Pcre.replace ~pat:"_" ~templ:"__"
95               (prefix ^
96               (match qbaseuri with
97               | Cic _ -> "//cic:"
98               | Theory _ -> "//theory:"))))
99         in
100         sprintf "%s/%s%s.%s"
101           (Lazy.force Http_getter_env.rdf_dir) escaped_prefix baseuri extension
102   in
103   let patch_fun =
104     let xmlbases =
105      if Http_getter_common.is_theory_uri uri then
106       Some (Filename.dirname uri, Filename.dirname url)
107      else
108       None
109     in
110      if patch then
111        Http_getter_common.patch_xml ?xmlbases ~via_http ()
112      else
113        (fun x -> x)
114   in
115   let basename = Pcre.replace ~pat:"\\.gz$" downloadname in
116   let contype = "text/xml" in
117     (* Fill cache if needed and return a short circuit file.
118       Short circuit is needed in situations like:
119         resource type = normal, cache type = gzipped, required encoding = normal
120       we would like to avoid normal -> gzipped -> normal conversions. To avoid
121       this tmp_short_circuit is used to remember the name of the intermediate
122       file name *)
123   let fill_cache () =
124     threadSafe#doWriter (lazy(
125       if not (is_in_cache basename) then begin  (* cache MISS *)
126         Http_getter_logger.log ~level:2 "Cache MISS :-(";
127         mkdir ~parents:true (Filename.dirname downloadname);
128         match (resource_type, Lazy.force Http_getter_env.cache_mode) with
129         | `Normal, `Normal | `Gzipped, `Gzipped ->
130             wget ~output:downloadname url;
131             None
132         | `Normal, `Gzipped ->  (* resource normal, cache gzipped *)
133             let tmp = tempfile () in
134             let (res, cleanup) =
135               if enc = `Normal then (* user wants normal: don't delete it! *)
136                 (Some (tmp, enc), (fun () -> ()))
137               else
138                 (None, (fun () -> Sys.remove tmp))
139             in
140             finally cleanup (lazy (
141               wget ~output:tmp url;
142               gzip ~output:(basename ^ ".gz") ~keep:true tmp; (* fill cache *)
143               res
144             ));
145         | `Gzipped, `Normal ->  (* resource gzipped, cache normal *)
146             let tmp = tempfile () in
147             let (res, cleanup) =
148               if enc = `Gzipped then (* user wants .gz: don't delete it! *)
149                 (Some (tmp, enc), (fun () -> ()))
150               else
151                 (None, (fun () -> Sys.remove tmp))
152             in
153             finally cleanup (lazy (
154               wget ~output:tmp url;
155               gunzip ~output:basename ~keep:true tmp; (* fill cache *)
156               res
157             ));
158       end else begin
159         Http_getter_logger.log ~level:2 "Cache HIT :-)";
160         None
161       end
162     )) in
163   let tmp_short_circuit = fill_cache () in
164   threadSafe#doReader (lazy(
165     assert (is_in_cache basename);
166     match (enc, Lazy.force Http_getter_env.cache_mode) with
167     | `Normal, `Normal | `Gzipped, `Gzipped ->
168         (* resource in cache is already in the required format *)
169         (match enc with
170         | `Normal ->
171             Http_getter_logger.log ~level:2
172               "No format mangling required (encoding = normal)";
173             return_file ~via_http ~fname:basename ~contype ~patch_fun outchan
174         | `Gzipped ->
175             Http_getter_logger.log ~level:2
176               "No format mangling required (encoding = gzipped)";
177             return_file
178               ~via_http ~fname:(basename ^ ".gz") ~contype ~contenc:"x-gzip"
179               ~patch_fun ~gunzip:true
180               outchan)
181     | `Normal, `Gzipped | `Gzipped, `Normal ->
182         (match tmp_short_circuit with
183         | None -> (* no short circuit possible, use cache *)
184           Http_getter_logger.log ~level:2
185             "No short circuit available, use cache";
186           let tmp = tempfile () in
187           finally (fun () -> Sys.remove tmp) (lazy (
188             (match enc with
189             | `Normal ->
190               (* required format is normal, cached version is gzipped *)
191               gunzip  (* gunzip to tmp *)
192                 ~output:tmp ~keep:true (basename ^ ".gz");
193               return_file ~via_http ~fname:tmp ~contype ~patch_fun outchan;
194             | `Gzipped ->
195               (* required format is gzipped, cached version is normal *)
196               gzip ~output:tmp ~keep:true basename;  (* gzip to tmp *)
197               return_file
198                 ~via_http ~fname:tmp ~contype ~contenc:"x-gzip"
199                 ~patch_fun ~gunzip:true
200                 outchan)
201           ))
202         | Some (fname, `Normal) ->  (* short circuit available, use it! *)
203             Http_getter_logger.log ~level:2
204               "Using short circuit (encoding = normal)";
205             finally (fun () -> Sys.remove fname) (lazy (
206               return_file ~via_http ~fname ~contype ~patch_fun outchan
207             ))
208         | Some (fname, `Gzipped) -> (* short circuit available, use it! *)
209             Http_getter_logger.log ~level:2
210               "Using short circuit (encoding = gzipped)";
211             finally (fun () -> Sys.remove fname) (lazy (
212               return_file ~via_http ~fname ~contype ~contenc:"x-gzip" ~patch_fun
213                 ~gunzip:true outchan
214             )))
215   ))
216
217   (* TODO enc is not yet supported *)
218 let respond_xsl
219   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url outchan
220   =
221   let patch_fun =
222     if patch then Http_getter_common.patch_xsl ~via_http () else (fun x -> x)
223   in
224   let fname = tempfile () in
225   finally (fun () -> Sys.remove fname) (lazy (
226     wget ~output:fname url;
227     return_file ~via_http ~fname ~contype:"text/xml" ~patch_fun outchan
228   ))
229
230   (* TODO enc is not yet supported *)
231 let respond_dtd
232   ?(via_http = true) ?(enc = `Normal) ?(patch = true) ~url outchan
233   =
234   let patch_fun =
235     if patch then Http_getter_common.patch_dtd ~via_http () else (fun x -> x)
236   in
237   if Sys.file_exists url then
238     (* TODO check this: old getter here used text/xml *)
239     return_file ~via_http ~fname:url ~contype:"text/plain" ~patch_fun outchan
240   else
241     raise (Dtd_not_found url)
242
243 let clean () =
244  let module E = Http_getter_env in
245   List.iter
246    (function dir -> ignore (Unix.system ("rm -rf " ^ dir ^ "/*")))
247    [ Lazy.force E.cic_dir; Lazy.force E.nuprl_dir; Lazy.force E.rdf_dir ]
248