json_util.ml 25.4 KB
Newer Older
1
open Itp_communication
2 3
open Controller_itp
open Call_provers
4
open Json_base
5

6
(* TODO match exceptions and complete some cases *)
7 8

let convert_prover_to_json (p: Whyconf.prover) =
9 10 11 12
  Record (convert_record
    ["prover_name", String p.Whyconf.prover_name;
     "prover_version", String p.Whyconf.prover_version;
     "prover_altern", String p.Whyconf.prover_altern])
13 14

let convert_infos (i: global_information) =
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17 18
  let convert_prover (s,p) =
    Record (convert_record ["prover_shorcut", String s;
                            "prover_name", String p])
  in
19
  Record (convert_record
MARCHE Claude's avatar
MARCHE Claude committed
20
    ["provers", List (List.map convert_prover i.provers);
21 22 23
     "transformations", List (List.map (fun x -> String x) i.transformations);
     "strategies", List (List.map (fun x -> String x) i.strategies);
     "commands", List (List.map (fun x -> String x) i.commands)])
24 25 26 27 28 29 30 31 32 33 34 35 36

let convert_prover_answer (pa: prover_answer) =
  match pa with
  | Valid             -> String "Valid"
  | Invalid           -> String "Invalid"
  | Timeout           -> String "Timeout"
  | OutOfMemory       -> String "OutOfMemory"
  | StepLimitExceeded -> String "StepLimitExceeded"
  | Unknown _         -> String "Unknown"
  | Failure _         -> String "Failure"
  | HighFailure       -> String "HighFailure"

let convert_limit (l: Call_provers.resource_limit) =
37 38 39 40
  Record (convert_record
    ["limit_time", Int l.Call_provers.limit_time;
     "limit_mem", Int l.Call_provers.limit_mem;
     "limit_steps", Int l.Call_provers.limit_steps])
41 42 43 44 45 46 47 48 49 50 51 52

let convert_unix_process (ps: Unix.process_status) =
  match ps with
  | Unix.WEXITED _   -> String "WEXITED"
  | Unix.WSIGNALED _ -> String "WSIGNALED"
  | Unix.WSTOPPED _  -> String "WSTOPPED"

let convert_model (m: Model_parser.model) =
  String (Pp.string_of (fun fmt m -> Model_parser.print_model fmt m) m)

(* TODO pr_model should have a different format *)
let convert_proof_result (pr: prover_result) =
53 54 55 56 57 58 59
  Record (convert_record
    ["pr_answer", convert_prover_answer pr.pr_answer;
     "pr_status", convert_unix_process pr.pr_status;
     "pr_output", String pr.pr_output;
     "pr_time", Float pr.pr_time;
     "pr_steps", Int pr.pr_steps;
     "pr_model", convert_model pr.pr_model])
60 61

let convert_proof_attempt (pas: proof_attempt_status) =
62
  Record (match pas with
63
  | Unedited ->
64
      convert_record ["proof_attempt", String "Unedited"]
65
  | JustEdited ->
66
      convert_record ["proof_attempt", String "JustEdited"]
67
  | Interrupted ->
68
      convert_record ["proof_attempt", String "Interrupted"]
69
  | Scheduled ->
70
      convert_record ["proof_attempt", String "Scheduled"]
71
  | Running ->
72
      convert_record ["proof_attempt", String "Running"]
73
  | Done pr ->
74 75
      convert_record ["proof_attempt", String "Done";
                      "prover_result", convert_proof_result pr]
76
  | Controller_itp.InternalFailure e ->
77 78
      convert_record ["proof_attempt", String "InternalFailure";
                      "exception", String (Pp.string_of Exn_printer.exn_printer e)]
79
  | Uninstalled p ->
80 81
      convert_record ["proof_attempt", String "Uninstalled";
                      "prover", convert_prover_to_json p])
82 83

