]> matita.cs.unibo.it Git - helm.git/blob - matita/components/getter/http_getter.ml
Merge remote-tracking branch 'origin/ld-0.99.3'
[helm.git] / matita / components / getter / http_getter.ml
1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 open Http_getter_common
31 open Http_getter_misc
32 open Http_getter_types
33
34 exception Not_implemented of string
35 exception UnexpectedGetterOutput
36
37 type resolve_result =
38   | Unknown
39   | Exception of exn
40   | Resolved of string
41
42 type logger_callback = HelmLogger.html_tag -> unit
43
44 let stdout_logger tag = print_string (HelmLogger.string_of_html_tag tag)
45
46 let not_implemented s = raise (Not_implemented ("Http_getter." ^ s))
47
48 let index_line_sep_RE     = Pcre.regexp "[ \t]+"
49 let index_sep_RE          = Pcre.regexp "\r\n|\r|\n"
50 let trailing_types_RE     = Pcre.regexp "\\.types$"
51 let heading_cic_RE        = Pcre.regexp "^cic:"
52 let heading_theory_RE     = Pcre.regexp "^theory:"
53 let heading_nuprl_RE      = Pcre.regexp "^nuprl:"
54 let types_RE              = Pcre.regexp "\\.types$"
55 let types_ann_RE          = Pcre.regexp "\\.types\\.ann$"
56 let body_RE               = Pcre.regexp "\\.body$"
57 let body_ann_RE           = Pcre.regexp "\\.body\\.ann$"
58 let proof_tree_RE         = Pcre.regexp "\\.proof_tree$"
59 let proof_tree_ann_RE     = Pcre.regexp "\\.proof_tree\\.ann$"
60 let theory_RE             = Pcre.regexp "\\.theory$"
61 let basepart_RE           = Pcre.regexp
62   "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
63 let slash_RE              = Pcre.regexp "/"
64 let pipe_RE               = Pcre.regexp "\\|"
65 let til_slash_RE          = Pcre.regexp "^.*/"
66 let no_slashes_RE         = Pcre.regexp "^[^/]*$"
67 let fix_regexp_RE         = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
68 let showable_file_RE      =
69   Pcre.regexp "(\\.con|\\.ind|\\.var|\\.body|\\.types|\\.proof_tree)$"
70
71 let xml_suffix = ".xml"
72 let theory_suffix = ".theory"
73
74   (* global maps, shared by all threads *)
75
76 let ends_with_slash s =
77   try
78     s.[String.length s - 1] = '/'
79   with Invalid_argument _ -> false
80
81   (* should we use a remote getter or not *)
82 let remote () =
83   try
84     Helm_registry.get "getter.mode" = "remote"
85   with Helm_registry.Key_not_found _ -> false
86
87 let getter_url () = Helm_registry.get "getter.url"
88
89 (* Remote interface: getter methods implemented using a remote getter *)
90
91   (* <TODO> *)
92 let getxml_remote _uri = not_implemented "getxml_remote"
93 let getxslt_remote _uri = not_implemented "getxslt_remote"
94 let getdtd_remote _uri = not_implemented "getdtd_remote"
95 let clean_cache_remote () = not_implemented "clean_cache_remote"
96 let list_servers_remote () = not_implemented "list_servers_remote"
97 let add_server_remote ~logger:_ ~position:_ _name =
98   not_implemented "add_server_remote"
99 let remove_server_remote ~logger:_ _position =
100   not_implemented "remove_server_remote"
101 let getalluris_remote () = not_implemented "getalluris_remote"
102 let ls_remote _lsuri = not_implemented "ls_remote"
103 let exists_remote _uri = not_implemented "exists_remote"
104   (* </TODO> *)
105
106 let resolve_remote ~writable uri =
107   (* deliver resolve request to http_getter *)
108   let doc =
109     Http_getter_wget.get (sprintf "%sresolve?uri=%s&writable=%b" (getter_url ())
110       uri writable)
111   in
112   let res = ref Unknown in
113   let start_element tag attrs =
114     match tag with
115     | "url" ->
116         (try
117           res := Resolved (List.assoc "value" attrs)
118         with Not_found -> ())
119     | "unresolvable" -> res := Exception (Unresolvable_URI uri)
120     | "not_found" -> res := Exception (Key_not_found uri)
121     | _ -> ()
122   in
123   let callbacks = {
124     XmlPushParser.default_callbacks with
125       XmlPushParser.start_element = Some start_element
126   } in
127   let xml_parser = XmlPushParser.create_parser callbacks in
128   XmlPushParser.parse xml_parser (`String doc);
129   XmlPushParser.final xml_parser;
130   match !res with
131   | Unknown -> raise UnexpectedGetterOutput
132   | Exception e -> raise e
133   | Resolved url -> url
134
135 let deref_index_theory ~local:_ uri =
136 (*  if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *)
137  if is_theory_uri uri && Filename.basename uri = "index.theory" then
138     strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
139  else
140     uri
141
142 (* API *)
143
144 let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
145
146 let exists ~local uri =
147 (*   prerr_endline ("Http_getter.exists " ^ uri); *)
148   if remote () then
149     exists_remote uri
150   else
151    let uri = deref_index_theory ~local uri in
152     Http_getter_storage.exists ~local (uri ^ xml_suffix)
153         
154 let is_an_obj s = s <> NUri.baseuri_of_uri (NUri.uri_of_string s)
155     
156 let resolve ~local ~writable uri =
157   if remote () then
158     resolve_remote ~writable uri
159   else
160    let uri = deref_index_theory ~local uri in
161     try
162       if is_an_obj uri then
163         Http_getter_storage.resolve ~writable ~local (uri ^ xml_suffix)
164       else
165         Http_getter_storage.resolve ~writable ~local uri
166     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
167
168 let filename ~local ~writable uri =
169   if remote () then
170     raise (Key_not_found uri)
171   else
172    let uri = deref_index_theory ~local uri in
173     try
174       Http_getter_storage.resolve 
175         ~must_exists:false ~writable ~local uri
176     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
177
178 let getxml uri =
179   if remote () then getxml_remote uri
180   else begin
181     let uri' = deref_index_theory ~local:false uri in
182     (try
183       Http_getter_storage.filename ~local:false (uri' ^ xml_suffix)
184     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
185   end
186
187 let getxslt uri =
188   if remote () then getxslt_remote uri
189   else Http_getter_storage.filename ~local:false ~find:true ("xslt:/" ^ uri)
190
191 let getdtd uri =
192   if remote () then
193     getdtd_remote uri
194   else begin
195     let fname = Http_getter_env.get_dtd_dir () ^ "/" ^ uri in
196     if not (Sys.file_exists fname) then raise (Dtd_not_found uri);
197     fname
198   end
199
200 let clean_cache () =
201   if remote () then
202     clean_cache_remote ()
203   else
204     Http_getter_storage.clean_cache ()
205
206 let (++) (oldann, oldtypes, oldbody, oldtree)
207          (newann, newtypes, newbody, newtree) =
208   ((if newann   > oldann    then newann   else oldann),
209    (if newtypes > oldtypes  then newtypes else oldtypes),
210    (if newbody  > oldbody   then newbody  else oldbody),
211    (if newtree  > oldtree   then newtree  else oldtree))
212     
213 let store_obj tbl o =
214 (*   prerr_endline ("Http_getter.store_obj " ^ o); *)
215   if Pcre.pmatch ~rex:showable_file_RE o then begin
216     let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
217     let no_flags = false, No, No, No in
218     let oldflags =
219       try
220         Hashtbl.find tbl basepart
221       with Not_found -> (* no ann, no types, no body, no proof tree *)
222         no_flags
223     in
224     let newflags =
225       match o with
226       | s when Pcre.pmatch ~rex:types_RE s          -> (false, Yes, No, No)
227       | s when Pcre.pmatch ~rex:types_ann_RE s      -> (true,  Ann, No, No)
228       | s when Pcre.pmatch ~rex:body_RE s           -> (false, No, Yes, No)
229       | s when Pcre.pmatch ~rex:body_ann_RE s       -> (true,  No, Ann, No)
230       | s when Pcre.pmatch ~rex:proof_tree_RE s     -> (false, No, No, Yes)
231       | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true,  No, No, Ann)
232       | _s -> no_flags
233     in
234     Hashtbl.replace tbl basepart (oldflags ++ newflags)
235   end
236   
237 let store_dir set_ref d =
238   set_ref := StringSet.add (List.hd (Pcre.split ~rex:slash_RE d)) !set_ref
239
240 let collect_ls_items dirs_set objs_tbl =
241   let items = ref [] in
242   StringSet.iter (fun dir -> items := Ls_section dir :: !items) dirs_set;
243   Http_getter_misc.hashtbl_sorted_iter
244     (fun uri (annflag, typesflag, bodyflag, treeflag) ->
245       items :=
246         Ls_object {
247           uri = uri; ann = annflag;
248           types = typesflag; body = bodyflag; proof_tree = treeflag
249         } :: !items)
250     objs_tbl;
251   List.rev !items
252
253 let contains_object = (<>) []
254
255   (** non regexp-aware version of ls *)
256 let rec dumb_ls ~local uri_prefix =
257 (*   prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
258   if is_cic_obj_uri uri_prefix then begin
259     let dirs = ref StringSet.empty in
260     let objs = Hashtbl.create 17 in
261     List.iter
262       (fun fname ->
263         if ends_with_slash fname then
264           store_dir dirs fname
265         else
266           try
267             store_obj objs (strip_suffix ~suffix:xml_suffix fname)
268           with Invalid_argument _ -> ())
269       (Http_getter_storage.ls ~local uri_prefix);
270     collect_ls_items !dirs objs
271   end else if is_theory_uri uri_prefix then begin
272     let items = ref [] in
273     let add_theory fname =
274       items :=
275         Ls_object {
276           uri = fname; ann = false; types = No; body = No; proof_tree = No }
277         :: !items
278     in
279     let cic_uri_prefix =
280       Pcre.replace_first ~rex:heading_theory_RE ~templ:"cic:" uri_prefix
281     in
282     List.iter
283       (fun fname ->
284         if ends_with_slash fname then
285           items := Ls_section (strip_trailing_slash fname) :: !items
286         else
287           try
288             let fname = strip_suffix ~suffix:xml_suffix fname in
289             let theory_name = strip_suffix ~suffix:theory_suffix fname in
290             let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
291             if is_empty_theory ~local sub_theory then add_theory fname
292           with Invalid_argument _ -> ())
293       (Http_getter_storage.ls ~local uri_prefix);
294     (try
295       if contains_object (dumb_ls ~local cic_uri_prefix)
296         && exists ~local:false (strip_trailing_slash uri_prefix ^ theory_suffix)
297       then
298         add_theory "index.theory";
299     with Unresolvable_URI _ -> ());
300     !items
301   end else
302     raise (Invalid_URI uri_prefix)
303
304 and is_empty_theory ~local uri_prefix =
305 (*   prerr_endline ("is_empty_theory " ^ uri_prefix); *)
306   not (contains_object (dumb_ls ~local uri_prefix))
307
308   (* handle simple regular expressions of the form "...(..|..|..)..." on cic
309    * uris, not meant to be a real implementation of regexp. The only we use is
310    * "(cic|theory):/..." *)
311 let explode_ls_regexp regexp =
312   try
313     let len = String.length regexp in
314     let lparen_idx = String.index regexp '(' in
315     let rparen_idx = String.index_from regexp lparen_idx ')' in
316     let choices_str = (* substring between parens, parens excluded *)
317       String.sub regexp (lparen_idx + 1) (rparen_idx - lparen_idx - 1)
318     in
319     let choices = Pcre.split ~rex:pipe_RE choices_str in
320     let prefix = String.sub regexp 0 lparen_idx in
321     let suffix = String.sub regexp (rparen_idx + 1) (len - (rparen_idx + 1)) in
322     List.map (fun choice -> prefix ^ choice ^ suffix) choices
323   with Not_found -> [regexp]
324
325 let merge_results results =
326   let rec aux objects_acc dirs_acc = function
327     | [] -> dirs_acc @ objects_acc
328     | Ls_object _ as obj :: tl -> aux (obj :: objects_acc) dirs_acc tl
329     | Ls_section _ as dir :: tl ->
330         if List.mem dir dirs_acc then (* filters out dir duplicates *)
331           aux objects_acc dirs_acc tl
332         else
333           aux objects_acc (dir :: dirs_acc) tl
334   in
335   aux [] [] (List.concat results)
336
337 let ls ~local regexp =
338   if remote () then
339     ls_remote regexp
340   else
341     let prefixes = explode_ls_regexp regexp in
342     merge_results (List.map (dumb_ls ~local) prefixes)
343
344 let getalluris () =
345   let rec aux acc = function
346     | [] -> acc
347     | dir :: todo ->
348         let acc', todo' =
349           List.fold_left
350             (fun (acc, subdirs) result ->
351               match result with
352               | Ls_object obj -> (dir ^ obj.uri) :: acc, subdirs
353               | Ls_section sect -> acc, (dir ^ sect ^ "/") :: subdirs)
354             (acc, todo)
355             (dumb_ls ~local:false dir)
356         in
357         aux acc' todo'
358   in
359   aux [] ["cic:/"] (* trailing slash required *)
360
361 (* Shorthands from now on *)
362
363 let getxml' uri = getxml (NUri.string_of_uri uri)
364 let resolve' ~local ~writable uri =
365   resolve ~local ~writable (NUri.string_of_uri uri)
366 ;;
367 let exists' ~local uri = exists ~local (NUri.string_of_uri uri)
368 let filename' ~local ~writable uri =
369   filename ~local ~writable (NUri.string_of_uri uri)
370 ;;
371
372 let tilde_expand_key k =
373   try
374     Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
375   with Helm_registry.Key_not_found _ -> ()
376
377 let init () =
378   List.iter tilde_expand_key ["getter.cache_dir"; "getter.dtd_dir"];
379   Http_getter_logger.set_log_level
380     (Helm_registry.get_opt_default Helm_registry.int ~default:1
381       "getter.log_level");
382   Http_getter_logger.set_log_file
383     (Helm_registry.get_opt Helm_registry.string "getter.log_file")
384