X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Ftutors%2Fsearch_pattern_apply_tutor.ml;fp=helm%2Fhbugs%2Ftutors%2Fsearch_pattern_apply_tutor.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=8ba1f8386b7c4846b2b8b4fbb07c2135fab54e2a;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml
deleted file mode 100644
index 8ba1f8386..000000000
--- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml
+++ /dev/null
@@ -1,125 +0,0 @@
-
-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_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 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_common.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_Luke 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_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 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 = 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 ;
-        (*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
-          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 ();
-  | 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 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");
-    let mqi_handle = MQIC.init mqi_flags prerr_string in 
-    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 ()
-