why3web.ml 3.89 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
31
  | "list-provers" -> (Command_req (root_node,"list-provers"))
32 33
  | _ -> invalid_arg "Why3web.interp_request"

MARCHE Claude's avatar
MARCHE Claude committed
34 35
let print_message_notification fmt n =
  match n with
36 37 38 39 40 41
  | Error _s -> ()
  | Open_File_Error _s -> ()
  | Proof_error(_nid,_s) -> ()
  | Transf_error(_nid,_s) -> ()
  | Strat_error(_nid,_s) -> ()
  | Replay_Info(_s) -> ()
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45
  | 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
46
  | Task_Monitor(_a,_b,_c) -> ()
MARCHE Claude's avatar
MARCHE Claude committed
47 48 49

let print_notification fmt n =
  match n with
50 51 52 53
  | Node_change(_nid,_info) -> ()
  | New_node(_nid,_nid',_nodetype,_info) -> ()
  | Remove(_nid) -> ()
  | Initialized(_ginfo) -> ()
MARCHE Claude's avatar
MARCHE Claude committed
54 55 56
  | Saved -> ()
  | Message n -> fprintf fmt "{ notification=\"message=\"; %a }"
                              print_message_notification n
57 58
  | Dead _s -> ()
  | Task(_nid,_task) -> ()
MARCHE Claude's avatar
MARCHE Claude committed
59

60 61
let handle_script s args =
  match s with
62 63 64 65 66 67 68 69
  | "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
70
    | "getNotifications" ->
MARCHE Claude's avatar
MARCHE Claude committed
71
       let n = P.get_notifications () in
72 73
       (* if n <> [] then  *)
         Pp.sprintf "getNotifications: %a@." (Pp.print_list Pp.space print_notification) n
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
    | _ -> "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 "@."

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

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

107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133
(************************)
(* parsing command line *)
(************************)

let files : string Queue.t = Queue.create ()

let opt_parser = ref None

let spec = Arg.align [
  "-F", Arg.String (fun s -> opt_parser := Some s),
      "<format> select input format (default: \"why\")";
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
(*
  "-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<file> add file to the project (ignored if it is already there)";
*)
  Termcode.arg_extra_expl_prefix
]

let usage_str = sprintf
  "Usage: %s [options] [<file.why>|<project directory>]..."
  (Filename.basename Sys.argv.(0))


let () =
134 135 136
    let config, base_config, env =
      Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
    in
137 138 139
    if Queue.is_empty files then
      Whyconf.Args.exit_with_usage spec usage_str;
    Queue.iter (fun f -> P.push_request (Itp_server.Open_session_req f)) files;
140
    S.init_server config env;
141
    Wserver.main_loop None 6789 handler stdin_handler