From: Andrea Asperti Date: Wed, 16 Jun 2004 09:39:15 +0000 (+0000) Subject: first moogle commit X-Git-Tag: pre_subst_in_kernel~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13d18f963d7342cfeddf17f3ae222ff1b14404a8;p=helm.git first moogle commit --- diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html index 298193f44..f608b9d28 100644 --- a/helm/searchEngine/html/moogle.html +++ b/helm/searchEngine/html/moogle.html @@ -4,65 +4,53 @@ Moogle -
- - - -
matita
-
-
- - - - - - - - - - - - - - - - - - - - - + + + + - + + + - + + - + + + + + +
moogle   - -
- - - - + 		+ + + + + +     - Advanced search
- Preferences + Help
+ Input Syntax
+
- - - - + + + +
- -
+ +
+ @RESULTS@ + diff --git a/helm/searchEngine/html/moogle.png b/helm/searchEngine/html/moogle.png new file mode 100644 index 000000000..07570d07a Binary files /dev/null and b/helm/searchEngine/html/moogle.png differ diff --git a/helm/searchEngine/html/moogle_chat.html b/helm/searchEngine/html/moogle_chat.html new file mode 100644 index 000000000..627c625a6 --- /dev/null +++ b/helm/searchEngine/html/moogle_chat.html @@ -0,0 +1,19 @@ + + + + + + + +

+ + + +
+
Andrea Asperti
+ + +Last modified: Fri Jun 11 12:47:42 CEST 2004 + + + diff --git a/helm/searchEngine/html/moogle_chat1.html b/helm/searchEngine/html/moogle_chat1.html new file mode 100644 index 000000000..eb48d3d30 --- /dev/null +++ b/helm/searchEngine/html/moogle_chat1.html @@ -0,0 +1,83 @@ + + + +Moogle_chat1 + + +

There are more than one possible interpretations.

+
Please select one or more of the following: +
+
+ @CHOICES@ + + + + + + + + +

+ + + + + diff --git a/helm/searchEngine/html/moogle_chat2.html b/helm/searchEngine/html/moogle_chat2.html new file mode 100644 index 000000000..d3253f4fa --- /dev/null +++ b/helm/searchEngine/html/moogle_chat2.html @@ -0,0 +1,22 @@ + + + +Moogle_chat2 + + +

There are more than one possible interpretations.

+
Please choose one of the following. +
+ + + + + + + + @INTERPRETATIONS@ +

+ + + + diff --git a/helm/searchEngine/html/moogle_constraints_choice.html b/helm/searchEngine/html/moogle_constraints_choice.html new file mode 100644 index 000000000..b27dd93f1 --- /dev/null +++ b/helm/searchEngine/html/moogle_constraints_choice.html @@ -0,0 +1,90 @@ + + + +Moogle_constraints_choice + + +
+ + + + + + + + You can now proceed using the default generated constraints or you + can refine them by hand before going on.

+ + @FORM@ +
+ + + diff --git a/helm/searchEngine/html/moogle_help.html b/helm/searchEngine/html/moogle_help.html new file mode 100644 index 000000000..e6252cc28 --- /dev/null +++ b/helm/searchEngine/html/moogle_help.html @@ -0,0 +1,85 @@ + + + +Moogle_help + + + + + + + + + + + + + + + + + + + + + + + + +
moogle   + + + + + + +     + + Help
+ Input Syntax + +
+ + + + + + +
+ +
+ +
    + +
  • hint +
  • +
  • +
  • + +

    ccccccccccccc

    +
+ +

+ + Locate and display an object by its short name.
+ For instance + locating the identifier "nat" gives you back the definition of + natural numbers, and locating "plus" returns several (axiomatic and + concrete) definitions of the sum. +

+ +

+ + Given a closed statement G of the form +

+ \forall x1:T1...xn:Tn.body +
+ returns all theorems in the library whose conclusion is a generalization + of body, that is all theorems which can be used (as a last step) to prove G + (for tecnical reasons, the actual result may be a superset of + the expected one). +

+ + + + diff --git a/helm/searchEngine/html/moogle_init.html b/helm/searchEngine/html/moogle_init.html new file mode 100644 index 000000000..af4c26c26 --- /dev/null +++ b/helm/searchEngine/html/moogle_init.html @@ -0,0 +1,52 @@ + + + +Moogle + + +
+ + + +
moogle
+
+ + + + + + + + + + + + +
+ +
+ + + + + 		+ + Help
+ Input Syntax + +
+ + + + + + +
+ +
+ +@RESULTS@ + + + + diff --git a/helm/searchEngine/html/moogle_small.png b/helm/searchEngine/html/moogle_small.png new file mode 100644 index 000000000..a387d9a93 Binary files /dev/null and b/helm/searchEngine/html/moogle_small.png differ diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 87bcad36a..4c9f34989 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -39,25 +39,39 @@ open Printf;; let daemon_name = "Search Engine";; +let string_tail s = + let len = String.length s in + String.sub s 1 (len-1) + (* First of all we load the configuration *) let _ = - let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in + let configuration_file = "searchEngine.conf.xml" in 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 ^ "/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";; +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 final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; *) +let start_TPL = pages_dir ^ "/moogle.html";; +let final_results_TPL = pages_dir ^ "/moogle.html";; + +let my_own_url = + let ic = Unix.open_process_in "hostname -f" in + let hostname = input_line ic in + 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 *) let javascript_quote s = let rex = Pcre.regexp "'" in @@ -121,9 +135,9 @@ let theory_of_result result = "" ^ string_of_int !idx ^ "." ^ i ) result "" in - "

