" ^
- (* 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
- "
" ^
- (* 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
- "
" ^
- (* 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 (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)
- 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
+ with
+ | Not_a_MutInd ->
+ send_results (`Error (MooglePp.pp_error "Not an inductive type"
+ ("elim requires as input an identifier corresponding to an inductive"
+ ^ " type")))
+ req outchan
-let callback mqi_handle (req: Http_types.request) outchan =
+let callback dbd (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
- (let is_permitted _ = true in
- let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
- let page = remove_fragment (req#param "url") in
+ (* TODO implement "is_permitted" *)
+ (let is_permitted page = not (Pcre.pmatch ~pat:"/" page) in
+ let page = req#param "url" in
+ let fname = sprintf "%s/%s" pages_dir page 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
+ | page when is_permitted page && Sys.file_exists fname ->
Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
Http_daemon.send_header "Content-Type" "text/html" outchan;
Http_daemon.send_CRLF outchan;
@@ -706,55 +382,79 @@ 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' =
- (Pcre.extract ~pat:"param\\.(.*)" key).(1)
- in
- Pcre.regexp ("@" ^ key' ^ "@"), value
- )
- (List.filter
- (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key)
- req#params)
- ))
+ ((tag "SEARCH_ENGINE_URL", my_own_url) ::
+ (tag "ADVANCED", "no") ::
+ (tag "RESULTS", "") ::
+ 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 begin
+ let results = MetadataQuery.locate ~dbd expression in
+ send_results (`Results results) req outchan
+ end
+ | "/hint"
+ | "/elim"
+ | "/match" -> exec_action dbd 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!"
+ | Chat_unfinished -> ()
| 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
+ | CicTextualParser2.Parse_error (_, msg) ->
+ 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 restore_environment () =
+ match
+ Helm_registry.get_opt Helm_registry.get "search_engine.environment_dump"
+ with
+ | None -> ()
+ | Some fname ->
+ printf "Restoring Cic environment from %s ... " fname; flush stdout;
+ let ic = open_in fname in
+ CicEnvironment.restore_from_channel ic;
+ close_in ic;
+ printf "done!\n"; flush stdout
+
let _ =
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" "";
- let mqi_handle = C.init ~log:debug_print () in
- Http_daemon.start' ~port (callback mqi_handle);
- C.close mqi_handle;
+ let dbd =
+ Mysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~database:(Helm_registry.get "db.database")
+ ~user:(Helm_registry.get "db.user")
+ ()
+ in
+ restore_environment ();
+ Http_daemon.start' ~port (callback dbd);
printf "%s is terminating, bye!\n" daemon_name