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
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))
* 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
<section name="mathql_interpreter">
<key name="db_map">mathql_db_map.txt</key>
<key name="postgresql_connection_string">dbname=mowgli host=mowgli.cs.unibo.it user=helm password=awH21Un</key>
+ <!-- flags is a string of the following characters: "S", "L", "W" -->
+ <!-- S logs statistical information (query execution times) -->
+ <!-- L logs the low-level queries (in SQL) -->
+ <!-- W logs some warnings (for mathql experts only) -->
+ <!-- By default the above information is not logged -->
+ <key name="flags"></key>
</section>
<section name="local_library">
<key name="dir">file://$(users_settings.per_user_work_directory)/objects</key>
(* 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";;
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)
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
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
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)
(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
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
close_out oc
let main () =
- let mqi_flags = [] in (* default MathQL interpreter options *)
try
Sys.catch_break true;
at_exit (fun () ->
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'
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 =
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;
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
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
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.
Http_common.debug := true;;
(* Http_common.debug := true;; *)
-let mqi_flags = [] (* default MathQL interpreter options *)
-
open Printf;;
let daemon_name = "Search Engine";;
(* 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" *)
| "/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
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)
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
-
projects / helm.git / commitdiff