X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=c42c01043f081b01251b8566c73caf009abf8c2f;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=57c90f068272516aa6dc9889644500153194ea28;hpb=d8ecc77eeaadb6a946b3f17e9aa7fc8570f0a6d2;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 57c90f068..c42c01043 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2002-2004, HELM Team. +(* Copyright (C) 2002-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -25,8 +25,6 @@ open Printf -module DB = Dbi_mysql - let debug = true let debug_print s = if debug then prerr_endline s let _ = Http_common.debug := false @@ -35,14 +33,18 @@ exception Chat_unfinished exception Unbound_identifier of string exception Invalid_action of string (* invalid action for "/search" method *) -let daemon_name = "Moogle" -let configuration_file = "/projects/helm/etc/moogle.conf.xml" + (** raised by elim when a MutInd is required but not found *) +exception Not_a_MutInd + +let daemon_name = "Whelp" +let configuration_file = "/projects/helm/etc/whelp.conf.xml" 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" + "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES"; + "EXPRESSION"; "ID"; "IDEN"; "ID_TO_URIS"; "INTERPRETATIONS"; + "INTERPRETATIONS_LABELS"; "MSG"; "NEW_ALIASES"; "NEXT_LINK"; "NO_CHOICES"; + "PAGE"; "PAGES"; "PAGELIST"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS"; + "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE"; ] let tag = @@ -50,15 +52,18 @@ let tag = List.iter (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag))) placeholders; - Hashtbl.find regexps + fun name -> + try + Hashtbl.find regexps name + with Not_found -> assert false (* First of all we load the configuration *) let _ = 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" -let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html" let moogle_TPL = pages_dir ^ "/moogle.html" +let choices_TPL = pages_dir ^ "/moogle_chat.html" let my_own_url = let ic = Unix.open_process_in "hostname -f" in @@ -98,7 +103,8 @@ let javascript_quote s = let string_tail s = let len = String.length s in String.sub s 1 (len-1) -let nonvar s = +let nonvar uri = + let s = UriManager.string_of_uri uri in let len = String.length s in let suffix = String.sub s (len-4) 4 in not (suffix = ".var") @@ -113,20 +119,54 @@ let add_param_substs params = params) let page_RE = Pcre.regexp "¶m\\.page=\\d+" +let identifier_RE = Pcre.regexp "^\\s*(\\w|')+\\s*$" +let qualified_mutind_RE = + Pcre.regexp "^\\s*cic:(/(\\w|')+)+\\.ind#xpointer\\(1/\\d+\\)\\s*$" + +let query_kind_of_req (req: Http_types.request) = + match req#path with + | "/match" -> "Match" + | "/hint" -> "Hint" + | "/locate" -> "Locate" + | "/elim" -> "Elim" + | "/instance" -> "Instance" + | _ -> "" + + (* given a uri with a query part in input try to find in it a string + * "¶m_name=..." (where param_name is given). If found its value will be + * set to param_value. If not, a trailing "¶m_name=param_value" (where + * both are given) is added to the input string *) +let patch_param param_name param_value url = + let rex = Pcre.regexp (sprintf "&%s=[^&]*" (Pcre.quote param_name)) in + if Pcre.pmatch ~rex url then + Pcre.replace ~rex ~templ:(sprintf "%s=%s" param_name param_value) url + else + sprintf "%s&%s=%s" url param_name param_value + + (** HTML encoding, e.g.: "<" -> "<" *) +let html_encode = Netencoding.Html.encode_from_latin1 + +let fold_n_to_m f n m acc = + let rec aux acc = + function + i when i <= m -> aux (f i acc) (i + 1) + | _ -> acc + in + aux acc n let send_results results - ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") + ?(id_to_uris = DisambiguateTypes.empty_environment) (req: Http_types.request) outchan = + let query_kind = query_kind_of_req req in + let interp = try req#param "interp" with Http_types.Param_not_found _ -> "" in 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 + (patch_param "param.interp" interp + (patch_param "param.page" (string_of_int page) + this)) in let target = Pcre.replace ~pat:"&" ~templ:"&" target in sprintf "%s" target anchor @@ -135,7 +175,7 @@ let send_results results Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; Http_daemon.send_header "Content-Type" "text/xml" outchan; Http_daemon.send_CRLF outchan ; - let subst, results_string = + let subst = match results with | `Results results -> let page = try int_of_string (req#param "page") with _ -> 1 in @@ -149,24 +189,56 @@ let send_results results 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 + let pages = if pages = 0 then 1 else pages in + let additional_pages = 3 in + let (summary, results) = MooglePp.theory_of_result page results in + [ tag "PAGE", string_of_int page; + tag "PAGES", string_of_int pages ^ " Pages"; + tag "PAGELIST", + (let inf = page - additional_pages in + let sup = page + additional_pages in + let superinf = inf - (sup - pages) in + let supersup = sup + (1 - inf) in + let n,m = + if inf >= 1 && sup <= pages then + inf,sup + else if inf < 1 then + 1, (if supersup <= pages then supersup else pages) + else (* sup > pages *) + (if superinf >= 1 then superinf else 1),pages + in + fold_n_to_m + (fun n acc -> acc ^ " " ^ + (if n = page then string_of_int n + else page_link (string_of_int n) n)) + n m ""); + 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 ""); + tag "QUERY_KIND", query_kind; + tag "QUERY_SUMMARY", summary; + tag "RESULTS", results ] | `Error msg -> - [ tag "PAGE", ""; tag "PAGES", ""; - tag "PREV_LINK", ""; tag "NEXT_LINK", "" ], - msg + [ tag "PAGE", "1"; + tag "PAGES", "1 Page"; + tag "PAGELIST", ""; + tag "PREV_LINK", ""; + tag "NEXT_LINK", ""; + tag "QUERY_KIND", query_kind; + tag "QUERY_SUMMARY", "error"; + tag "RESULTS", msg ] + in + let advanced = + try + req#param "advanced" + with Http_types.Param_not_found _ -> "no" in let subst = (tag "SEARCH_ENGINE_URL", my_own_url) :: - (tag "RESULTS", results_string) :: - (tag "ADVANCED", req#param "advanced") :: - (tag "EXPRESSION", req#param "expression") :: + (tag "ADVANCED", advanced) :: + (tag "EXPRESSION", html_encode (req#param "expression")) :: add_param_substs req#params @ - (if req#param "advanced" = "no" then + (if advanced = "no" then [ tag "SIMPLE_CHECKED", "checked='true'"; tag "ADVANCED_CHECKED", "" ] else @@ -176,9 +248,7 @@ let send_results results in iter_file (fun line -> - let new_aliases = - CicTextualParser2.EnvironmentP3.to_string id_to_uris - in + let new_aliases = DisambiguatePp.pp_environment id_to_uris in let processed_line = apply_substs (* CSC: Bug here: this is a string, not an array! *) @@ -191,114 +261,140 @@ let send_results results 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 = - try req#param "aliases" - with Http_types.Param_not_found _ -> "" - 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 - (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 = - try - parse_choices (req#param "choices") - with Http_types.Param_not_found _ -> (fun _ -> None) - in - let interpretation_choices = - try - let choices_raw = req#param "interpretation_choices" in - if choices_raw = "" then None - else Some (parse_interpretation_choices choices_raw) - with Http_types.Param_not_found _ -> None - in - let module Chat: DisambiguateTypes.Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?enable_button_for_non_vars ~(title: string) ~(msg: string) - ~(id: string) (choices: string list) - = - match id_to_choices id with - | Some choices -> choices - | None -> List.filter nonvar choices + try + if req#path = "/elim" && + not (Pcre.pmatch ~rex:identifier_RE term_str || + Pcre.pmatch ~rex:qualified_mutind_RE term_str) then + raise Not_a_MutInd; + let (context, metasenv) = ([], []) in + let id_to_uris_raw = + try req#param "aliases" + with Http_types.Param_not_found _ -> "" + 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 + (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 -> UriManager.uri_of_string + (Netencoding.Url.decode u)) + tail) + else + f id') + | _ -> failwith "Can't parse choices") + (fun _ -> None) + choices + in + let id_to_uris = DisambiguatePp.parse_environment id_to_uris_raw in + let id_to_choices = + try + parse_choices (req#param "choices") + with Http_types.Param_not_found _ -> (fun _ -> None) + in + let interpretation_choices = + try + let choices_raw = req#param "interpretation_choices" in + if choices_raw = "" then None + else Some (parse_interpretation_choices choices_raw) + with Http_types.Param_not_found _ -> None + in + let module Chat: DisambiguateTypes.Callbacks = + struct + let interactive_user_uri_choice ~selection_mode ?ok + ?enable_button_for_non_vars ~(title: string) ~(msg: string) + ~(id: string) (choices: UriManager.uri list) + = + match id_to_choices id with + | Some choices -> choices + | None -> List.filter nonvar choices - let interactive_interpretation_choice interpretations = - match interpretation_choices with - | Some l -> l - | None -> - let html_interpretations = - MooglePp.html_of_interpretations interpretations - in - Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [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")) - interactive_interpretation_choice_TPL; - raise Chat_unfinished + let interactive_interpretation_choice interpretations = + match interpretation_choices with + | Some l -> l + | None -> + let html_interpretations = + MooglePp.html_of_interpretations interpretations + in + Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; + Http_daemon.send_CRLF outchan ; + let advanced = + try + req#param "advanced" + with Http_types.Param_not_found _ -> "no" + in + let query_kind = query_kind_of_req req in + iter_file + (fun line -> + let processed_line = + apply_substs + [ tag "SEARCH_ENGINE_URL", my_own_url; + tag "ADVANCED", advanced; + tag "INTERPRETATIONS", html_interpretations; + tag "CURRENT_CHOICES", req#param "choices"; + tag "EXPRESSION", html_encode (req#param "expression"); + tag "QUERY_KIND", query_kind; + tag "QUERY_SUMMARY", "disambiguation"; + tag "ACTION", string_tail req#path ] + line + in + output_string outchan (processed_line ^ "\n")) + choices_TPL; + raise Chat_unfinished - let input_or_locate_uri ~title ?id () = - match id with - | Some id -> raise (Unbound_identifier id) - | None -> assert false - end - in - let module Disambiguate' = Disambiguate.Make(Chat) in - let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in - let (id_to_uris, metasenv, term) = - match - Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris - with - | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term - | _ -> assert false - in - let uris = - match req#path with - | "/match" -> MetadataQuery.match_term ~dbd term - | "/hint" -> - 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 ~dbd (proof, goal)) - | _ -> assert false) - | "/elim" -> - let uri = - match term with - | Cic.MutInd (uri, typeno, _) -> - UriManager.string_of_uriref (uri, [typeno]) - | _ -> assert false - in - MetadataQuery.elim ~dbd uri - | _ -> assert false - in - send_results ~id_to_uris (`Results uris) req outchan + let input_or_locate_uri ~title ?id () = + match id with + | Some id -> raise (Unbound_identifier id) + | None -> assert false + end + in + let module Disambiguate' = Disambiguate.Make(Chat) in + let ast = Grammar.Entry.parse CicNotationParser.term (Stream.of_string term_str) in + let (id_to_uris, metasenv, term) = + match + Disambiguate'.disambiguate_term ~dbd ~context ~metasenv + ~aliases:id_to_uris ast + with + | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term + | _ -> assert false + in + let uris = + match req#path with + | "/match" -> MetadataQuery.match_term ~dbd term + | "/instance" -> MetadataQuery.instance ~dbd term + | "/hint" -> + 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.experimental_hint ~dbd (proof, goal)) + | _ -> assert false) + | "/elim" -> + let uri = + match term with + | Cic.MutInd (uri, typeno, _) -> + UriManager.uri_of_uriref uri typeno None + | _ -> raise Not_a_MutInd + in + MetadataQuery.elim ~dbd uri + | _ -> assert false + in + let uris = List.map UriManager.string_of_uri uris in + send_results ~id_to_uris (`Results uris) req outchan + with + | Not_a_MutInd -> + send_results (`Error (MooglePp.pp_error "Not an inductive type" + ("elim requires as input an identifier corresponding to an inductive" + ^ " type"))) + req outchan let callback dbd (req: Http_types.request) outchan = try @@ -306,16 +402,16 @@ let callback dbd (req: Http_types.request) outchan = (match req#path with | "/getpage" -> (* TODO implement "is_permitted" *) - (let is_permitted _ = true in + (let is_permitted page = not (Pcre.pmatch ~pat:"/" page) in let page = req#param "url" in + let fname = sprintf "%s/%s" pages_dir page in let preprocess = (try bool_of_string (req#param "preprocess") with Invalid_argument _ | Http_types.Param_not_found _ -> false) in (match page with - | page when is_permitted page -> - (let fname = sprintf "%s/%s" pages_dir page in + | page when is_permitted page && Sys.file_exists fname -> Http_daemon.send_basic_headers ~code:(`Code 200) outchan; Http_daemon.send_header "Content-Type" "text/html" outchan; Http_daemon.send_CRLF outchan; @@ -332,7 +428,7 @@ let callback dbd (req: Http_types.request) outchan = "\n")) fname end else - Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan) + Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan | page -> Http_daemon.respond_forbidden ~url:page outchan)) | "/help" -> Http_daemon.respond ~body:daemon_name outchan | "/locate" -> @@ -345,11 +441,14 @@ let callback dbd (req: Http_types.request) outchan = in if expression = "" then send_results (`Results []) req outchan - else + else begin let results = MetadataQuery.locate ~dbd expression in + let results = List.map UriManager.string_of_uri results in send_results (`Results results) req outchan + end | "/hint" | "/elim" + | "/instance" | "/match" -> exec_action dbd req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) @@ -359,8 +458,8 @@ let callback dbd (req: Http_types.request) outchan = | Chat_unfinished -> () | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan - | CicTextualParser2.Parse_error (_, msg) -> - send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan + | CicNotationParser.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 outchan @@ -370,6 +469,22 @@ let callback dbd (req: Http_types.request) outchan = let msg = MooglePp.pp_error "Uncaught exception" exn_string in send_results (`Error msg) req outchan +let restore_environment () = + match + Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump" + with + | None -> () + | Some fname -> + printf "Restoring Cic environment from %s ... " fname; flush stdout; + let ic = open_in fname in + CicEnvironment.restore_from_channel ic; + close_in ic; + printf "done!\n"; flush stdout + +let read_notation () = + CicNotation.load_notation (Helm_registry.get "search_engine.notations"); + CicNotation.load_notation (Helm_registry.get "search_engine.interpretations") + let _ = printf "%s started and listening on port %d\n" daemon_name port; printf "Current directory is %s\n" (Sys.getcwd ()); @@ -383,6 +498,8 @@ let _ = ~user:(Helm_registry.get "db.user") () in + restore_environment (); + read_notation (); Http_daemon.start' ~port (callback dbd); printf "%s is terminating, bye!\n" daemon_name