components/hbugs/hbugs_tutors.ml

   1 (*
   2  * Copyright (C) 2003:
   3  *    Stefano Zacchiroli <zack@cs.unibo.it>
   4  *    for the HELM Team http://helm.cs.unibo.it/
   5  *
   6  *  This file is part of HELM, an Hypertextual, Electronic
   7  *  Library of Mathematics, developed at the Computer Science
   8  *  Department, University of Bologna, Italy.
   9  *
  10  *  HELM is free software; you can redistribute it and/or
  11  *  modify it under the terms of the GNU General Public License
  12  *  as published by the Free Software Foundation; either version 2
  13  *  of the License, or (at your option) any later version.
  14  *
  15  *  HELM is distributed in the hope that it will be useful,
  16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
  17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  18  *  GNU General Public License for more details.
  19  *
  20  *  You should have received a copy of the GNU General Public License
  21  *  along with HELM; if not, write to the Free Software
  22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  23  *  MA  02111-1307, USA.
  24  *
  25  *  For details, see the HELM World-Wide-Web page,
  26  *  http://helm.cs.unibo.it/
  27  *)
  28
  29 (* $Id$ *)
  30
  31 open Hbugs_types;;
  32 open Printf;;
  33
  34 let broker_url = "localhost:49081/act";;
  35 let dump_environment_on_exit = false;;
  36
  37 let init_tutor = Hbugs_id_generator.new_tutor_id;;
  38
  39   (** register a tutor to broker *)
  40 let register_to_broker id url hint_type dsc =
  41   try
  42     let res =
  43       Hbugs_messages.submit_req
  44         ~url:broker_url (Register_tutor (id, url, hint_type, dsc))
  45     in
  46     (match res with
  47     | Tutor_registered id ->
  48         prerr_endline (sprintf "Tutor registered, broker id: %s" id);
  49         id
  50     | unexpected_msg ->
  51         raise (Hbugs_messages.Unexpected_message unexpected_msg))
  52   with e ->
  53     failwith (sprintf "Can't register tutor to broker: uncaught exception: %s"
  54       (Printexc.to_string e))
  55 ;;
  56   (** unregister a tutor from the broker *)
  57 let unregister_from_broker id =
  58   let res = Hbugs_messages.submit_req ~url:broker_url (Unregister_tutor id) in
  59   match res with
  60   | Tutor_unregistered _ -> prerr_endline "Tutor unregistered!"
  61   | unexpected_msg ->
  62       failwith
  63         (sprintf "Can't unregister from broker, received unexpected msg: %s"
  64           (Hbugs_messages.string_of_msg unexpected_msg))
  65 ;;
  66
  67   (* typecheck a loaded proof *)
  68   (* TODO this is a cut and paste from gTopLevel.ml *)
  69 let typecheck_loaded_proof metasenv bo ty =
  70  let module T = CicTypeChecker in
  71   ignore (
  72    List.fold_left
  73     (fun metasenv ((_,context,ty) as conj) ->
  74       ignore (T.type_of_aux' metasenv context ty) ;
  75       metasenv @ [conj]
  76     ) [] metasenv) ;
  77   ignore (T.type_of_aux' metasenv [] ty) ;
  78   ignore (T.type_of_aux' metasenv [] bo)
  79 ;;
  80
  81 type xml_kind = Body | Type;;
  82 let mk_dtdname ~ask_dtd_to_the_getter dtd =
  83  if ask_dtd_to_the_getter then
  84   Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  85  else
  86   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
  87 ;;
  88   (** this function must be the inverse function of GTopLevel.strip_xml_headings
  89   *)
  90 let add_xml_headings ~kind s =
  91   let dtdname = mk_dtdname ~ask_dtd_to_the_getter:true "cic.dtd" in
  92   let root =
  93     match kind with
  94     | Body -> "CurrentProof"
  95     | Type -> "ConstantType"
  96   in
  97   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n" ^
  98   "<!DOCTYPE " ^ root ^ " SYSTEM \""^ dtdname ^ "\">\n\n" ^
  99   s
 100 ;;
 101
 102 let load_state (type_string, body_string, goal) =
 103   prerr_endline "a0";
 104   let ((tmp1, oc1), (tmp2, oc2)) =
 105     (Filename.open_temp_file "" "", Filename.open_temp_file "" "")
 106   in
 107   prerr_endline "a1";
 108   output_string oc1 (add_xml_headings ~kind:Type type_string);
 109   output_string oc2 (add_xml_headings ~kind:Body body_string);
 110   close_out oc1; close_out oc2;
 111   prerr_endline (sprintf "Proof Type available in %s" tmp1);
 112   prerr_endline (sprintf "Proof Body available in %s" tmp2);
 113   let (proof, goal) =
 114     prerr_endline "a2";
 115     (match CicParser.obj_of_xml tmp1 (Some tmp2) with
 116     | Cic.CurrentProof (_,metasenv,bo,ty,_) ->  (* TODO il primo argomento e' una URI valida o e' casuale? *)
 117         prerr_endline "a3";
 118         let uri = UriManager.uri_of_string "cic:/foo.con" in
 119         prerr_endline "a4";
 120         typecheck_loaded_proof metasenv bo ty;
 121         prerr_endline "a5";
 122         ((uri, metasenv, bo, ty), goal)
 123     | _ -> assert false)
 124   in
 125   prerr_endline "a6";
 126   Sys.remove tmp1; Sys.remove tmp2;
 127   (proof, goal)
 128
 129 (* tutors creation stuff from now on *)
 130
 131 module type HbugsTutor =
 132   sig
 133     val start: unit -> unit
 134   end
 135
 136 module type HbugsTutorDescription =
 137   sig
 138     val addr: string
 139     val port: int
 140     val tactic: ProofEngineTypes.tactic
 141     val hint: hint
 142     val hint_type: hint_type
 143     val description: string
 144     val environment_file: string
 145   end
 146
 147 module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
 148   struct
 149     let broker_id = ref None
 150     let my_own_id = init_tutor ()
 151     let my_own_addr, my_own_port = Dsc.addr, Dsc.port
 152     let my_own_url = sprintf "%s:%d" my_own_addr my_own_port
 153
 154     let is_authenticated id =
 155       match !broker_id with
 156       | None -> false
 157       | Some broker_id -> id = broker_id
 158
 159       (* thread who do the dirty work *)
 160     let slave (state, musing_id) =
 161       prerr_endline (sprintf "Hi, I'm the slave for musing %s" musing_id);
 162       let (proof, goal) = load_state state in
 163       let success =
 164         try
 165           ignore (Dsc.tactic (proof, goal));
 166           true
 167         with e -> false
 168       in
 169       let answer =
 170         Musing_completed
 171           (my_own_id, musing_id, (if success then Eureka Dsc.hint else Sorry))
 172       in
 173       ignore (Hbugs_messages.submit_req ~url:broker_url answer);
 174       prerr_endline
 175         (sprintf "Bye, I've completed my duties (success = %b)" success)
 176
 177     let hbugs_callback =
 178         (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
 179         work *)
 180       let slaves = Hashtbl.create 17 in
 181       let forbidden () =
 182         prerr_endline "ignoring request from unauthorized broker";
 183         Exception ("forbidden", "")
 184       in
 185       function  (* _the_ callback *)
 186       | Start_musing (broker_id, state) ->
 187           if is_authenticated broker_id then begin
 188             prerr_endline "received Start_musing";
 189             let new_musing_id = Hbugs_id_generator.new_musing_id () in
 190             prerr_endline
 191               (sprintf "starting a new musing (id = %s)" new_musing_id);
 192 (*             let slave_thread = Thread.create slave (state, new_musing_id) in *)
 193             let slave_thread =
 194               ExtThread.create slave (state, new_musing_id)
 195             in
 196             Hashtbl.add slaves new_musing_id slave_thread;
 197             Musing_started (my_own_id, new_musing_id)
 198           end else  (* broker unauthorized *)
 199             forbidden ();
 200       | Abort_musing (broker_id, musing_id) ->
 201           if is_authenticated broker_id then begin
 202             (try  (* kill thread responsible for "musing_id" *)
 203               let slave_thread = Hashtbl.find slaves musing_id in
 204               ExtThread.kill slave_thread;
 205               Hashtbl.remove slaves musing_id
 206             with
 207             | ExtThread.Can_t_kill (_, reason) ->
 208                 prerr_endline (sprintf "Unable to kill slave: %s" reason)
 209             | Not_found ->
 210                 prerr_endline (sprintf
 211                   "Can't find slave corresponding to musing %s, can't kill it"
 212                   musing_id));
 213             Musing_aborted (my_own_id, musing_id)
 214           end else (* broker unauthorized *)
 215             forbidden ();
 216       | unexpected_msg ->
 217           Exception ("unexpected_msg",
 218             Hbugs_messages.string_of_msg unexpected_msg)
 219
 220     let callback (req: Http_types.request) outchan =
 221       try
 222         let req_msg = Hbugs_messages.msg_of_string req#body in
 223         let answer = hbugs_callback req_msg in
 224         Http_daemon.respond ~body:(Hbugs_messages.string_of_msg answer) outchan
 225       with Hbugs_messages.Parse_error (subj, reason) ->
 226         Http_daemon.respond
 227           ~body:(Hbugs_messages.string_of_msg
 228             (Exception ("parse_error", reason)))
 229           outchan
 230
 231     let restore_environment () =
 232       let ic = open_in Dsc.environment_file in
 233       prerr_endline "Restoring environment ...";
 234       CicEnvironment.restore_from_channel
 235         ~callback:(fun uri -> prerr_endline uri) ic;
 236       prerr_endline "... done!";
 237       close_in ic
 238
 239     let dump_environment () =
 240       let oc = open_out Dsc.environment_file in
 241       prerr_endline "Dumping environment ...";
 242       CicEnvironment.dump_to_channel
 243         ~callback:(fun uri -> prerr_endline uri) oc;
 244       prerr_endline "... done!";
 245       close_out oc
 246
 247     let main () =
 248       try
 249         Sys.catch_break true;
 250         at_exit (fun () ->
 251           if dump_environment_on_exit then
 252             dump_environment ();
 253           unregister_from_broker my_own_id);
 254         broker_id :=
 255           Some (register_to_broker
 256             my_own_id my_own_url Dsc.hint_type Dsc.description);
 257         if Sys.file_exists Dsc.environment_file then
 258           restore_environment ();
 259         Http_daemon.start'
 260           ~addr:my_own_addr ~port:my_own_port ~mode:`Thread callback
 261       with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)
 262
 263     let start = main
 264
 265   end
 266