X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;fp=helm%2FsearchEngine%2FsearchEngine.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=e4e33c629c4f808204dd2b48dcb03057fc6b8240;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml deleted file mode 100644 index e4e33c629..000000000 --- a/helm/searchEngine/searchEngine.ml +++ /dev/null @@ -1,651 +0,0 @@ -(* Copyright (C) 2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -module T = MQGTypes -module U = MQGUtil -module G = MQueryGenerator -module C = MQIConn - -open Http_types ;; - -let debug = true;; -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 *) -;; -let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";; -let interactive_interpretation_choice_TPL = - pages_dir ^ "/templateambigpdq2.html";; -let constraints_choice_TPL = pages_dir ^ "/constraints_choice_template.html";; -let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; - -exception Chat_unfinished - - (* build a bool from a 1-character-string *) -let bool_of_string' = function - | "0" -> false - | "1" -> true - | s -> failwith ("Can't parse a boolean from string: " ^ s) -;; - - (* build an int option from a string *) -let int_of_string' = function - | "_" -> None - | s -> - try - Some (int_of_string s) - with Failure "int_of_string" -> - failwith ("Can't parse an int option from string: " ^ s) -;; - - (* HTML pretty printers for mquery_generator types *) - -let html_of_r_obj (pos, uri) = - sprintf - "%s%s%s" - uri (U.text_of_position pos) - (if U.is_main_position pos then - sprintf "" - (U.text_of_depth pos "") - else - "") -;; - -let html_of_r_rel pos = - sprintf - "%s" - (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "") -;; - -let html_of_r_sort (pos, sort) = - sprintf - "%s%s" - (U.text_of_sort sort) (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "") -;; - - (** pretty print a MathQL query result to an HELM theory file *) -let theory_of_result result = - let results_no = List.length result in - if results_no > 0 then - let mode = if results_no > 10 then "linkonly" else "typeonly" in - let results = - let idx = ref (results_no + 1) in - List.fold_right - (fun (uri,attrs) i -> - decr idx ; - "" ^ string_of_int !idx ^ "." ^ i - ) result "" - in - "

Query Results:

" ^ results ^ "
" - else - "

Query Results:

No results found!

" -;; - -let pp_result result = - "\nQuery Results\n" ^ theory_of_result result ^ "" -;; - - (** chain application of Pcre substitutions *) -let rec apply_substs substs line = - match substs with - | [] -> line - | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line) - (** fold like function on files *) -let fold_file f init fname = - let inchan = open_in fname in - let rec fold_lines' value = - try - let line = input_line inchan in - fold_lines' (f value line) - with End_of_file -> value - in - let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in - close_in inchan; - res - (** iter like function on files *) -let iter_file f = fold_file (fun _ line -> f line) () - -let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, - interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, - form_RE, variables_initialization_RE) - = - (Pcre.regexp "@TITLE@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", - Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", - Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@", - Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", - 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 pp_error = sprintf "

Error: %s

