removed spurious dependency on Dbi_mysql

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

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 8bcd141b0fdfe218c15cfc2a90d454cc49395d39..87546b1ffdff61fbdd0a73e93a859aa087427674 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -25,8 +25,6 @@
 
 open Printf
 
-module DB = Dbi_mysql
-
 let debug = true
 let debug_print s = if debug then prerr_endline s
 let _ = Http_common.debug := false
@@ -37,6 +35,7 @@ exception Invalid_action of string  (* invalid action for "/search" method *)
 
 let daemon_name = "Moogle"
 let configuration_file = "/projects/helm/etc/moogle.conf.xml" 
+(*let configuration_file = "searchEngine.conf.xml" *)
 
 let placeholders = [
   "EXPRESSION"; "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "SIMPLE_CHECKED";
@@ -98,6 +97,10 @@ let javascript_quote 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 add_param_substs params =
   List.map
@@ -185,7 +188,7 @@ let send_results results
       output_string outchan (processed_line ^ "\n"))
     moogle_TPL
 
-let exec_action dbh (req: Http_types.request) outchan =
+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 = 
@@ -196,19 +199,19 @@ let exec_action dbh (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 = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
   let id_to_choices =
@@ -231,7 +234,7 @@ let exec_action dbh (req: Http_types.request) outchan =
       =
         match id_to_choices id with
         | Some choices -> choices
-        | None -> assert false
+        | None -> List.filter nonvar choices
 
       let interactive_interpretation_choice interpretations =
         match interpretation_choices with
@@ -267,14 +270,14 @@ let exec_action dbh (req: Http_types.request) outchan =
   let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
   let (id_to_uris, metasenv, term) =
     match
-      Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
+      Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
     with
-    | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
+    | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
     | _ -> assert false
   in
   let uris =
     match req#path with
-    | "/match" -> MetadataQuery.match_term ~dbh term
+    | "/match" -> MetadataQuery.match_term ~dbd term
     | "/hint" ->
         let status = ProofEngineTypes.initial_status term metasenv in
         let intros = PrimitiveTactics.intros_tac () in
@@ -282,7 +285,7 @@ let exec_action dbh (req: Http_types.request) outchan =
         (match subgoals with
         | proof, [goal] ->
             let (uri,metasenv,bo,ty) = proof in
-            List.map fst (MetadataQuery.hint ~dbh (proof, goal))
+            List.map fst (MetadataQuery.hint ~dbd (proof, goal))
         | _ -> assert false)
     | "/elim" ->
         let uri =
@@ -291,12 +294,12 @@ let exec_action dbh (req: Http_types.request) outchan =
               UriManager.string_of_uriref (uri, [typeno])
           | _ -> assert false
         in
-        MetadataQuery.elim ~dbh uri
+        MetadataQuery.elim ~dbd uri
     | _ -> assert false
   in
   send_results ~id_to_uris (`Results uris) req outchan
 
-let callback dbh (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
@@ -342,11 +345,11 @@ let callback dbh (req: Http_types.request) outchan =
         if expression = "" then
           send_results (`Results []) req outchan
         else
-          let results = MetadataQuery.locate ~dbh expression in
+          let results = MetadataQuery.locate ~dbd expression in
           send_results (`Results results) req outchan
     | "/hint"
     | "/elim"
-    | "/match" -> exec_action dbh req outchan
+    | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
           outchan);
@@ -355,7 +358,7 @@ let callback dbh (req: Http_types.request) outchan =
   | Chat_unfinished -> ()
   | Http_types.Param_not_found attr_name ->
       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
-  | CicTextualParser2.Parse_error msg ->
+  | CicTextualParser2.Parse_error (_, msg) ->
       send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
   | Unbound_identifier id ->
       send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
@@ -372,10 +375,13 @@ let _ =
   printf "HTML directory is %s\n" pages_dir;
   flush stdout;
   Unix.putenv "http_proxy" "";
-  let dbh =
-    new DB.connection ~host:(Helm_registry.get "db.host")
-      ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
+  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 dbh);
+  Http_daemon.start' ~port (callback dbd);
   printf "%s is terminating, bye!\n" daemon_name