Skip to content

GitLab

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.

Commit 0e08fabb authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

Json related stuff put in util.

parent 1c3b0740
Hide whitespace changes
Inline Side-by-side
Showing with 128 additions and 154 deletions
Makefile.in
View file @ 0e08fabb
......@@ -166,8 +166,8 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
hashcons stdlib exn_printer pp json json_parser json_lexer debug loc \
lexlib print_tree cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \
task pretty dterm env trans printer model_parser
......@@ -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 json_util json_parser json_lexer
session_scheduler server_utils itp_server json_util
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
......
src/ide/why3ide.ml
View file @ 0e08fabb
......@@ -15,28 +15,14 @@ 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 *)
(* TODO remove 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
let x = Json_util.parse_request s in
if r = x then () else raise Badparsing)
with
_ -> Format.eprintf "Bad parsing@.");
......@@ -44,7 +30,7 @@ let print_request_json fmt (r: ide_request) =
let print_notification_json fmt (n: notification) =
(try (
let x = parse_notification (Pp.string_of Json_util.print_notification n) in
let x = Json_util.parse_notification (Pp.string_of Json_util.print_notification n) in
if n = x then () else raise Badparsing)
with
_ -> Format.eprintf "Bad parsing@.");
......
src/session/json_util.ml
View file @ 0e08fabb
open Itp_server
open Controller_itp
open Call_provers
open Json
(* 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
(* TODO match exceptions and complete some cases *)
let convert_prover_to_json (p: Whyconf.prover) =
Assoc ["prover_name", String p.Whyconf.prover_name;
Obj ["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);
Obj ["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)]
......@@ -37,7 +28,7 @@ let convert_prover_answer (pa: prover_answer) =
| HighFailure -> String "HighFailure"
let convert_limit (l: Call_provers.resource_limit) =
Assoc ["limit_time", Int l.Call_provers.limit_time;
Obj ["limit_time", Int l.Call_provers.limit_time;
"limit_mem", Int l.Call_provers.limit_mem;
"limit_steps", Int l.Call_provers.limit_steps]
......@@ -52,7 +43,7 @@ let convert_model (m: Model_parser.model) =
(* TODO pr_model should have a different format *)
let convert_proof_result (pr: prover_result) =
Assoc ["pr_answer", convert_prover_answer pr.pr_answer;
Obj ["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;
......@@ -62,32 +53,32 @@ let convert_proof_result (pr: prover_result) =
let convert_proof_attempt (pas: proof_attempt_status) =
match pas with
| Unedited ->
Assoc ["proof_attempt", String "Unedited"]
Obj ["proof_attempt", String "Unedited"]
| JustEdited ->
Assoc ["proof_attempt", String "JustEdited"]
Obj ["proof_attempt", String "JustEdited"]
| Interrupted ->
Assoc ["proof_attempt", String "Interrupted"]
Obj ["proof_attempt", String "Interrupted"]
| Scheduled ->
Assoc ["proof_attempt", String "Scheduled"]
Obj ["proof_attempt", String "Scheduled"]
| Running ->
Assoc ["proof_attempt", String "Running"]
Obj ["proof_attempt", String "Running"]
| Done pr ->
Assoc ["proof_attempt", String "Done";
Obj ["proof_attempt", String "Done";
"prover_result", convert_proof_result pr]
| Controller_itp.InternalFailure e ->
Assoc ["proof_attempt", String "InternalFailure";
Obj ["proof_attempt", String "InternalFailure";
"exception", String (Pp.string_of Exn_printer.exn_printer e)]
| Uninstalled p ->
Assoc ["proof_attempt", String "Uninstalled";
Obj ["proof_attempt", String "Uninstalled";
"prover", convert_prover_to_json p]
let convert_update u =
match u with
| Proved b ->
Assoc ["update_info", String "Proved";
Obj ["update_info", String "Proved";
"proved", Bool b]
| Proof_status_change (pas, b, l) ->
Assoc ["update_info", String "Proof_status_change";
Obj ["update_info", String "Proof_status_change";
"proof_attempt", convert_proof_attempt pas;
"obsolete", Bool b;
"limit", convert_limit l]
......@@ -131,59 +122,59 @@ let convert_request_constructor (r: ide_request) =
| Replay_req -> String "Replay_req"
| Exit_req -> String "Exit_req"
let print_request_to_json (r: ide_request): json_object =
let print_request_to_json (r: ide_request): Json.value =
let cc = convert_request_constructor in
match r with
| Command_req (nid, s) ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"node_ID", Int nid;
"command", String s]
| Prove_req (nid, p, l) ->
Assoc ["ide_request", cc r;
Obj ["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;
Obj ["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;
Obj ["ide_request", cc r;
"node_ID", Int nid;
"strategy", String str]
| Open_session_req f ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"file", String f]
| Add_file_req f ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"file", String f]
| Set_max_tasks_req n ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"tasks", Int n]
| Get_task n ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"node_ID", Int n]
| Remove_subtree n ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"node_ID", Int n]
| Copy_paste (from_id, to_id) ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"node_ID", Int from_id;
"node_ID", Int to_id]
| Copy_detached from_id ->
Assoc ["ide_request", cc r;
Obj ["ide_request", cc r;
"node_ID", Int from_id]
| Get_Session_Tree_req ->
Assoc ["ide_request", cc r]
Obj ["ide_request", cc r]
| Save_req ->
Assoc ["ide_request", cc r]
Obj ["ide_request", cc r]
| Reload_req ->
Assoc ["ide_request", cc r]
Obj ["ide_request", cc r]
| Replay_req ->
Assoc ["ide_request", cc r]
Obj ["ide_request", cc r]
| Exit_req ->
Assoc ["ide_request", cc r]
Obj ["ide_request", cc r]
let convert_constructor_message (m: message_notification) =
match m with
......@@ -204,106 +195,90 @@ let convert_message (m: message_notification) =
let cc = convert_constructor_message in
match m with
| Proof_error (nid, s) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"node_ID", Int nid;
"error", String s]
| Transf_error (nid, s) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"node_ID", Int nid;
"error", String s]
| Strat_error (nid, s) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"node_ID", Int nid;
"error", String s]
| Replay_Info s ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"replay_info", String s]
| Query_Info (nid, s) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"node_ID", Int nid;
"qinfo", String s]
| Query_Error (nid, s) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"node_ID", Int nid;
"qerror", String s]
| Help s ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"qhelp", String s]
| Information s ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"information", String s]
| Task_Monitor (n, k, p) ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"monitor", Array [Int n; Int k; Int p]]
| Error s ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"error", String s]
| Open_File_Error s ->
Assoc ["mess_notif", cc m;
Obj ["mess_notif", cc m;
"open_error", String s]
let print_notification_to_json (n: notification): json_object =
let print_notification_to_json (n: notification): Json.value =
let cc = convert_notification_constructor in
match n with
| New_node (nid, parent, node_type, name, detached) ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"node_ID", Int nid;
"parent_ID", Int parent;
"node_type", convert_node_type node_type;
"name", String name;
"detached", Bool detached]
| Node_change (nid, update) ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"node_ID", Int nid;
"update", convert_update update]
| Remove nid ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"node_ID", Int nid]
| Initialized infos ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"infos", convert_infos infos]
| Saved ->
Assoc ["notification", cc n]
Obj ["notification", cc n]
| Message m ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"message", convert_message m]
| Dead s ->
Assoc ["notification", cc n;
Obj ["notification", cc n;
"message", String s]
| Task (nid, s) ->
Assoc ["notification", cc n;
Obj ["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)
Format.fprintf fmt "%a" Json.print (print_notification_to_json n)
let print_request fmt (r: ide_request) =
Format.fprintf fmt "%a" print_json (print_request_to_json r)
Format.fprintf fmt "%a" Json.print (print_request_to_json r)
exception NotProver
let parse_prover_from_json (j: json_object) =
let parse_prover_from_json (j: Json.value) =
match j with
| Assoc ["prover_name", String pn;
| Obj ["prover_name", String pn;
"prover_version", String pv;
"prover_altern", String pa] ->
{Whyconf.prover_name = pn; prover_version = pv; prover_altern = pa}
......@@ -311,9 +286,9 @@ let parse_prover_from_json (j: json_object) =
exception NotLimit
let parse_limit_from_json (j: json_object) =
let parse_limit_from_json (j: Json.value) =
match j with
| Assoc ["limit_time", Int t;
| Obj ["limit_time", Int t;
"limit_mem", Int m;
"limit_steps", Int s] ->
{limit_time = t; limit_mem = m; limit_steps = s}
......@@ -367,11 +342,11 @@ let parse_request (constr: string) l =
Exit_req
| _ -> raise (NotRequest "")
let parse_request (j: json_object): ide_request =
let parse_request (j: Json.value): ide_request =
match j with
| Assoc (("ide_request", String constr) :: l) ->
| Obj (("ide_request", String constr) :: l) ->
parse_request constr l
| _ -> let s =Pp.string_of print_json j in
| _ -> let s =Pp.string_of Json.print j in
begin Format.eprintf "BEGIN \n %s \nEND\n@." s; raise (NotRequest s); end
exception NotNodeType
......@@ -413,7 +388,7 @@ exception NotProverResult
let parse_prover_result j =
match j with
| Assoc ["pr_answer", pr_answer;
| Obj ["pr_answer", pr_answer;
"pr_status", pr_status_unix;
"pr_output", String pr_output;
"pr_time", Float pr_time;
......@@ -431,23 +406,23 @@ exception NotProofAttempt
let parse_proof_attempt j =
match j with
| Assoc ["proof_attempt", String "Unedited"] ->
| Obj ["proof_attempt", String "Unedited"] ->
Unedited
| Assoc ["proof_attempt", String "JustEdited"] ->
| Obj ["proof_attempt", String "JustEdited"] ->
JustEdited
| Assoc ["proof_attempt", String "Interrupted"] ->
| Obj ["proof_attempt", String "Interrupted"] ->
Interrupted
| Assoc ["proof_attempt", String "Scheduled"] ->
| Obj ["proof_attempt", String "Scheduled"] ->
Scheduled
| Assoc ["proof_attempt", String "Running"] ->
| Obj ["proof_attempt", String "Running"] ->
Running
| Assoc ["proof_attempt", String "Done";
| Obj ["proof_attempt", String "Done";
"prover_result", pr] ->
Done (parse_prover_result pr)
| Assoc ["proof_attempt", String "InternalFailure";
| Obj ["proof_attempt", String "InternalFailure";
"exception", _e] ->
raise NotProofAttempt (* TODO *)
| Assoc ["proof_attempt", String "Uninstalled";
| Obj ["proof_attempt", String "Uninstalled";
"prover", p] ->
Uninstalled (parse_prover_from_json p)
| _ -> raise NotProofAttempt
......@@ -456,10 +431,10 @@ exception NotUpdate
let parse_update j =
match j with
| Assoc ["update_info", String "Proved";
| Obj ["update_info", String "Proved";
"proved", Bool b] ->
Proved b
| Assoc ["update_info", String "Proof_status_change";
| Obj ["update_info", String "Proof_status_change";
"proof_attempt", pas;
"obsolete", Bool b;
"limit", l] ->
......@@ -470,7 +445,7 @@ exception NotInfos
let parse_infos j =
match j with
| Assoc ["provers", Array pr;
| Obj ["provers", Array pr;
"transformations", Array tr;
"strategies", Array str;
"commands", Array com] ->
......@@ -516,7 +491,7 @@ let parse_message constr l =
let parse_message j =
match j with
| Assoc (("mess_notif", String constr) :: l) ->
| Obj (("mess_notif", String constr) :: l) ->
parse_message constr l
| _ -> raise NotMessage
......@@ -551,6 +526,19 @@ let parse_notification constr l =
let parse_notification j =
match j with
| Assoc (("notification", String constr) :: l) ->
| Obj (("notification", String constr) :: l) ->
parse_notification constr l
| _ -> raise NotNotification
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
parse_notification json
let parse_request (s: string) : ide_request =
let json = parse_json_object s in
parse_request json
src/session/json_util.mli
View file @ 0e08fabb
open Itp_server
(* 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
(** Print in Json format *)
val print_request: Format.formatter -> ide_request -> unit
val print_notification: Format.formatter -> notification -> unit
val parse_request: json_object -> ide_request
val parse_notification: json_object -> notification
(** Parse from Json format *)
val parse_request: string -> ide_request
val parse_notification: string -> notification
src/util/json.ml
View file @ 0e08fabb
......@@ -14,11 +14,19 @@ open Format
let string fmt s =
let b = Buffer.create (2 * String.length s) in
Buffer.add_char b '"';
for i = 0 to String.length s -1 do
match s.[i] with
| '"' -> Buffer.add_string b "\\\""
let i = ref 0 in
while !i <= String.length s -1 do
(match s.[!i] with
| '"' -> Buffer.add_string b "\\\""
| '\\' -> Buffer.add_string b "\\\\"
| c -> Buffer.add_char b c
| '/' -> Buffer.add_string b "\\/"
| '\b' -> Buffer.add_string b "\\b"
| c when c = Char.chr 12 -> Buffer.add_string b "\\f"
| '\n' -> Buffer.add_string b "\\n"
| '\r' -> Buffer.add_string b "\\r"
| '\t' -> Buffer.add_string b "\\t"
| c -> Buffer.add_char b c);
i := !i + 1
done;
Buffer.add_char b '"';
fprintf fmt "%s" (Buffer.contents b)
......@@ -65,6 +73,3 @@ let rec print fmt v =
| Float f -> float fmt f
| Bool b -> bool fmt b
| Null -> fprintf fmt "null"
let parse _s = failwith "Json.parse not yet implemented"
src/util/json.mli
View file @ 0e08fabb
......@@ -10,8 +10,8 @@
(********************************************************************)
val string : Format.formatter -> string -> unit
(* print json string, that is add '"' to the front and back, and escape '"' and
'\' in the string *)
(* print json string, that is add '"' to the front and back, and escape
characters escaped in JSON string *)
val int : Format.formatter -> int -> unit
(* print an integer *)
val bool : Format.formatter -> bool -> unit
......@@ -54,4 +54,7 @@ type value =
val print : Format.formatter -> value -> unit
(* To parse a json value, use file Json_parser and function json_object. See
end of session/Json_util.ml for an example use.
val parse : string -> value
*)
src/session/json_parser.mly → src/util/json_parser.mly
View file @ 0e08fabb
......@@ -3,7 +3,7 @@
by Yaron Minsky, Anil Madhavapeddy, and Jason Hickey. Their 'unlicence' allows
it. *)
(****************************************************************************)
%start <Json_util.json_object> json_object
%start <Json.value> json_object
%token <int> INT
%token <float> FLOAT
%token <string> STRING
......@@ -18,18 +18,18 @@ it. *)
%%
json_object:
| EOF { Json_util.Empty }
| LEFTBRC RIGHTBRC { Json_util.Empty }
| EOF { Json.Null }
| LEFTBRC RIGHTBRC { Json.Null }
(* Left recursive rule are more efficient *)
| LEFTBRC members RIGHTBRC { Json_util.Assoc (List.rev $2) }
| LEFTBRC members RIGHTBRC { Json.Obj (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) }
| LEFTSQ RIGHTSQ { Json.Array [] }
| LEFTSQ elements RIGHTSQ { Json.Array (List.rev $2) }
elements:
| value { [$1] }
......@@ -39,10 +39,10 @@ json_pair:
| STRING COLON value { ($1, $3) }
value:
| STRING { Json_util.String $1 }
| INT { Json_util.Int $1 }
| FLOAT { Json_util.Float $1 }
| STRING { Json.String $1 }
| INT { Json.Int $1 }
| FLOAT { Json.Float $1 }
| json_object { $1 }
| array { $1 }
| TRUE { Json_util.Bool true}
| FALSE { Json_util.Bool false }
| TRUE { Json.Bool true}
| FALSE { Json.Bool false }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment