* http://cs.unibo.it/helm/.
*)
+open Http_types ;;
+
let debug = true;;
let debug_print s = if debug then prerr_endline s;;
Http_common.debug := true;;
(* Http_common.debug := true;; *)
(** accepted HTTP servers for ask_uwobo method forwarding *)
-let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "localhost:58080" ] ;;
+let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ] ;;
-open Printf;;
+module MQICallbacks =
+ struct
+ let log s = debug_print s
+ end
-let postgresConnectionString =
- try
- Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
- Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
+module MQI = MQueryInterpreter.Make(MQICallbacks)
+
+let mqi_options = "" (* default MathQL interpreter options *)
+
+open Printf;;
let daemon_name = "Search Engine";;
let default_port = 58085;;
Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@")
let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
+exception NotAnInductiveDefinition
+
let port =
try
int_of_string (Sys.getenv port_env_var)
(* SEARCH ENGINE functions *)
-let refine_constraints (x, y, z) = (x, y, z), (Some x, Some y, Some z) in
+let refine_constraints (constr_obj, constr_rel, constr_sort) =
+ function
+ "/searchPattern" ->
+ (constr_obj, constr_rel, constr_sort),
+ (Some constr_obj, Some constr_rel, Some constr_sort)
+ | "/matchConclusion" ->
+ let constr_obj' =
+ 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)
+ in
+ (*CSC: we must select the must constraints here!!! *)
+ (constr_obj',[],[]),(Some constr_obj', None, None)
+ | _ -> assert false
+in
+
+let get_constraints term =
+ function
+ "/locateInductivePrinciple" ->
+ let uri =
+ match term with
+ Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
+ | _ -> raise NotAnInductiveDefinition
+ in
+ let constr_obj =
+ [uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis",
+ None ;
+ uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+ Some 0
+ ]
+ in
+ let constr_rel =
+ ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion",
+ None] in
+ let constr_sort =
+ ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+ Some 1, "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"]
+ in
+ (constr_obj, constr_rel, constr_sort), (None,None,None)
+ | req_path ->
+ let must = MQueryLevels2.get_constraints term in
+ refine_constraints must req_path
+in
(* HTTP DAEMON CALLBACK *)
try
debug_print (sprintf "Received request: %s" req#path);
if req#path <> "/getpage" then
- Mqint.init postgresConnectionString;
+ ignore (MQI.init mqi_options);
(match req#path with
| "/execute" ->
let query_string = req#param "query" in
in
(match page with
| page when is_permitted page ->
- let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
+ (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
+ Http_daemon.send_basic_headers ~code:200 outchan;
+ Http_daemon.send_header "Content-Type" "text/html" outchan;
+ Http_daemon.send_CRLF outchan;
if preprocess then begin
- Http_daemon.send_basic_headers ~code:200 outchan;
- Http_daemon.send_CRLF outchan;
iter_file
(fun line ->
output_string outchan
"\n"))
fname
end else
- Http_daemon.respond_file ~fname outchan
+ Http_daemon.send_file ~src:(FileSrc fname) outchan)
| page -> Http_daemon.respond_forbidden ~url:page outchan))
| "/ask_uwobo" ->
let url = req#param "url" in
in
if List.mem server_and_port valid_servers then
Http_daemon.respond
+ ~headers:["Content-Type", "text/html"]
~body:(Http_client.Convenience.http_get url)
outchan
else
Http_daemon.respond
- ~body:(pp_error ("Invalid UWOBO server: " ^ server_and_port))
+ ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port))
outchan
- | "/searchPattern" ->
+ | "/searchPattern"
+ | "/matchConclusion"
+ | "/locateInductivePrinciple" ->
let term_string = req#param "term" in
let lexbuf = Lexing.from_string term_string in
let (context, metasenv) = ([], []) in
in
(match metasenv' with
| [] ->
- let must = MQueryLevels2.get_constraints term' in
- let must',only = refine_constraints must in
+ let must',only = get_constraints term' req#path in
let results = MQueryGenerator.searchPattern must' only in
Http_daemon.send_basic_headers ~code:200 outchan ;
Http_daemon.send_CRLF outchan ;
| invalid_request ->
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
if req#path <> "/getpage" then
- Mqint.close ();
+ MQI.close mqi_options;
debug_print (sprintf "%s done!" req#path)
with
| Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
printf "HTML directory is %s\n" pages_dir;
flush stdout;
Unix.putenv "http_proxy" "";
-Mqint.set_database Mqint.postgres_db;
Http_daemon.start' ~port callback;
printf "%s is terminating, bye!\n" daemon_name