X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fhbugs%2Fsearch_pattern_apply_tutor.ml;fp=helm%2Focaml%2Fhbugs%2Fsearch_pattern_apply_tutor.ml;h=79c94beedbce7d3b68e9b774063799a19328216a;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953

diff --git a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml
new file mode 100644
index 000000000..79c94beed
--- /dev/null
+++ b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml
@@ -0,0 +1,147 @@
+(* $Id$ *)
+
+open Hbugs_types;;
+open Printf;;
+
+exception Empty_must;;
+
+module MQI  = MQueryInterpreter
+module MQIC = MQIConn
+
+let broker_id = ref None
+let my_own_id = Hbugs_tutors.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
+  | None -> false
+  | Some broker_id -> id = broker_id
+
+  (* thread who do the dirty work *)
+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.load_state state in
+  let hint =
+    try
+      let choose_must must only = (* euristic: use 2nd precision level
+                                  1st is more precise but is more slow *)
+        match must with
+        | [] -> raise Empty_must
+        | _::hd::tl -> hd
+        | hd::tl -> hd
+      in
+      let uris =
+        TacticChaser.matchConclusion mqi_handle
+         ~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
+      in
+      if uris = [] then
+        Sorry
+      else
+        Eureka (Hints (List.map (fun uri -> Use_apply uri) uris))
+    with Empty_must -> Sorry
+  in
+  let answer = Musing_completed (my_own_id, musing_id, hint) in
+  ignore (Hbugs_messages.submit_req ~url:Hbugs_tutors.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 mqi_handle =
+  let ids = Hashtbl.create 17 in
+  let forbidden () =
+    prerr_endline "ignoring request from unauthorized broker";
+    Exception ("forbidden", "")
+  in
+  function
+  | Start_musing (broker_id, state) ->
+      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 = ExtThread.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 ..."; *)
+        (try
+          ExtThread.kill (Hashtbl.find ids musing_id) ;
+          Hashtbl.remove ids musing_id ;
+         with
+            Not_found
+          | ExtThread.Can_t_kill _ ->
+             prerr_endline ("Can not kill slave " ^ musing_id)) ;
+        Musing_aborted (my_own_id, musing_id)
+      end else (* broker unauthorized *)
+        forbidden ();
+  | unexpected_msg ->
+      Exception ("unexpected_msg",
+        Hbugs_messages.string_of_msg unexpected_msg)
+
+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 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
+      ~body:(Hbugs_messages.string_of_msg
+        (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 () ->
+      if dump_environment_on_exit then
+        dump_environment ();
+      Hbugs_tutors.unregister_from_broker my_own_id);
+    broker_id :=
+      Some (Hbugs_tutors.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 mqi_handle);
+    MQIC.close mqi_handle
+  with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
+;;
+
+main ()
+