X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=d262029ed55f5d2d6fe1293f8653631953e0588d;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=1f45fe67c8424f6b075f24676d17b404e16792e3;hpb=aeac77539da374b9c9a0f3aae1c7b43963c9dab9;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 1f45fe67c..d262029ed 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2002-2004, HELM Team.
+(* Copyright (C) 2002-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,150 +23,55 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module T = MQGTypes
-module U = MQGUtil
-module G = MQueryGenerator
-module C = MQIConn
-
-open Http_types
+open Printf
 
 let debug = true
 let debug_print s = if debug then prerr_endline s
-let _ = Http_common.debug := true
-(* let _ = Http_common.debug := false *)
+let _ = Http_common.debug := false
 
-open Printf
-
-let daemon_name = "Search Engine"
+exception Chat_unfinished
+exception Unbound_identifier of string
+exception Invalid_action of string  (* invalid action for "/search" method *)
 
-let string_tail s =
-  let len = String.length s in
-  String.sub s 1 (len-1)
+let daemon_name = "Moogle"
+let configuration_file = "/projects/helm/etc/moogle.conf.xml"
+
+let placeholders = [
+  "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
+  "EXPRESSION"; "ID"; "IDEN"; "ID_TO_URIS"; "INTERPRETATIONS";
+  "INTERPRETATIONS_LABELS"; "MSG"; "NEW_ALIASES"; "NEXT_LINK"; "NO_CHOICES";
+  "PAGE"; "PAGES"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS";
+  "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE";
+]
+
+let tag =
+  let regexps = Hashtbl.create 25 in
+  List.iter
+    (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag)))
+    placeholders;
+  fun name ->
+    try
+      Hashtbl.find regexps name
+    with Not_found -> assert false
 
   (* First of all we load the configuration *)
-let _ =
- let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in
-  Helm_registry.load_from configuration_file
-
+let _ = Helm_registry.load_from configuration_file
 let port = Helm_registry.get_int "search_engine.port"
-
 let pages_dir = Helm_registry.get "search_engine.html_dir"
 
-  (** accepted HTTP servers for ask_uwobo method forwarding *)
-let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers"
-
-let interactive_user_uri_choice_TPL = pages_dir ^ "/moogle_chat1.html"
-let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
-let constraints_choice_TPL = pages_dir ^ "/moogle_constraints_choice.html"
 let moogle_TPL = pages_dir ^ "/moogle.html"
+let choices_TPL = pages_dir ^ "/moogle_chat.html"
 
 let my_own_url =
  let ic = Unix.open_process_in "hostname -f" in
  let hostname = input_line ic in
  ignore (Unix.close_process_in ic);
  sprintf "http://%s:%d" hostname port
+let _ = Helm_registry.set "search_engine.my_own_url" my_own_url
 
