X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=f7fae9481e6d0ac093705fa5fd21f7f50fba5dd7;hb=36d9dada5eb3894d96c807781e1056b73a1c0a79;hp=6e3b846d2ea3ff6d6db6450e15e6aaabcc7b5ab8;hpb=0e74e8e94eada756157addce67e4adeb8dff1feb;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 6e3b846d2..f7fae9481 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -155,8 +155,6 @@ let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
   Pcre.regexp "@VARIABLES_INITIALIZATION@")
 let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
 
-exception NotAnInductiveDefinition
-
 let port =
   try
     int_of_string (Sys.getenv port_env_var)
@@ -177,44 +175,25 @@ let contype = "Content-Type", "text/html";;
 
 (* SEARCH ENGINE functions *)
 
-let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =
- function
-    "/searchPattern" ->
-      U.universe_for_search_pattern,
-       (constr_obj, constr_rel, constr_sort),
-       (Some constr_obj, Some constr_rel, Some constr_sort)
-  | "/matchConclusion" ->
-      let constr_obj' =
-       List.map
-        (function (pos, uri) -> U.set_full_position pos None, uri)
-        (List.filter
-          (function (pos, _) -> U.is_conclusion pos)
-          constr_obj)
-      in
-       U.universe_for_match_conclusion,
-       (*CSC: we must select the must constraints here!!! *)
-       (constr_obj',[],[]),(Some constr_obj', None, None)
-  | _ -> assert false
-;;
-
 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 =
-       [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
-      in
-      let constr_rel = [`MainConclusion None] in
-      let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
-       U.universe_for_search_pattern,
-        (constr_obj, constr_rel, constr_sort), (None,None,None)
-  | req_path ->
-     let must = MQueryLevels2.get_constraints term in
-      refine_constraints must req_path
+    | "/locateInductivePrinciple" ->
+      None,
+      (CGLocateInductive.get_constraints term),
+      (None,None,None)
+    | "/searchPattern" ->
+     let constr_obj, constr_rel, constr_sort =
+       CGSearchPattern.get_constraints term in
+     (Some CGSearchPattern.universe),
+     (constr_obj, constr_rel, constr_sort),
+     (Some constr_obj, Some constr_rel, Some constr_sort)
+    | "/matchConclusion" ->
+     let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
+(* FG: there is no way to choose the block number ***************************)
+     let block = pred (List.length list_of_must) in 
+      (Some CGMatchConclusion.universe), 
+      (List.nth list_of_must block, [], []), (Some only, None, None)
+    | _ -> assert false
 ;;
 
 (*
@@ -242,20 +221,21 @@ let add_user_constraints ~constraints
     (* to be used on "obj" *)
   let add_user_must33 user_must must =
     List.map2
-      (fun (b, i) (p, u) -> U.set_full_position p (if b then i else None), u)
-      user_must must
+     (fun (b, i) (p, u) ->
+       if b then Some (U.set_full_position p i, u) else None)
+     user_must must
   in
     (* to be used on "rel" *)
   let add_user_must22 user_must must =
     List.map2
-      (fun (b, i) p -> U.set_main_position p (if b then i else None))
-      user_must must
+     (fun (b, i) p -> if b then Some (U.set_main_position p i) else None)
+     user_must must
   in
     (* to be used on "sort" *)
   let add_user_must32 user_must must =
     List.map2
-      (fun (b, i) (p, s) -> U.set_main_position p (if b then i else None), s)
-      user_must must
+     (fun (b, i) (p, s)-> if b then Some (U.set_main_position p i, s) else None)
+     user_must must
   in
   match Pcre.split ~pat:":" constraints with
   | [user_obj;user_rel;user_sort;user_only_obj;user_only_rel;user_only_sort] ->
@@ -275,9 +255,15 @@ let add_user_constraints ~constraints
        (if user_only_sort then only_sort else None)
       in
       let must' =
-        add_user_must33 user_obj obj,
-        add_user_must22 user_rel rel,
-        add_user_must32 user_sort sort
+       let rec filter_some =
+        function
+           [] -> []
+         | None::tl -> filter_some tl
+         | (Some x)::tl -> x::(filter_some tl) 
+       in
+        filter_some (add_user_must33 user_obj obj),
+        filter_some (add_user_must22 user_rel rel),
+        filter_some (add_user_must32 user_sort sort)
       in
       (must', only')
   | _ -> failwith ("Can't parse constraint string: " ^ constraints)
@@ -305,6 +291,14 @@ let callback (req: Http_types.request) outchan =
 	let result = MQueryInterpreter.execute mqi_handle query in
 	      C.close mqi_handle;
         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
+    | "/unreferred" ->
+        let mqi_handle = C.init mqi_flags debug_print in
+        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
+	      C.close mqi_handle;
+        Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
     | "/getpage" ->
         (* TODO implement "is_permitted" *)
         (let is_permitted _ = true in
@@ -585,7 +579,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   raise Chat_unfinished)
             in
             let query =
-             G.query_of_constraints (Some universe) must'' only'
+             G.query_of_constraints universe must'' only'
             in
 	          let results = MQueryInterpreter.execute mqi_handle query in 
              Http_daemon.send_basic_headers ~code:200 outchan ;