Query Results:

" ^ results ^ "
" + "Query Results:" ^ results ^ "
" else - "

Query Results:

No results found!

" + "Query Results:

No results found!

" ;; let pp_result result = @@ -150,19 +164,26 @@ let fold_file f init fname = (** 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) +let (expression_tag_RE, + action_tag_RE, + advanced_tag_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 "@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@") + (Pcre.regexp "@EXPRESSION@", + Pcre.regexp "@ACTION@", + Pcre.regexp "@ADVANCED@", + 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 port = Helm_registry.get_int "search_engine.port";; - let pp_error = sprintf "

Error: %s

";; let bad_request body outchan = @@ -176,17 +197,17 @@ let contype = "Content-Type", "text/html";; let get_constraints term = function - | "/locateInductivePrinciple" -> + | "/elim" -> None, (CGLocateInductive.get_constraints term), (None,None,None) - | "/searchPattern" -> + | "/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) - | "/matchConclusion" -> + | "/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 @@ -268,13 +289,343 @@ let add_user_constraints ~constraints | _ -> failwith ("Can't parse constraint string: " ^ constraints) in +let send_results results + ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") + (req: Http_types.request) outchan + = + Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; + Http_daemon.send_header "Content-Type" "text/xml" outchan; + Http_daemon.send_CRLF outchan ; + let subst = + (search_engine_url_RE, my_own_url) :: + (results_RE, theory_of_result results):: + (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)) + in + iter_file + (fun line -> + let new_aliases = + DisambiguatingParser.EnvironmentP3.to_string id_to_uris + in + let processed_line = + apply_substs + (* CSC: Bug here: this is a string, not an array! *) + ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) + line + in + output_string outchan (processed_line ^ "\n")) + final_results_TPL +in + +let exec_action mqi_handle (req: Http_types.request) outchan = + let term_string = req#param "expression" in + let (context, metasenv) = ([], []) in + let id_to_uris_raw = + try req#param "aliases" + with Http_types.Param_not_found _ -> "" + 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 + (fun f x -> + match Pcre.split ~pat:"\\s" x with + | ""::id::tail + | id::tail when id<>"" -> + (fun id' -> + 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 = + 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 interpretation_choices = + try + let choices_raw = req#param "interpretation_choices" in + if choices_raw = "" then None + else Some (parse_interpretation_choices choices_raw) + with Http_types.Param_not_found _ -> None + in + let module Chat: DisambiguateTypes.Callbacks = + struct + + 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)) + + 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 + + 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 _ -> + 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' + in + let results = MQueryInterpreter.execute mqi_handle query in + send_results results ~id_to_uris:id_to_uris' req outchan +in + (* 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 +in + +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 ^ + (String.concat "\n" valid_servers))) + outchan +in + +let proxy url outchan = + 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.http_get url) + outchan + else + Http_daemon.respond + ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) + outchan +in + 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 + | "/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 [] req outchan + else + let results = + let query = G.locate expression in + MQueryInterpreter.execute mqi_handle query + in + send_results results req outchan | "/execute" -> let query_string = req#param "query" in let lexbuf = Lexing.from_string query_string in @@ -282,11 +633,7 @@ let callback mqi_handle (req: Http_types.request) outchan = let result = MQueryInterpreter.execute mqi_handle query in let result_string = pp_result result in Http_daemon.respond ~body:result_string ~headers:[contype] outchan - | "/locate" -> - let id = req#param "id" in - let query = G.locate id in - let result = MQueryInterpreter.execute mqi_handle query in - Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan +(* Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan *) | "/unreferred" -> let target = req#param "target" in let source = req#param "source" in @@ -295,6 +642,8 @@ let callback mqi_handle (req: Http_types.request) outchan = Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) + let _ = prerr_endline + (Netencoding.Url.encode "http://mowgli.cs.unibo.it:38080/") in (let is_permitted _ = true in let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in let page = remove_fragment (req#param "url") in @@ -314,6 +663,9 @@ let callback mqi_handle (req: Http_types.request) outchan = (fun line -> output_string outchan ((apply_substs + ((search_engine_url_RE, my_own_url) :: + (advanced_tag_RE, "no") :: + (results_RE, "") :: (List.map (function (key,value) -> let key' = @@ -324,253 +676,19 @@ let callback mqi_handle (req: Http_types.request) outchan = (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.http_get url) - outchan - else - Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) - outchan - | "/searchPattern" - | "/matchConclusion" - | "/locateInductivePrinciple" -> - let term_string = req#param "term" in - let (context, metasenv) = ([], []) in - let id_to_uris_raw = req#param "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 - (fun f x -> - match Pcre.split ~pat:"\\s" x with - | ""::id::tail - | id::tail when id<>"" -> - (fun id' -> - 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 = - 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 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 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 - | `MULTIPLE -> - Http_daemon.send_basic_headers ~code:(`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 = - 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 - 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:(`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 ?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:(`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:(`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 + (* OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *) + | "/ask_uwobo" -> build_uwobo_request req outchan + | "/hint" + | "/match" + | "/elim" -> + exec_action mqi_handle req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) outchan);