From: Claudio Sacerdoti Coen Date: Tue, 9 Mar 2004 10:43:54 +0000 (+0000) Subject: - non empty metasenv after the parsing phase are now accepted X-Git-Tag: v0_0_4~29 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d4edf383bab53053da30ab591dc0d3140adec34;p=helm.git - non empty metasenv after the parsing phase are now accepted - still many bugs open (due to the new aliases for symbols) --- diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 2d8a7067c..e5cb733bf 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -30,7 +30,7 @@ module C = MQIConn open Http_types ;; -let debug = false;; +let debug = true;; let debug_print s = if debug then prerr_endline s;; Http_common.debug := true;; (* Http_common.debug := true;; *) @@ -59,6 +59,11 @@ let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; exception Chat_unfinished +let javascript_quote = + let rex = Pcre.regexp "'" in + Pcre.replace ~rex ~templ:"\\'" +;; + (* build a bool from a 1-character-string *) let bool_of_string' = function | "0" -> false @@ -430,7 +435,9 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id (String.concat "
" (List.map (fun (id, value) -> - (sprintf "alias id %s = %s" id value)) + let id = javascript_quote id in + let value = javascript_quote value in + sprintf "alias id %s = %s" id value) l)) ^ "\'") interpretations) @@ -443,10 +450,12 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id (String.concat " " (List.map (fun (id, value) -> - (sprintf "alias id %s = %s" + let id = javascript_quote id in + let value = javascript_quote value in + sprintf "alias id %s = %s" id (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - value))) + value)) l)) ^ "\'") interpretations) @@ -479,124 +488,117 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term' | _ -> assert false 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 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 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 (*XXX - 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 + 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) + 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 | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print (sprintf "%s done!" req#path) @@ -605,9 +607,9 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id | 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 ());