let convert_update u =
84
  Record (match u with
85
  | Proved b ->
86
      convert_record ["update_info", String "Proved";
87 88
             "proved", Bool b]
  | Proof_status_change (pas, b, l) ->
89
      convert_record ["update_info", String "Proof_status_change";
90 91 92
             "proof_attempt", convert_proof_attempt pas;
             "obsolete", Bool b;
             "limit", convert_limit l]
93
  | Obsolete b ->
94 95
      convert_record ["update_info", String "Obsolete";
           "obsolete", Bool b])
96 97 98

let convert_notification_constructor n =
  match n with
Sylvain Dailler's avatar
Sylvain Dailler committed
99 100 101 102 103 104 105 106 107 108
  | New_node _                   -> String "New_node"
  | Node_change _                -> String "Node_change"
  | Remove _                     -> String "Remove"
  | Next_Unproven_Node_Id (_, _) -> String "Next_Unproven_Node_Id"
  | Initialized _                -> String "Initialized"
  | Saved                        -> String "Saved"
  | Message _                    -> String "Message"
  | Dead _                       -> String "Dead"
  | Task _                       -> String "Task"
  | File_contents _              -> String "File_contents"
109

110
let convert_node_type_string nt =
111
  match nt with
112 113 114 115 116 117 118 119 120
  | NRoot           -> "NRoot"
  | NFile           -> "NFile"
  | NTheory         -> "NTheory"
  | NTransformation -> "NTransformation"
  | NGoal           -> "NGoal"
  | NProofAttempt   -> "NProofAttempt"

let convert_node_type nt =
  String (convert_node_type_string nt)
121 122 123

let convert_request_constructor (r: ide_request) =
  match r with
Sylvain Dailler's avatar
Sylvain Dailler committed
124 125 126 127
  | Command_req _             -> String "Command_req"
  | Prove_req _               -> String "Prove_req"
  | Transform_req _           -> String "Transform_req"
  | Strategy_req _            -> String "Strategy_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
128
  | Edit_req _                -> String "Edit_req"
129
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
130
  | Open_session_req _        -> String "Open_session_req"
131
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
132
  | Add_file_req _            -> String "Add_file_req"
MARCHE Claude's avatar
MARCHE Claude committed
133
  | Save_file_req _           -> String "Save_file_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
134 135
  | Set_max_tasks_req _       -> String "Set_max_tasks_req"
  | Get_file_contents _       -> String "Get_file_contents"
Sylvain Dailler's avatar
Sylvain Dailler committed
136 137
  | Focus_req _               -> String "Focus_req"
  | Unfocus_req               -> String "Unfocus_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
138 139 140 141 142 143
  | Get_task _                -> String "Get_task"
  | Remove_subtree _          -> String "Remove_subtree"
  | Copy_paste _              -> String "Copy_paste"
  | Copy_detached _           -> String "Copy_detached"
  | Get_first_unproven_node _ -> String "Get_first_unproven_node"
  | Get_Session_Tree_req      -> String "Get_Session_Tree_req"
144
  | Mark_obsolete_req _       -> String "Mark_obsolete_req"
145
  | Clean_req                 -> String "Clean_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
146 147 148 149
  | Save_req                  -> String "Save_req"
  | Reload_req                -> String "Reload_req"
  | Replay_req                -> String "Replay_req"
  | Exit_req                  -> String "Exit_req"
150
  | Interrupt_req             -> String "Interrupt_req"
151

152
let print_request_to_json (r: ide_request): Json_base.json =
153
  let cc = convert_request_constructor in
