X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=b7c24137194a297fb204f75a13dc6dbb8c1a87d3;hb=1bfef566743ddd81db375cf66ed3868c5d7df542;hp=0e28725feabcb510f10ae95754fca67919c7f5f5;hpb=09151f33b14507e4d20380f3100a6db5f49f3f46;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 0e28725fe..b7c241371 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -47,11 +47,67 @@ let pages_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 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) +;; + +let is_concl_pos pos = + pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + or + pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" +;; + +let is_main_pos pos = + pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + or + pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" +;; + + (* HTML pretty printers for mquery_generator types *) + +let html_of_r_obj (uri, pos, depth) = + sprintf + "%s%s%s" + uri (Str.string_after pos ((String.rindex pos '#') + 1)) + (if is_main_pos pos then + sprintf "" + (match depth with Some i -> string_of_int i | None -> "") + else + "") +;; + +let html_of_r_rel (pos, depth) = + sprintf + "%s" + pos (match depth with Some i -> string_of_int i | None -> "") +;; + +let html_of_r_sort (pos, depth, sort) = + sprintf + "%s%s" + sort pos (match depth with Some i -> string_of_int i | None -> "") +;; + (** pretty print a MathQL query result to an HELM theory file *) let theory_of_result result = let results_no = List.length result in @@ -95,12 +151,14 @@ let fold_file f init fname = 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) + 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 "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", + Pcre.regexp "@VARIABLES_INITIALIZATION@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" exception NotAnInductiveDefinition @@ -132,11 +190,8 @@ let refine_constraints (constr_obj, constr_rel, constr_sort) = List.map (function (uri,pos,_) -> (uri,pos,None)) (List.filter - (function (uri,pos,depth) as constr -> - pos="http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" - or - pos="http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" - ) constr_obj) + (function (uri,pos,depth) as constr -> is_concl_pos pos) + constr_obj) in (*CSC: we must select the must constraints here!!! *) (constr_obj',[],[]),(Some constr_obj', None, None) @@ -171,6 +226,72 @@ let get_constraints term = refine_constraints must req_path in +(* + 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) (p1, p2, p3) -> if b then (p1, p2, i) else (p1, p2, None)) + user_must must + in + (* to be used on "rel" *) + let add_user_must22 user_must must = + List.map2 + (fun (b, i) (p1, p2) -> if b then (p1, i) else (p1, None)) + user_must must + in + (* to be used on "sort" *) + let add_user_must32 user_must must = + List.map2 + (fun (b, i) (p1, p2, p3) -> if b then (p1, i, p3) else (p1, None, p3)) + 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' = + add_user_must33 user_obj obj, + add_user_must22 user_rel rel, + 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 = @@ -184,13 +305,13 @@ let callback (req: Http_types.request) outchan = let query = MQueryUtil.query_of_text lexbuf in let result = MQueryGenerator.execute_query mqi_handle query in let result_string = pp_result result in - MQIConn.close mqi_handle; + MQIConn.close mqi_handle; Http_daemon.respond ~body:result_string ~headers:[contype] outchan | "/locate" -> let mqi_handle = MQIConn.init mqi_flags debug_print in let id = req#param "id" in let result = MQueryGenerator.locate mqi_handle id in - MQIConn.close mqi_handle; + MQIConn.close mqi_handle; Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) @@ -316,7 +437,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; (match id_to_choices id with | Some choices -> choices | None -> - let msg = Pcre.replace ~pat:"\"" ~templ:"\\\"" msg in + let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in (match selection_mode with | `SINGLE -> assert false | `EXTENDED -> @@ -326,7 +447,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; (fun line -> let formatted_choices = String.concat "," - (List.map (fun uri -> sprintf "\"%s\"" uri) choices) + (List.map (fun uri -> sprintf "\'%s\'" uri) choices) in let processed_line = apply_substs @@ -346,20 +467,20 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; 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) -> @@ -368,7 +489,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' value))) l)) ^ - "\"") + "\'") interpretations) in Http_daemon.send_basic_headers ~code:200 outchan ; @@ -397,8 +518,81 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; in (match metasenv' with | [] -> - let must',only = get_constraints term' req#path in - let results = MQueryGenerator.searchPattern mqi_handle must' only in + let ((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 results = + MQueryGenerator.searchPattern mqi_handle must'' only' in Http_daemon.send_basic_headers ~code:200 outchan ; Http_daemon.send_CRLF outchan ; iter_file @@ -409,7 +603,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; String.concat ", " (List.map (fun name -> - sprintf "\"alias %s cic:%s\"" + sprintf "\'alias %s cic:%s\'" (match name with CicTextualParser0.Id name -> name | _ -> assert false (*CSC: completare *)) @@ -434,7 +628,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; ~headers:[contype] ~body:"some implicit variables are still unistantiated :-(" outchan); - MQIConn.close mqi_handle + MQIConn.close mqi_handle | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print (sprintf "%s done!" req#path)