X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=655235c1e538121ca0b72bc124a90bc47db2b139;hb=03b76418d261acfb3b33d64283ea0269ba596859;hp=d994ac11a361e336e8b51f0af720c7862197e1a0;hpb=a240236d1e9d5154e8cb5da73f8e98cf7734a73e;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index d994ac11a..655235c1e 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -33,8 +33,11 @@ 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"; @@ -115,6 +118,7 @@ let add_param_substs params = params) let page_RE = Pcre.regexp "¶m\\.page=\\d+" +let identifier_RE = Pcre.regexp "^\\s*\\w+\\s*$" let query_kind_of_req (req: Http_types.request) = match req#path with @@ -122,7 +126,8 @@ let query_kind_of_req (req: Http_types.request) = | "/hint" -> "Hint" | "/locate" -> "Locate" | "/elim" -> "Elim" - | _ -> assert false + | "/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 @@ -135,6 +140,9 @@ let patch_param 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 send_results results ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") (req: Http_types.request) outchan @@ -197,7 +205,7 @@ let send_results results let subst = (tag "SEARCH_ENGINE_URL", my_own_url) :: (tag "ADVANCED", advanced) :: - (tag "EXPRESSION", req#param "expression") :: + (tag "EXPRESSION", html_encode (req#param "expression")) :: add_param_substs req#params @ (if advanced = "no" then [ tag "SIMPLE_CHECKED", "checked='true'"; @@ -224,123 +232,134 @@ 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) 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 -> 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 - 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", 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 - 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 = CicTextualParser2.parse_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.string_of_uriref (uri, [typeno]) + | _ -> raise Not_a_MutInd + in + MetadataQuery.elim ~dbd uri + | _ -> assert false + 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 @@ -348,16 +367,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; @@ -374,7 +393,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" -> @@ -393,6 +412,7 @@ let callback dbd (req: Http_types.request) outchan = end | "/hint" | "/elim" + | "/instance" | "/match" -> exec_action dbd req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) @@ -403,7 +423,7 @@ let callback dbd (req: Http_types.request) outchan = | 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 + 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 @@ -413,6 +433,18 @@ 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.get "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 _ = printf "%s started and listening on port %d\n" daemon_name port; printf "Current directory is %s\n" (Sys.getcwd ()); @@ -426,6 +458,7 @@ let _ = ~user:(Helm_registry.get "db.user") () in + restore_environment (); Http_daemon.start' ~port (callback dbd); printf "%s is terminating, bye!\n" daemon_name