From: Stefano Zacchiroli Date: Mon, 25 Oct 2004 12:48:58 +0000 (+0000) Subject: - reimplemented basic features using the helm-metadata library instead X-Git-Tag: V_0_0_10~17 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git - reimplemented basic features using the helm-metadata library instead of MathQL. Previous version has been tagged "moogle_mathql" --- diff --git a/helm/searchEngine/.depend b/helm/searchEngine/.depend new file mode 100644 index 000000000..508403bdc --- /dev/null +++ b/helm/searchEngine/.depend @@ -0,0 +1,2 @@ +mooglePp.cmo: mooglePp.cmi +mooglePp.cmx: mooglePp.cmi diff --git a/helm/searchEngine/Makefile b/helm/searchEngine/Makefile index 519629b54..b0836f5b0 100644 --- a/helm/searchEngine/Makefile +++ b/helm/searchEngine/Makefile @@ -1,29 +1,40 @@ -REQUIRES = http helm-cic_textual_parser2 helm-cic_proof_checking \ - helm-xml gdome2-xslt helm-cic_unification helm-mathql \ - helm-mathql_interpreter helm-mathql_generator helm-logger \ - helm-tex_cic_textual_parser helm-tactics -OCAMLOPTIONS = -thread -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel +REQUIRES = http dbi.mysql helm-cic_textual_parser2 helm-logger helm-tactics +OCAMLOPTIONS = -thread -package "$(REQUIRES)" -pp camlp4o OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamlfind ocamldep -package "$(REQUIRES)" -pp camlp4o -GTOPLEVEL_MODULES = oldDisambiguate disambiguatingParser -MODULES = +MODULES = mooglePp +SRCS = $(patsubst %,%.ml,$(MODULES)) $(patsubst %,%.mli,$(MODULES)) \ + searchEngine.ml CMOS = $(patsubst %,%.cmo,$(MODULES)) CMXS = $(patsubst %,%.cmx,$(MODULES)) -LIBRARIES = $(patsubst %,../gTopLevel/%.cmo,$(GTOPLEVEL_MODULES)) -LIBRARIES_OPT = $(patsubst %,../gTopLevel/%.cmx,$(GTOPLEVEL_MODULES)) all: byte world: byte opt byte: searchEngine opt: searchEngine.opt -searchEngine: $(LIBRARIES) $(CMOS) searchEngine.ml +%.cmi: %.mli + $(OCAMLC) -c $< +%.cmo %.cmi: %.ml + $(OCAMLC) -c $< +%.cmx: %.ml + $(OCAMLOPT) -c $< + +searchEngine: $(CMOS) searchEngine.ml $(OCAMLC) -linkpkg -o $@ $^ -searchEngine.opt: $(LIBRARIES_OPT) $(CMXS) searchEngine.ml +searchEngine.opt: $(CMXS) searchEngine.ml $(OCAMLOPT) -linkpkg -o $@ $^ clean: rm -f *.cm[aiox] *.o searchEngine{,.opt} +.PHONY: depend +depend: + $(OCAMLDEP) $(SRCS) > .depend + .PHONY: all opt clean + +include .depend + diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml new file mode 100644 index 000000000..807fcc219 --- /dev/null +++ b/helm/searchEngine/mooglePp.ml @@ -0,0 +1,80 @@ + +open Printf + +let pp_request (req: Http_types.request) = + match req#path with + | "/elim" -> "Elim" + | "/match" -> "Match" + | "/hint" -> "Hint" + | "/locate" -> "Locate" + | _ -> assert false + +let pp_error title msg = + sprintf "
%s: %s
" title msg + + (** pretty print a list of URIs to an HELM theory file *) +let theory_of_result req result = + let max_results_no = + Helm_registry.get_opt_default Helm_registry.get_int 10 + "search_engine.max_results_no" + in + let results_no = List.length result in + let query_kind = pp_request req in + let template query_kind summary results = + sprintf + "
+ + + + + +
%s%s
+
+
+
+ %s +
" + query_kind summary results + in + if results_no > 0 then + let mode = if results_no > max_results_no then "linkonly" else "typeonly" in + let results = + let idx = ref (results_no + 1) in + List.fold_right + (fun uri i -> + decr idx ; + sprintf + " + %d. + + %s" + !idx uri mode i) + result "" + in + template query_kind + (sprintf "%d result%s found" + results_no (if results_no > 1 then "s" else "")) + (sprintf + " + %s +
" + results) + else + template query_kind "no results found" "" + +let html_of_interpretations interps = + let radio_button n = + sprintf "" n + in + let text interp = + String.concat "
" + (List.map + (fun (id, value) -> sprintf "%s = %s" id value) + interp) + in + let rec aux n = function + | [] -> [] + | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl) + in + String.concat "
" (aux 0 interps) + diff --git a/helm/searchEngine/mooglePp.mli b/helm/searchEngine/mooglePp.mli new file mode 100644 index 000000000..1cea1074f --- /dev/null +++ b/helm/searchEngine/mooglePp.mli @@ -0,0 +1,3 @@ +val pp_error : string -> string -> string +val theory_of_result : Http_types.request -> string list -> string +val html_of_interpretations: (string * string) list list -> string diff --git a/helm/searchEngine/searchEngine.conf.xml.sample b/helm/searchEngine/searchEngine.conf.xml.sample index 435552e44..728b7c632 100644 --- a/helm/searchEngine/searchEngine.conf.xml.sample +++ b/helm/searchEngine/searchEngine.conf.xml.sample @@ -1,21 +1,9 @@ -
- mathql_db_map.txt -
+
mowgli.cs.unibo.it - mowgli - - helm -
- dbname=mowgli host=mowgli.cs.unibo.it user=helm password=awH21Un - - - - - - + mowgli
remote @@ -24,6 +12,5 @@
html 58085 - mowgli.cs.unibo.it:58080 mowgli.cs.unibo.it localhost:58080
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 1c58e5d29..bc4cd729a 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -23,44 +23,49 @@ * http://cs.unibo.it/helm/. *) -module T = MQGTypes -module U = MQGUtil -module G = MQueryGenerator -module C = MQIConn +open Printf -open Http_types +module DB = Dbi_mysql let debug = true let debug_print s = if debug then prerr_endline s -let _ = Http_common.debug := true -(* let _ = Http_common.debug := false *) - -open Printf +let _ = Http_common.debug := false -let daemon_name = "Search Engine" +exception Chat_unfinished +exception Unbound_identifier of string +exception Invalid_action of string (* invalid action for "/search" method *) -let string_tail s = - let len = String.length s in - String.sub s 1 (len-1) +let daemon_name = "Moogle" +let configuration_file = "searchEngine.conf.xml" + +let expression_tag_RE = Pcre.regexp "@EXPRESSION@" +let action_tag_RE = Pcre.regexp "@ACTION@" +let advanced_tag_RE = Pcre.regexp "@ADVANCED@" +let advanced_checked_RE = Pcre.regexp "@ADVANCED_CHECKED@" +let simple_checked_RE = Pcre.regexp "@SIMPLE_CHECKED@" +let title_tag_RE = Pcre.regexp "@TITLE@" +let no_choices_tag_RE = Pcre.regexp "@NO_CHOICES@" +let current_choices_tag_RE = Pcre.regexp "@CURRENT_CHOICES@" +let choices_tag_RE = Pcre.regexp "@CHOICES@" +let msg_tag_RE = Pcre.regexp "@MSG@" +let id_to_uris_RE = Pcre.regexp "@ID_TO_URIS@" +let id_RE = Pcre.regexp "@ID@" +let iden_tag_RE = Pcre.regexp "@IDEN@" +let interpretations_RE = Pcre.regexp "@INTERPRETATIONS@" +let interpretations_labels_RE = Pcre.regexp "@INTERPRETATIONS_LABELS@" +let results_RE = Pcre.regexp "@RESULTS@" +let new_aliases_RE = Pcre.regexp "@NEW_ALIASES@" +let form_RE = Pcre.regexp "@FORM@" +let variables_initialization_RE = Pcre.regexp "@VARIABLES_INITIALIZATION@" +let search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@" +let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" (* 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 max_results_no = - Helm_registry.get_opt_default Helm_registry.get_int 10 - "search_engine.max_results_no" - +let _ = Helm_registry.load_from configuration_file let port = Helm_registry.get_int "search_engine.port" - 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 ^ "/moogle_chat1.html" let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html" -let constraints_choice_TPL = pages_dir ^ "/moogle_constraints_choice.html" let moogle_TPL = pages_dir ^ "/moogle.html" let my_own_url = @@ -69,117 +74,9 @@ let my_own_url = ignore (Unix.close_process_in ic); sprintf "http://%s:%d" hostname port -exception Chat_unfinished -exception Invalid_action of string (* invalid action for "/search" method *) -exception Unbound_identifier of string - -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 - | "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) "") - -let query_of_req (req: Http_types.request) = - match req#path with - | "/elim" -> "Elim" - | "/match" -> "Match" - | "/hint" -> "Hint" - | "/locate" -> "Locate" - | _ -> assert false - - (** pretty print a MathQL query result to an HELM theory file *) -let theory_of_result req result = - let results_no = List.length result in - let query_kind = query_of_req req in - let template query_kind summary results = - sprintf - "
- - - - - -
%s%s
-
-
-
- %s -
" - query_kind summary results - in - if results_no > 0 then - let mode = if results_no > max_results_no then "linkonly" else "typeonly" in - let results = - let idx = ref (results_no + 1) in - List.fold_right - (fun uri i -> - decr idx ; - sprintf - " - %d. - - %s" - !idx uri mode i) - result "" - in - template query_kind - (sprintf "%d result%s found" - results_no (if results_no > 1 then "s" else "")) - (sprintf - " - %s -
" - results) - else - template query_kind "no results found" "" - -let pp_result req result = - sprintf - " - - Query results - - - %s - " - (theory_of_result req result) +let bad_request body outchan = + Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body + outchan (** chain application of Pcre substitutions *) let rec apply_substs substs line = @@ -200,131 +97,26 @@ let fold_file f init fname = res (** iter like function on files *) let iter_file f = fold_file (fun _ line -> f line) () +let javascript_quote s = + let rex = Pcre.regexp "'" in + let rex' = Pcre.regexp "\"" in + Pcre.replace ~rex ~templ:"\\'" + (Pcre.replace ~rex:rex' ~templ:"\\\"" s) +let string_tail s = + let len = String.length s in + String.sub s 1 (len-1) -let (expression_tag_RE, action_tag_RE, advanced_tag_RE, - advanced_checked_RE, simple_checked_RE, - title_tag_RE, no_choices_tag_RE, current_choices_tag_RE, - choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, iden_tag_RE, - interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, - form_RE, variables_initialization_RE, search_engine_url_RE) - = - (Pcre.regexp "@EXPRESSION@", Pcre.regexp "@ACTION@", Pcre.regexp "@ADVANCED@", - Pcre.regexp "@ADVANCED_CHECKED@", Pcre.regexp "@SIMPLE_CHECKED@", - Pcre.regexp "@TITLE@", Pcre.regexp "@NO_CHOICES@", - Pcre.regexp "@CURRENT_CHOICES@", - Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", - Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", Pcre.regexp "@IDEN@", - Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@", - Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@", - Pcre.regexp "@VARIABLES_INITIALIZATION@", Pcre.regexp "@SEARCH_ENGINE_URL@") -let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" - -(* let pp_error = sprintf "

Error: %s

" *) -let pp_error title msg = - sprintf "
%s: %s
" title msg - -let bad_request body outchan = - Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body - outchan - -let contype = "Content-Type", "text/html" - -(* SEARCH ENGINE functions *) - -let get_constraints term = - function - | "/elim" -> - None, - (CGLocateInductive.get_constraints term), - (None,None,None) - | "/match" -> - 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) - | "/hint" -> - 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 - -(* - 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) +let add_param_substs params = + List.map + (fun (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) + params) let send_results results - ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") + ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") (req: Http_types.request) outchan = Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; @@ -332,7 +124,7 @@ let send_results results Http_daemon.send_CRLF outchan ; let results_string = match results with - | `Results r -> theory_of_result req r + | `Results r -> MooglePp.theory_of_result req r | `Error msg -> msg in let subst = @@ -340,13 +132,7 @@ let send_results results (results_RE, results_string):: (advanced_tag_RE, req#param "advanced"):: (expression_tag_RE, req#param "expression"):: - (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)) @ + add_param_substs req#params @ (if req#param "advanced" = "no" then [ simple_checked_RE, "checked='true'"; advanced_checked_RE, "" ] @@ -357,7 +143,7 @@ let send_results results iter_file (fun line -> let new_aliases = - DisambiguatingParser.EnvironmentP3.to_string id_to_uris + CicTextualParser2.EnvironmentP3.to_string id_to_uris in let processed_line = apply_substs @@ -368,8 +154,8 @@ let send_results results output_string outchan (processed_line ^ "\n")) moogle_TPL -let exec_action mqi_handle (req: Http_types.request) outchan = - let term_string = req#param "expression" in +let exec_action dbh (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" @@ -393,12 +179,10 @@ let exec_action mqi_handle (req: Http_types.request) outchan = (fun _ -> None) choices in - let id_to_uris = - DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in + let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in let id_to_choices = try - let choices_raw = req#param "choices" in - parse_choices choices_raw + parse_choices (req#param "choices") with Http_types.Param_not_found _ -> (fun _ -> None) in let interpretation_choices = @@ -410,310 +194,83 @@ let exec_action mqi_handle (req: Http_types.request) outchan = in let module Chat: DisambiguateTypes.Callbacks = struct - - let interactive_user_uri_choice - ~selection_mode ?ok + 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 -> - if req#param "advanced" = "no" then - let isvar s = - let len = String.length s in - let suffix = String.sub s (len-4) 4 in - not (suffix = ".var") in - List.filter isvar choices - else - let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in - (match selection_mode with - | `SINGLE -> assert false - | `MULTIPLE -> - Http_daemon.send_basic_headers ~code:(`Code 200) outchan; - Http_daemon.send_CRLF outchan ; - let check_box uri = - "" ^ "" ^ uri ^ "" in -(* aggiungere gli hyperlinks? *) - let check_boxes = - String.concat "
" - (List.map check_box choices) in - iter_file - (fun line -> - let processed_line = - apply_substs - [advanced_tag_RE, req#param "advanced"; - choices_tag_RE, check_boxes; - no_choices_tag_RE, - string_of_int (List.length choices); - iden_tag_RE, id; - current_choices_tag_RE, req#param "choices"; - expression_tag_RE, req#param "expression"; - action_tag_RE, string_tail req#path ] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_user_uri_choice_TPL; - raise Chat_unfinished)) + = + match id_to_choices id with + | Some choices -> choices + | None -> assert false let interactive_interpretation_choice interpretations = match interpretation_choices with - Some l -> prerr_endline "CARRAMBA" ; l - | None -> - let html_interpretations = - let radio_button n = - "" in - let text interp = - String.concat "
" - (List.map - (fun (id, value) -> - sprintf "%s = %s" id value) - interp) in - let rec aux n = - function - [] -> [] - | interp::tl -> - ((radio_button n)^(text interp))::(aux (n+1) tl) in - String.concat "
" (aux 0 interpretations) - in - Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [advanced_tag_RE, req#param "advanced"; - interpretations_RE, html_interpretations; - current_choices_tag_RE, req#param "choices"; - expression_tag_RE, req#param "expression"; - action_tag_RE, string_tail req#path ] - line - in - output_string outchan (processed_line ^ "\n")) - interactive_interpretation_choice_TPL; - raise Chat_unfinished + | Some l -> prerr_endline "CARRAMBA" ; 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 ; + iter_file + (fun line -> + let processed_line = + apply_substs + [advanced_tag_RE, req#param "advanced"; + interpretations_RE, html_interpretations; + current_choices_tag_RE, req#param "choices"; + expression_tag_RE, req#param "expression"; + action_tag_RE, string_tail req#path ] + line + in + output_string outchan (processed_line ^ "\n")) + interactive_interpretation_choice_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' = DisambiguatingParser.Make(Chat) in - let (id_to_uris', metasenv', term') = + 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 mqi_handle - context metasenv term_string id_to_uris + Disambiguate'.disambiguate_term dbh context metasenv ast 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 - if - (try ignore (req#param "constraints"); false - with Http_types.Param_not_found _ -> true) && - (req#param "advanced" = "no") && (req#path = "/hint") - then - let dbd = - match mqi_handle.MQIConn.pgc with - | MQIConn.MySQL_C conn -> conn - | _ -> assert false - in -(* - (* ZACK: constraints sulla conclusione, no apply *) - let results = List.map snd (Match_concl.cmatch dbd term') in -*) - (* ZACK: constraints sulle costanti + apply *) - let status = ProofEngineTypes.initial_status term' [] in - let intros = PrimitiveTactics.intros_tac () in - let subgoals = ProofEngineTypes.apply_tactic intros status in - let results = - match subgoals with - | proof, [goal] -> - let (uri,metasenv,bo,ty) = proof in - TacticChaser.searchTheorems_for_hint mqi_handle (proof, goal) - | _ -> assert false - in - send_results (`Results results) ~id_to_uris:id_to_uris' req outchan - else - let must'', only' = - (try - add_user_constraints - ~constraints:(req#param "constraints") - (must', only) - with Http_types.Param_not_found _ -> - if req#param "advanced" = "no" then - (must',only) - else - 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:(`Code 200) outchan ; - Http_daemon.send_CRLF outchan ; - iter_file - (fun line -> - let processed_line = - apply_substs - [form_RE, form ; - variables_initialization_RE, variables; - advanced_tag_RE, req#param "advanced"; - current_choices_tag_RE, req#param "choices"; - interpretations_RE, req#param "interpretation_choices"; - expression_tag_RE, req#param "expression"; - action_tag_RE, string_tail req#path] line - in - output_string outchan (processed_line ^ "\n")) - constraints_choice_TPL; - raise Chat_unfinished) - in - let query = - G.query_of_constraints universe must'' only' + | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term + | _ -> assert false in - let results = MQueryInterpreter.execute mqi_handle query in - send_results (`Results (List.map fst results)) - ~id_to_uris:id_to_uris' req outchan - -(* HTTP DAEMON CALLBACK *) - -let build_dynamic_uri url params = - let p = - String.concat "&" (List.map (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in - url ^ "?" ^ p - -let build_uwobo_request (req: Http_types.request) outchan = - prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL"); - let xmluri = build_dynamic_uri ((req#param "param.SEARCH_ENGINE_URL") ^ "/search") req#params in - prerr_endline ("xmluri: " ^ xmluri); - (*let xmluri = Netencoding.Url.encode xmluri in*) - let server_and_port = req#param "param.processorURL" in - let newreq = - build_dynamic_uri - (server_and_port ^ "apply") - (("xmluri",xmluri)::("keys",(req#param "param.thkeys"))::req#params) in - (* if List.mem server_and_port valid_servers then *) - prerr_endline newreq; - if true then - Http_daemon.respond - ~headers:["Content-Type", "text/html"] - ~body:(Http_client.http_get newreq) - outchan - else - Http_daemon.respond - ~body:(pp_error "Untrusted UWOBO server" server_and_port) - outchan - -let proxy url outchan = - let server_and_port = - (Pcre.extract ~rex:server_and_port_url_RE url).(1) + let uris = + match req#path with + | "/match" -> MetadataQuery.match_term ~dbh term + | "/hint" -> + let status = ProofEngineTypes.initial_status term [] 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 ~dbh (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 ~dbh uri + | _ -> assert false in - if List.mem server_and_port valid_servers then - Http_daemon.respond - ~headers:["Content-Type", "text/html"] - ~body:(Http_client.http_get url) - outchan - else - Http_daemon.respond - ~body:(pp_error "Untrusted UWOBO server" server_and_port) - outchan + send_results ~id_to_uris (`Results uris) req outchan -let callback mqi_handle (req: Http_types.request) outchan = +let callback dbh (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 - | "/locate" -> - let initial_expression = - try req#param "expression" with Http_types.Param_not_found _ -> "" - in - let expression = - Pcre.replace ~pat:"\\s*$" - (Pcre.replace ~pat:"^\\s*" initial_expression) - in - if expression = "" then - send_results (`Results []) req outchan - else - let results = - let query = G.locate expression in - MQueryInterpreter.execute mqi_handle query - in - send_results (`Results (List.map fst results)) req outchan - | "/execute" -> - 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 req (List.map fst result) in - Http_daemon.respond ~body:result_string ~headers:[contype] outchan -(* Http_daemon.respond ~headers:[contype] ~body:(pp_result req 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 req (List.map fst result)) outchan | "/getpage" -> - (* TODO implement "is_permitted" *) - let _ = prerr_endline - (Netencoding.Url.encode "http://mowgli.cs.unibo.it:38080/") in + (* 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 @@ -736,42 +293,46 @@ let callback mqi_handle (req: Http_types.request) outchan = ((search_engine_url_RE, my_own_url) :: (advanced_tag_RE, "no") :: (results_RE, "") :: - (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) - )) + add_param_substs req#params) line) ^ "\n")) fname end else - Http_daemon.send_file ~src:(FileSrc fname) outchan) + Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan) | page -> Http_daemon.respond_forbidden ~url:page outchan)) - (* OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *) - | "/ask_uwobo" -> build_uwobo_request req outchan - | "/hint" | "/match" | "/elim" -> exec_action mqi_handle req outchan + | "/help" -> Http_daemon.respond ~body:daemon_name outchan + | "/locate" -> + let initial_expression = + try req#param "expression" with Http_types.Param_not_found _ -> "" + in + let expression = + Pcre.replace ~pat:"\\s*$" + (Pcre.replace ~pat:"^\\s*" initial_expression) + in + if expression = "" then + send_results (`Results []) req outchan + else + let results = MetadataQuery.locate ~dbh expression in + send_results (`Results results) req outchan + | "/hint" + | "/elim" + | "/match" -> exec_action dbh req outchan | invalid_request -> Http_daemon.respond_error ~code:(`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 | CicTextualParser2.Parse_error msg -> - send_results (`Error (pp_error "Parse_error" msg)) req outchan + send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan | Unbound_identifier id -> - send_results (`Error (pp_error "Unbound identifier" id)) req outchan + send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req + outchan | exn -> let exn_string = Printexc.to_string exn in debug_print exn_string; - let msg = pp_error "Uncaught exception" exn_string in + let msg = MooglePp.pp_error "Uncaught exception" exn_string in send_results (`Error msg) req outchan let _ = @@ -780,8 +341,10 @@ let _ = printf "HTML directory is %s\n" pages_dir; flush stdout; Unix.putenv "http_proxy" ""; - let mqi_handle = C.init ~log:debug_print () in - Http_daemon.start' ~port (callback mqi_handle); - C.close mqi_handle; + let dbh = + new DB.connection ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database") + in + Http_daemon.start' ~port (callback dbh); printf "%s is terminating, bye!\n" daemon_name