1 (* Copyright (C) 2002-2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
31 let debug_print s = if debug then prerr_endline s
32 let _ = Http_common.debug := false
34 exception Chat_unfinished
35 exception Unbound_identifier of string
36 exception Invalid_action of string (* invalid action for "/search" method *)
38 let daemon_name = "Moogle"
39 let configuration_file = "/projects/helm/etc/moogle.conf.xml"
40 (*let configuration_file = "searchEngine.conf.xml" *)
43 "EXPRESSION"; "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "SIMPLE_CHECKED";
44 "TITLE"; "NO_CHOICES"; "CURRENT_CHOICES"; "CHOICES"; "MSG"; "ID_TO_URIS";
45 "ID"; "IDEN"; "INTERPRETATIONS"; "INTERPRETATIONS_LABELS"; "RESULTS";
46 "NEW_ALIASES"; "SEARCH_ENGINE_URL"; "PREV_LINK"; "PAGE"; "PAGES"; "NEXT_LINK"
50 let regexps = Hashtbl.create 25 in
52 (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag)))
56 (* First of all we load the configuration *)
57 let _ = Helm_registry.load_from configuration_file
58 let port = Helm_registry.get_int "search_engine.port"
59 let pages_dir = Helm_registry.get "search_engine.html_dir"
61 let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
62 let moogle_TPL = pages_dir ^ "/moogle.html"
65 let ic = Unix.open_process_in "hostname -f" in
66 let hostname = input_line ic in
67 ignore (Unix.close_process_in ic);
68 sprintf "http://%s:%d" hostname port
69 let _ = Helm_registry.set "search_engine.my_own_url" my_own_url
71 let bad_request body outchan =
72 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
75 (** chain application of Pcre substitutions *)
76 let rec apply_substs substs line =
79 | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
80 (** fold like function on files *)
81 let fold_file f init fname =
82 let inchan = open_in fname in
83 let rec fold_lines' value =
85 let line = input_line inchan in
86 fold_lines' (f value line)
87 with End_of_file -> value
89 let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
92 (** iter like function on files *)
93 let iter_file f = fold_file (fun _ line -> f line) ()
94 let javascript_quote s =
95 let rex = Pcre.regexp "'" in
96 let rex' = Pcre.regexp "\"" in
97 Pcre.replace ~rex ~templ:"\\'"
98 (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
100 let len = String.length s in
101 String.sub s 1 (len-1)
103 let len = String.length s in
104 let suffix = String.sub s (len-4) 4 in
105 not (suffix = ".var")
107 let add_param_substs params =
110 let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in
111 Pcre.regexp ("@" ^ key' ^ "@"), value)
113 (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key)
116 let page_RE = Pcre.regexp "¶m\\.page=\\d+"
118 let send_results results
119 ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "")
120 (req: Http_types.request) outchan
122 let page_link anchor page =
124 let this = req#param "this" in
126 if Pcre.pmatch ~rex:page_RE this then
127 Pcre.replace ~rex:page_RE ~templ:(sprintf "¶m.page=%d" page)
130 sprintf "%s¶m.page=%d" this page
132 let target = Pcre.replace ~pat:"&" ~templ:"&" target in
133 sprintf "<a href=\"%s\">%s</a>" target anchor
134 with Http_types.Param_not_found _ -> ""
136 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
137 Http_daemon.send_header "Content-Type" "text/xml" outchan;
138 Http_daemon.send_CRLF outchan ;
139 let subst, results_string =
141 | `Results results ->
142 let page = try int_of_string (req#param "page") with _ -> 1 in
143 let results_no = List.length results in
144 let results_per_page =
145 Helm_registry.get_int "search_engine.results_per_page"
148 if results_no mod results_per_page = 0 then
149 results_no / results_per_page
151 results_no / results_per_page + 1
153 ([ tag "PAGE", string_of_int page; tag "PAGES", string_of_int pages ] @
155 if page > 1 then page_link "Prev" (page-1) else "" ] @
157 if page < pages then page_link "Next" (page+1) else "" ]),
158 MooglePp.theory_of_result req page results
160 [ tag "PAGE", ""; tag "PAGES", "";
161 tag "PREV_LINK", ""; tag "NEXT_LINK", "" ],
165 (tag "SEARCH_ENGINE_URL", my_own_url) ::
166 (tag "RESULTS", results_string) ::
167 (tag "ADVANCED", req#param "advanced") ::
168 (tag "EXPRESSION", req#param "expression") ::
169 add_param_substs req#params @
170 (if req#param "advanced" = "no" then
171 [ tag "SIMPLE_CHECKED", "checked='true'";
172 tag "ADVANCED_CHECKED", "" ]
174 [ tag "SIMPLE_CHECKED", "";
175 tag "ADVANCED_CHECKED", "checked='true'" ]) @
181 CicTextualParser2.EnvironmentP3.to_string id_to_uris
185 (* CSC: Bug here: this is a string, not an array! *)
186 ((tag "NEW_ALIASES", "'" ^ javascript_quote new_aliases ^ "'") ::
190 output_string outchan (processed_line ^ "\n"))
193 let exec_action dbd (req: Http_types.request) outchan =
194 let term_str = req#param "expression" in
195 let (context, metasenv) = ([], []) in
197 try req#param "aliases"
198 with Http_types.Param_not_found _ -> ""
200 let parse_interpretation_choices choices =
201 List.map int_of_string (Pcre.split ~pat:" " choices) in
202 let parse_choices choices_raw =
203 let choices = Pcre.split ~pat:";" choices_raw in
206 match Pcre.split ~pat:"\\s" x with
208 | id::tail when id<>"" ->
211 Some (List.map (fun u -> Netencoding.Url.decode u) tail)
214 | _ -> failwith "Can't parse choices")
218 let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
221 parse_choices (req#param "choices")
222 with Http_types.Param_not_found _ -> (fun _ -> None)
224 let interpretation_choices =
226 let choices_raw = req#param "interpretation_choices" in
227 if choices_raw = "" then None
228 else Some (parse_interpretation_choices choices_raw)
229 with Http_types.Param_not_found _ -> None
231 let module Chat: DisambiguateTypes.Callbacks =
233 let interactive_user_uri_choice ~selection_mode ?ok
234 ?enable_button_for_non_vars ~(title: string) ~(msg: string)
235 ~(id: string) (choices: string list)
237 match id_to_choices id with
238 | Some choices -> choices
239 | None -> List.filter nonvar choices
241 let interactive_interpretation_choice interpretations =
242 match interpretation_choices with
245 let html_interpretations =
246 MooglePp.html_of_interpretations interpretations
248 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
249 Http_daemon.send_CRLF outchan ;
254 [tag "ADVANCED", req#param "advanced";
255 tag "INTERPRETATIONS", html_interpretations;
256 tag "CURRENT_CHOICES", req#param "choices";
257 tag "EXPRESSION", req#param "expression";
258 tag "ACTION", string_tail req#path ]
261 output_string outchan (processed_line ^ "\n"))
262 interactive_interpretation_choice_TPL;
263 raise Chat_unfinished
265 let input_or_locate_uri ~title ?id () =
267 | Some id -> raise (Unbound_identifier id)
268 | None -> assert false
271 let module Disambiguate' = Disambiguate.Make(Chat) in
272 let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
273 let (id_to_uris, metasenv, term) =
275 Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
277 | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
282 | "/match" -> MetadataQuery.match_term ~dbd term
284 let status = ProofEngineTypes.initial_status term metasenv in
285 let intros = PrimitiveTactics.intros_tac () in
286 let subgoals = ProofEngineTypes.apply_tactic intros status in
289 let (uri,metasenv,bo,ty) = proof in
290 List.map fst (MetadataQuery.hint ~dbd (proof, goal))
295 | Cic.MutInd (uri, typeno, _) ->
296 UriManager.string_of_uriref (uri, [typeno])
299 MetadataQuery.elim ~dbd uri
302 send_results ~id_to_uris (`Results uris) req outchan
304 let callback dbd (req: Http_types.request) outchan =
306 debug_print (sprintf "Received request: %s" req#path);
309 (* TODO implement "is_permitted" *)
310 (let is_permitted _ = true in
311 let page = req#param "url" in
314 bool_of_string (req#param "preprocess")
315 with Invalid_argument _ | Http_types.Param_not_found _ -> false)
318 | page when is_permitted page ->
319 (let fname = sprintf "%s/%s" pages_dir page in
320 Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
321 Http_daemon.send_header "Content-Type" "text/html" outchan;
322 Http_daemon.send_CRLF outchan;
323 if preprocess then begin
326 output_string outchan
328 ((tag "SEARCH_ENGINE_URL", my_own_url) ::
329 (tag "ADVANCED", "no") ::
330 (tag "RESULTS", "") ::
331 add_param_substs req#params)
336 Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan)
337 | page -> Http_daemon.respond_forbidden ~url:page outchan))
338 | "/help" -> Http_daemon.respond ~body:daemon_name outchan
340 let initial_expression =
341 try req#param "expression" with Http_types.Param_not_found _ -> ""
344 Pcre.replace ~pat:"\\s*$"
345 (Pcre.replace ~pat:"^\\s*" initial_expression)
347 if expression = "" then
348 send_results (`Results []) req outchan
350 let results = MetadataQuery.locate ~dbd expression in
351 send_results (`Results results) req outchan
354 | "/match" -> exec_action dbd req outchan
356 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
358 debug_print (sprintf "%s done!" req#path)
360 | Chat_unfinished -> ()
361 | Http_types.Param_not_found attr_name ->
362 bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
363 | CicTextualParser2.Parse_error (_, msg) ->
364 send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
365 | Unbound_identifier id ->
366 send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
369 let exn_string = Printexc.to_string exn in
370 debug_print exn_string;
371 let msg = MooglePp.pp_error "Uncaught exception" exn_string in
372 send_results (`Error msg) req outchan
375 printf "%s started and listening on port %d\n" daemon_name port;
376 printf "Current directory is %s\n" (Sys.getcwd ());
377 printf "HTML directory is %s\n" pages_dir;
379 Unix.putenv "http_proxy" "";
382 ~host:(Helm_registry.get "db.host")
383 ~database:(Helm_registry.get "db.database")
384 ~user:(Helm_registry.get "db.user")
387 Http_daemon.start' ~port (callback dbd);
388 printf "%s is terminating, bye!\n" daemon_name