why3web.ml 2.86 KB
Newer Older
1 2 3 4 5

open Why3

module P = struct

MARCHE Claude's avatar
MARCHE Claude committed
6
 let notifications = ref []
7

MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11
 let notify n = notifications := n :: ! notifications

 let get_notifications () =
   let l = !notifications in notifications := []; List.rev l
12

13 14 15 16 17 18
 let requests = ref []

 let push_request r =
   requests := r :: !requests

 let get_requests () =
MARCHE Claude's avatar
MARCHE Claude committed
19
   let l = !requests in requests := []; List.rev l
20 21 22

end

MARCHE Claude's avatar
MARCHE Claude committed
23 24 25
open Itp_server

module S = Make (Wserver) (P)
26 27 28

open Format

29 30
let interp_request args =
  match args with
MARCHE Claude's avatar
MARCHE Claude committed
31
  | "list-provers" -> (Command_req "list-provers", root_node)
32 33
  | _ -> invalid_arg "Why3web.interp_request"

MARCHE Claude's avatar
MARCHE Claude committed
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
let print_message_notification fmt n =
  match n with
  | Proof_error(nid,s) -> ()
  | Transf_error(nid,s) -> ()
  | Strat_error(nid,s) -> ()
  | Replay_Info(s) -> ()
  | Query_Info(nid,s) -> fprintf fmt "kind=\"query_info\", node=\"%d\", text=\"%s\"" nid s
  | Query_Error(nid,s) -> fprintf fmt "kind=\"query_error\", node=\"%d\", text=\"%s\"" nid s
  | Help s -> fprintf fmt "kind=\"help\", text=\"%s\"" s
  | Information s -> fprintf fmt "kind=\"information\", text=\"%s\"" s
  | Task_Monitor(a,b,c) -> ()

let print_notification fmt n =
  match n with
  | Node_change(nid,info) -> ()
  | New_node(nid,nid',nodetype,info) -> ()
  | Remove(nid) -> ()
  | Initialized(ginfo) -> ()
  | Saved -> ()
  | Message n -> fprintf fmt "{ notification=\"message=\"; %a }"
                              print_message_notification n
  | Dead s -> ()
  | Proof_update(nid,status) -> ()
  | Task(nid,task) -> ()

59 60
let handle_script s args =
  match s with
61 62 63 64 65 66 67 68
  | "request" ->
     begin
       try P.push_request (interp_request args);
           "{ \"request_received\": \"" ^ args ^ "\" }"
       with e ->
         "{ \"request_error\": \"" ^ args ^ "\" ; \"error\": \"" ^
           (Pp.sprintf "%a" Exn_printer.exn_printer e) ^ "\" } "
     end
69
    | "getNotifications" ->
MARCHE Claude's avatar
MARCHE Claude committed
70 71
       let n = P.get_notifications () in
       Pp.sprintf "getNotifications: %a@." (Pp.print_list Pp.space print_notification) n
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
    | _ -> "bad request"

let plist fmt l =
  List.iter  (fun x -> fprintf fmt "'%s'@\n" x) l

let string_of_addr addr =
  match addr with
    | Unix.ADDR_UNIX s -> s
    | Unix.ADDR_INET (ie,i) ->
	(Unix.string_of_inet_addr ie)^":"^string_of_int(i)

let handler (addr,req) script cont fmt =
       eprintf "addr : %s@." (string_of_addr addr);
       eprintf "req: @[%a@]@." plist req;
       eprintf "script: `%s'@." script;
       eprintf "cont: `%s'@." cont;
       let ans = handle_script script cont in
       Wserver.http_header fmt "HTTP/1.0 200 OK";
       fprintf fmt "Access-Control-Allow-Origin: *\n";
       fprintf fmt "\n"; (* end of header *)
       fprintf fmt "%s" ans;
       fprintf fmt "@."

95 96 97 98 99 100 101 102 103 104 105
let help () =
  printf "Available commands:@.";
  printf "q : quit@."

let stdin_handler s =
  match s with
    | "?" -> help ()
    | "q" -> exit 0
    | _ -> printf "unknown command '%s'@." s

let () = Wserver.main_loop None 6789 handler stdin_handler