X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=0bb29ec495dde61b29813f92b41cfe346051fc26;hb=2026624f827b29c35d54aa67b301250123ea7311;hp=bc4cd729a67128de91304c2c5c100c272554e4c6;hpb=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index bc4cd729a..0bb29ec49 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -36,29 +36,22 @@ exception Unbound_identifier of string exception Invalid_action of string (* invalid action for "/search" method *) let daemon_name = "Moogle" -let configuration_file = "searchEngine.conf.xml" +let configuration_file = "/projects/helm/etc/moogle.conf.xml" +(*let configuration_file = "searchEngine.conf.xml" *) -let expression_tag_RE = Pcre.regexp "@EXPRESSION@" -let action_tag_RE = Pcre.regexp "@ACTION@" -let advanced_tag_RE = Pcre.regexp "@ADVANCED@" -let advanced_checked_RE = Pcre.regexp "@ADVANCED_CHECKED@" -let simple_checked_RE = Pcre.regexp "@SIMPLE_CHECKED@" -let title_tag_RE = Pcre.regexp "@TITLE@" -let no_choices_tag_RE = Pcre.regexp "@NO_CHOICES@" -let current_choices_tag_RE = Pcre.regexp "@CURRENT_CHOICES@" -let choices_tag_RE = Pcre.regexp "@CHOICES@" -let msg_tag_RE = Pcre.regexp "@MSG@" -let id_to_uris_RE = Pcre.regexp "@ID_TO_URIS@" -let id_RE = Pcre.regexp "@ID@" -let iden_tag_RE = Pcre.regexp "@IDEN@" -let interpretations_RE = Pcre.regexp "@INTERPRETATIONS@" -let interpretations_labels_RE = Pcre.regexp "@INTERPRETATIONS_LABELS@" -let results_RE = Pcre.regexp "@RESULTS@" -let new_aliases_RE = Pcre.regexp "@NEW_ALIASES@" -let form_RE = Pcre.regexp "@FORM@" -let variables_initialization_RE = Pcre.regexp "@VARIABLES_INITIALIZATION@" -let search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@" -let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" +let placeholders = [ + "EXPRESSION"; "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "SIMPLE_CHECKED"; + "TITLE"; "NO_CHOICES"; "CURRENT_CHOICES"; "CHOICES"; "MSG"; "ID_TO_URIS"; + "ID"; "IDEN"; "INTERPRETATIONS"; "INTERPRETATIONS_LABELS"; "RESULTS"; + "NEW_ALIASES"; "SEARCH_ENGINE_URL"; "PREV_LINK"; "PAGE"; "PAGES"; "NEXT_LINK" +] + +let tag = + let regexps = Hashtbl.create 25 in + List.iter + (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag))) + placeholders; + Hashtbl.find regexps (* First of all we load the configuration *) let _ = Helm_registry.load_from configuration_file @@ -73,6 +66,7 @@ let my_own_url = let hostname = input_line ic in ignore (Unix.close_process_in ic); sprintf "http://%s:%d" hostname port +let _ = Helm_registry.set "search_engine.my_own_url" my_own_url let bad_request body outchan = Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body @@ -105,6 +99,10 @@ let javascript_quote s = let string_tail s = let len = String.length s in String.sub s 1 (len-1) +let nonvar s = + let len = String.length s in + let suffix = String.sub s (len-4) 4 in + not (suffix = ".var") let add_param_substs params = List.map @@ -115,30 +113,67 @@ let add_param_substs params = (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key) params) +let page_RE = Pcre.regexp "¶m\\.page=\\d+" + let send_results results ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") (req: Http_types.request) outchan = + let page_link anchor page = + try + let this = req#param "this" in + let target = + if Pcre.pmatch ~rex:page_RE this then + Pcre.replace ~rex:page_RE ~templ:(sprintf "¶m.page=%d" page) + this + else + sprintf "%s¶m.page=%d" this page + in + let target = Pcre.replace ~pat:"&" ~templ:"&" target in + sprintf "%s" target anchor + with Http_types.Param_not_found _ -> "" + in Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; Http_daemon.send_header "Content-Type" "text/xml" outchan; Http_daemon.send_CRLF outchan ; - let results_string = + let subst, results_string = match results with - | `Results r -> MooglePp.theory_of_result req r - | `Error msg -> msg + | `Results results -> + let page = try int_of_string (req#param "page") with _ -> 1 in + let results_no = List.length results in + let results_per_page = + Helm_registry.get_int "search_engine.results_per_page" + in + let pages = + if results_no mod results_per_page = 0 then + results_no / results_per_page + else + results_no / results_per_page + 1 + in + ([ tag "PAGE", string_of_int page; tag "PAGES", string_of_int pages ] @ + [ tag "PREV_LINK", + if page > 1 then page_link "Prev" (page-1) else "" ] @ + [ tag "NEXT_LINK", + if page < pages then page_link "Next" (page+1) else "" ]), + MooglePp.theory_of_result req page results + | `Error msg -> + [ tag "PAGE", ""; tag "PAGES", ""; + tag "PREV_LINK", ""; tag "NEXT_LINK", "" ], + msg in let subst = - (search_engine_url_RE, my_own_url) :: - (results_RE, results_string):: - (advanced_tag_RE, req#param "advanced"):: - (expression_tag_RE, req#param "expression"):: + (tag "SEARCH_ENGINE_URL", my_own_url) :: + (tag "RESULTS", results_string) :: + (tag "ADVANCED", req#param "advanced") :: + (tag "EXPRESSION", req#param "expression") :: add_param_substs req#params @ (if req#param "advanced" = "no" then - [ simple_checked_RE, "checked='true'"; - advanced_checked_RE, "" ] + [ tag "SIMPLE_CHECKED", "checked='true'"; + tag "ADVANCED_CHECKED", "" ] else - [ simple_checked_RE, ""; - advanced_checked_RE, "checked='true'" ]) + [ tag "SIMPLE_CHECKED", ""; + tag "ADVANCED_CHECKED", "checked='true'" ]) @ + subst in iter_file (fun line -> @@ -148,13 +183,14 @@ let send_results results let processed_line = apply_substs (* CSC: Bug here: this is a string, not an array! *) - ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) + ((tag "NEW_ALIASES", "'" ^ javascript_quote new_aliases ^ "'") :: + subst) line in output_string outchan (processed_line ^ "\n")) moogle_TPL -let exec_action dbh (req: Http_types.request) outchan = +let exec_action dbd (req: Http_types.request) outchan = let term_str = req#param "expression" in let (context, metasenv) = ([], []) in let id_to_uris_raw = @@ -165,19 +201,19 @@ let exec_action dbh (req: Http_types.request) outchan = 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 - (fun f x -> - match Pcre.split ~pat:"\\s" x with - | ""::id::tail - | id::tail when id<>"" -> - (fun id' -> - if id = id' then - Some (List.map (fun u -> Netencoding.Url.decode u) tail) - else - f id') - | _ -> failwith "Can't parse choices") - (fun _ -> None) - choices + List.fold_left + (fun f x -> + match Pcre.split ~pat:"\\s" x with + | ""::id::tail + | id::tail when id<>"" -> + (fun id' -> + if id = id' then + Some (List.map (fun u -> Netencoding.Url.decode u) tail) + else + f id') + | _ -> failwith "Can't parse choices") + (fun _ -> None) + choices in let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in let id_to_choices = @@ -200,11 +236,11 @@ let exec_action dbh (req: Http_types.request) outchan = = match id_to_choices id with | Some choices -> choices - | None -> assert false + | None -> List.filter nonvar choices let interactive_interpretation_choice interpretations = match interpretation_choices with - | Some l -> prerr_endline "CARRAMBA" ; l + | Some l -> l | None -> let html_interpretations = MooglePp.html_of_interpretations interpretations @@ -215,11 +251,11 @@ let exec_action dbh (req: Http_types.request) outchan = (fun line -> let processed_line = apply_substs - [advanced_tag_RE, req#param "advanced"; - interpretations_RE, html_interpretations; - current_choices_tag_RE, req#param "choices"; - expression_tag_RE, req#param "expression"; - action_tag_RE, string_tail req#path ] + [tag "ADVANCED", req#param "advanced"; + tag "INTERPRETATIONS", html_interpretations; + tag "CURRENT_CHOICES", req#param "choices"; + tag "EXPRESSION", req#param "expression"; + tag "ACTION", string_tail req#path ] line in output_string outchan (processed_line ^ "\n")) @@ -236,22 +272,22 @@ let exec_action dbh (req: Http_types.request) outchan = let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in let (id_to_uris, metasenv, term) = match - Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris + Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris with - | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term + | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term | _ -> assert false in let uris = match req#path with - | "/match" -> MetadataQuery.match_term ~dbh term + | "/match" -> MetadataQuery.match_term ~dbd term | "/hint" -> - let status = ProofEngineTypes.initial_status term [] in + let status = ProofEngineTypes.initial_status term metasenv in let intros = PrimitiveTactics.intros_tac () in let subgoals = ProofEngineTypes.apply_tactic intros status in (match subgoals with | proof, [goal] -> let (uri,metasenv,bo,ty) = proof in - List.map fst (MetadataQuery.hint ~dbh (proof, goal)) + List.map fst (MetadataQuery.hint ~dbd (proof, goal)) | _ -> assert false) | "/elim" -> let uri = @@ -260,20 +296,19 @@ let exec_action dbh (req: Http_types.request) outchan = UriManager.string_of_uriref (uri, [typeno]) | _ -> assert false in - MetadataQuery.elim ~dbh uri + MetadataQuery.elim ~dbd uri | _ -> assert false in send_results ~id_to_uris (`Results uris) req outchan -let callback dbh (req: Http_types.request) outchan = +let callback dbd (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); (match req#path with | "/getpage" -> (* TODO implement "is_permitted" *) (let is_permitted _ = true in - let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in - let page = remove_fragment (req#param "url") in + let page = req#param "url" in let preprocess = (try bool_of_string (req#param "preprocess") @@ -281,7 +316,7 @@ let callback dbh (req: Http_types.request) outchan = in (match page with | page when is_permitted page -> - (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in + (let fname = sprintf "%s/%s" pages_dir page in Http_daemon.send_basic_headers ~code:(`Code 200) outchan; Http_daemon.send_header "Content-Type" "text/html" outchan; Http_daemon.send_CRLF outchan; @@ -290,9 +325,9 @@ let callback dbh (req: Http_types.request) outchan = (fun line -> output_string outchan ((apply_substs - ((search_engine_url_RE, my_own_url) :: - (advanced_tag_RE, "no") :: - (results_RE, "") :: + ((tag "SEARCH_ENGINE_URL", my_own_url) :: + (tag "ADVANCED", "no") :: + (tag "RESULTS", "") :: add_param_substs req#params) line) ^ "\n")) @@ -312,19 +347,20 @@ let callback dbh (req: Http_types.request) outchan = if expression = "" then send_results (`Results []) req outchan else - let results = MetadataQuery.locate ~dbh expression in + let results = MetadataQuery.locate ~dbd expression in send_results (`Results results) req outchan | "/hint" | "/elim" - | "/match" -> exec_action dbh req outchan + | "/match" -> exec_action dbd req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) outchan); debug_print (sprintf "%s done!" req#path) with + | Chat_unfinished -> () | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan - | CicTextualParser2.Parse_error msg -> + | CicTextualParser2.Parse_error (_, msg) -> send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan | Unbound_identifier id -> send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req @@ -341,10 +377,13 @@ let _ = printf "HTML directory is %s\n" pages_dir; flush stdout; Unix.putenv "http_proxy" ""; - let dbh = - new DB.connection ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database") + let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~database:(Helm_registry.get "db.database") + ~user:(Helm_registry.get "db.user") + () in - Http_daemon.start' ~port (callback dbh); + Http_daemon.start' ~port (callback dbd); printf "%s is terminating, bye!\n" daemon_name