X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=fc0fb9cbee4ec2af67bb77d7f2b12ccfc1f269c2;hb=978a25d9392e5fc1a19fa37c86339c5d0b67ddd6;hp=aaa5f48fa34af5210bd8fd43bf2175d684bbdc98;hpb=19802b6487148ac232b560b43f131ffa679e4ee8;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index aaa5f48fa..fc0fb9cbe 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -35,23 +35,22 @@ let debug_print s = if debug then prerr_endline s;; Http_common.debug := true;; (* Http_common.debug := true;; *) - (** accepted HTTP servers for ask_uwobo method forwarding *) -let valid_servers = - [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ];; - -let mqi_flags = [] (* default MathQL interpreter options *) - open Printf;; let daemon_name = "Search Engine";; -let default_port = 58085;; -let port_env_var = "SEARCH_ENGINE_PORT";; -let pages_dir = - try - Sys.getenv "SEARCH_ENGINE_HTML_DIR" - with Not_found -> "html" (* relative to searchEngine's document root *) + (* First of all we load the configuration *) +let _ = + let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in + Helm_registry.load_from configuration_file ;; + +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";; @@ -60,6 +59,13 @@ let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; exception Chat_unfinished +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 *) let bool_of_string' = function | "0" -> false @@ -155,17 +161,7 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, Pcre.regexp "@VARIABLES_INITIALIZATION@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" -exception NotAnInductiveDefinition - -let port = - try - int_of_string (Sys.getenv port_env_var) - with - | Not_found -> default_port - | Failure "int_of_string" -> - prerr_endline "Warning: invalid port, reverting to default"; - default_port -;; +let port = Helm_registry.get_int "search_engine.port";; let pp_error = sprintf "

Error: %s

";; @@ -177,44 +173,25 @@ let contype = "Content-Type", "text/html";; (* SEARCH ENGINE functions *) -let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) = - function - "/searchPattern" -> - U.universe_for_search_pattern, - (constr_obj, constr_rel, constr_sort), - (Some constr_obj, Some constr_rel, Some constr_sort) - | "/matchConclusion" -> - let constr_obj' = - List.map - (function (pos, uri) -> U.set_full_position pos None, uri) - (List.filter - (function (pos, _) -> U.is_conclusion pos) - constr_obj) - in - U.universe_for_match_conclusion, - (*CSC: we must select the must constraints here!!! *) - (constr_obj',[],[]),(Some constr_obj', None, None) - | _ -> assert false -;; - let get_constraints term = function - "/locateInductivePrinciple" -> - let uri = - match term with - Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t]) - | _ -> raise NotAnInductiveDefinition - in - let constr_obj = - [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)] - in - let constr_rel = [`MainConclusion None] in - let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in - U.universe_for_search_pattern, - (constr_obj, constr_rel, constr_sort), (None,None,None) - | req_path -> - let must = MQueryLevels2.get_constraints term in - refine_constraints must req_path + | "/locateInductivePrinciple" -> + None, + (CGLocateInductive.get_constraints term), + (None,None,None) + | "/searchPattern" -> + let constr_obj, constr_rel, constr_sort = + CGSearchPattern.get_constraints term in + (Some CGSearchPattern.universe), + (constr_obj, constr_rel, constr_sort), + (Some constr_obj, Some constr_rel, Some constr_sort) + | "/matchConclusion" -> + let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in +(* FG: there is no way to choose the block number ***************************) + let block = pred (List.length list_of_must) in + (Some CGMatchConclusion.universe), + (List.nth list_of_must block, [], []), (Some only, None, None) + | _ -> assert false ;; (* @@ -292,25 +269,28 @@ in (* HTTP DAEMON CALLBACK *) -let callback (req: Http_types.request) outchan = +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 | "/execute" -> - let mqi_handle = C.init mqi_flags debug_print in let query_string = req#param "query" in let lexbuf = Lexing.from_string query_string in let query = MQueryUtil.query_of_text lexbuf in let result = MQueryInterpreter.execute mqi_handle query in let result_string = pp_result result in - C.close mqi_handle; Http_daemon.respond ~body:result_string ~headers:[contype] outchan | "/locate" -> - let mqi_handle = C.init mqi_flags debug_print in let id = req#param "id" in let query = G.locate id in - let result = MQueryInterpreter.execute mqi_handle query in - C.close mqi_handle; + let result = MQueryInterpreter.execute mqi_handle query in + Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan + | "/unreferred" -> + let target = req#param "target" in + let source = req#param "source" in + let query = G.unreferred target source in + let result = MQueryInterpreter.execute mqi_handle query in Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) @@ -358,7 +338,7 @@ let callback (req: Http_types.request) outchan = if List.mem server_and_port valid_servers then Http_daemon.respond ~headers:["Content-Type", "text/html"] - ~body:(Http_client.Convenience.http_get url) + ~body:(Http_client.http_get url) outchan else Http_daemon.respond @@ -367,30 +347,11 @@ let callback (req: Http_types.request) outchan = | "/searchPattern" | "/matchConclusion" | "/locateInductivePrinciple" -> - let mqi_handle = C.init mqi_flags debug_print in let term_string = req#param "term" in - let lexbuf = Lexing.from_string term_string in let (context, metasenv) = ([], []) in - let (dom, mk_metasenv_and_expr) = - CicTextualParserContext.main - ~context ~metasenv CicTextualLexer.token lexbuf - in let id_to_uris_raw = req#param "aliases" in - let tokens = Pcre.split ~pat:"\\s" id_to_uris_raw in - let rec parse_tokens keys lookup = function (* TODO spostarla fuori *) - | [] -> keys, lookup - | "alias" :: key :: value :: rest -> - let key' = CicTextualParser0.Id key in - parse_tokens - (key'::keys) - (fun id -> - if id = key' then - Some - (CicTextualParser0.Uri (MQueryMisc.cic_textual_parser_uri_of_string value)) - else lookup id) - rest - | _ -> failwith "Can't parse 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 @@ -399,8 +360,6 @@ let callback (req: Http_types.request) outchan = | ""::id::tail | id::tail when id<>"" -> (fun id' -> -prerr_endline ("#### " ^ id ^ " :="); -List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; if id = id' then Some (List.map (fun u -> Netencoding.Url.decode u) tail) else @@ -409,25 +368,23 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; (fun _ -> None) choices in - let (id_to_uris : Disambiguate.domain_and_interpretation) = - parse_tokens [] (fun _ -> None) tokens in + let id_to_uris = + DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in 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 module Chat: Disambiguate.Callbacks = + 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 - let get_metasenv () = - !CicTextualParser0.metasenv - - let set_metasenv metasenv = - CicTextualParser0.metasenv := metasenv - - let output_html = prerr_endline - let interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~(title: string) ~(msg: string) @@ -439,7 +396,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in (match selection_mode with | `SINGLE -> assert false - | `EXTENDED -> + | `MULTIPLE -> Http_daemon.send_basic_headers ~code:200 outchan ; Http_daemon.send_CRLF outchan ; iter_file @@ -462,121 +419,31 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; 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) -> - (sprintf "alias %s %s" id value)) - l)) ^ - "\'") - interpretations) - in - let html_interpretations = - String.concat ", " - (List.map - (fun l -> - "\'" ^ - (String.concat " " - (List.map - (fun (id, value) -> - (sprintf "alias %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" - - end - in - let module Disambiguate' = Disambiguate.Make (Chat) in - let (id_to_uris', metasenv', term') = - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr id_to_uris - in - (match metasenv' with - | [] -> - let universe, - ((must_obj, must_rel, must_sort) as must'), - ((only_obj, only_rel, only_sort) as only) = - get_constraints term' req#path - in - let must'', only' = - (try - add_user_constraints - ~constraints:(req#param "constraints") - (must', only) - with Http_types.Param_not_found _ -> - let variables = - "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^ - "var constr_obj_len = " ^ - string_of_int (List.length must_obj) ^ ";\n" ^ - "var constr_rel_len = " ^ - string_of_int (List.length must_rel) ^ ";\n" ^ - "var constr_sort_len = " ^ - string_of_int (List.length must_sort) ^ ";\n" in - let form = - (if must_obj = [] then "" else - "

Obj constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_obj must_obj)) ^ - "
" ^ - (* The following three lines to make Javascript create *) - (* the constr_obj[] and obj_depth[] arrays even if we *) - (* have only one real entry. *) - "" ^ - "") ^ - (if must_rel = [] then "" else - "

Rel constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_rel must_rel)) ^ - "
" ^ - (* The following two lines to make Javascript create *) - (* the constr_rel[] and rel_depth[] arrays even if *) - (* we have only one real entry. *) - "" ^ - "") ^ - (if must_sort = [] then "" else - "