154
  Record (
155 156
  match r with
  | Command_req (nid, s) ->
157
      convert_record ["ide_request", cc r;
158 159
           "node_ID", Int nid;
           "command", String s]
160
  | Prove_req (nid, p, l) ->
161
      convert_record ["ide_request", cc r;
162 163 164
           "node_ID", Int nid;
           "prover", String p;
           "limit", convert_limit l]
165
  | Transform_req (nid, tr, args) ->
166
      convert_record ["ide_request", cc r;
167 168
           "node_ID", Int nid;
           "transformation", String tr;
169
           "arguments", List (List.map (fun x -> String x) args)]
170
  | Strategy_req (nid, str) ->
171
      convert_record ["ide_request", cc r;
172 173
           "node_ID", Int nid;
           "strategy", String str]
Sylvain Dailler's avatar
Sylvain Dailler committed
174 175 176 177
  | Edit_req (nid, prover) ->
      convert_record ["ide_request", cc r;
                      "node_ID", Int nid;
                      "prover", String prover]
178
(*
179
  | Open_session_req f ->
180
      convert_record ["ide_request", cc r;
181
           "file", String f]
182
*)
183
  | Add_file_req f ->
184
      convert_record ["ide_request", cc r;
185
           "file", String f]
MARCHE Claude's avatar
MARCHE Claude committed
186
  | Save_file_req (f,_) ->
187
      convert_record ["ide_request", cc r;
MARCHE Claude's avatar
MARCHE Claude committed
188
           "file", String f]
189
  | Set_max_tasks_req n ->
190
      convert_record ["ide_request", cc r;
191
           "tasks", Int n]
192
  | Get_task n ->
193
      convert_record ["ide_request", cc r;
194 195
           "node_ID", Int n]
  | Get_file_contents s ->
196
      convert_record ["ide_request", cc r;
197
           "file", String s]
198
  | Remove_subtree n ->
199
      convert_record ["ide_request", cc r;
200
           "node_ID", Int n]
Sylvain Dailler's avatar
Sylvain Dailler committed
201
  | Copy_paste (from_id, to_id) ->
202 203 204
      convert_record ["ide_request", cc r;
           "node_ID1", Int from_id;
           "node_ID2", Int to_id]
Sylvain Dailler's avatar
Sylvain Dailler committed
205
  | Copy_detached from_id ->
206
      convert_record ["ide_request", cc r;
207
           "node_ID", Int from_id]
Sylvain Dailler's avatar
Sylvain Dailler committed
208
  | Get_first_unproven_node id ->
209
      convert_record ["ide_request", cc r;
Sylvain Dailler's avatar
Sylvain Dailler committed
210
           "node_ID", Int id]
Sylvain Dailler's avatar
Sylvain Dailler committed
211 212 213 214 215
  | Focus_req id ->
      convert_record ["ide_request", cc r;
                      "node_ID", Int id]
  | Unfocus_req ->
      convert_record ["ide_request", cc r]
216
  | Get_Session_Tree_req ->
217
      convert_record ["ide_request", cc r]
218
  | Mark_obsolete_req n ->
219
      convert_record ["ide_request", cc r;
220
           "node_ID", Int n]
221
  | Clean_req ->
222
      convert_record ["ide_request", cc r]
223
  | Save_req ->
224
      convert_record ["ide_request", cc r]
225
  | Reload_req ->
226
      convert_record ["ide_request", cc r]
227
  | Replay_req ->
228
      convert_record ["ide_request", cc r]
229
  | Exit_req ->
230
      convert_record ["ide_request", cc r]
231
  | Interrupt_req ->
232
      convert_record ["ide_request", cc r])
233 234 235

let convert_constructor_message (m: message_notification) =
  match m with
236 237 238 239 240 241 242 243 244 245 246 247
  | Proof_error _         -> String "Proof_error"
  | Transf_error _        -> String "Transf_error"
  | Strat_error _         -> String "Strat_error"
  | Replay_Info _         -> String "Replay_Info"
  | Query_Info _          -> String "Query_Info"
  | Query_Error _         -> String "Query_Error"
  | Help _                -> String "Help"
  | Information _         -> String "Information"
  | Task_Monitor _        -> String "Task_Monitor"
  | Parse_Or_Type_Error _ -> String "Parse_Or_Type_Error"
  | Error _               -> String "Error"
  | Open_File_Error _     -> String "Open_File_Error"
