X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=c42c01043f081b01251b8566c73caf009abf8c2f;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=341ace5cc625a6200fa9f2a51af66e31bc4fbaec;hpb=1616bc6fd4ed16b14e340a3e0070403fcbf70db9;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 341ace5cc..c42c01043 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -33,14 +33,17 @@ 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 = [ "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"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS"; + "PAGE"; "PAGES"; "PAGELIST"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS"; "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE"; ] @@ -100,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") @@ -115,6 +119,9 @@ 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 @@ -122,6 +129,7 @@ let query_kind_of_req (req: Http_types.request) = | "/hint" -> "Hint" | "/locate" -> "Locate" | "/elim" -> "Elim" + | "/instance" -> "Instance" | _ -> "" (* given a uri with a query part in input try to find in it a string @@ -138,8 +146,16 @@ let patch_param param_name param_value url = (** 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 @@ -174,9 +190,28 @@ let send_results results results_no / results_per_page + 1 in 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; + 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 ""); @@ -185,7 +220,8 @@ let send_results results tag "RESULTS", results ] | `Error msg -> [ tag "PAGE", "1"; - tag "PAGES", "1"; + tag "PAGES", "1 Page"; + tag "PAGELIST", ""; tag "PREV_LINK", ""; tag "NEXT_LINK", ""; tag "QUERY_KIND", query_kind; @@ -212,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! *) @@ -227,125 +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 ; - 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 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 - prerr_endline "prima della disambiguazione"; - 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 - prerr_endline "dopo la disambiguazione"; - 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 @@ -394,10 +443,12 @@ let callback dbd (req: Http_types.request) outchan = send_results (`Results []) req outchan 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)) @@ -407,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 @@ -418,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 ()); @@ -431,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