Sort constraints

" ^ - "" ^ - (String.concat "\n" (List.map html_of_r_sort must_sort)) ^ - "
" ^ - (* The following two lines to make Javascript create *) - (* the constr_sort[] and sort_depth[] arrays even if *) - (* we have only one real entry. *) - "" ^ - "") ^ - "

Only constraints

" ^ - "Enforce Only constraints for objects: " ^ - "
" ^ - "Enforce Rel constraints for objects: " ^ - "
" ^ - "Enforce Sort constraints for objects: " ^ - "
" + 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 ; @@ -584,53 +451,121 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; (fun line -> let processed_line = apply_substs - [form_RE, form ; - variables_initialization_RE, variables] line + [interpretations_RE, html_interpretations; + interpretations_labels_RE, html_interpretations_labels] + line in output_string outchan (processed_line ^ "\n")) - constraints_choice_TPL; - raise Chat_unfinished) - in - let query = - G.query_of_constraints (Some 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 = - match id_to_uris' with - | (domain, f) -> - String.concat ", " - (List.map - (fun name -> - sprintf "\'alias %s cic:%s\'" - (match name with - CicTextualParser0.Id name -> name - | _ -> assert false (*CSC: completare *)) - (match f name with - | None -> assert false - | Some (CicTextualParser0.Uri t) -> - MQueryMisc.string_of_cic_textual_parser_uri - t - | _ -> assert false (*CSC: completare *))) - domain) - 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 - | _ -> (* unable to instantiate some implicit variable *) - Http_daemon.respond - ~headers:[contype] - ~body:"some implicit variables are still unistantiated :-(" - outchan); - C.close mqi_handle + interactive_interpretation_choice_TPL; + raise Chat_unfinished + + let input_or_locate_uri ~title ?id () = + assert false + + end + in + let module Disambiguate' = DisambiguatingParser.Make(Chat) in + let (id_to_uris', metasenv', term') = + match + Disambiguate'.disambiguate_term mqi_handle + context metasenv term_string id_to_uris + with + [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term' + | _ -> assert false + in + let universe, + ((must_obj, must_rel, must_sort) as must'), + ((only_obj, only_rel, only_sort) as only) = + get_constraints term' req#path + in + let must'', only' = + (try + add_user_constraints + ~constraints:(req#param "constraints") + (must', only) + with Http_types.Param_not_found _ -> + let variables = + "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^ + "var constr_obj_len = " ^ + string_of_int (List.length must_obj) ^ ";\n" ^ + "var constr_rel_len = " ^ + string_of_int (List.length must_rel) ^ ";\n" ^ + "var constr_sort_len = " ^ + string_of_int (List.length must_sort) ^ ";\n" in + let form = + (if must_obj = [] then "" else + "

Obj constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_obj must_obj)) ^ + "
" ^ + (* The following three lines to make Javascript create *) + (* the constr_obj[] and obj_depth[] arrays even if we *) + (* have only one real entry. *) + "" ^ + "") ^ + (if must_rel = [] then "" else + "

Rel constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_rel must_rel)) ^ + "
" ^ + (* The following two lines to make Javascript create *) + (* the constr_rel[] and rel_depth[] arrays even if *) + (* we have only one real entry. *) + "" ^ + "") ^ + (if must_sort = [] then "" else + "

