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