From: Ferruccio Guidi Date: Wed, 18 Feb 2004 17:52:54 +0000 (+0000) Subject: mathql interpreter flags can be now red from helm registry X-Git-Tag: v0_0_4~137 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c911fe913e84cda448e2f0df20c1e023f6f8043d;p=helm.git mathql interpreter flags can be now red from helm registry --- diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index 1e301eaf9..7cbc31201 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -50,11 +50,7 @@ module DisambiguateCallbacks = module Disambiguate' = DisambiguatingParser.Make (DisambiguateCallbacks) -let mqi_debug_fun = ignore -let mqi_flags = [] - -let parse ?(uri_pred = constants_only) = - let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun in +let parse mqi_handle ?(uri_pred = constants_only) = uri_predicate := uri_pred; let empty_environment = DisambiguatingParser.EnvironmentP3.of_string @@ -67,7 +63,8 @@ let parse ?(uri_pred = constants_only) = Disambiguate'.disambiguate_term mqi_handle empty_context empty_metasenv input empty_environment in - MQIConn.close mqi_handle; (metasenv, term) + (metasenv, term) -let parse_pp ?uri_pred input = CicPp.ppterm (snd (parse ?uri_pred input)) +let parse_pp mqi_handle ?uri_pred input = + CicPp.ppterm (snd (parse mqi_handle ?uri_pred input)) diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index b63845aa8..ba5d5ab58 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -37,10 +37,10 @@ val uri_pred_of_conf: bool -> string -> (string -> bool) * batch mode if possible, otherwise raises Failure above. * uri_pred is the predicate used to select which uris are tried. Per default * only constant URIs are accepted *) -val parse: ?uri_pred:(string -> bool) -> string -> Cic.metasenv * Cic.term +val parse: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> Cic.metasenv * Cic.term (** as above, but instead of returning the parsed cic term, pretty prints it * (ignoring returned metasenv) *) -val parse_pp: ?uri_pred:(string -> bool) -> string -> string +val parse_pp: MQIConn.handle -> ?uri_pred:(string -> bool) -> string -> string diff --git a/helm/gTopLevel/gTopLevel.conf.xml.sample b/helm/gTopLevel/gTopLevel.conf.xml.sample index 8e26407e6..f955b5036 100644 --- a/helm/gTopLevel/gTopLevel.conf.xml.sample +++ b/helm/gTopLevel/gTopLevel.conf.xml.sample @@ -14,6 +14,12 @@
mathql_db_map.txt dbname=mowgli host=mowgli.cs.unibo.it user=helm password=awH21Un + + + + + +
file://$(users_settings.per_user_work_directory)/objects diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 8643ec313..69ad5d502 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -62,8 +62,7 @@ let _ = (* GLOBAL CONSTANTS *) let mqi_debug_fun s = debug_print ~level:2 s -let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] -let mqi_handle = MQIC.init mqi_flags mqi_debug_fun +let mqi_handle = MQIC.init mqi_debug_fun let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index a1ecd302f..5e246c97c 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -154,9 +154,9 @@ let as_expected report_fname expected found = (* ignores "term" field *) end; outcome -let test_this uri_pred raw_term = +let test_this mqi_handle uri_pred raw_term = let empty_context = [] in - let (metasenv, cic_term) = BatchParser.parse ~uri_pred raw_term in + let (metasenv, cic_term) = BatchParser.parse mqi_handle ~uri_pred raw_term in let etype = try CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv empty_context cic_term) @@ -202,7 +202,7 @@ let restore_environment filename = else CicEnvironment.empty () -let main generate dump fnames tryvars varsprefix = +let main mqi_handle generate dump fnames tryvars varsprefix = let uri_pred = BatchParser.uri_pred_of_conf tryvars varsprefix in if generate then begin @@ -215,7 +215,7 @@ let main generate dump fnames tryvars varsprefix = print_endline (sprintf "Generating regtest %s -> %s\n ..." fname test_fname); let raw_term = (parse_regtest fname).term in - let result = test_this uri_pred raw_term in + let result = test_this mqi_handle uri_pred raw_term in print_test result test_fname ; if dump then dump_environment env_fname ; ) fnames @@ -235,7 +235,7 @@ let main generate dump fnames tryvars varsprefix = let is_ok = try let expected = parse_regtest test_fname in - let actual = test_this uri_pred expected.term in + let actual = test_this mqi_handle uri_pred expected.term in if dump then dump_environment env_fname ; if as_expected report_fname expected actual then (incr ok ; true) @@ -265,6 +265,10 @@ let _ = (fun ?(append_NL = true) msg -> (if append_NL then prerr_endline else prerr_string) (HelmLogger.string_of_html_msg msg)); + + let mqi_debug_fun = ignore in + let mqi_handle = MQIConn.init mqi_debug_fun in + let fnames = ref [] in let gen = ref false in let tryvars = ref false in @@ -292,5 +296,5 @@ let _ = Arg.parse spec (fun filename -> fnames := filename::!fnames ) usage ; if !fnames = [] then Arg.usage spec (Sys.argv.(0) ^ ": missing argument test. You must provide at least one test file.\n" ^ usage) ; - main !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix - + main mqi_handle !gen ((!gen || !dump) && (not !nodump)) !fnames !tryvars !varsprefix; + MQIConn.close mqi_handle diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index b410b6048..0943dd146 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -125,7 +125,6 @@ let dump_environment () = close_out oc let main () = - let mqi_flags = [] in (* default MathQL interpreter options *) try Sys.catch_break true; at_exit (fun () -> @@ -135,7 +134,7 @@ let main () = broker_id := Some (Hbugs_tutors_common.register_to_broker my_own_id my_own_url "FOO" "Search_pattern_apply tutor"); - let mqi_handle = MQIC.init mqi_flags prerr_string in + let mqi_handle = MQIC.init prerr_string in if Sys.file_exists environment_file then restore_environment (); Http_daemon.start' diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index cc40f3369..7f8e2b85b 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -52,7 +52,7 @@ module C1 = CGMatchConclusion module GU = MQGUtil let get_handle () = - C.init (C.flags_of_string ! int_options) + C.init ~flags:(C.flags_of_string ! int_options) (fun s -> print_string s; flush stdout) let issue handle q = diff --git a/helm/mathql_test/mqitop.ml b/helm/mathql_test/mqitop.ml index 1b4b387c0..efac469a8 100644 --- a/helm/mathql_test/mqitop.ml +++ b/helm/mathql_test/mqitop.ml @@ -36,7 +36,7 @@ let _ = let ich = Lexing.from_channel stdin in let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in let log s = print_string s; flush stdout in - let handle = C.init (C.flags_of_string flags) log in + let handle = C.init ~flags:(C.flags_of_string flags) log in if not (C.connected handle) then begin print_endline "mqitop: no connection"; flush stdout end; diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index 460ef41d0..2b1847008 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -78,16 +78,22 @@ let string_of_flags flags = let flags_of_string s = string_fold_left (fun l c -> l @ flag_of_char c) [] s -let init myflags mylog = +let init ?(flags = []) mylog = + let flags = + if flags = [] then + flags_of_string (Helm_registry.get "mathql_interpreter.flags") + else + flags + in let m, a = let g = - if List.mem Galax myflags + if List.mem Galax flags then MQIMap.empty_map else MQIMap.read_map in g () in - {log = mylog; set = myflags; + {log = mylog; set = flags; pgc = - if List.mem Galax myflags then + if List.mem Galax flags then None else MQIPostgres.init @@ -101,7 +107,7 @@ let close handle = let connected handle = if set handle Galax then false else (pgc handle) <> None -let init_if_connected myflags mylog = - let handle = init myflags mylog in +let init_if_connected ?(flags = []) mylog = + let handle = init ~flags:flags mylog in ignore (pgc handle); handle diff --git a/helm/ocaml/mathql_interpreter/mQIConn.mli b/helm/ocaml/mathql_interpreter/mQIConn.mli index 649b54854..889b373d8 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.mli +++ b/helm/ocaml/mathql_interpreter/mQIConn.mli @@ -33,11 +33,11 @@ val flags_of_string : string -> flag list type handle -val init : flag list -> (string -> unit) -> handle +val init : ?flags:(flag list) -> (string -> unit) -> handle val close : handle -> unit val connected : handle -> bool -val init_if_connected : flag list -> (string -> unit) -> handle +val init_if_connected : ?flags:(flag list) -> (string -> unit) -> handle (* The following functions allow to read the handle internal fields. * For exclusive use of the interpreter. diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index d79e6ebd4..507dadb63 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -35,8 +35,6 @@ let debug_print s = if debug then prerr_endline s;; Http_common.debug := true;; (* Http_common.debug := true;; *) -let mqi_flags = [] (* default MathQL interpreter options *) - open Printf;; let daemon_name = "Search Engine";; @@ -264,33 +262,27 @@ in (* HTTP DAEMON CALLBACK *) -let callback (req: Http_types.request) outchan = +let callback mqi_handle (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); (match req#path with | "/execute" -> - let mqi_handle = C.init mqi_flags debug_print in 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 result in - C.close mqi_handle; Http_daemon.respond ~body:result_string ~headers:[contype] outchan | "/locate" -> - let mqi_handle = C.init mqi_flags debug_print in let id = req#param "id" in let query = G.locate id in 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" *) @@ -347,7 +339,6 @@ let callback (req: Http_types.request) outchan = | "/searchPattern" | "/matchConclusion" | "/locateInductivePrinciple" -> - let mqi_handle = C.init mqi_flags debug_print in let term_string = req#param "term" in let (context, metasenv) = ([], []) in let id_to_uris_raw = req#param "aliases" in @@ -601,8 +592,7 @@ print_endline ("id_to_uris: " ^ (DisambiguatingParser.EnvironmentP3.to_string id Http_daemon.respond ~headers:[contype] ~body:"some implicit variables are still unistantiated :-(" - outchan); - C.close mqi_handle + outchan) | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); debug_print (sprintf "%s done!" req#path) @@ -620,6 +610,7 @@ printf "Current directory is %s\n" (Sys.getcwd ()); printf "HTML directory is %s\n" pages_dir; flush stdout; Unix.putenv "http_proxy" ""; -Http_daemon.start' ~port callback; +let mqi_handle = C.init debug_print in +Http_daemon.start' ~port (callback mqi_handle); +C.close mqi_handle; printf "%s is terminating, bye!\n" daemon_name -