why3web.ml 4.89 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15

open Why3

module P = struct

MARCHE Claude's avatar
MARCHE Claude committed
16
 let notifications = ref []
17

MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21
 let notify n = notifications := n :: ! notifications

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

23 24 25 26 27 28
 let requests = ref []

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

 let get_requests () =
MARCHE Claude's avatar
MARCHE Claude committed
29
   let l = !requests in requests := []; List.rev l
30 31 32

end

33
open Itp_communication
MARCHE Claude's avatar
MARCHE Claude committed
34 35 36
open Itp_server

module S = Make (Wserver) (P)
37 38 39

open Format

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
(* Decode URI *)
let decode s =
  let b = Buffer.create (String.length s) in
  let i = ref 0 in
  while !i <= String.length s -1 do
    (match s.[!i] with
    (* | '+' -> Buffer.add_string b " " *)
    | '%' ->
        begin
          let a = int_of_string ("0x" ^ (String.sub s (!i + 1) 2)) in
          i := !i + 2;
          Buffer.add_char b (char_of_int a);
        end
    | a -> Buffer.add_char b a);
    i := !i + 1;
  done;
  Buffer.contents b

(* TODO make it cleaner and less inefficient with adapted functions *)
59
let interp_request args =
60 61 62 63 64 65 66 67 68 69 70
  match args with
  | args when Strings.has_prefix "reload" args -> Reload_req
  | args when Strings.has_prefix "list-provers" args ->
      Command_req (root_node,"list-provers")
  | args when Strings.has_prefix "command=" args ->
      let com = Strings.remove_prefix "command=" args in
      (match (Strings.bounded_split ',' com 2) with
      | n :: com :: [] ->
          Command_req (int_of_string n, com)
      | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'"))
  | args when Strings.has_prefix "gettask_" args ->
71
     let c = false in
72
     let loc = true in
73
     Get_task (int_of_string (Strings.remove_prefix "gettask_" args),c,loc)
MARCHE Claude's avatar
MARCHE Claude committed
74
  | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'")
75

76 77
let handle_script s args =
  match s with
78 79 80 81 82 83 84 85
  | "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
86 87 88 89
  | "getNotifications" ->
      let n = P.get_notifications () in
      Pp.sprintf "%a@." Json_util.print_list_notification n
  | _ -> "bad request"
90 91 92 93 94 95 96 97 98 99 100 101 102 103

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;
104
       let cont = decode cont in
105 106
       eprintf "cont: `%s'@." cont;
       let ans = handle_script script cont in
107
       eprintf "answer: `%s'@." ans;
108 109 110 111 112 113
       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 "@."

114 115 116 117 118 119 120 121 122 123
let help () =
  printf "Available commands:@.";
  printf "q : quit@."

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

124 125 126 127 128 129 130 131
(************************)
(* parsing command line *)
(************************)

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

let opt_parser = ref None

132
let spec = [
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  "-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 () =
151
    let config, _base_config, env =
152 153
      Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
    in
154 155 156 157 158 159 160 161
    let dir =
      try
        Server_utils.get_session_dir ~allow_mkdir:true files
      with Invalid_argument s ->
        Format.eprintf "Error: %s@." s;
        Whyconf.Args.exit_with_usage spec usage_str
    in
    S.init_server config env dir;
162
    Queue.iter (fun f -> P.push_request (Add_file_req f)) files;
163
    Wserver.main_loop None 6789 handler stdin_handler