From: Stefano Zacchiroli Date: Fri, 22 Nov 2002 13:36:22 +0000 (+0000) Subject: - first (draft) version of searchEngine X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b44dc89c918d3703fd7cc4e36037912b34fd0f61;p=helm.git - first (draft) version of searchEngine --- diff --git a/helm/searchEngine/.cvsignore b/helm/searchEngine/.cvsignore new file mode 100644 index 000000000..6ecb17c4d --- /dev/null +++ b/helm/searchEngine/.cvsignore @@ -0,0 +1 @@ +*.cm[ioxa] *.o searchEngine searchEngine.opt diff --git a/helm/searchEngine/Makefile b/helm/searchEngine/Makefile new file mode 100644 index 000000000..3d979cd34 --- /dev/null +++ b/helm/searchEngine/Makefile @@ -0,0 +1,22 @@ +REQUIRES = http helm-cic_textual_parser helm-cic_proof_checking \ + helm-xml gdome2-xslt helm-cic_unification helm-mathql \ + helm-mathql_interpreter +OCAMLOPTIONS = -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel -thread +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) + +LIBRARIES = ../gTopLevel/mQueryGenerator.cmo +LIBRARIES_OPT = ../gTopLevel/mQueryGenerator.cmx + +all: searchEngine +opt: searchEngine.opt + +searchEngine: $(LIBRARIES) searchEngine.ml + $(OCAMLC) -linkpkg -o $@ $^ +searchEngine.opt: $(LIBRARIES_OPT) searchEngine.ml + $(OCAMLOPT) -linkpkg -o $@ $^ + +clean: + rm -f *.cm[aiox] *.o searchEngine{,.opt} + +.PHONY: all opt clean diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml new file mode 100644 index 000000000..03c0bb389 --- /dev/null +++ b/helm/searchEngine/searchEngine.ml @@ -0,0 +1,102 @@ + +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +let debug = true;; +let debug_print s = if debug then prerr_endline s;; +Http_common.debug := debug;; + +open Printf;; + +let daemon_name = "Search Engine";; +let default_port = 48085;; +let port_env_var = "SEARCH_ENGINE_PORT";; + +let port = + try + int_of_string (Sys.getenv port_env_var) + with + | Not_found -> default_port + | Failure "int_of_string" -> + prerr_endline "Warning: invalid port, reverting to default"; + default_port +in +let pp_result result = + let result_string = MQueryUtil.text_of_result result "\n" in + (sprintf "

%s

" result_string) +in +let pp_error = sprintf "

Error: %s

" in +let callback req outchan = + try + (* TODO catch exceptions *) + (match req#path with + | "/execute" -> + let query_string = req#param "query" in + let lexbuf = Lexing.from_string query_string in + let query = MQueryTParser.query MQueryTLexer.query_token lexbuf in + let result = MQueryGenerator.execute_query query in + let result_string = MQueryUtil.text_of_result result "\n" in + Http_daemon.respond + ~body: + (sprintf + "

%s

" + result_string) + outchan + | "/locate" -> + let id = req#param "id" in + let result = MQueryGenerator.locate id in + Http_daemon.respond ~body:(pp_result result) outchan + | "/searchPattern" -> + let term_string = req#param "term" in + let precision = int_of_string (req#param "precision") in + let lexbuf = Lexing.from_string term_string in + let (dom, mkterm) = + CicTextualParser.main CicTextualLexer.token lexbuf + in + (match dom with + | [] -> (* no free variables *) + let term = mkterm (fun _ -> None) in + let result = MQueryGenerator.searchPattern [] [] term precision in + Http_daemon.respond ~body:(pp_result result) outchan + | _ -> + Http_daemon.respond + ~body:(pp_error + "identifiers resolution in the environment not yet implemented") + outchan) + | invalid_request -> + Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan) + with + | Http_request.Param_not_found attr_name -> + Http_daemon.respond_error + ~status:(`Client_error `Bad_request) + ~body:(sprintf "Parameter '%s' is missing" attr_name) + outchan +in +printf "%s started and listening on port %d\n" daemon_name port; +printf "current directory is %s\n" (Sys.getcwd ()); +flush stdout; +Http_daemon.start' ~port callback; +printf "%s is terminating, bye!\n" daemon_name +