MARCHE Claude's avatar
MARCHE Claude committed
248
  | File_Saved _          -> String "File_Saved"
249

Sylvain Dailler's avatar
Sylvain Dailler committed
250 251 252 253 254 255 256
let convert_loc (loc: Loc.position) : Json_base.json =
  let (file, line, col1, col2) = Loc.get loc in
  Record (convert_record ["file", Json_base.String file;
                          "line", Json_base.Int line;
                          "col1", Json_base.Int col1;
                          "col2", Json_base.Int col2])

257 258
let convert_message (m: message_notification) =
  let cc = convert_constructor_message in
259
  Record (match m with
260
  | Proof_error (nid, s) ->
261
      convert_record ["mess_notif", cc m;
262 263
           "node_ID", Int nid;
           "error", String s]
264
  | Transf_error (nid, s) ->
265
      convert_record ["mess_notif", cc m;
266 267
           "node_ID", Int nid;
           "error", String s]
268
  | Strat_error (nid, s) ->
269
      convert_record ["mess_notif", cc m;
270 271
           "node_ID", Int nid;
           "error", String s]
272
  | Replay_Info s ->
273
      convert_record ["mess_notif", cc m;
274
           "replay_info", String s]
275
  | Query_Info (nid, s) ->
276
      convert_record ["mess_notif", cc m;
277 278
           "node_ID", Int nid;
           "qinfo", String s]
279
  | Query_Error (nid, s) ->
280
      convert_record ["mess_notif", cc m;
281 282
           "node_ID", Int nid;
           "qerror", String s]
283
  | Help s ->
284
      convert_record ["mess_notif", cc m;
285
           "qhelp", String s]
286
  | Information s ->
287
      convert_record ["mess_notif", cc m;
288
           "information", String s]
289
  | Task_Monitor (n, k, p) ->
290 291
      convert_record ["mess_notif", cc m;
           "monitor", List [Int n; Int k; Int p]]
Sylvain Dailler's avatar
Sylvain Dailler committed
292
  | Parse_Or_Type_Error (loc, s) ->
293
      convert_record ["mess_notif", cc m;
Sylvain Dailler's avatar
Sylvain Dailler committed
294 295
                      "loc", convert_loc loc;
                      "error", String s]
296
  | Error s ->
297
      convert_record ["mess_notif", cc m;
298
           "error", String s]
299
  | Open_File_Error s ->
300
      convert_record ["mess_notif", cc m;
301
           "open_error", String s]
MARCHE Claude's avatar
MARCHE Claude committed
302
  | File_Saved s ->
303 304
      convert_record ["mess_notif", cc m;
           "information", String s])
305

306
let convert_color (color: color) : Json_base.json =
307 308 309 310 311 312
  Json_base.String (
    match color with
    | Neg_premise_color -> "Neg_premise_color"
    | Premise_color -> "Premise_color"
    | Goal_color -> "Goal_color")

313
let convert_loc_color (loc,color: Loc.position * color) : Json_base.json =
314 315
  let loc = convert_loc loc in
  let color = convert_color color in
316
  Record (convert_record ["loc", loc; "color", color])
317

318
let convert_list_loc (l: (Loc.position * color) list) : json =
319
  let list_of_loc = List.map convert_loc_color l in
320
  List list_of_loc
321 322 323

exception Notcolor

324
let parse_color (j: json) : color =
325 326 327 328 329 330 331 332
  match j with
  | String "Neg_premise_color" -> Neg_premise_color
  | String "Premise_color"     -> Premise_color
  | String "Goal_color"        -> Goal_color
  | _ -> raise Notcolor

exception Notposition

333 334 335 336 337 338
let parse_loc (j: json) : Loc.position =
  try
    let file = get_string (get_field j "file") in
    let line = get_int (get_field j "line") in
    let col1 = get_int (get_field j "col1") in
    let col2 = get_int (get_field j "col2") in
