Proof of concept on printing/parsing json request/notification for

why3ide.

Makefile.in

@@ -205,7 +205,7 @@ LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
 
 LIB_SESSION = compress xml termcode session session_itp \
               session_tools strategy strategy_parser controller_itp \
-	      session_scheduler server_utils itp_server
+	      session_scheduler server_utils itp_server json_util json_parser json_lexer
 
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \

src/ide/why3ide.ml

-open Format
 open Why3
+open Format
 open Gconfig
 open Stdlib
 open Ide_utils.History
@@ -8,10 +8,53 @@ external reset_gc : unit -> unit = "ml_reset_gc"
 
 let debug = Debug.lookup_flag "ide_info"
 
+open Itp_server
+
+(***************************)
+(* Debugging Json protocol *)
+(***************************)
+
+(* TODO This part is temporarly here because it is the only place it can be defined
+   without cyclic dependencies *)
+let parse_json_object (s: string) =
+  let lb = Lexing.from_string s in
+  let x = Json_parser.json_object (fun x -> Json_lexer.read x) lb in
+  x
+
+let parse_notification (s: string) : notification =
+  let json = parse_json_object s in
+  Json_util.parse_notification json
+
+let parse_request (s: string) : ide_request =
+  let json = parse_json_object s in
+  Json_util.parse_request json
+
+(* TODO remove exception handling in print_request_json and print_notification_json *)
+exception Badparsing
+
+let print_request_json fmt (r: ide_request) =
+  (try (
+    let s = Pp.string_of Json_util.print_request r in
+    let x = parse_request s in
+    if r = x then () else raise Badparsing)
+  with
+    _ -> Format.eprintf "Bad parsing@.");
+  Json_util.print_request fmt r
+
+let print_notification_json fmt (n: notification) =
+  (try (
+    let x = parse_notification (Pp.string_of Json_util.print_notification n) in
+    if n = x then () else raise Badparsing)
+  with
+    _ -> Format.eprintf "Bad parsing@.");
+  Json_util.print_notification fmt n
+
+let debug_json = Debug.register_flag "json_proto"
+    ~desc:"Print@ json@ requests@ and@ notifications@"
+
 (*******************)
 (* server protocol *)
 (*******************)
-open Itp_server
 
 module Protocol_why3ide = struct
 
@@ -20,7 +63,8 @@ module Protocol_why3ide = struct
 
   let print_request_debug r =
     Debug.dprintf debug_proto "[request]";
-    Debug.dprintf debug_proto "%a@." print_request r
+    Debug.dprintf debug_proto "%a@." print_request r;
+    Debug.dprintf debug_json "%a@." print_request_json r
 
   let print_msg_debug m =
     Debug.dprintf debug_proto "[message]";
@@ -28,7 +72,8 @@ module Protocol_why3ide = struct
 
   let print_notify_debug n =
     Debug.dprintf debug_proto "[notification]";
-    Debug.dprintf debug_proto "%a@." print_notify n
+    Debug.dprintf debug_proto "%a@." print_notify n;
+    Debug.dprintf debug_json "%a@." print_notification_json n
 
   let list_requests: ide_request list ref = ref []
 

src/session/json_lexer.mll

