* 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" ] ;;
+let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ] ;;
-open Printf;;
+let mqi_flags = [] (* default MathQL interpreter options *)
-let postgresConnectionString =
- try
- Sys.getenv "POSTGRESQL_CONNECTION_STRING"
- with
- Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
-;;
+open Printf;;
let daemon_name = "Search Engine";;
let default_port = 58085;;
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,
- processorURL_RE)
+ interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_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 "@processorURL@")
+ 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 *)
let callback (req: Http_types.request) outchan =
try
debug_print (sprintf "Received request: %s" req#path);
- if req#path <> "/getpage" then
- Mqint.init postgresConnectionString;
(match req#path with
| "/execute" ->
+ let mqi_handle = MQIConn.init mqi_flags debug_print in
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 = MQueryGenerator.execute_query query in
+ let result = MQueryGenerator.execute_query mqi_handle query in
let result_string = pp_result result in
+ 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 id in
+ let result = MQueryGenerator.locate mqi_handle id in
+ MQIConn.close mqi_handle;
Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
| "/getpage" ->
(* TODO implement "is_permitted" *)
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
((apply_substs
- [processorURL_RE, req#param "processorURL"] line) ^
+ (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)
+ )
+ line) ^
"\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 mqi_handle = MQIConn.init mqi_flags debug_print in
let term_string = req#param "term" in
let lexbuf = Lexing.from_string term_string in
let (context, metasenv) = ([], []) in
in
let module Disambiguate' = Disambiguate.Make (Chat) in
let (id_to_uris', metasenv', term') =
- Disambiguate'.disambiguate_input
+ Disambiguate'.disambiguate_input mqi_handle
context metasenv dom mk_metasenv_and_expr id_to_uris
in
(match metasenv' with
| [] ->
- let must = MQueryLevels2.get_constraints term' in
- let must',only = refine_constraints must in
- let results = MQueryGenerator.searchPattern must' only in
+ let must',only = get_constraints term' req#path 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
Http_daemon.respond
~headers:[contype]
~body:"some implicit variables are still unistantiated :-("
- outchan)
-
+ outchan);
+ MQIConn.close mqi_handle
| invalid_request ->
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
- if req#path <> "/getpage" then
- Mqint.close ();
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
projects / helm.git / blobdiff