* 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;;
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 *)
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 ;