+(****************************************************************************)
+(* This is extracted/adapted from the code found in the book Real World Ocaml
+by Yaron Minsky, Anil Madhavapeddy, and Jason Hickey. Their 'unlicence' allows
+it. *)
+(****************************************************************************)
+
+{
+exception SyntaxError of string
+
+open Lexing
+open Json_parser
+}
+
+let int = '-'? ['0'-'9'] ['0'-'9']*
+let digit = ['0'-'9']
+let frac = '.' digit*
+let exp = ['e' 'E'] ['-' '+']? digit+
+let float = digit* frac? exp?
+let white = [' ' '\t']+
+let newline = '\r' | '\n' | "\r\n"
+let name = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*
+
+rule read =
+  parse
+  | white    { read lexbuf }
+  | newline  { new_line lexbuf; read lexbuf }
+  | int      { INT (int_of_string (Lexing.lexeme lexbuf)) }
+  | float    { FLOAT (float_of_string (Lexing.lexeme lexbuf)) }
+  | "true"   { TRUE }
+  | "false"  { FALSE }
+  | '"'      { read_string (Buffer.create 17) lexbuf }
+  | '{'      { LEFTBRC }
+  | '}'      { RIGHTBRC }
+  | '['      { LEFTSQ }
+  | ']'      { RIGHTSQ }
+  | ':'      { COLON }
+  | ','      { COMMA }
+  | _ { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) }
+  | eof      { EOF }
+
+and read_string buf =
+  parse
+  | '"'       { STRING (Buffer.contents buf) }
+  | '\\' '/'  { Buffer.add_char buf '/'; read_string buf lexbuf }
+  | '\\' '\\' { Buffer.add_char buf '\\'; read_string buf lexbuf }
+  | '\\' 'b'  { Buffer.add_char buf '\b'; read_string buf lexbuf }
+  | '\\' 'f'  { Buffer.add_char buf '\012'; read_string buf lexbuf }
+  | '\\' 'n'  { Buffer.add_char buf '\n'; read_string buf lexbuf }
+  | '\\' 'r'  { Buffer.add_char buf '\r'; read_string buf lexbuf }
+  | '\\' 't'  { Buffer.add_char buf '\t'; read_string buf lexbuf }
+  | [^ '"' '\\']+
+    { Buffer.add_string buf (Lexing.lexeme lexbuf);
+      read_string buf lexbuf
+    }
+  | _ { raise (SyntaxError ("Illegal string character: " ^ Lexing.lexeme lexbuf ^ (Buffer.contents buf))) }
+  | eof { raise (SyntaxError ("String is not terminated")) }

src/session/json_parser.mly

+(****************************************************************************)
+(* This is extracted/adapted from the code found in the book Real World Ocaml
+by Yaron Minsky, Anil Madhavapeddy, and Jason Hickey. Their 'unlicence' allows
+it. *)
+(****************************************************************************)
+%start <Json_util.json_object> json_object
+%token <int> INT
+%token <float> FLOAT
+%token <string> STRING
+%token TRUE
+%token FALSE
+%token LEFTBRC RIGHTBRC
+%token LEFTSQ
+%token RIGHTSQ
+%token COLON
+%token COMMA
+%token EOF
+%%
+
+json_object:
+| EOF { Json_util.Empty }
+| LEFTBRC RIGHTBRC { Json_util.Empty }
+(* Left recursive rule are more efficient *)
+| LEFTBRC members RIGHTBRC { Json_util.Assoc (List.rev $2) }
+
+members:
+| json_pair { [ $1 ] }
+| members COMMA json_pair { $3 :: $1 }
+
+array:
+| LEFTSQ RIGHTSQ { Json_util.Array [] }
+| LEFTSQ elements RIGHTSQ { Json_util.Array (List.rev $2) }
+
+elements:
+| value { [$1] }
+| elements COMMA value { $3 :: $1 }
+
+json_pair:
+| STRING COLON value { ($1, $3) }
+
+value:
+| STRING { Json_util.String $1 }
+| INT { Json_util.Int $1 }
+| FLOAT { Json_util.Float $1 }
+| json_object { $1 }
+| array { $1 }
+| TRUE { Json_util.Bool true}
+| FALSE { Json_util.Bool false }

src/session/json_util.ml

