worker_proto.ml 986 Bytes
Newer Older
1 2 3
type id = string

type why3_command =  ParseBuffer of string
4 5 6
              | ExecuteBuffer of string


7
type why3_output = Error of string (* msg *)
8
             | ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
9 10 11
             | Tasks of ((id * string) (* Theory (id, name) *)
                       * (id * string) (* Task (id, name *)
                       * (id * string * string)) (* VC (id, expl, code ) *)
12 13
             | Result of string list

14 15 16
type prover_command = OptionSteps of int | Task of id * string

type prover_output = Valid | Unknown of string | Invalid of string
17 18 19 20 21 22 23 24 25 26 27 28 29 30

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



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)