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"
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 search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@"
60 (* First of all we load the configuration *)
61 let _ = Helm_registry.load_from configuration_file
62 let port = Helm_registry.get_int "search_engine.port"
63 let pages_dir = Helm_registry.get "search_engine.html_dir"
65 let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
66 let moogle_TPL = pages_dir ^ "/moogle.html"
69 let ic = Unix.open_process_in "hostname -f" in
70 let hostname = input_line ic in
71 ignore (Unix.close_process_in ic);
72 sprintf "http://%s:%d" hostname port
74 let bad_request body outchan =
75 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
78 (** chain application of Pcre substitutions *)
79 let rec apply_substs substs line =
82 | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
83 (** fold like function on files *)
84 let fold_file f init fname =
85 let inchan = open_in fname in
86 let rec fold_lines' value =
88 let line = input_line inchan in
89 fold_lines' (f value line)
90 with End_of_file -> value
92 let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
95 (** iter like function on files *)
96 let iter_file f = fold_file (fun _ line -> f line) ()
97 let javascript_quote s =
98 let rex = Pcre.regexp "'" in
99 let rex' = Pcre.regexp "\"" in
100 Pcre.replace ~rex ~templ:"\\'"
101 (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
103 let len = String.length s in
104 String.sub s 1 (len-1)
106 let add_param_substs params =
109 let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in
110 Pcre.regexp ("@" ^ key' ^ "@"), value)
112 (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key)
115 let send_results results
116 ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "")
117 (req: Http_types.request) outchan
119 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
120 Http_daemon.send_header "Content-Type" "text/xml" outchan;
121 Http_daemon.send_CRLF outchan ;
124 | `Results r -> MooglePp.theory_of_result req r
128 (search_engine_url_RE, my_own_url) ::
129 (results_RE, results_string) ::
130 (advanced_tag_RE, req#param "advanced") ::
131 (expression_tag_RE, req#param "expression") ::
132 add_param_substs req#params @
133 (if req#param "advanced" = "no" then
134 [ simple_checked_RE, "checked='true'";
135 advanced_checked_RE, "" ]
137 [ simple_checked_RE, "";
138 advanced_checked_RE, "checked='true'" ])
143 CicTextualParser2.EnvironmentP3.to_string id_to_uris
147 (* CSC: Bug here: this is a string, not an array! *)
148 ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst)
151 output_string outchan (processed_line ^ "\n"))
154 let exec_action dbh (req: Http_types.request) outchan =
155 let term_str = req#param "expression" in
156 let (context, metasenv) = ([], []) in
158 try req#param "aliases"
159 with Http_types.Param_not_found _ -> ""
161 let parse_interpretation_choices choices =
162 List.map int_of_string (Pcre.split ~pat:" " choices) in
163 let parse_choices choices_raw =
164 let choices = Pcre.split ~pat:";" choices_raw in
167 match Pcre.split ~pat:"\\s" x with
169 | id::tail when id<>"" ->
172 Some (List.map (fun u -> Netencoding.Url.decode u) tail)
175 | _ -> failwith "Can't parse choices")
179 let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
182 parse_choices (req#param "choices")
183 with Http_types.Param_not_found _ -> (fun _ -> None)
185 let interpretation_choices =
187 let choices_raw = req#param "interpretation_choices" in
188 if choices_raw = "" then None
189 else Some (parse_interpretation_choices choices_raw)
190 with Http_types.Param_not_found _ -> None
192 let module Chat: DisambiguateTypes.Callbacks =
194 let interactive_user_uri_choice ~selection_mode ?ok
195 ?enable_button_for_non_vars ~(title: string) ~(msg: string)
196 ~(id: string) (choices: string list)
198 match id_to_choices id with
199 | Some choices -> choices
200 | None -> assert false
202 let interactive_interpretation_choice interpretations =
203 match interpretation_choices with
206 let html_interpretations =
207 MooglePp.html_of_interpretations interpretations
209 Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
210 Http_daemon.send_CRLF outchan ;
215 [advanced_tag_RE, req#param "advanced";
216 interpretations_RE, html_interpretations;
217 current_choices_tag_RE, req#param "choices";
218 expression_tag_RE, req#param "expression";
219 action_tag_RE, string_tail req#path ]
222 output_string outchan (processed_line ^ "\n"))
223 interactive_interpretation_choice_TPL;
224 raise Chat_unfinished
226 let input_or_locate_uri ~title ?id () =
228 | Some id -> raise (Unbound_identifier id)
229 | None -> assert false
232 let module Disambiguate' = Disambiguate.Make(Chat) in
233 let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
234 let (id_to_uris, metasenv, term) =
236 Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
238 | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
243 | "/match" -> MetadataQuery.match_term ~dbh term
245 let status = ProofEngineTypes.initial_status term metasenv in
246 let intros = PrimitiveTactics.intros_tac () in
247 let subgoals = ProofEngineTypes.apply_tactic intros status in
250 let (uri,metasenv,bo,ty) = proof in
251 List.map fst (MetadataQuery.hint ~dbh (proof, goal))
256 | Cic.MutInd (uri, typeno, _) ->
257 UriManager.string_of_uriref (uri, [typeno])
260 MetadataQuery.elim ~dbh uri
263 send_results ~id_to_uris (`Results uris) req outchan
265 let callback dbh (req: Http_types.request) outchan =
267 debug_print (sprintf "Received request: %s" req#path);
270 (* TODO implement "is_permitted" *)
271 (let is_permitted _ = true in
272 let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
273 let page = remove_fragment (req#param "url") in
276 bool_of_string (req#param "preprocess")
277 with Invalid_argument _ | Http_types.Param_not_found _ -> false)
280 | page when is_permitted page ->
281 (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
282 Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
283 Http_daemon.send_header "Content-Type" "text/html" outchan;
284 Http_daemon.send_CRLF outchan;
285 if preprocess then begin
288 output_string outchan
290 ((search_engine_url_RE, my_own_url) ::
291 (advanced_tag_RE, "no") ::
293 add_param_substs req#params)
298 Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan)
299 | page -> Http_daemon.respond_forbidden ~url:page outchan))
300 | "/help" -> Http_daemon.respond ~body:daemon_name outchan
302 let initial_expression =
303 try req#param "expression" with Http_types.Param_not_found _ -> ""
306 Pcre.replace ~pat:"\\s*$"
307 (Pcre.replace ~pat:"^\\s*" initial_expression)
309 if expression = "" then
310 send_results (`Results []) req outchan
312 let results = MetadataQuery.locate ~dbh expression in
313 send_results (`Results results) req outchan
316 | "/match" -> exec_action dbh req outchan
318 Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
320 debug_print (sprintf "%s done!" req#path)
322 | Chat_unfinished -> ()
323 | Http_types.Param_not_found attr_name ->
324 bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
325 | CicTextualParser2.Parse_error msg ->
326 send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
327 | Unbound_identifier id ->
328 send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
331 let exn_string = Printexc.to_string exn in
332 debug_print exn_string;
333 let msg = MooglePp.pp_error "Uncaught exception" exn_string in
334 send_results (`Error msg) req outchan
337 printf "%s started and listening on port %d\n" daemon_name port;
338 printf "Current directory is %s\n" (Sys.getcwd ());
339 printf "HTML directory is %s\n" pages_dir;
341 Unix.putenv "http_proxy" "";
343 new DB.connection ~host:(Helm_registry.get "db.host")
344 ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
346 Http_daemon.start' ~port (callback dbh);
347 printf "%s is terminating, bye!\n" daemon_name