worker_proto.ml 2.16 KB
Newer Older
Kim Nguyễn's avatar
Kim Nguyễn committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Kim Nguyễn's avatar
Kim Nguyễn committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
type id = string
Kim Nguyễn's avatar
Kim Nguyễn committed
13
type loc = int * int * int * int
14
type why3_loc = string * (int * int * int) (* kind, line, column, length *)
Kim Nguyễn's avatar
Kim Nguyễn committed
15
type status = [`New | `Valid | `Unknown ]
16

17
type why3_command =  ParseBuffer of string
18 19
		   | ExecuteBuffer of string
		   | ProveAll
20
		   | Transform of [ `Prove of int | `Split | `Clean ] * id
21
		   | SetStatus of status * id
22

23
type why3_output = Error of string (* msg *)
Kim Nguyễn's avatar
Kim Nguyễn committed
24 25
                 | ErrorLoc of (loc * string) (* loc * msg *)
                 | Theory of id * string (* Theory (id, name) *)
26 27
                 | Task of (id * id * string * string * why3_loc list * string * int)
                 (* id, parent id, expl, code, location list, pretty, steps*)
Kim Nguyễn's avatar
Kim Nguyễn committed
28
                 | Result of string list
29
                 | UpdateStatus of status * id
30
                 | Warning of ((int*int) * string) list
31
                 | Idle
32

33
type prover_command = OptionSteps of int | Goal of id * string * int
34
type prover_output = Valid | Unknown of string | Invalid of string
35 36 37 38 39 40 41

let marshal a =
  Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))

let unmarshal a =
  Marshal.from_string (Scanf.unescaped (Js.to_string a)) 0

Kim Nguyễn's avatar
Kim Nguyễn committed
42 43 44
let status_of_result = function
    (id, Valid) -> SetStatus(`Valid, id)
  | (id, _) -> SetStatus(`Unknown, id)
45 46 47

let log s = ignore (Firebug.console ## log (Js.string s))
let log_time s =
48 49
  let date = new%js Js.date_now in
  let date_str = string_of_float (date ## getTime /. 1000.) in
50
  log (date_str ^ " : " ^ s)