X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fsearch_pattern_apply_tutor.ml;h=be2c68d702c00b7d337a68f2e6bfe7e3446226c6;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=531e94e0eae552df99896c198d1c62346740ce3a;hpb=ed90e027472d0250d45ae7200600c8804dd476f1;p=helm.git diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index 531e94e0e..be2c68d70 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -4,10 +4,15 @@ 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 let my_own_url = sprintf "%s:%d" my_own_addr my_own_port +let environment_file = "search_pattern_apply.environment" +let dump_environment_on_exit = false let is_authenticated id = match !broker_id with @@ -15,7 +20,8 @@ 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 let hint = @@ -28,8 +34,8 @@ let slave (state, musing_id) = | hd::tl -> hd in let uris = - TacticChaser.searchPattern ~choose_must () ~status:(proof, goal) -(* ["cic:/pippo.con"; "cic:/pluto.con"] *) + TacticChaser.matchConclusion mqi_handle + ~output_html:prerr_endline ~choose_must () ~status:(proof, goal) in if uris = [] then Sorry @@ -41,8 +47,21 @@ let slave (state, musing_id) = ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors_common.broker_url answer); prerr_endline (sprintf "Bye, I've completed my duties (success = %b)" (hint <> Sorry)) + with + (Pxp_types.At _) as e -> + let rec unbox_exception = + function + Pxp_types.At (_,e) -> unbox_exception e + | e -> e + in + prerr_endline ("Uncaught PXP exception: " ^ Pxp_types.string_of_exn e) ; + (* e could be the Thread.exit exception; otherwise we will release an *) + (* uncaught exception and the Pxp_types.At was already an uncaught *) + (* 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"; Exception ("forbidden", "") @@ -52,15 +71,24 @@ 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 - prerr_endline - (sprintf "starting a new musing (id = %s)" new_musing_id); - ignore (Thread.create slave (state, new_musing_id)); + let id = Hbugs_deity.create (slave mqi_handle) (state, new_musing_id) in + prerr_endline (sprintf "starting a new musing (id = %s)" new_musing_id); + Hashtbl.add ids new_musing_id id; + (*ignore (Thread.create slave (state, new_musing_id));*) Musing_started (my_own_id, new_musing_id) end else (* broker unauthorized *) forbidden (); | Abort_musing (broker_id, musing_id) -> + prerr_endline "CSC: Abort_musing received" ; if is_authenticated broker_id then begin - prerr_endline "Ignoring 'Abort_musing' message ..."; + (* prerr_endline "Ignoring 'Abort_musing' message ..."; *) + (try + Hbugs_deity.kill (Hashtbl.find ids musing_id) ; + Hashtbl.remove ids musing_id ; + with + Not_found + | Hbugs_deity.Can_t_kill _ -> + prerr_endline ("Can not kill slave " ^ musing_id)) ; Musing_aborted (my_own_id, musing_id) end else (* broker unauthorized *) forbidden (); @@ -68,10 +96,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 @@ -79,15 +107,38 @@ let callback (req: Http_types.request) outchan = (Exception ("parse_error", reason))) outchan +let restore_environment () = + let ic = open_in environment_file in + prerr_endline "Restoring environment ..."; + CicEnvironment.restore_from_channel + ~callback:(fun uri -> prerr_endline uri) ic; + prerr_endline "... done!"; + close_in ic + +let dump_environment () = + let oc = open_out environment_file in + prerr_endline "Dumping environment ..."; + CicEnvironment.dump_to_channel + ~callback:(fun uri -> prerr_endline uri) oc; + prerr_endline "... done!"; + close_out oc + let main () = try Sys.catch_break true; - at_exit (fun () -> Hbugs_tutors_common.unregister_from_broker my_own_id); + at_exit (fun () -> + if dump_environment_on_exit then + dump_environment (); + 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"); + let mqi_handle = MQIC.init ~log:prerr_string () in + if Sys.file_exists environment_file then + restore_environment (); Http_daemon.start' - ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback + ~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 *) ;;