339
    Loc.user_position file line col1 col2
340 341
  with
    Not_found -> raise Notposition
342

343 344 345 346
let parse_loc_color (j: json): Loc.position * color =
  let loc = parse_loc j in
  let color = parse_color j in
  (loc, color)
347

348
let parse_list_loc (j: json): (Loc.position * color) list =
349
  match j with
350
  | List l -> List.map parse_loc_color l
351 352
  | _ -> raise Notposition

353
let print_notification_to_json (n: notification): json =
354
  let cc = convert_notification_constructor in
355
  Record (
356
  match n with
357
  | New_node (nid, parent, node_type, name, detached) ->
358
      convert_record ["notification", cc n;
359 360 361 362 363
           "node_ID", Int nid;
           "parent_ID", Int parent;
           "node_type", convert_node_type node_type;
           "name", String name;
           "detached", Bool detached]
364
  | Node_change (nid, update) ->
365
      convert_record ["notification", cc n;
366 367
           "node_ID", Int nid;
           "update", convert_update update]
368
  | Remove nid ->
369
      convert_record ["notification", cc n;
370
           "node_ID", Int nid]
Sylvain Dailler's avatar
Sylvain Dailler committed
371
  | Next_Unproven_Node_Id (from_id, unproved_id) ->
372 373 374
      convert_record ["notification", cc n;
           "node_ID1", Int from_id;
           "node_ID2", Int unproved_id]
375
  | Initialized infos ->
376
      convert_record ["notification", cc n;
377
           "infos", convert_infos infos]
378
  | Saved ->
379
      convert_record ["notification", cc n]
380
  | Message m ->
381
      convert_record ["notification", cc n;
382
           "message", convert_message m]
383
  | Dead s ->
384
      convert_record ["notification", cc n;
385
           "message", String s]
386
  | Task (nid, s, list_loc) ->
387
      convert_record ["notification", cc n;
388
           "node_ID", Int nid;
389 390
           "task", String s;
           "list_loc", convert_list_loc list_loc]
391
  | File_contents (f, s) ->
392
      convert_record ["notification", cc n;
393
           "file", String f;
394
           "content", String s])
395 396

let print_notification fmt (n: notification) =
397
  Format.fprintf fmt "%a" print_json (print_notification_to_json n)
398 399

let print_request fmt (r: ide_request) =
400
  Format.fprintf fmt "%a" print_json (print_request_to_json r)
401 402 403 404 405 406

let print_list_notification fmt (nl: notification list) =
  Format.fprintf fmt "%a" (Json_base.list print_notification) nl

let print_list_request fmt (rl: ide_request list) =
  Format.fprintf fmt "%a" (Json_base.list print_request) rl
407 408 409

exception NotProver

410 411 412 413 414 415 416
let parse_prover_from_json (j: json) =
  try
    let pn = get_string (get_field j "prover_name") in
    let pv = get_string (get_field j "prover_version") in
    let pa = get_string (get_field j "prover_altern") in
    {Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
  with Not_found -> raise NotProver
417 418 419

exception NotLimit

420 421 422 423 424 425 426
let parse_limit_from_json (j: json) =
  try
    let t = get_int (get_field j "limit_time") in
    let m = get_int (get_field j "limit_mem") in
    let s = get_int (get_field j "limit_steps") in
    {limit_time = t; limit_mem = m; limit_steps = s}
  with Not_found -> raise NotLimit
427 428 429

exception NotRequest of string

430 431 432 433 434
let parse_request (constr: string) j =
  match constr with
  | "Command_req" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "command") in
435
    Command_req (nid, s)
436 437 438 439 440

  | "Prove_req" ->
    let nid = get_int (get_field j "node_ID") in
    let p = get_string (get_field j "prover") in
    let l = get_field j "limit" in
441
    Prove_req (nid, p, parse_limit_from_json l)
