Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

worker_proto.ml 1.25 KB
Newer Older
1
type id = string
Kim Nguyễn's avatar
Kim Nguyễn committed
2 3
type loc = int * int * int * int
type status = [`New | `Valid | `Unknown ]
4
type why3_command =  ParseBuffer of string
5
              | ExecuteBuffer of string
Kim Nguyễn's avatar
Kim Nguyễn committed
6 7
              | Transform of [ `Split ] * id
              | SetStatus of status * id
8

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

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

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

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)