json_util.ml 24.5 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) =
15 16 17 18 19
  Record (convert_record
    ["provers", List (List.map (fun x -> String x) i.provers);
     "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)])
20 21 22 23 24 25 26 27 28 29 30 31 32

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) =
33 34 35 36
  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])
37 38 39 40 41 42 43 44 45 46 47 48

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) =
49 50 51 52 53 54 55
  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])
56 57

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

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

let convert_notification_constructor n =
  match n with
Sylvain Dailler's avatar
Sylvain Dailler committed
95 96 97 98 99 100 101 102 103 104
  | 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"
105

106
let convert_node_type_string nt =
107
  match nt with
108 109 110 111 112 113 114 115 116
  | NRoot           -> "NRoot"
  | NFile           -> "NFile"
  | NTheory         -> "NTheory"
  | NTransformation -> "NTransformation"
  | NGoal           -> "NGoal"
  | NProofAttempt   -> "NProofAttempt"

let convert_node_type nt =
  String (convert_node_type_string nt)
117 118 119

let convert_request_constructor (r: ide_request) =
  match r with
Sylvain Dailler's avatar
Sylvain Dailler committed
120 121 122 123
  | 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
124
  | Edit_req _                -> String "Edit_req"
125
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
126
  | Open_session_req _        -> String "Open_session_req"
127
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
128
  | Add_file_req _            -> String "Add_file_req"
MARCHE Claude's avatar
MARCHE Claude committed
129
  | Save_file_req _           -> String "Save_file_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
130 131 132 133 134 135 136 137
  | Set_max_tasks_req _       -> String "Set_max_tasks_req"
  | Get_file_contents _       -> String "Get_file_contents"
  | 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"
138
  | Mark_obsolete_req _       -> String "Mark_obsolete_req"
139
  | Clean_req                 -> String "Clean_req"
Sylvain Dailler's avatar
Sylvain Dailler committed
140 141 142 143
  | Save_req                  -> String "Save_req"
  | Reload_req                -> String "Reload_req"
  | Replay_req                -> String "Replay_req"
  | Exit_req                  -> String "Exit_req"
144
  | Interrupt_req             -> String "Interrupt_req"
145

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

let convert_constructor_message (m: message_notification) =
  match m with
225 226 227 228 229 230 231 232 233 234 235 236
  | 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
237
  | File_Saved _          -> String "File_Saved"
238 239 240

let convert_message (m: message_notification) =
  let cc = convert_constructor_message in
241
  Record (match m with
242
  | Proof_error (nid, s) ->
243
      convert_record ["mess_notif", cc m;
244 245
           "node_ID", Int nid;
           "error", String s]
246
  | Transf_error (nid, s) ->
247
      convert_record ["mess_notif", cc m;
248 249
           "node_ID", Int nid;
           "error", String s]
250
  | Strat_error (nid, s) ->
251
      convert_record ["mess_notif", cc m;
252 253
           "node_ID", Int nid;
           "error", String s]
254
  | Replay_Info s ->
255
      convert_record ["mess_notif", cc m;
256
           "replay_info", String s]
257
  | Query_Info (nid, s) ->
258
      convert_record ["mess_notif", cc m;
259 260
           "node_ID", Int nid;
           "qinfo", String s]
261
  | Query_Error (nid, s) ->
262
      convert_record ["mess_notif", cc m;
263 264
           "node_ID", Int nid;
           "qerror", String s]
265
  | Help s ->
266
      convert_record ["mess_notif", cc m;
267
           "qhelp", String s]
268
  | Information s ->
269
      convert_record ["mess_notif", cc m;
270
           "information", String s]
271
  | Task_Monitor (n, k, p) ->
272 273
      convert_record ["mess_notif", cc m;
           "monitor", List [Int n; Int k; Int p]]
274
  | Parse_Or_Type_Error s ->
275
      convert_record ["mess_notif", cc m;
276
           "error", String s]
277
  | Error s ->
278
      convert_record ["mess_notif", cc m;
279
           "error", String s]
280
  | Open_File_Error s ->
281
      convert_record ["mess_notif", cc m;
282
           "open_error", String s]
MARCHE Claude's avatar
MARCHE Claude committed
283
  | File_Saved s ->
284 285
      convert_record ["mess_notif", cc m;
           "information", String s])
286

287
let convert_color (color: color) : Json_base.json =
288 289 290 291 292 293
  Json_base.String (
    match color with
    | Neg_premise_color -> "Neg_premise_color"
    | Premise_color -> "Premise_color"
    | Goal_color -> "Goal_color")

294
let convert_loc (loc: Loc.position) : Json_base.json =
295
  let (file, line, col1, col2) = Loc.get loc in
296 297 298 299
  Record (convert_record ["file", Json_base.String file;
                          "line", Json_base.Int line;
                          "col1", Json_base.Int col1;
                          "col2", Json_base.Int col2])
300

301
let convert_loc_color (loc,color: Loc.position * color) : Json_base.json =
302 303
  let loc = convert_loc loc in
  let color = convert_color color in
304
  Record (convert_record ["loc", loc; "color", color])
305

306
let convert_list_loc (l: (Loc.position * color) list) : json =
307
  let list_of_loc = List.map convert_loc_color l in
308
  List list_of_loc
309 310 311

exception Notcolor

312
let parse_color (j: json) : color =
313 314 315 316 317 318 319 320
  match j with
  | String "Neg_premise_color" -> Neg_premise_color
  | String "Premise_color"     -> Premise_color
  | String "Goal_color"        -> Goal_color
  | _ -> raise Notcolor