";; - -let bad_request body outchan = - Http_daemon.respond_error ~status:(`Client_error `Bad_request) ~body outchan -;; - -let contype = "Content-Type", "text/html";; - -(* SEARCH ENGINE functions *) - -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) - | "/searchPattern" -> - let constr_obj, constr_rel, constr_sort = - CGSearchPattern.get_constraints term in - U.universe_for_search_pattern, - (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 - U.universe_for_match_conclusion, - (List.nth list_of_must block, [], []), (Some only, None, None) - | _ -> assert false -;; - -(* - format: - ':' ':' ':' ':' ':' - - ::= ('0'|'1') ('_'|) (',' ('0'|'1') ('_'|))* - ::= '0'|'1' -*) -let add_user_constraints ~constraints - ((obj, rel, sort), (only_obj, only_rel, only_sort)) -= - let parse_must s = - let l = Pcre.split ~pat:"," s in - (try - List.map - (fun s -> - let subs = Pcre.extract ~pat:"^(.)(\\d+|_)$" s in - (bool_of_string' subs.(1), int_of_string' subs.(2))) - l - with - Not_found -> failwith ("Can't parse constraint string: " ^ constraints) - ) - in - (* to be used on "obj" *) - let add_user_must33 user_must must = - List.map2 - (fun (b, i) (p, u) -> - if b then Some (U.set_full_position p i, u) else None) - user_must must - in - (* to be used on "rel" *) - let add_user_must22 user_must must = - List.map2 - (fun (b, i) p -> if b then Some (U.set_main_position p i) else None) - user_must must - in - (* to be used on "sort" *) - let add_user_must32 user_must must = - List.map2 - (fun (b, i) (p, s)-> if b then Some (U.set_main_position p i, s) else None) - user_must must - in - match Pcre.split ~pat:":" constraints with - | [user_obj;user_rel;user_sort;user_only_obj;user_only_rel;user_only_sort] -> - let - (user_obj,user_rel,user_sort,user_only_obj,user_only_rel,user_only_sort) - = - (parse_must user_obj, - parse_must user_rel, - parse_must user_sort, - bool_of_string' user_only_obj, - bool_of_string' user_only_rel, - bool_of_string' user_only_sort) - in - let only' = - (if user_only_obj then only_obj else None), - (if user_only_rel then only_rel else None), - (if user_only_sort then only_sort else None) - in - let must' = - let rec filter_some = - function - [] -> [] - | None::tl -> filter_some tl - | (Some x)::tl -> x::(filter_some tl) - in - filter_some (add_user_must33 user_obj obj), - filter_some (add_user_must22 user_rel rel), - filter_some (add_user_must32 user_sort sort) - in - (must', only') - | _ -> failwith ("Can't parse constraint string: " ^ constraints) -in - -(* HTTP DAEMON CALLBACK *) - -let callback (req: Http_types.request) outchan = - try - debug_print (sprintf "Received request: %s" req#path); - (match req#path with - | "/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; - Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan - | "/unreferred" -> - let mqi_handle = C.init mqi_flags debug_print in - 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 - C.close mqi_handle; - Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan - | "/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 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 (remove_fragment page) in - Http_daemon.send_basic_headers ~code:200 outchan; - Http_daemon.send_header "Content-Type" "text/html" outchan; - Http_daemon.send_CRLF outchan; - if preprocess then begin - iter_file - (fun line -> - output_string outchan - ((apply_substs - (List.map - (function (key,value) -> - let key' = - (Pcre.extract ~pat:"param\\.(.*)" key).(1) - in - Pcre.regexp ("@" ^ key' ^ "@"), value - ) - (List.filter - (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) - req#params) - ) - line) ^ - "\n")) - fname - end else - Http_daemon.send_file ~src:(FileSrc fname) outchan) - | page -> Http_daemon.respond_forbidden ~url:page outchan)) - | "/ask_uwobo" -> - let url = req#param "url" in - let server_and_port = - (Pcre.extract ~rex:server_and_port_url_RE url).(1) - in - if List.mem server_and_port valid_servers then - Http_daemon.respond - ~headers:["Content-Type", "text/html"] - ~body:(Http_client.Convenience.http_get url) - outchan - else - Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) - 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_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' -> -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 - f id') - | _ -> failwith "Can't parse choices") - (fun _ -> None) - choices - in - let (id_to_uris : Disambiguate.domain_and_interpretation) = - parse_tokens [] (fun _ -> None) tokens 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 = - 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) - ~(id: string) (choices: string list) - = - (match id_to_choices id with - | Some choices -> choices - | None -> - let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in - (match selection_mode with - | `SINGLE -> assert false - | `EXTENDED -> - Http_daemon.send_basic_headers ~code:200 outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let formatted_choices = - String.concat "," - (List.map (fun uri -> sprintf "\'%s\'" uri) choices) - in - let processed_line = - apply_substs - [title_tag_RE, title; - choices_tag_RE, formatted_choices; - msg_tag_RE, msg; - id_to_uris_RE, id_to_uris_raw; - id_RE, id] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_user_uri_choice_TPL; - 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)) ^ - "\'") - 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 - 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 (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 - | invalid_request -> - Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); - debug_print (sprintf "%s done!" req#path) - with - | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!" - | 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 -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; -printf "%s is terminating, bye!\n" daemon_name -