442 443 444 445 446

  | "Transform_req" ->
    let nid = get_int (get_field j "node_ID") in
    let tr = get_string (get_field j "transformation") in
    let args = get_list (get_field j "arguments") in
447 448 449 450 451
    Transform_req (nid, tr,
                   List.map (fun x ->
                     match x with
                     | String t -> t
                     | _ -> raise (NotRequest "")) args)
452 453 454 455

  | "Strategy_req" ->
    let nid = get_int (get_field j "node_ID") in
    let str = get_string (get_field j "strategy") in
456
    Strategy_req (nid, str)
457

Sylvain Dailler's avatar
Sylvain Dailler committed
458 459 460 461
  | "Edit_req" ->
    let nid = get_int (get_field j "node_ID") in
    let p = get_string (get_field j "prover") in
    Edit_req (nid, p)
462
(*
463 464
  | "Open_session_req" ->
    let f = get_string (get_field j "file") in
465
    Open_session_req f
466
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
467 468 469 470 471 472 473
  | "Focus_req" ->
    let nid = get_int (get_field j "node_ID") in
    Focus_req nid

  | "Unfocus_req" ->
    Unfocus_req

474 475
  | "Add_file_req" ->
    let f = get_string (get_field j "file") in
476
    Add_file_req f
477 478 479

  | "Set_max_tasks_req" ->
    let n = get_int (get_field j "tasks") in
480
    Set_max_tasks_req n
481 482 483

  | "Get_task" ->
    let n = get_int (get_field j "node_ID") in
484
    Get_task n
485 486 487

  | "Remove_subtree" ->
    let n = get_int (get_field j "node_ID") in
488
    Remove_subtree n
489 490 491 492

  | "Copy_paste" ->
    let from_id = get_int (get_field j "node_ID1") in
    let to_id = get_int (get_field j "node_ID2") in
Sylvain Dailler's avatar
Sylvain Dailler committed
493
    Copy_paste (from_id, to_id)
494 495 496

  | "Copy_detached" ->
    let n = get_int (get_field j "node_ID") in
Sylvain Dailler's avatar
Sylvain Dailler committed
497
    Copy_detached n
498 499

  | "Get_Session_Tree_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
500
    Get_Session_Tree_req
501 502 503

  | "Mark_obsolete_req" ->
    let n = get_int (get_field j "node_ID") in
504
    Mark_obsolete_req n
505
  | "Clean_req" ->
506
    Clean_req
507
  | "Save_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
508
    Save_req
509
  | "Reload_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
510
    Reload_req
511
  | "Replay_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
512
    Replay_req
513
  | "Exit_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
514
    Exit_req
515 516
  | _ -> raise (NotRequest "")

517 518 519 520 521 522
let parse_request_json (j: json): ide_request =
  try
    let constr = get_string (get_field j "ide_request") in
    parse_request constr j
  with
  | _ -> let s =Pp.string_of print_json j in
523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562
    begin Format.eprintf "BEGIN \n %s \nEND\n@." s; raise (NotRequest s); end

exception NotNodeType

let parse_node_type_from_json j =
  match j with
  | String "NRoot"           -> NRoot
  | String "NFile"           -> NFile
  | String "NTheory"         -> NTheory
  | String "NTransformation" -> NTransformation
  | String "NGoal"           -> NGoal
  | String "NProofAttempt"   -> NProofAttempt
  | _                        -> raise NotNodeType

exception NotProverAnswer

let parse_prover_answer j =
  match j with
  | String "Valid"             -> Valid
  | String "Invalid"           -> Invalid
  | String "Timeout"           -> Timeout
  | String "OutOfMemory"       -> OutOfMemory
  | String "StepLimitExceeded" -> StepLimitExceeded
  | String "Unknown"           -> raise NotProverAnswer (* TODO *)
  | String "Failure"           -> raise NotProverAnswer (* TODO *)
  | String "HighFailure"       -> HighFailure
  | _                          -> raise NotProverAnswer

exception NotUnixProcess

let parse_unix_process j =
  match j with
  | String "WEXITED" -> Unix.WEXITED 0 (* TODO dummy value *)
  | String "WSIGNALED" -> Unix.WSIGNALED 0 (* TODO dummy value *)
  | String "WSTOPPED" -> Unix.WSTOPPED 0 (* TODO dummy value *)
  | _ -> raise NotUnixProcess

exception NotProverResult

let parse_prover_result j =
563 564 565 566 567 568 569 570 571 572 573 574 575 576
  try
    let pr_answer = get_field j "pr_answer" in
    let pr_status_unix = get_field j "pr_status" in
    let pr_output = get_string (get_field j "pr_output") in
    let pr_time = get_float (get_field j "pr_time") in
    let pr_steps = get_int (get_field j "pr_steps") in
    let pr_model = get_string (get_field j "pr_model") in
    {pr_answer = parse_prover_answer pr_answer;
     pr_status = parse_unix_process pr_status_unix;
     pr_output = pr_output;
     pr_time = pr_time;
     pr_steps = pr_steps;
     pr_model = Obj.magic pr_model} (* TODO pr_model is a string, should be model *)
  with
577 578 579 580 581
  | _ -> raise NotProverResult

exception NotProofAttempt

let parse_proof_attempt j =
582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
  let s = get_string (get_field j "proof_attempt") in
  match s with
  | "Unedited" -> Unedited
  | "JustEdited" -> JustEdited
  | "Interrupted" -> Interrupted
  | "Scheduled" -> Scheduled
  | "Running" -> Running
  | "Done" ->
    let pr = get_field j "prover_result" in
    Done (parse_prover_result pr)
  | "InternalFailure" ->
    raise NotProofAttempt (* TODO *)
  | "Uninstalled" ->
    let p = get_field j "prover" in
    Uninstalled (parse_prover_from_json p)
597 598 599 600 601
  | _ -> raise NotProofAttempt

exception NotUpdate

let parse_update j =
602 603 604 605
  let update = get_string (get_field j "update_info") in
  match update with
  | "Proved" ->
    let b = get_bool (get_field j "proved") in
606
    Proved b
607 608 609 610
  | "Proof_status_change" ->
    let pas = get_field j "proof_attempt" in
    let b = get_bool (get_field j "obsolete") in
    let l = get_field j "limit" in
611
    Proof_status_change (parse_proof_attempt pas, b, parse_limit_from_json l)
612 613
  | "Obsolete" ->
    let b = get_bool (get_field j "obsolete") in
614
    Obsolete b
615 616 617 618 619
  | _ -> raise NotUpdate

exception NotInfos

let parse_infos j =
620 621 622 623 624
  try
    let pr = get_list (get_field j "provers") in
    let tr = get_list (get_field j "transformations") in
    let str = get_list (get_field j "strategies") in
    let com = get_list (get_field j "commands") in
MARCHE Claude's avatar
MARCHE Claude committed
625 626 627 628
    {provers = List.map (fun j -> try
                                 (get_string (get_field j "prover_shortcut"),
                                  get_string (get_field j "prover_name"))
                               with Not_found -> raise NotInfos) pr;
629 630 631 632
     transformations = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) tr;
     strategies = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) str;
     commands = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) com}
  with _ -> raise NotInfos