exception Notposition

321 322 323 324 325 326
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
327
    Loc.user_position file line col1 col2
328 329
  with
    Not_found -> raise Notposition
330

331 332 333 334
let parse_loc_color (j: json): Loc.position * color =
  let loc = parse_loc j in
  let color = parse_color j in
  (loc, color)
335

336
let parse_list_loc (j: json): (Loc.position * color) list =
337
  match j with
338
  | List l -> List.map parse_loc_color l
339 340
  | _ -> raise Notposition

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

let print_notification fmt (n: notification) =
385
  Format.fprintf fmt "%a" print_json (print_notification_to_json n)
386 387

let print_request fmt (r: ide_request) =
388
  Format.fprintf fmt "%a" print_json (print_request_to_json r)
389 390 391 392 393 394

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
395 396 397

exception NotProver

398 399 400 401 402 403 404
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
405 406 407

exception NotLimit

408 409 410 411 412 413 414
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
415 416 417

exception NotRequest of string

418 419 420 421 422
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
423
    Command_req (nid, s)
424 425 426 427 428

  | "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
429
    Prove_req (nid, p, parse_limit_from_json l)
430 431 432 433 434

  | "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
435 436 437 438 439
    Transform_req (nid, tr,
                   List.map (fun x ->
                     match x with
                     | String t -> t
                     | _ -> raise (NotRequest "")) args)
440 441 442 443

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

Sylvain Dailler's avatar
Sylvain Dailler committed
446 447 448 449
  | "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)
450
(*
451 452
  | "Open_session_req" ->
    let f = get_string (get_field j "file") in
453
    Open_session_req f
454
*)
455 456
  | "Add_file_req" ->
    let f = get_string (get_field j "file") in
457
    Add_file_req f
458 459 460

  | "Set_max_tasks_req" ->
    let n = get_int (get_field j "tasks") in
461
    Set_max_tasks_req n
462 463 464

  | "Get_task" ->
    let n = get_int (get_field j "node_ID") in
465
    Get_task n
466 467 468

  | "Remove_subtree" ->
    let n = get_int (get_field j "node_ID") in
469
    Remove_subtree n
470 471 472 473

  | "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
474
    Copy_paste (from_id, to_id)
475 476 477

  | "Copy_detached" ->
    let n = get_int (get_field j "node_ID") in
Sylvain Dailler's avatar
Sylvain Dailler committed
478
    Copy_detached n
479 480

  | "Get_Session_Tree_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
481
    Get_Session_Tree_req
482 483 484

  | "Mark_obsolete_req" ->
    let n = get_int (get_field j "node_ID") in
485
    Mark_obsolete_req n
486
  | "Clean_req" ->
487
    Clean_req
488
  | "Save_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
489
    Save_req
490
  | "Reload_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
491
    Reload_req
492
  | "Replay_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
493
    Replay_req
494
  | "Exit_req" ->
Sylvain Dailler's avatar
Sylvain Dailler committed
495
    Exit_req
496 497
  | _ -> raise (NotRequest "")

498 499 500 501 502 503
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
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
    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 =
544 545 546 547 548 549 550 551 552 553 554 555 556 557
  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
558 559 560 561 562
  | _ -> raise NotProverResult

exception NotProofAttempt

let parse_proof_attempt j =
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577
  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)
578 579 580 581 582
  | _ -> raise NotProofAttempt

exception NotUpdate

let parse_update j =
583 584 585 586
  let update = get_string (get_field j "update_info") in
  match update with
  | "Proved" ->
    let b = get_bool (get_field j "proved") in
587
    Proved b
588 589 590 591
  | "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
592
    Proof_status_change (parse_proof_attempt pas, b, parse_limit_from_json l)
593 594
  | "Obsolete" ->
    let b = get_bool (get_field j "obsolete") in
595
    Obsolete b
596 597 598 599 600
  | _ -> raise NotUpdate

exception NotInfos

let parse_infos j =
601 602 603 604 605 606 607 608 609 610
  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
    {provers = List.map (fun j -> match j with | String x -> x | _ -> raise NotInfos) pr;
     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
611 612 613

exception NotMessage

614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 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
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

668 669 670 671
  | _ -> raise NotMessage


let parse_message j =
672 673
  let constr = get_string (get_field j "mess_notif") in
  parse_message constr j
674

MARCHE Claude's avatar
MARCHE Claude committed
675
exception NotNotification of string
676

677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726
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))
727

728
let parse_notification_json j =
729 730 731 732
  try
    let constr = get_string (get_field j "notification") in
    parse_notification constr j
  with
MARCHE Claude's avatar
MARCHE Claude committed
733
  | _ -> raise (NotNotification "<from parse_notification_json>")
734 735 736

let parse_json_object (s: string) =
  let lb = Lexing.from_string s in
737
  let x = Json_parser.value (fun x -> Json_lexer.read x) lb in
738 739 740 741
  x

let parse_notification (s: string) : notification =
  let json = parse_json_object s in
742
  parse_notification_json json
743 744 745

let parse_request (s: string) : ide_request =
  let json = parse_json_object s in
746 747 748 749 750 751
  parse_request_json json


let parse_list_notification (s: string): notification list =
  let json = parse_json_object s in
  match json with
752 753
  | List [Null] -> []
  | List l -> List.map parse_notification_json l
Sylvain Dailler's avatar
Sylvain Dailler committed
754
  | _ -> []
755 756 757 758

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