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