New queries added:

[helm.git] / helm / searchEngine / searchEngine.ml

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 2da581bf7514799962a6f0c0eb60554a5be8abba..35270fd62c8ee31d46ca2469a819b94e57ebfeb8 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -108,6 +108,8 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
   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)
@@ -125,7 +127,54 @@ let contype = "Content-Type", "text/html" in
 
 (* 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 *)
 
@@ -198,7 +247,9 @@ let callback (req: Http_types.request) outchan =
         Http_daemon.respond
           ~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
@@ -348,8 +399,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
         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 ;