X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FsearchEngine%2FsearchEngine.ml;h=87546b1ffdff61fbdd0a73e93a859aa087427674;hb=ccb56bd6ddeec70a1fb32304aec60a0721d260cc;hp=8bcd141b0fdfe218c15cfc2a90d454cc49395d39;hpb=5cb2fa1e3e6f5d9d7a273b45c56a6c1196982c4a;p=helm.git diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 8bcd141b0..87546b1ff 100644 --- 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