633 634 635

exception NotMessage

636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689
let parse_message constr j =
  match constr with
  | "Proof_error" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "error") in
    Proof_error (nid, s)

  | "Transf_error" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "error") in
    Transf_error (nid, s)

  | "Strat_error" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "error") in
    Strat_error (nid, s)

  | "Replay_Info" ->
    let s = get_string (get_field j "replay_info") in
    Replay_Info s
  | "Query_Info" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "qinfo") in
    Query_Info (nid, s)

  | "Query_Error" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "qerror") in
    Query_Error (nid, s)

  | "Help" ->
    let s = get_string (get_field j "qhelp") in
    Help s

  | "Information" ->
    let s = get_string (get_field j "information") in
    Information s

  | "Task_Monitor" ->
    let m = get_list (get_field j "monitor") in
    begin
      match m with
      | Int n :: Int k :: Int p :: [] -> Task_Monitor (n, k, p)
      | _ -> raise NotMessage
    end

  | "Error" ->
    let s = get_string (get_field j "error") in
    Error s

  | "Open_File_Error" ->
    let s = get_string (get_field j "open_error") in
    Open_File_Error s

Sylvain Dailler's avatar
Sylvain Dailler committed
690 691 692 693 694
  | "Parse_Or_Type_Error" ->
    let loc = parse_loc (get_field j "loc") in
    let error = get_string (get_field j "error") in
    Parse_Or_Type_Error (loc, error)