+open Itp_server
+open Controller_itp
+open Call_provers
+
+(* TODO match exceptions *)
+
+(* Simplified json value *)
+type json_object =
+  | Assoc of (string * json_object) list
+  | Array of json_object list
+  | Int of int
+  | Bool of bool
+  | Float of float
+  | String of string
+  | Empty
+
+let convert_prover_to_json (p: Whyconf.prover) =
+  Assoc ["prover_name", String p.Whyconf.prover_name;
+         "prover_version", String p.Whyconf.prover_version;
+         "prover_altern", String p.Whyconf.prover_altern]
+
+let convert_infos (i: global_information) =
+  Assoc ["provers", Array (List.map (fun x -> String x) i.provers);
+         "transformations", Array (List.map (fun x -> String x) i.transformations);
+         "strategies", Array (List.map (fun x -> String x) i.strategies);
+         "commands", Array (List.map (fun x -> String x) i.commands)]
+
+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) =
+  Assoc ["limit_time", Int l.Call_provers.limit_time;
+         "limit_mem", Int l.Call_provers.limit_mem;
+         "limit_steps", Int l.Call_provers.limit_steps]
+
+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) =
+  Assoc ["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]
+
+let convert_proof_attempt (pas: proof_attempt_status) =
+  match pas with
+  | Unedited ->
+      Assoc ["proof_attempt", String "Unedited"]
+  | JustEdited ->
+      Assoc ["proof_attempt", String "JustEdited"]
+  | Interrupted ->
+      Assoc ["proof_attempt", String "Interrupted"]
+  | Scheduled ->
+      Assoc ["proof_attempt", String "Scheduled"]
+  | Running ->
+      Assoc ["proof_attempt", String "Running"]
+  | Done pr ->
+      Assoc ["proof_attempt", String "Done";
+             "prover_result", convert_proof_result pr]
+  | Controller_itp.InternalFailure e ->
+      Assoc ["proof_attempt", String "InternalFailure";
+             "exception", String (Pp.string_of Exn_printer.exn_printer e)]
+  | Uninstalled p ->
+      Assoc ["proof_attempt", String "Uninstalled";
+             "prover", convert_prover_to_json p]
+
+let convert_update u =
+  match u with
+  | Proved b ->
+      Assoc ["update_info", String "Proved";
+             "proved", Bool b]
+  | Proof_status_change (pas, b, l) ->
+      Assoc ["update_info", String "Proof_status_change";
+             "proof_attempt", convert_proof_attempt pas;
+             "obsolete", Bool b;
+             "limit", convert_limit l]
+
+let convert_notification_constructor n =
+  match n with
+  | New_node _    -> String "New_node"
+  | Node_change _ -> String "Node_change"
+  | Remove _      -> String "Remove"
+  | Initialized _ -> String "Initialized"
+  | Saved         -> String "Saved"
+  | Message _     -> String "Message"
+  | Dead _        -> String "Dead"
+  | Task _        -> String "Task"
+
+let convert_node_type nt =
+  match nt with
+  | NRoot           -> String "NRoot"
+  | NFile           -> String "NFile"
+  | NTheory         -> String "NTheory"
+  | NTransformation -> String "NTransformation"
+  | NGoal           -> String "NGoal"
+  | NProofAttempt   -> String "NProofAttempt"
+
+let convert_request_constructor (r: ide_request) =
+  match r with
+  | Command_req _        -> String "Command_req"
+  | Prove_req _          -> String "Prove_req"
+  | Transform_req _      -> String "Transform_req"
+  | Strategy_req _       -> String "Strategy_req"
+  | Open_session_req _   -> String "Open_session_req"
+  | Add_file_req _       -> String "Add_file_req"
+  | Set_max_tasks_req _  -> String "Set_max_tasks_req"
+  | Get_task _           -> String "Get_task"
+  | Remove_subtree _     -> String "Remove_subtree"
+  | Get_Session_Tree_req -> String "Get_Session_Tree_req"
+  | Save_req             -> String "Save_req"
+  | Reload_req           -> String "Reload_req"
+  | Replay_req           -> String "Replay_req"
+  | Exit_req             -> String "Exit_req"
+
+let print_request_to_json (r: ide_request): json_object =
+  let cc = convert_request_constructor in
+  match r with
+  | Command_req (nid, s) ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int nid;
+             "command", String s]
+  | Prove_req (nid, p, l) ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int nid;
+             "prover", String p;
+             "limit", convert_limit l]
+  | Transform_req (nid, tr, args) ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int nid;
+             "transformation", String tr;
+             "arguments", Array (List.map (fun x -> String x) args)]
+  | Strategy_req (nid, str) ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int nid;
+             "strategy", String str]
+  | Open_session_req f ->
+      Assoc ["ide_request", cc r;
+             "file", String f]
+  | Add_file_req f ->
+      Assoc ["ide_request", cc r;
+             "file", String f]
+  | Set_max_tasks_req n ->
+      Assoc ["ide_request", cc r;
+             "tasks", Int n]
+  | Get_task n ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int n]
+  | Remove_subtree n ->
+      Assoc ["ide_request", cc r;
+             "node_ID", Int n]
+  | Get_Session_Tree_req ->
+      Assoc ["ide_request", cc r]
+  | Save_req ->
+      Assoc ["ide_request", cc r]
+  | Reload_req ->
+      Assoc ["ide_request", cc r]
+  | Replay_req ->
+      Assoc ["ide_request", cc r]
+  | Exit_req ->
+      Assoc ["ide_request", cc r]
+
+let convert_constructor_message (m: message_notification) =
+  match m with
+  | 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"
+  | Error _           -> String "Error"
+  | Open_File_Error _ -> String "Open_File_Error"
+
+
+let convert_message (m: message_notification) =
+  let cc = convert_constructor_message in
+  match m with
+  | Proof_error (nid, s) ->
+      Assoc ["mess_notif", cc m;
+             "node_ID", Int nid;
+             "error", String s]
+  | Transf_error (nid, s) ->
+      Assoc ["mess_notif", cc m;
+             "node_ID", Int nid;
+             "error", String s]
+  | Strat_error (nid, s) ->
+      Assoc ["mess_notif", cc m;
+             "node_ID", Int nid;
+             "error", String s]
+  | Replay_Info s ->
+      Assoc ["mess_notif", cc m;
+             "replay_info", String s]
+  | Query_Info (nid, s) ->
+      Assoc ["mess_notif", cc m;
+             "node_ID", Int nid;
+             "qinfo", String s]
+  | Query_Error (nid, s) ->
+      Assoc ["mess_notif", cc m;
+             "node_ID", Int nid;
+             "qerror", String s]
+  | Help s ->
+      Assoc ["mess_notif", cc m;
+             "qhelp", String s]
+  | Information s ->
+      Assoc ["mess_notif", cc m;
+             "information", String s]
+  | Task_Monitor (n, k, p) ->
+      Assoc ["mess_notif", cc m;
+             "monitor", Array [Int n; Int k; Int p]]
+  | Error s ->
+      Assoc ["mess_notif", cc m;
+             "error", String s]
+  | Open_File_Error s ->
+      Assoc ["mess_notif", cc m;
+             "open_error", String s]
+
+let print_notification_to_json (n: notification): json_object =
+  let cc = convert_notification_constructor in
+  match n with
+  | New_node (nid, parent, node_type, name) ->
+      Assoc ["notification", cc n;
+             "node_ID", Int nid;
+             "parent_ID", Int parent;
+             "node_type", convert_node_type node_type;
+             "name", String name]
+  | Node_change (nid, update) ->
+      Assoc ["notification", cc n;
+             "node_ID", Int nid;
+             "update", convert_update update]
+  | Remove nid ->
+      Assoc ["notification", cc n;
+             "node_ID", Int nid]
+  | Initialized infos ->
+      Assoc ["notification", cc n;
+             "infos", convert_infos infos]
+  | Saved ->
+      Assoc ["notification", cc n]
+  | Message m ->
+      Assoc ["notification", cc n;
+             "message", convert_message m]
+  | Dead s ->
+      Assoc ["notification", cc n;
+             "message", String s]
+  | Task (nid, s) ->
+      Assoc ["notification", cc n;
+             "node_ID", Int nid;
+             "task", String s]
+
+(* Needs to print strings as JSON strings. So we have to convert them before
+  they are printed *)
+let convert_string (s: string) =
+  Str.global_replace (Str.regexp "/") "\\/" s
+
+let rec print_pair fmt ((s, j): string * json_object) : unit =
+  Format.fprintf fmt "\"%s\" : %a" s print_json j
+
+and print_json fmt (j: json_object) : unit  =
+  match j with
+  | Assoc l -> Format.fprintf fmt "{ %a }" (Pp.print_list Pp.comma print_pair) l
+  | Array l -> Format.fprintf fmt "[ %a ]" (Pp.print_list Pp.comma print_json) l
+  | Int x -> Format.fprintf fmt "%d" x
+  | Bool b -> Format.fprintf fmt "%b" b
+  | Float f -> Format.fprintf fmt "%f" f
+  | String s -> Format.fprintf fmt "\"%s\"" (convert_string (String.escaped s))
+  | Empty -> Format.fprintf fmt "null"
+
+let print_notification fmt (n: notification) =
+  Format.fprintf fmt "%a" print_json (print_notification_to_json n)
+
+let print_request fmt (r: ide_request) =
+  Format.fprintf fmt "%a" print_json (print_request_to_json r)
+
+exception NotProver
+
+let parse_prover_from_json (j: json_object) =
+  match j with
+  | Assoc ["prover_name", String pn;
+           "prover_version", String pv;
+           "prover_altern", String pa] ->
+            {Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
+  | _ -> raise NotProver
+
+exception NotLimit
+
+let parse_limit_from_json (j: json_object) =
+  match j with
+  | Assoc ["limit_time", Int t;
+           "limit_mem", Int m;
+           "limit_steps", Int s] ->
+             {limit_time = t; limit_mem = m; limit_steps = s}
+  | _ -> raise NotLimit
+
+exception NotRequest of string
+
+let parse_request (constr: string) l =
+  match constr, l with
+  | "Command_req", ["node_ID", Int nid;
+                    "command", String s] ->
+    Command_req (nid, s)
+  | "Prove_req", ["node_ID", Int nid;
+                  "prover", String p;
+                  "limit", l] ->
+    Prove_req (nid, p, parse_limit_from_json l)
+  | "Transform_req", ["node_ID", Int nid;
+                      "transformation", String tr;
+                      "arguments", Array args] ->
+    Transform_req (nid, tr,
+                   List.map (fun x ->
+                     match x with
+                     | String t -> t
+                     | _ -> raise (NotRequest "")) args)
+  | "Strategy_req", ["node_ID", Int nid;
+                     "strategy", String str] ->
+    Strategy_req (nid, str)
+  | "Open_session_req", ["file", String f] ->
+    Open_session_req f
+  | "Add_file_req", ["file", String f] ->
+    Add_file_req f
+  | "Set_max_tasks_req", ["tasks", Int n] ->
+    Set_max_tasks_req n
+  | "Get_task", ["node_ID", Int n] ->
+    Get_task n
+  |  "Remove_subtree", ["node_ID", Int n] ->
+    Remove_subtree n
+  | "Get_Session_Tree_req", [] ->
+      Get_Session_Tree_req
+  | "Save_req", [] ->
+      Save_req
+  | "Reload_req", [] ->
+      Reload_req
+  | "Replay_req", [] ->
+      Replay_req
+  | "Exit_req", [] ->
+      Exit_req
+  | _ -> raise (NotRequest "")
+
+let parse_request (j: json_object): ide_request =
+  match j with
+  | Assoc (("ide_request", String constr) :: l) ->
+      parse_request constr l
+  | _ -> let s =Pp.string_of print_json j in
+    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 =
+  match j with
+  | Assoc ["pr_answer", pr_answer;
+           "pr_status", pr_status_unix;
+           "pr_output", String pr_output;
+           "pr_time", Float pr_time;
+           "pr_steps", Int pr_steps;
+           "pr_model", String pr_model] ->
+     {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;