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 = "searchEngine.conf.xml"
41 let expression_tag_RE = Pcre.regexp "@EXPRESSION@"
42 let action_tag_RE = Pcre.regexp "@ACTION@"
43 let advanced_tag_RE = Pcre.regexp "@ADVANCED@"
44 let advanced_checked_RE = Pcre.regexp "@ADVANCED_CHECKED@"
45 let simple_checked_RE = Pcre.regexp "@SIMPLE_CHECKED@"
46 let title_tag_RE = Pcre.regexp "@TITLE@"
47 let no_choices_tag_RE = Pcre.regexp "@NO_CHOICES@"
48 let current_choices_tag_RE = Pcre.regexp "@CURRENT_CHOICES@"
49 let choices_tag_RE = Pcre.regexp "@CHOICES@"
50 let msg_tag_RE = Pcre.regexp "@MSG@"
51 let id_to_uris_RE = Pcre.regexp "@ID_TO_URIS@"
52 let id_RE = Pcre.regexp "@ID@"
53 let iden_tag_RE = Pcre.regexp "@IDEN@"
54 let interpretations_RE = Pcre.regexp "@INTERPRETATIONS@"
55 let interpretations_labels_RE = Pcre.regexp "@INTERPRETATIONS_LABELS@"
56 let results_RE = Pcre.regexp "@RESULTS@"
57 let new_aliases_RE = Pcre.regexp "@NEW_ALIASES@"
58 let form_RE = Pcre.regexp "@FORM@"
59 let variables_initialization_RE = Pcre.regexp "@VARIABLES_INITIALIZATION@"
60 let search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@"
61 let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
63 (* First of all we load the configuration *)
64 let _ = Helm_registry.load_from configuration_file
65 let port = Helm_registry.get_int "search_engine.port"
66 let pages_dir = Helm_registry.get "search_engine.html_dir"
68 let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
69 let moogle_TPL = pages_dir ^ "/moogle.html"
72 let ic = Unix.open_process_in "hostname -f" in
73 let hostname = input_line ic in
74 ignore (Unix.close_process_in ic);
75 sprintf "http://%s:%d" hostname port
77 let bad_request body outchan =
78 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
81 (** chain application of Pcre substitutions *)
82 let rec apply_substs substs line =
85 | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
86 (** fold like function on files *)
87 let fold_file f init fname =
88 let inchan = open_in fname in
89 let rec fold_lines' value =
91 let line = input_line inchan in
92 fold_lines' (f value line)
93 with End_of_file -> value
95 let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
98 (** iter like function on files *)
99 let iter_file f = fold_file (fun _ line -> f line) ()
100 let javascript_quote s =
101 let rex = Pcre.regexp "'" in
102 let rex' = Pcre.regexp "\"" in
103 Pcre.replace ~rex ~templ:"\\'"
104 (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
106 let len = String.length s in
107 String.sub s 1 (len-1)
109 let add_param_substs params =
112 let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in
113 Pcre.regexp ("@" ^ key' ^ "@"), value)
115 (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key)
118 let send_results results
119 ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "")
120 (req: Http_types.request) outchan
122 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
123 Http_daemon.send_header "Content-Type" "text/xml" outchan;
124 Http_daemon.send_CRLF outchan ;
127 | `Results r -> MooglePp.theory_of_result req r
131 (search_engine_url_RE, my_own_url) ::
132 (results_RE, results_string)::
133 (advanced_tag_RE, req#param "advanced")::
134 (expression_tag_RE, req#param "expression")::
135 add_param_substs req#params @
136 (if req#param "advanced" = "no" then
137 [ simple_checked_RE, "checked='true'";
138 advanced_checked_RE, "" ]
140 [ simple_checked_RE, "";
141 advanced_checked_RE, "checked='true'" ])
146 CicTextualParser2.EnvironmentP3.to_string id_to_uris
150 (* CSC: Bug here: this is a string, not an array! *)
151 ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst)
154 output_string outchan (processed_line ^ "\n"))
157 let exec_action dbh (req: Http_types.request) outchan =
158 let term_str = req#param "expression" in
159 let (context, metasenv) = ([], []) in
161 try req#param "aliases"
162 with Http_types.Param_not_found _ -> ""
164 let parse_interpretation_choices choices =
165 List.map int_of_string (Pcre.split ~pat:" " choices) in
166 let parse_choices choices_raw =
167 let choices = Pcre.split ~pat:";" choices_raw in
170 match Pcre.split ~pat:"\\s" x with
172 | id::tail when id<>"" ->
175 Some (List.map (fun u -> Netencoding.Url.decode u) tail)
178 | _ -> failwith "Can't parse choices")
182 let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
185 parse_choices (req#param "choices")
186 with Http_types.Param_not_found _ -> (fun _ -> None)
188 let interpretation_choices =
190 let choices_raw = req#param "interpretation_choices" in
191 if choices_raw = "" then None
192 else Some (parse_interpretation_choices choices_raw)
193 with Http_types.Param_not_found _ -> None
195 let module Chat: DisambiguateTypes.Callbacks =
197 let interactive_user_uri_choice ~selection_mode ?ok
198 ?enable_button_for_non_vars ~(title: string) ~(msg: string)
199 ~(id: string) (choices: string list)
201 match id_to_choices id with
202 | Some choices -> choices
203 | None -> assert false
205 let interactive_interpretation_choice interpretations =
206 match interpretation_choices with
207 | Some l -> prerr_endline "CARRAMBA" ; l
209 let html_interpretations =
210 MooglePp.html_of_interpretations interpretations
212 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
213 Http_daemon.send_CRLF outchan ;
218 [advanced_tag_RE, req#param "advanced";
219 interpretations_RE, html_interpretations;
220 current_choices_tag_RE, req#param "choices";
221 expression_tag_RE, req#param "expression";
222 action_tag_RE, string_tail req#path ]
225 output_string outchan (processed_line ^ "\n"))
226 interactive_interpretation_choice_TPL;
227 raise Chat_unfinished
229 let input_or_locate_uri ~title ?id () =
231 | Some id -> raise (Unbound_identifier id)
232 | None -> assert false
235 let module Disambiguate' = Disambiguate.Make(Chat) in
236 let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
237 let (id_to_uris, metasenv, term) =
239 Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
241 | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
246 | "/match" -> MetadataQuery.match_term ~dbh term
248 let status = ProofEngineTypes.initial_status term [] in
249 let intros = PrimitiveTactics.intros_tac () in
250 let subgoals = ProofEngineTypes.apply_tactic intros status in
253 let (uri,metasenv,bo,ty) = proof in
254 List.map fst (MetadataQuery.hint ~dbh (proof, goal))
259 | Cic.MutInd (uri, typeno, _) ->
260 UriManager.string_of_uriref (uri, [typeno])
263 MetadataQuery.elim ~dbh uri
266 send_results ~id_to_uris (`Results uris) req outchan
268 let callback dbh (req: Http_types.request) outchan =
270 debug_print (sprintf "Received request: %s" req#path);
273 (* TODO implement "is_permitted" *)
274 (let is_permitted _ = true in
275 let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
276 let page = remove_fragment (req#param "url") in
279 bool_of_string (req#param "preprocess")
280 with Invalid_argument _ | Http_types.Param_not_found _ -> false)
283 | page when is_permitted page ->
284 (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
285 Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
286 Http_daemon.send_header "Content-Type" "text/html" outchan;
287 Http_daemon.send_CRLF outchan;
288 if preprocess then begin
291 output_string outchan
293 ((search_engine_url_RE, my_own_url) ::
294 (advanced_tag_RE, "no") ::
296 add_param_substs req#params)
301 Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan)
302 | page -> Http_daemon.respond_forbidden ~url:page outchan))
303 | "/help" -> Http_daemon.respond ~body:daemon_name outchan
305 let initial_expression =
306 try req#param "expression" with Http_types.Param_not_found _ -> ""
309 Pcre.replace ~pat:"\\s*$"
310 (Pcre.replace ~pat:"^\\s*" initial_expression)
312 if expression = "" then
313 send_results (`Results []) req outchan
315 let results = MetadataQuery.locate ~dbh expression in
316 send_results (`Results results) req outchan
319 | "/match" -> exec_action dbh req outchan
321 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
323 debug_print (sprintf "%s done!" req#path)
325 | Http_types.Param_not_found attr_name ->
326 bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
327 | CicTextualParser2.Parse_error msg ->
328 send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
329 | Unbound_identifier id ->
330 send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
333 let exn_string = Printexc.to_string exn in
334 debug_print exn_string;
335 let msg = MooglePp.pp_error "Uncaught exception" exn_string in
336 send_results (`Error msg) req outchan
339 printf "%s started and listening on port %d\n" daemon_name port;
340 printf "Current directory is %s\n" (Sys.getcwd ());
341 printf "HTML directory is %s\n" pages_dir;
343 Unix.putenv "http_proxy" "";
345 new DB.connection ~host:(Helm_registry.get "db.host")
346 ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
348 Http_daemon.start' ~port (callback dbh);
349 printf "%s is terminating, bye!\n" daemon_name