Sort constraints

" ^ + "" ^ + (String.concat "\n" (List.map html_of_r_sort must_sort)) ^ + "
" ^ + (* The following two lines to make Javascript create *) + (* the constr_sort[] and sort_depth[] arrays even if *) + (* we have only one real entry. *) + "" ^ + "") ^ + "

Only constraints

" ^ + "Enforce Only constraints for objects: " ^ + "
" ^ + "Enforce Rel constraints for objects: " ^ + "
" ^ + "Enforce Sort constraints for objects: " ^ + "
" + in + Http_daemon.send_basic_headers ~code:200 outchan ; + Http_daemon.send_CRLF outchan ; + iter_file + (fun line -> + let processed_line = + apply_substs + [form_RE, form ; + variables_initialization_RE, variables] line + in + output_string outchan (processed_line ^ "\n")) + constraints_choice_TPL; + raise Chat_unfinished) + in + let query = + 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 ; + (* CSC: Bug here: this is a string, not an array! *) + new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'"] + line + in + output_string outchan (processed_line ^ "\n")) + final_results_TPL | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print (sprintf "%s done!" req#path) @@ -639,15 +574,16 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan | exc -> - Http_daemon.respond - ~body:(pp_error ("Uncaught exception: " ^ (Printexc.to_string exc))) - outchan + let msg = sprintf "Uncaught exception: %s" (Printexc.to_string exc) in + debug_print msg ; + Http_daemon.respond ~body:(pp_error msg) outchan in printf "%s started and listening on port %d\n" daemon_name port; printf "Current directory is %s\n" (Sys.getcwd ()); printf "HTML directory is %s\n" pages_dir; flush stdout; Unix.putenv "http_proxy" ""; -Http_daemon.start' ~port callback; +let mqi_handle = C.init ~log:debug_print () in +Http_daemon.start' ~port (callback mqi_handle); +C.close mqi_handle; printf "%s is terminating, bye!\n" daemon_name -