X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=97e91ebe5d942845d7ce1dc339e91b15983d46ec;hb=c7880fc29b14ac9cb13b305b24466bd4f3826f82;hp=4a5c2e1b5df82414056e8dabc71042c0f7988807;hpb=01a159421d87064d2e5397bfc90630a671e7824a;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 4a5c2e1b5..97e91ebe5 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -41,27 +41,39 @@ let daemon_name = "Search Engine";; (* First of all we load the configuration *) let _ = - let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in + let configuration_file = "searchEngine.conf.xml" in Helm_registry.load_from configuration_file ;; +let port = Helm_registry.get_int "search_engine.port";; + let pages_dir = Helm_registry.get "search_engine.html_dir";; (** accepted HTTP servers for ask_uwobo method forwarding *) let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers";; - let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";; let interactive_interpretation_choice_TPL = pages_dir ^ "/templateambigpdq2.html";; let constraints_choice_TPL = pages_dir ^ "/constraints_choice_template.html";; -let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; +(* let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; *) +let final_results_TPL = pages_dir ^ "/moogle.html";; + +let my_own_url = + let ic = Unix.open_process_in "hostname -f" in + let hostname = input_line ic in + ignore (Unix.close_process_in ic); + sprintf "http://%s:%d" hostname port +;; exception Chat_unfinished +exception Invalid_action of string (* invalid action for "/search" method *) -let javascript_quote = +let javascript_quote s = let rex = Pcre.regexp "'" in + let rex' = Pcre.regexp "\"" in Pcre.replace ~rex ~templ:"\\'" + (Pcre.replace ~rex:rex' ~templ:"\\\"" s) ;; (* build a bool from a 1-character-string *) @@ -150,17 +162,15 @@ let iter_file f = fold_file (fun _ line -> f line) () let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, - form_RE, variables_initialization_RE) + form_RE, variables_initialization_RE, search_engine_url_RE) = (Pcre.regexp "@TITLE@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@", Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", - Pcre.regexp "@VARIABLES_INITIALIZATION@") + Pcre.regexp "@VARIABLES_INITIALIZATION@", Pcre.regexp "@SEARCH_ENGINE_URL@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" -let port = Helm_registry.get_int "search_engine.port";; - let pp_error = sprintf "

Error: %s

";; let bad_request body outchan = @@ -265,12 +275,117 @@ let add_user_constraints ~constraints | _ -> failwith ("Can't parse constraint string: " ^ constraints) in +let send_results results + ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") req outchan + = + Http_daemon.send_basic_headers ~code:200 outchan ; + Http_daemon.send_header "Content-Type" "text/xml" outchan; + Http_daemon.send_CRLF outchan ; + let subst = + (search_engine_url_RE, my_own_url) :: + (results_RE, theory_of_result results):: + (List.map + (function (key,value) -> + let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in + Pcre.regexp ("@" ^ key' ^ "@"), value) + (List.filter + (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) + req#params)) + in + iter_file + (fun line -> + let new_aliases = + DisambiguatingParser.EnvironmentP3.to_string id_to_uris + in + let processed_line = + apply_substs + (* CSC: Bug here: this is a string, not an array! *) + ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) + line + in + output_string outchan (processed_line ^ "\n")) + final_results_TPL +in + (* HTTP DAEMON CALLBACK *) +let build_dynamic_uri url params = + let p = + String.concat "&" (List.map (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in + url ^ "?" ^ p +in + +let build_uwobo_request (req: Http_types.request) outchan = + prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL"); + let xmluri = build_dynamic_uri ((req#param "param.SEARCH_ENGINE_URL") ^ "/search") req#params in + prerr_endline ("xmluri: " ^ xmluri); + (*let xmluri = Netencoding.Url.encode xmluri in*) + let server_and_port = req#param "param.processorURL" in + let newreq = + build_dynamic_uri + (server_and_port ^ "apply") + (("xmluri",xmluri)::("keys",(req#param "param.thkeys"))::req#params) in + (* if List.mem server_and_port valid_servers then *) + prerr_endline newreq; + if true then + Http_daemon.respond + ~headers:["Content-Type", "text/html"] + ~body:(Http_client.http_get newreq) + outchan + else + Http_daemon.respond + ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port ^ + (String.concat "\n" valid_servers))) + outchan +in + +let proxy url outchan = + let server_and_port = + (Pcre.extract ~rex:server_and_port_url_RE url).(1) + in + if List.mem server_and_port valid_servers then + Http_daemon.respond + ~headers:["Content-Type", "text/html"] + ~body:(Http_client.http_get url) + outchan + else + Http_daemon.respond + ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) + outchan +in + let callback mqi_handle (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); (match req#path with + | "/help" -> Http_daemon.respond ~body:"HELM Search Engine" outchan + | "/search" -> + let initial_expression = + try req#param "expression" with Http_types.Param_not_found _ -> "" + in + let expression = + Pcre.replace ~pat:"\\s*$" + (Pcre.replace ~pat:"^\\s*" initial_expression) + in + if expression = "" then + send_results [] req outchan + else + (try + let results = + match req#param "action" with + | "locate" -> + prerr_endline ("EXPRESSION : " ^ expression); + let query = G.locate expression in + MQueryInterpreter.execute mqi_handle query + | "hint" -> failwith "NOT IMPLEMENTED" (* TODO *) + | "match" -> failwith "NOT IMPLEMENTED" (* TODO *) + | "elim" -> failwith "NOT IMPLEMENTED" (* TODO *) + | action -> raise (Invalid_action action) + in + send_results results req outchan + with Invalid_action action -> + Http_daemon.respond_error ~status:(`Client_error `Bad_request) + ~body:("Invalid action " ^ action) outchan) | "/execute" -> let query_string = req#param "query" in let lexbuf = Lexing.from_string query_string in @@ -278,11 +393,7 @@ let callback mqi_handle (req: Http_types.request) outchan = let result = MQueryInterpreter.execute mqi_handle query in let result_string = pp_result result in Http_daemon.respond ~body:result_string ~headers:[contype] outchan - | "/locate" -> - let id = req#param "id" in - let query = G.locate id in - let result = MQueryInterpreter.execute mqi_handle query in - Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan +(* Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan *) | "/unreferred" -> let target = req#param "target" in let source = req#param "source" in @@ -310,6 +421,7 @@ let callback mqi_handle (req: Http_types.request) outchan = (fun line -> output_string outchan ((apply_substs + ((search_engine_url_RE, my_own_url) :: (List.map (function (key,value) -> let key' = @@ -320,33 +432,23 @@ let callback mqi_handle (req: Http_types.request) outchan = (List.filter (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) req#params) - ) + )) line) ^ "\n")) fname end else Http_daemon.send_file ~src:(FileSrc fname) outchan) | page -> Http_daemon.respond_forbidden ~url:page outchan)) - | "/ask_uwobo" -> - let url = req#param "url" in - let server_and_port = - (Pcre.extract ~rex:server_and_port_url_RE url).(1) - in - if List.mem server_and_port valid_servers then - Http_daemon.respond - ~headers:["Content-Type", "text/html"] - ~body:(Http_client.http_get url) - outchan - else - Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) - outchan + (* OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *) + | "/ask_uwobo" -> build_uwobo_request req outchan | "/searchPattern" | "/matchConclusion" | "/locateInductivePrinciple" -> let term_string = req#param "term" in let (context, metasenv) = ([], []) in let id_to_uris_raw = req#param "aliases" in + let parse_interpretation_choices choices = + List.map int_of_string (Pcre.split ~pat:" " choices) in let parse_choices choices_raw = let choices = Pcre.split ~pat:";" choices_raw in List.fold_left @@ -365,14 +467,18 @@ let callback mqi_handle (req: Http_types.request) outchan = in let id_to_uris = DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in -print_endline ("id_to_uris_raw: " ^ id_to_uris_raw) ; -print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id_to_uris)) ; let id_to_choices = try let choices_raw = req#param "choices" in parse_choices choices_raw with Http_types.Param_not_found _ -> (fun _ -> None) in + let interpretation_choices = + try + let choices_raw = req#param "interpretation_choices" in + Some (parse_interpretation_choices choices_raw) + with Http_types.Param_not_found _ -> None + in let module Chat: DisambiguateTypes.Callbacks = struct @@ -410,55 +516,48 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id raise Chat_unfinished)) let interactive_interpretation_choice interpretations = - let html_interpretations_labels = - String.concat ", " - (List.map - (fun l -> - "\'" ^ - (String.concat "
" - (List.map - (fun (id, value) -> - let id = javascript_quote id in - let value = javascript_quote value in - sprintf "alias id %s = %s" id value) - l)) ^ - "\'") - interpretations) - in - let html_interpretations = - String.concat ", " - (List.map - (fun l -> - "\'" ^ - (String.concat " " - (List.map - (fun (id, value) -> - let id = javascript_quote id in - let value = javascript_quote value in - sprintf "alias id %s = %s" - id - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - value)) - l)) ^ - "\'") + match interpretation_choices with + Some l -> prerr_endline "CARRAMBA" ; l + | None -> + let html_interpretations_labels = + String.concat ", " + (List.map + (fun l -> + "\'" ^ + (String.concat "
" + (List.map + (fun (id, value) -> + let id = javascript_quote id in + let value = javascript_quote value in + sprintf "%s = %s" id value) + l)) ^ + "\'") interpretations) - in - Http_daemon.send_basic_headers ~code:200 outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [interpretations_RE, html_interpretations; - interpretations_labels_RE, html_interpretations_labels] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_interpretation_choice_TPL; - raise Chat_unfinished - - let input_or_locate_uri ~title = - UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con" + in + let html_interpretations = + let rec aux n = + function + [] -> [] + | _::tl -> ("'" ^ string_of_int n ^ "'")::(aux (n+1) tl) + in + String.concat ", " (aux 0 interpretations) + in + Http_daemon.send_basic_headers ~code:200 outchan ; + Http_daemon.send_CRLF outchan ; + iter_file + (fun line -> + let processed_line = + apply_substs + [interpretations_RE, html_interpretations; + interpretations_labels_RE, html_interpretations_labels] + line + in + output_string outchan (processed_line ^ "\n")) + interactive_interpretation_choice_TPL; + raise Chat_unfinished + + let input_or_locate_uri ~title ?id () = + assert false end in @@ -549,20 +648,7 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id G.query_of_constraints universe must'' only' in let results = MQueryInterpreter.execute mqi_handle query in - Http_daemon.send_basic_headers ~code:200 outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let new_aliases = - DisambiguatingParser.EnvironmentP3.to_string id_to_uris' in - let processed_line = - apply_substs - [results_RE, theory_of_result results ; - new_aliases_RE, new_aliases] - line - in - output_string outchan (processed_line ^ "\n")) - final_results_TPL + send_results results ~id_to_uris:id_to_uris' req outchan | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print (sprintf "%s done!" req#path)