695 696 697 698
  | _ -> raise NotMessage


let parse_message j =
699 700
  let constr = get_string (get_field j "mess_notif") in
  parse_message constr j
701

MARCHE Claude's avatar
MARCHE Claude committed
702
exception NotNotification of string
703

704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
let parse_notification constr j =
  match constr with
  | "New_node" ->
    let nid = get_int (get_field j "node_ID") in
    let parent = get_int (get_field j "parent_ID") in
    let node_type = get_field j "node_type" in
    let name = get_string (get_field j "name") in
    let detached = get_bool (get_field j "detached") in
    New_node (nid, parent, parse_node_type_from_json node_type, name, detached)

  | "Node_change" ->
    let nid = get_int (get_field j "node_ID") in
    let update = get_field j "update" in
    Node_change (nid, parse_update update)

  | "Remove" ->
    let nid = get_int (get_field j "node_ID") in
    Remove nid

  | "Initialized" ->
    let infos = get_field j "infos" in
    Initialized (parse_infos infos)

  | "Saved" -> Saved

  | "Message" ->
    let m = get_field j "message" in
    Message (parse_message m)

  | "Dead" ->
    let s = get_string (get_field j "message") in
    Dead s

  | "Task" ->
    let nid = get_int (get_field j "node_ID") in
    let s = get_string (get_field j "task") in
    let l = get_field j "loc_list" in
    Task (nid, s, parse_list_loc l)

  | "Next_Unproven_Node_Id" ->
    let nid1 = get_int (get_field j "node_ID1") in
    let nid2 = get_int (get_field j "node_ID2") in
    Next_Unproven_Node_Id (nid1, nid2)

  | "File_contents" ->
    let f = get_string (get_field j "file") in
    let s = get_string (get_field j "content") in
    File_contents(f,s)

  | s -> raise (NotNotification ("<from parse_notification> " ^ s))
754

755
let parse_notification_json j =
756 757 758 759
  try
    let constr = get_string (get_field j "notification") in
    parse_notification constr j
  with
MARCHE Claude's avatar
MARCHE Claude committed
760
  | _ -> raise (NotNotification "<from parse_notification_json>")
761 762 763

let parse_json_object (s: string) =
  let lb = Lexing.from_string s in
764
  let x = Json_parser.value (fun x -> Json_lexer.read x) lb in
765 766 767 768
  x

let parse_notification (s: string) : notification =
  let json = parse_json_object s in
769
  parse_notification_json json
770 771 772

let parse_request (s: string) : ide_request =
  let json = parse_json_object s in
773 774 775 776 777 778
  parse_request_json json


let parse_list_notification (s: string): notification list =
  let json = parse_json_object s in
  match json with
779 780
  | List [Null] -> []
  | List l -> List.map parse_notification_json l
Sylvain Dailler's avatar
Sylvain Dailler committed
781
  | _ -> []
782 783 784 785

let parse_list_request (s: string): ide_request list =
  let json = parse_json_object s in
  match json with
786
  | List l -> List.map parse_request_json l
787
  | _ -> raise (NotRequest "Not list")