X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fsearch_pattern_apply_tutor.ml;h=8ba1f8386b7c4846b2b8b4fbb07c2135fab54e2a;hb=0e74e8e94eada756157addce67e4adeb8dff1feb;hp=0893c195f0843492b277f217cd8da3ed03a31432;hpb=969950f7f464f94f2918a844833395920a51319c;p=helm.git diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index 0893c195f..8ba1f8386 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -4,6 +4,9 @@ open Printf;; exception Empty_must;; +module MQI = MQueryInterpreter +module MQIC = MQIConn + let broker_id = ref None let my_own_id = Hbugs_tutors_common.init_tutor () let my_own_addr, my_own_port = "127.0.0.1", 50011 @@ -15,7 +18,7 @@ let is_authenticated id = | Some broker_id -> id = broker_id (* thread who do the dirty work *) -let slave (state, musing_id) = +let slave mqi_handle (state, musing_id) = try prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id); let (proof, goal) = Hbugs_tutors_common.load_state state in @@ -29,7 +32,7 @@ let slave (state, musing_id) = | hd::tl -> hd in let uris = - TacticChaser.searchPattern + TacticChaser.matchConclusion mqi_handle ~output_html:prerr_endline ~choose_must () ~status:(proof, goal) in if uris = [] then @@ -55,7 +58,7 @@ let slave (state, musing_id) = (* exception ==> no additional arm *) raise (unbox_exception e) -let hbugs_callback = +let hbugs_callback mqi_handle = let ids = Hashtbl.create 17 in let forbidden () = prerr_endline "ignoring request from unauthorized broker"; @@ -66,7 +69,7 @@ let hbugs_callback = if is_authenticated broker_id then begin prerr_endline "received Start_musing"; let new_musing_id = Hbugs_id_generator.new_musing_id () in - let id = Hbugs_deity.create slave (state, new_musing_id) in + let id = Hbugs_deity.create (slave mqi_handle) (state, new_musing_id) in prerr_endline (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id); Hashtbl.add ids new_musing_id id ; @@ -92,10 +95,10 @@ let hbugs_callback = Exception ("unexpected_msg", Hbugs_messages.string_of_msg unexpected_msg) -let callback (req: Http_types.request) outchan = +let callback mqi_handle (req: Http_types.request) outchan = try let req_msg = Hbugs_messages.msg_of_string req#body in - let answer = hbugs_callback req_msg in + let answer = hbugs_callback mqi_handle req_msg in Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan with Hbugs_messages.Parse_error (subj, reason) -> Http_daemon.respond @@ -103,25 +106,18 @@ let callback (req: Http_types.request) outchan = (Exception ("parse_error", reason))) outchan -let postgresqlconnectionstring = - try - Sys.getenv "POSTGRESQL_CONNECTION_STRING" - with - Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" -;; - let main () = + let mqi_flags = [] in (* default MathQL interpreter options *) try Sys.catch_break true; at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id); broker_id := Some (Hbugs_tutors_common.register_to_broker my_own_id my_own_url "FOO" "Search_pattern_apply tutor"); - Mqint.set_database Mqint.postgres_db ; - Mqint.init postgresqlconnectionstring ; + let mqi_handle = MQIC.init mqi_flags prerr_string in Http_daemon.start' - ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback; - Mqint.close () + ~addr:my_own_addr ~port:my_own_port ~mode:`Thread (callback mqi_handle); + MQIC.close mqi_handle with Sys.Break -> () (* exit nicely, invoking at_exit functions *) ;;