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=4790ab88ab7620c1d89045a8873f1ced8e838c85;hpb=03dee221bd1f2c9a6e7f74d9abf88be14aac7763;p=helm.git

diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
index 4790ab88a..be2c68d70 100644
--- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml
+++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
@@ -4,17 +4,15 @@ open Printf;;
 
 exception Empty_must;;
 
-module MQICallbacks =
-   struct
-      let log s = prerr_string s
-   end
-
-module MQI = MQueryInterpreter.Make(MQICallbacks)
+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
@@ -22,7 +20,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
@@ -36,7 +34,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
@@ -62,7 +60,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";
@@ -73,10 +71,9 @@ 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
-        prerr_endline
-         (sprintf "starting a new musing (tid = %d, id = %s)" id new_musing_id);
-        Hashtbl.add ids new_musing_id 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 *)
@@ -99,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
@@ -110,18 +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 () =
-  let mqi_options = "" in (* default MathQL interpreter options *)
   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");
-    ignore (MQI.init mqi_options) ;
+    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;
-    MQI.close mqi_options
+      ~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 *)
 ;;