worker_proto.ml 1.33 KB
Newer Older
1
type id = string
Kim Nguyễn's avatar
Kim Nguyễn committed
2
type loc = int * int * int * int
3
type why3_loc = int * int * int (* line, column, length *)
Kim Nguyễn's avatar
Kim Nguyễn committed
4
type status = [`New | `Valid | `Unknown ]
5
type why3_command =  ParseBuffer of string
6
              | ExecuteBuffer of string
7
              | Transform of [ `Prove | `Split | `Clean ] * id
Kim Nguyễn's avatar
Kim Nguyễn committed
8
              | SetStatus of status * id
9

10
type why3_output = Error of string (* msg *)
Kim Nguyễn's avatar
Kim Nguyễn committed
11 12
                 | ErrorLoc of (loc * string) (* loc * msg *)
                 | Theory of id * string (* Theory (id, name) *)
13
                 | Task of (id * id * string * string * why3_loc list) (* id, parent id, expl, code, location list *)
Kim Nguyễn's avatar
Kim Nguyễn committed
14
                 | Result of string list
15
                 | UpdateStatus of status * id
16

Kim Nguyễn's avatar
Kim Nguyễn committed
17
type prover_command = OptionSteps of int | Goal of id * string
18
type prover_output = Valid | Unknown of string | Invalid of string
19 20 21 22 23 24 25

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
26 27 28
let status_of_result = function
    (id, Valid) -> SetStatus(`Valid, id)
  | (id, _) -> SetStatus(`Unknown, id)
29 30 31 32 33 34

let log s = ignore (Firebug.console ## log (Js.string s))
let log_time s =
  let date = jsnew Js.date_now () in
  let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
  log (date_str ^ " : " ^ s)