-exception Chat_unfinished
-exception Invalid_action of string  (* invalid action for "/search" method *)
-exception Unbound_identifier of string
-
-let javascript_quote s =
- let rex = Pcre.regexp "'" in
- let rex' = Pcre.regexp "\"" in
-  Pcre.replace ~rex ~templ:"\\'"
-   (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
-
-  (* build a bool from a 1-character-string *)
-let bool_of_string' = function
-  | "0" -> false
-  | "1" -> true
-  | s -> failwith ("Can't parse a boolean from string: " ^ s)
-
-  (* build an int option from a string *)
-let int_of_string' = function
-  | "_" -> None
-  | s ->
-      try
-        Some (int_of_string s)
-      with Failure "int_of_string" ->
-        failwith ("Can't parse an int option from string: " ^ s)
-
-  (* HTML pretty printers for mquery_generator types *)
-
-let html_of_r_obj (pos, uri) =
-  sprintf
-    "<tr><td><input type='checkbox' name='constr_obj' checked='on'/></td><td>%s</td><td>%s</td><td>%s</td></tr>"
-    uri (U.text_of_position pos)
-    (if U.is_main_position pos then
-      sprintf "<input name='obj_depth' size='2' type='text' value='%s' />"
-        (U.text_of_depth pos "")
-    else
-      "<input type=\"hidden\" name=\"obj_depth\" />")
-
-let html_of_r_rel pos =
-  sprintf
-    "<tr><td><input type='checkbox' name='constr_rel' checked='on'/></td><td>%s</td><td><input name='rel_depth' size='2' type='text' value='%s' /></td></tr>"
-    (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
-
-let html_of_r_sort (pos, sort) =
-  sprintf
-    "<tr><td><input type='checkbox' name='constr_sort' checked='on'/></td><td>%s</td><td>%s</td><td><input name='sort_depth' size='2' type='text' value='%s'/></td></tr>"
-    (U.text_of_sort sort) (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
-
-let query_of_req (req: Http_types.request) =
-  match req#path with
-  | "/elim" -> "Elim"
-  | "/match" -> "Match"
-  | "/hint" -> "Hint"
-  | "/locate" -> "Locate"
-  | _ -> assert false
-
-  (** pretty print a MathQL query result to an HELM theory file *)
-let theory_of_result req result =
- let results_no = List.length result in
-  if results_no > 0 then
-   let mode = if results_no > 10 then "linkonly" else "typeonly" in
-   let results =
-    let idx = ref (results_no + 1) in
-     List.fold_right
-      (fun uri i ->
-        decr idx ;
-        sprintf
-          "<tr>
-           <td valign=\"top\">%d.</td>
-           <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
-           </tr>%s"
-          !idx uri mode i)
-      result ""
-   in
-   sprintf
-    "<div class='resultsbar'>
-      <table width='100%%'>
-       <tr>
-        <td class='left'><b class='query_kind'>%s</b></td>
-        <td class='right'><b>%d</b> result%s found</td>
-       </tr>
-      </table>
-     </div>
-     <br />
-     <div>
-      <table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">%s</table>
-     </div>"
-    (query_of_req req)
-    results_no (if results_no > 1 then "s" else "") results
-  else
-    "<div class='resultsbar'>no results found</div>"
-
-let pp_result req result =
- sprintf
-   "<html xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
-     <head>
-      <title>Query results</title>
-      <style> A { text-decoration: none } </style>
-     </head>
-     <body>%s</body>
-    </html>"
-   (theory_of_result req result)
+let bad_request body outchan =
+  Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
+    outchan
 
   (** chain application of Pcre substitutions *)
 let rec apply_substs substs line =
@@ -187,176 +92,138 @@ let fold_file f init fname =
   res
   (** iter like function on files *)
 let iter_file f = fold_file (fun _ line -> f line) ()
+let javascript_quote s =
+ let rex = Pcre.regexp "'" in
+ let rex' = Pcre.regexp "\"" in
+  Pcre.replace ~rex ~templ:"\\'"
+   (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
+let string_tail s =
+  let len = String.length s in
+  String.sub s 1 (len-1)
+let nonvar s =
+  let len = String.length s in
+  let suffix = String.sub s (len-4) 4 in
+  not (suffix  = ".var")
 
-let (expression_tag_RE, action_tag_RE, advanced_tag_RE,
-     advanced_checked_RE, simple_checked_RE,
-     title_tag_RE, no_choices_tag_RE, current_choices_tag_RE,  
-     choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, iden_tag_RE,
-     interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE,
-     form_RE, variables_initialization_RE, search_engine_url_RE)
-  =
-  (Pcre.regexp "@EXPRESSION@", Pcre.regexp "@ACTION@", Pcre.regexp "@ADVANCED@",
-   Pcre.regexp "@ADVANCED_CHECKED@", Pcre.regexp "@SIMPLE_CHECKED@",
-   Pcre.regexp "@TITLE@", Pcre.regexp "@NO_CHOICES@",  
-   Pcre.regexp "@CURRENT_CHOICES@",
-   Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@",
-   Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@", Pcre.regexp "@IDEN@",
-   Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@",
-   Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@", Pcre.regexp "@FORM@",
-   Pcre.regexp "@VARIABLES_INITIALIZATION@", Pcre.regexp "@SEARCH_ENGINE_URL@")
-let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
-
-(* let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>" *)
-let pp_error title msg =
-  sprintf "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" title msg
-
-let bad_request body outchan =
-  Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
-    outchan
-
-let contype = "Content-Type", "text/html"
-
-(* SEARCH ENGINE functions *)
-
-let get_constraints term =
- function
-    | "/elim" ->
-      None,
-      (CGLocateInductive.get_constraints term),
-      (None,None,None)
-    | "/match" ->
-     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)
-    | "/hint" ->
-     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
+let add_param_substs params =
+  List.map
+    (fun (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)
+      params)
 
-(*
-  format:
-    <must_obj> ':' <must_rel> ':' <must_sort> ':' <only_obj> ':' <only_rel> ':' <only_sort>
+let page_RE = Pcre.regexp "&param\\.page=\\d+"
 
-    <must_*> ::= ('0'|'1') ('_'|<int>) (',' ('0'|'1') ('_'|<int>))*
-    <only> ::= '0'|'1'
-*)
-let add_user_constraints ~constraints
- ((obj, rel, sort), (only_obj, only_rel, only_sort))
-=
-  let parse_must s =
-    let l = Pcre.split ~pat:"," s in
-    (try
-      List.map
-        (fun s ->
-          let subs = Pcre.extract ~pat:"^(.)(\\d+|_)$" s in
-          (bool_of_string' subs.(1), int_of_string' subs.(2)))
-        l
-     with
-      Not_found -> failwith ("Can't parse constraint string: " ^ constraints)
-    )
-  in
-    (* to be used on "obj" *)
-  let add_user_must33 user_must must =
-    List.map2
-     (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 -> 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)-> 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] ->
-      let
-       (user_obj,user_rel,user_sort,user_only_obj,user_only_rel,user_only_sort)
-      =
-        (parse_must user_obj,
-        parse_must user_rel,
-        parse_must user_sort,
-        bool_of_string' user_only_obj,
-        bool_of_string' user_only_rel,
-        bool_of_string' user_only_sort)
-      in
-      let only' =
-       (if user_only_obj  then only_obj else None),
-       (if user_only_rel  then only_rel else None),
-       (if user_only_sort then only_sort else None)
-      in
-      let must' =
-       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)
+let query_kind_of_req (req: Http_types.request) =
+  match req#path with
+  | "/match" -> "Match"
+  | "/hint" -> "Hint"
+  | "/locate" -> "Locate"
+  | "/elim" -> "Elim"
+  | _ -> ""
+
+  (* given a uri with a query part in input try to find in it a string
+   * "&param_name=..." (where param_name is given). If found its value will be
+   * set to param_value. If not, a trailing "&param_name=param_value" (where
+   * both are given) is added to the input string *)
+let patch_param param_name param_value url =
+  let rex = Pcre.regexp (sprintf "&%s=[^&]*" (Pcre.quote param_name)) in
+  if Pcre.pmatch ~rex url then
+    Pcre.replace ~rex ~templ:(sprintf "%s=%s" param_name param_value) url
+  else
+    sprintf "%s&%s=%s" url param_name param_value
 
 let send_results results
-  ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") 
+  ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") 
    (req: Http_types.request) outchan
   =
+  let query_kind = query_kind_of_req req in
+  let interp = try req#param "interp" with Http_types.Param_not_found _ -> "" in
+  let page_link anchor page =
+    try
+      let this = req#param "this" in
+      let target =
+        (patch_param "param.interp" interp
+           (patch_param "param.page" (string_of_int page)
+              this))
+      in
+      let target = Pcre.replace ~pat:"&" ~templ:"&amp;" target in
+      sprintf "<a href=\"%s\">%s</a>" target anchor
+    with Http_types.Param_not_found _ -> ""
+  in
   Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
   Http_daemon.send_header "Content-Type" "text/xml" outchan;
   Http_daemon.send_CRLF outchan ;
-  let results_string =
+  let subst =
     match results with
-    | `Results r -> theory_of_result req r
-    | `Error msg -> msg
+    | `Results results ->
+        let page = try int_of_string (req#param "page") with _ -> 1 in
+        let results_no = List.length results in
+        let results_per_page =
+          Helm_registry.get_int "search_engine.results_per_page"
+        in
+        let pages =
+          if results_no mod results_per_page = 0 then
+            results_no / results_per_page
+          else
+            results_no / results_per_page + 1
+        in
+        let pages = if pages = 0 then 1 else pages in
+        let (summary, results) = MooglePp.theory_of_result page results in
+        [ tag "PAGE", string_of_int page;
+          tag "PAGES", string_of_int pages;
+          tag "PREV_LINK", (if page > 1 then page_link "Prev" (page-1) else "");
+          tag "NEXT_LINK",
+            (if page < pages then page_link "Next" (page+1) else "");
+          tag "QUERY_KIND", query_kind;
+          tag "QUERY_SUMMARY", summary;
+          tag "RESULTS", results ]
+    | `Error msg ->
+        [ tag "PAGE", "1";
+          tag "PAGES", "1";
+          tag "PREV_LINK", "";
+          tag "NEXT_LINK", "";
+          tag "QUERY_KIND", query_kind;
+          tag "QUERY_SUMMARY", "error";
+          tag "RESULTS", msg ]
+  in
+  let advanced =
+    try
+      req#param "advanced"
+    with Http_types.Param_not_found _ -> "no"
   in
   let subst =
-    (search_engine_url_RE, my_own_url) ::
-    (results_RE, results_string)::
-    (advanced_tag_RE, req#param "advanced")::
-    (expression_tag_RE, req#param "expression")::
-    (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)) @
-    (if req#param "advanced" = "no" then
-      [ simple_checked_RE, "checked='true'";
-        advanced_checked_RE, "" ]
+    (tag "SEARCH_ENGINE_URL", my_own_url) ::
+    (tag "ADVANCED", advanced) ::
+    (tag "EXPRESSION", req#param "expression") ::
+    add_param_substs req#params @
+    (if advanced = "no" then
+      [ tag "SIMPLE_CHECKED", "checked='true'";
+        tag "ADVANCED_CHECKED", "" ]
     else
-      [ simple_checked_RE, "";
-        advanced_checked_RE, "checked='true'" ])
+      [ tag "SIMPLE_CHECKED", "";
+        tag "ADVANCED_CHECKED", "checked='true'" ]) @
+    subst
   in
   iter_file
     (fun line ->
       let new_aliases =
-        DisambiguatingParser.EnvironmentP3.to_string id_to_uris
+        CicTextualParser2.EnvironmentP3.to_string id_to_uris
       in
       let processed_line =
         apply_substs
           (* CSC: Bug here: this is a string, not an array! *)
-          ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) 
+          ((tag "NEW_ALIASES", "'" ^ javascript_quote new_aliases ^ "'") ::
+            subst) 
           line
       in
       output_string outchan (processed_line ^ "\n"))
     moogle_TPL
 
-let exec_action mqi_handle (req: Http_types.request) outchan =
-  let term_string = req#param "expression" in
+let exec_action dbd (req: Http_types.request) outchan =
+  let term_str = req#param "expression" in
   let (context, metasenv) = ([], []) in
   let id_to_uris_raw = 
     try req#param "aliases" 
@@ -366,26 +233,24 @@ let exec_action mqi_handle (req: Http_types.request) outchan =
     List.map int_of_string (Pcre.split ~pat:" " choices) in
   let parse_choices choices_raw =
     let choices = Pcre.split ~pat:";" choices_raw in
-      List.fold_left
-        (fun f x ->
-           match Pcre.split ~pat:"\\s" x with
-             | ""::id::tail
-             | id::tail when id<>"" ->
-                 (fun id' ->
-                    if id = id' then
-                      Some (List.map (fun u -> Netencoding.Url.decode u) tail)
-                    else
-                      f id')
-             | _ -> failwith "Can't parse choices")
-        (fun _ -> None)
-        choices
+    List.fold_left
+      (fun f x ->
+         match Pcre.split ~pat:"\\s" x with
+           | ""::id::tail
+           | id::tail when id<>"" ->
+               (fun id' ->
+                  if id = id' then
+                    Some (List.map (fun u -> Netencoding.Url.decode u) tail)
+                  else
+                    f id')
+           | _ -> failwith "Can't parse choices")
+      (fun _ -> None)
+      choices
   in
-  let id_to_uris =
-    DisambiguatingParser.EnvironmentP3.of_string id_to_uris_raw in
+  let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
   let id_to_choices =
     try
-      let choices_raw = req#param "choices" in
-        parse_choices choices_raw
+      parse_choices (req#param "choices")
     with Http_types.Param_not_found _ -> (fun _ -> None)
   in
   let interpretation_choices =
@@ -397,307 +262,102 @@ let exec_action mqi_handle (req: Http_types.request) outchan =
   in 
   let module Chat: DisambiguateTypes.Callbacks =
     struct
-
-      let interactive_user_uri_choice
-        ~selection_mode ?ok
+      let interactive_user_uri_choice ~selection_mode ?ok
         ?enable_button_for_non_vars ~(title: string) ~(msg: string)
         ~(id: string) (choices: string list)
-        =
-        (match id_to_choices id with
-           | Some choices -> choices
-           | None ->
-              if req#param "advanced" = "no" then
-                let isvar s =
-		  let len = String.length s in
-		  let suffix = String.sub s (len-4) 4 in
-		    not (suffix  = ".var") in
-		List.filter isvar choices
-	      else 
-               let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
-               (match selection_mode with
-                  | `SINGLE -> assert false
-                  | `MULTIPLE ->
-                      Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
-                      Http_daemon.send_CRLF outchan ;
-                      let check_box uri =
-			"<input type=\"checkbox\" name=\"param.choices\" 
-                        value=\"" ^
-			uri ^ "\" />" ^ "<b>" ^ uri ^ "</b>" in
-(* aggiungere gli hyperlinks? *)
-                      let check_boxes = 
-			String.concat "<br />" 
-			  (List.map check_box choices) in
-		      iter_file
-                        (fun line ->
-                           let processed_line =
-			     apply_substs
- 			       [advanced_tag_RE, req#param "advanced";
-                                choices_tag_RE, check_boxes;
-                                no_choices_tag_RE, 
-				   string_of_int (List.length choices);
-                                iden_tag_RE, id;
-                                current_choices_tag_RE, req#param "choices";  
-                                expression_tag_RE, req#param "expression";
-                                action_tag_RE, string_tail req#path ]
-			       line
-			   in
-                             output_string outchan (processed_line ^ "\n"))
-                        interactive_user_uri_choice_TPL;
-			raise Chat_unfinished))
+      =
+        match id_to_choices id with
+        | Some choices -> choices
+        | None -> List.filter nonvar choices
 
       let interactive_interpretation_choice interpretations =
         match interpretation_choices with
-            Some l -> prerr_endline "CARRAMBA" ; l
-          | None ->
-              let html_interpretations =
-		let radio_button n = 
-		  "<input type=\"radio\" name=\"param.interp\" value=\"" ^
-		  (string_of_int n) ^ "\" />" in
-                let text interp =
-		  String.concat "<br />" 
-		    (List.map
-                       (fun (id, value) -> 
-			  sprintf "<span>%s = %s</span>" id value) 
-		       interp) in
-		let rec aux n = 
-		  function
-		      [] -> []
-                    | interp::tl ->
-			((radio_button n)^(text interp))::(aux (n+1) tl) in
-                String.concat "<br />" (aux 0 interpretations)
-              in
-              Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
-              Http_daemon.send_CRLF outchan ;
-              iter_file
-                (fun line ->
-                   let processed_line =
-                     apply_substs
-                       [advanced_tag_RE, req#param "advanced";
-                        interpretations_RE, html_interpretations;
-                        current_choices_tag_RE, req#param "choices";
-			expression_tag_RE, req#param "expression";
-                        action_tag_RE, string_tail req#path ]
-                        line
-                   in
-                   output_string outchan (processed_line ^ "\n"))
-                interactive_interpretation_choice_TPL;
-              raise Chat_unfinished
+        | Some l -> l
+        | None ->
+            let html_interpretations =
+              MooglePp.html_of_interpretations interpretations
+            in
+            Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
+            Http_daemon.send_CRLF outchan ;
+            let advanced =
+              try
+                req#param "advanced"
+              with Http_types.Param_not_found _ -> "no"
+            in
+            let query_kind = query_kind_of_req req in
+            iter_file
+              (fun line ->
+                 let processed_line =
+                   apply_substs
+                     [ tag "SEARCH_ENGINE_URL", my_own_url;
+                       tag "ADVANCED", advanced;
+                       tag "INTERPRETATIONS", html_interpretations;
+                       tag "CURRENT_CHOICES", req#param "choices";
+                       tag "EXPRESSION", req#param "expression";
+                       tag "QUERY_KIND", query_kind;
+                       tag "QUERY_SUMMARY", "disambiguation";
+                       tag "ACTION", string_tail req#path ]
+                     line
+                 in
+                 output_string outchan (processed_line ^ "\n"))
+              choices_TPL;
+            raise Chat_unfinished
 
       let input_or_locate_uri ~title ?id () =
         match id with
         | Some id -> raise (Unbound_identifier id)
         | None -> assert false
-
     end
   in
-  let module Disambiguate' = DisambiguatingParser.Make(Chat) in
-  let (id_to_uris', metasenv', term') =
+  let module Disambiguate' = Disambiguate.Make(Chat) in
+  let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
+  let (id_to_uris, metasenv, term) =
     match
-      Disambiguate'.disambiguate_term mqi_handle
-        context metasenv term_string id_to_uris
+      Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
     with
-        [id_to_uris',metasenv',term'] -> id_to_uris',metasenv',term'
-      | _ -> assert false
-        in
-  let universe,
-  ((must_obj, must_rel, must_sort) as must'),
-  ((only_obj, only_rel, only_sort) as only) =
-    get_constraints term' req#path
-  in
-  if
-    (try ignore (req#param "constraints"); false
-    with Http_types.Param_not_found _ -> true) &&
-    (req#param "advanced" = "no") && (req#path = "/hint")
-  then
-    let dbd =
-      match mqi_handle.MQIConn.pgc with
-      |   MQIConn.MySQL_C conn -> conn
-      | _ -> assert false
-    in
-    let results = List.map snd (Match_concl.cmatch dbd term') in
-    send_results (`Results results) ~id_to_uris:id_to_uris' req outchan
-  else
-  let must'', only' =
-    (try
-       add_user_constraints
-         ~constraints:(req#param "constraints")
-         (must', only)
-     with Http_types.Param_not_found _ ->
-       if req#param "advanced" = "no" then
-	 (must',only)
-       else
-       let variables =
-         "var aliases = '" ^ id_to_uris_raw ^ "';\n" ^
-         "var constr_obj_len = " ^
-         string_of_int (List.length must_obj) ^ ";\n" ^
-         "var constr_rel_len = " ^
-         string_of_int (List.length must_rel) ^ ";\n" ^
-         "var constr_sort_len = " ^
-         string_of_int (List.length must_sort) ^ ";\n" in
-       let form =
-         (if must_obj = [] then "" else
-            "<h4>Obj constraints</h4>" ^
-            "<table>" ^
-            (String.concat "\n" (List.map html_of_r_obj must_obj)) ^
-            "</table>" ^
-            (* The following three lines to make Javascript create *)
-            (* the constr_obj[] and obj_depth[] arrays even if we  *)
-            (* have only one real entry.                           *)
-            "<input type=\"hidden\" name=\"constr_obj\" />" ^
-            "<input type=\"hidden\" name=\"obj_depth\" />") ^
-         (if must_rel = [] then "" else
-            "<h4>Rel constraints</h4>" ^
-            "<table>" ^
-            (String.concat "\n" (List.map html_of_r_rel must_rel)) ^
-            "</table>" ^
-            (* The following two lines to make Javascript create *)
-            (* the constr_rel[] and rel_depth[] arrays even if   *)
-            (* we have only one real entry.                      *)
-            "<input type=\"hidden\" name=\"constr_rel\" />" ^
-            "<input type=\"hidden\" name=\"rel_depth\" />") ^
-         (if must_sort = [] then "" else
-            "<h4>Sort constraints</h4>" ^
-            "<table>" ^
-            (String.concat "\n" (List.map html_of_r_sort must_sort)) ^
-            "</table>" ^
-            (* The following two lines to make Javascript create *)
-            (* the constr_sort[] and sort_depth[] arrays even if *)
-            (* we have only one real entry.                      *)
-            "<input type=\"hidden\" name=\"constr_sort\" />" ^
-            "<input type=\"hidden\" name=\"sort_depth\" />") ^
-         "<h4>Only constraints</h4>" ^
-         "Enforce Only constraints for objects: " ^
-         "<input type='checkbox' name='only_obj'" ^
-         (if only_obj = None then "" else " checked='yes'") ^
-         " /><br />" ^
-         "Enforce Rel constraints for objects: " ^
-         "<input type='checkbox' name='only_rel'" ^
-         (if only_rel = None then "" else " checked='yes'") ^
-         " /><br />" ^
-         "Enforce Sort constraints for objects: " ^
-         "<input type='checkbox' name='only_sort'" ^
-         (if only_sort = None then "" else " checked='yes'") ^
-         " /><br />"
-       in
-       Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
-       Http_daemon.send_CRLF outchan ;
-       iter_file
-         (fun line ->
-            let processed_line =
-              apply_substs
-                [form_RE, form ;
-                 variables_initialization_RE, variables;
-                 advanced_tag_RE, req#param "advanced";
-                 current_choices_tag_RE, req#param "choices";
-                 interpretations_RE, req#param "interpretation_choices"; 
-                 expression_tag_RE, req#param "expression";
-                 action_tag_RE, string_tail req#path]  line
-            in
-              output_string outchan (processed_line ^ "\n"))
-         constraints_choice_TPL; 
-       raise Chat_unfinished)
-  in
-  let query =
-    G.query_of_constraints universe must'' only'
+    | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
+    | _ -> assert false
   in
-  let results = MQueryInterpreter.execute mqi_handle query in 
-  send_results (`Results (List.map fst results))
-    ~id_to_uris:id_to_uris' req outchan
-
-(* HTTP DAEMON CALLBACK *)
-
-let build_dynamic_uri url params =
-  let p = 
-    String.concat "&" (List.map  (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in
-  url ^ "?" ^ p
-
-let build_uwobo_request (req: Http_types.request) outchan =
-  prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL");
-  let xmluri = build_dynamic_uri ((req#param "param.SEARCH_ENGINE_URL") ^ "/search") req#params in
-  prerr_endline ("xmluri: " ^ xmluri);
-  (*let xmluri = Netencoding.Url.encode xmluri in*)
-  let server_and_port = req#param "param.processorURL" in
-  let newreq = 
-    build_dynamic_uri 
-      (server_and_port ^ "apply") 
-      (("xmluri",xmluri)::("keys",(req#param "param.thkeys"))::req#params) in
-  (* if List.mem server_and_port valid_servers then *)
-  prerr_endline newreq;
-  if true then 
-    Http_daemon.respond
-      ~headers:["Content-Type", "text/html"]
-      ~body:(Http_client.http_get newreq)
-      outchan
-  else
-    Http_daemon.respond
-      ~body:(pp_error "Untrusted UWOBO server" server_and_port)
-      outchan
-
-let proxy url outchan =
-  let server_and_port =
-    (Pcre.extract ~rex:server_and_port_url_RE url).(1)
+  let uris =
+    match req#path with
+    | "/match" -> MetadataQuery.match_term ~dbd term
+    | "/hint" ->
+        let status = ProofEngineTypes.initial_status term metasenv in
+        let intros = PrimitiveTactics.intros_tac () in
+        let subgoals = ProofEngineTypes.apply_tactic intros status in
+        (match subgoals with
+        | proof, [goal] ->
+            let (uri,metasenv,bo,ty) = proof in
+            List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+        | _ -> assert false)
+    | "/elim" ->
+        let uri =
+          match term with
+          | Cic.MutInd (uri, typeno, _) ->
+              UriManager.string_of_uriref (uri, [typeno])
+          | _ -> assert false
+        in
+        MetadataQuery.elim ~dbd uri
+    | _ -> assert false
   in
-  if List.mem server_and_port valid_servers then
-    Http_daemon.respond
-      ~headers:["Content-Type", "text/html"]
-      ~body:(Http_client.http_get url)
-      outchan
-  else
-    Http_daemon.respond
-      ~body:(pp_error "Untrusted UWOBO server" server_and_port)
-      outchan
+  send_results ~id_to_uris (`Results uris) req outchan
 
-let callback mqi_handle (req: Http_types.request) outchan =
+let callback dbd (req: Http_types.request) outchan =
   try
     debug_print (sprintf "Received request: %s" req#path);
     (match req#path with
-    | "/help" -> Http_daemon.respond ~body:"HELM Search Engine" outchan
-    | "/locate" ->
-        let initial_expression =
-          try req#param "expression" with Http_types.Param_not_found _ -> ""
-        in
-        let expression =
-          Pcre.replace ~pat:"\\s*$"
-            (Pcre.replace ~pat:"^\\s*" initial_expression)
-        in
-        if expression = "" then
-          send_results (`Results []) req outchan
-        else
-          let results =
-            let query = G.locate expression in
-             MQueryInterpreter.execute mqi_handle query
-          in
-          send_results (`Results (List.map fst results)) req outchan
-    | "/execute" ->
-        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 = MQueryInterpreter.execute mqi_handle query in
-        let result_string = pp_result req (List.map fst result) in
-        Http_daemon.respond ~body:result_string ~headers:[contype] outchan
-(*  Http_daemon.respond ~headers:[contype] ~body:(pp_result req result) outchan *)
-    | "/unreferred" ->
-        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
-        Http_daemon.respond ~headers:[contype]
-          ~body:(pp_result req (List.map fst result)) outchan
     | "/getpage" ->
-        (* TODO implement "is_permitted" *)
-        let _ = prerr_endline 
-	  (Netencoding.Url.encode "http://mowgli.cs.unibo.it:38080/") in 
-        (let is_permitted _ = true in
-        let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
-        let page = remove_fragment (req#param "url") in
+          (* TODO implement "is_permitted" *)
+        (let is_permitted page = not (Pcre.pmatch ~pat:"/" page) in
+        let page = req#param "url" in
+        let fname = sprintf "%s/%s" pages_dir page in
         let preprocess =
           (try
             bool_of_string (req#param "preprocess")
           with Invalid_argument _ | Http_types.Param_not_found _ -> false)
         in
         (match page with
-        | page when is_permitted page ->
-            (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
+        | page when is_permitted page && Sys.file_exists fname ->
             Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
             Http_daemon.send_header "Content-Type" "text/html" outchan;
             Http_daemon.send_CRLF outchan;
@@ -706,45 +366,51 @@ let callback mqi_handle (req: Http_types.request) outchan =
                 (fun line ->
                   output_string outchan
                     ((apply_substs
-                       ((search_engine_url_RE, my_own_url) ::
-                        (advanced_tag_RE, "no") ::
-                        (results_RE, "") ::
-                       (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)
-                       ))
+                       ((tag "SEARCH_ENGINE_URL", my_own_url) ::
+                        (tag "ADVANCED", "no") ::
+                        (tag "RESULTS", "") ::
+                        add_param_substs req#params)
                        line) ^
                     "\n"))
                 fname
             end else
-              Http_daemon.send_file ~src:(FileSrc fname) outchan)
+              Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan
         | page -> Http_daemon.respond_forbidden ~url:page outchan))
-    (* OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *)
-    | "/ask_uwobo" -> build_uwobo_request req outchan
-    | "/hint" | "/match" | "/elim" -> exec_action mqi_handle req outchan
+    | "/help" -> Http_daemon.respond ~body:daemon_name outchan
+    | "/locate" ->
+        let initial_expression =
+          try req#param "expression" with Http_types.Param_not_found _ -> ""
+        in
+        let expression =
+          Pcre.replace ~pat:"\\s*$"
+            (Pcre.replace ~pat:"^\\s*" initial_expression)
+        in
+        if expression = "" then
+          send_results (`Results []) req outchan
+        else begin
+          let results = MetadataQuery.locate ~dbd expression in
+          send_results (`Results results) req outchan
+        end
+    | "/hint"
+    | "/elim"
+    | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
           outchan);
     debug_print (sprintf "%s done!" req#path)
   with
-  | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
+  | Chat_unfinished -> ()
   | Http_types.Param_not_found attr_name ->
       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
-  | CicTextualParser2.Parse_error msg ->
-      send_results (`Error (pp_error "Parse_error" msg)) req outchan
+  | CicTextualParser2.Parse_error (_, msg) ->
+      send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
   | Unbound_identifier id ->
-      send_results (`Error (pp_error "Unbound identifier" id)) req outchan
+      send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
+        outchan
   | exn ->
       let exn_string = Printexc.to_string exn in
       debug_print exn_string;
-      let msg = pp_error "Uncaught exception" exn_string in
+      let msg = MooglePp.pp_error "Uncaught exception" exn_string in
       send_results (`Error msg) req outchan
 
 let _ =
@@ -753,8 +419,13 @@ let _ =
   printf "HTML directory is %s\n" pages_dir;
   flush stdout;
   Unix.putenv "http_proxy" "";
-  let mqi_handle = C.init ~log:debug_print () in
-  Http_daemon.start' ~port (callback mqi_handle);
-  C.close mqi_handle;
+  let dbd =
+    Mysql.quick_connect
+      ~host:(Helm_registry.get "db.host")
+      ~database:(Helm_registry.get "db.database")
+      ~user:(Helm_registry.get "db.user")
+      ()
+  in
+  Http_daemon.start' ~port (callback dbd);
   printf "%s is terminating, bye!\n" daemon_name