Skip to content

GitLab

why3
why3
Commit a478fd6d authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files
Options

Json file to Json_base for compatibility with js_of_ocaml. 

Entry in Makefile to compile ocaml code to js (like trywhy3).
Put why3webserver parsing/printing into Json_util.
Split Itp_server into Itp_communication and Itp_server to isolate
notification and request from the rest in an attempt to reduce
dependencies.
parent 79addf12
Hide whitespace changes
Inline Side-by-side
Showing with 110 additions and 244 deletions
Makefile.in
View file @ a478fd6d
......@@ -166,7 +166,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp json json_parser json_lexer debug loc \
hashcons stdlib exn_printer pp json_base 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 \
......@@ -205,7 +205,8 @@ 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
session_scheduler server_utils itp_communication \
itp_server json_util
LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/core/, $(LIB_CORE)) \
......@@ -1533,6 +1534,9 @@ install_local:: bin/why3doc
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/ide
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
......@@ -1592,7 +1596,6 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
......@@ -1602,6 +1605,16 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3js_ocaml.cmo: src/ide/why3js_ocaml.ml
$(JSOCAMLCW) $(BFLAGS) -c $<
src/ide/why3js_ocaml.byte: $(TRYWHY3CMO) src/ide/why3js_ocaml.cmo
$(JSOCAMLCW) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3js_ocaml.js: src/ide/why3js_ocaml.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
new_src_ide: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3js_ocaml.js
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
......
src/core/model_parser.ml
View file @ a478fd6d
......@@ -316,18 +316,18 @@ let interleave_with_source
*)
let print_model_element_json me_name_to_str fmt me =
let print_value fmt =
fprintf fmt "%a" (print_model_value_sanit Json.string) me.me_value in
fprintf fmt "%a" (print_model_value_sanit Json_base.string) me.me_value in
let print_kind fmt =
match me.me_name.men_kind with
| Result -> fprintf fmt "%a" Json.string "result"
| Old -> fprintf fmt "%a" Json.string "old"
| Error_message -> fprintf fmt "%a" Json.string "error_message"
| Other -> fprintf fmt "%a" Json.string "other" in
| Result -> fprintf fmt "%a" Json_base.string "result"
| Old -> fprintf fmt "%a" Json_base.string "old"
| Error_message -> fprintf fmt "%a" Json_base.string "error_message"
| Other -> fprintf fmt "%a" Json_base.string "other" in
let print_name fmt =
Json.string fmt (me_name_to_str me) in
Json_base.string fmt (me_name_to_str me) in
let print_value_or_kind_or_name fmt printer =
printer fmt in
Json.map_bindings
Json_base.map_bindings
(fun s -> s)
print_value_or_kind_or_name
fmt
......@@ -336,14 +336,14 @@ let print_model_element_json me_name_to_str fmt me =
("kind", print_kind)]
let print_model_elements_json me_name_to_str fmt model_elements =
Json.list
Json_base.list
(print_model_element_json me_name_to_str)
fmt
model_elements
let print_model_elements_on_lines_json model me_name_to_str vc_line_trans fmt
(file_name, model_file) =
Json.map_bindings
Json_base.map_bindings
(fun i ->
match model.vc_term_loc with
| None ->
......@@ -371,7 +371,7 @@ let print_model_json
List.append bindings [(file_name, (file_name, model_file))])
[]
(StringMap.bindings model.model_files) in
Json.map_bindings
Json_base.map_bindings
(fun s -> s)
(print_model_elements_on_lines_json model me_name_to_str vc_line_trans)
fmt
......
src/ide/index.html
View file @ a478fd6d
......@@ -30,6 +30,6 @@
<p>Answer zone</p>
</div>
</div>
<script type="text/javascript" src="why3ide.js"></script>
<script type="text/javascript" src="why3js_ocaml.js"></script>
</body>
</html>
src/ide/why3ide.ml
View file @ a478fd6d
......@@ -4,13 +4,13 @@ open Gconfig
open Stdlib
open Ide_utils
open History
open Itp_communication
open Itp_server
external reset_gc : unit -> unit = "ml_reset_gc"
let debug = Debug.lookup_flag "ide_info"
open Itp_server
(***************************)
(* Debugging Json protocol *)
(***************************)
......
src/ide/why3web.ml
View file @ a478fd6d
......@@ -20,6 +20,7 @@ module P = struct
end
open Itp_communication
open Itp_server
module S = Make (Wserver) (P)
......@@ -32,7 +33,7 @@ let interp_request args =
| "list-provers" -> Command_req (root_node,"list-provers")
| _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'")
open Json
open Json_base
let message_notification n =
match n with
......@@ -90,11 +91,7 @@ let handle_script s args =
end
| "getNotifications" ->
let n = P.get_notifications () in
let n =
if n = [] then [Obj ["notification",String "None"]]
else List.map notification n
in
Pp.sprintf "%a@." Json.print (Array n)
Pp.sprintf "%a@." Json_util.print_list_notification n
| _ -> "bad request"
let plist fmt l =
......@@ -161,6 +158,6 @@ let () =
in
if Queue.is_empty files then
Whyconf.Args.exit_with_usage spec usage_str;
Queue.iter (fun f -> P.push_request (Itp_server.Open_session_req f)) files;
Queue.iter (fun f -> P.push_request (Open_session_req f)) files;
S.init_server config env;
Wserver.main_loop None 6789 handler stdin_handler
src/session/itp_server.ml
View file @ a478fd6d
open Format
open Stdlib
open Call_provers
open Session_itp
open Controller_itp
open Server_utils
open Itp_communication
exception Bad_prover_name of string
......@@ -258,94 +258,6 @@ let get_exception_message ses id fmt e =
(* Information that the IDE may want to have *)
type prover = string
type transformation = string
type strategy = string
type node_ID = int
let root_node : node_ID = 0
type global_information =
{
provers : prover list;
transformations : transformation list;
strategies : strategy list;
commands : string list;
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
(* session_mem_limit : int; *)
(* session_nb_processes : int; *)
(* session_cntexample : bool; *)
(* main_dir : string *)
}
type message_notification =
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
| Information of string
| Task_Monitor of int * int * int
| Error of string
| Open_File_Error of string
type node_type =
| NRoot
| NFile
| NTheory
| NTransformation
| NGoal
| NProofAttempt
type update_info =
| Proved of bool
| Proof_status_change of
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
(* Notification of creation of new_node:
New_node (new_node, parent_node, node_type, name, detached). *)
| Node_change of node_ID * update_info
(* inform that the data of the given node changed *)
| Remove of node_ID
(* the given node was removed *)
| Initialized of global_information
(* initial global data *)
| Saved
(* the session was saved on disk *)
| Message of message_notification
(* an informative message, can be an error message *)
| Dead of string
(* server exited *)
| Task of node_ID * string
(* the node_ID's task *)
type ide_request =
| Command_req of node_ID * string
| Prove_req of node_ID * prover * resource_limit
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
| Open_session_req of string
| Add_file_req of string
| Set_max_tasks_req of int
| Get_task of node_ID
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
| Get_Session_Tree_req
| Save_req
| Reload_req
| Replay_req
| Exit_req
(* Debugging functions *)
let print_request fmt r =
......
src/session/itp_server.mli
View file @ a478fd6d
open Call_provers
type prover = string
type transformation = string
type strategy = string
type node_ID = int
val root_node : node_ID
(* --------------------------- types to be expanded if needed --------------------------------- *)
(* Global information known when server process has started and that can be
shared with the IDE through communication *)
type global_information =
{
provers : prover list;
transformations : transformation list;
strategies : strategy list;
commands : string list
(* hidden_provers : string list; *)
(* session_time_limit : int; *)
(* session_mem_limit : int; *)
(* session_nb_processes : int; *)
(* session_cntexample : bool; *)
(* main_dir : string *)
}
type message_notification =
| Proof_error of node_ID * string
| Transf_error of node_ID * string
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string
| Help of string
(* General information *)
| Information of string
(* Number of task scheduled, running, etc *)
| Task_Monitor of int * int * int
(* An error happened that could not be identified in server *)
| Error of string
| Open_File_Error of string
type node_type =
| NRoot
| NFile
| NTheory
| NTransformation
| NGoal
| NProofAttempt
type update_info =
| Proved of bool
| Proof_status_change of
Controller_itp.proof_attempt_status
* bool (* obsolete or not *)
* Call_provers.resource_limit
type notification =
| New_node of node_ID * node_ID * node_type * string * bool
(* Notification of creation of new_node:
New_node (new_node, parent_node, node_type, name, detached). *)
| Node_change of node_ID * update_info
(* inform that the data of the given node changed *)
| Remove of node_ID
(* the given node was removed *)
| Initialized of global_information
(* initial global data *)
| Saved
(* the session was saved on disk *)
| Message of message_notification
(* an informative message, can be an error message *)
| Dead of string
(* server exited *)
| Task of node_ID * string
(* the node_ID's task *)
type ide_request =
| Command_req of node_ID * string
| Prove_req of node_ID * prover * resource_limit
| Transform_req of node_ID * transformation * string list
| Strategy_req of node_ID * strategy
| Open_session_req of string
| Add_file_req of string
| Set_max_tasks_req of int
| Get_task of node_ID
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Copy_detached of node_ID
| Get_Session_Tree_req
| Save_req
| Reload_req
| Replay_req
| Exit_req
open Itp_communication
val print_request: Format.formatter -> ide_request -> unit
val print_msg: Format.formatter -> message_notification -> unit
......
src/session/json_util.ml
View file @ a478fd6d
open Itp_server
open Itp_communication
open Controller_itp
open Call_provers
open Json
open Json_base
(* TODO match exceptions and complete some cases *)
......@@ -94,14 +94,17 @@ let convert_notification_constructor n =
| Dead _ -> String "Dead"
| Task _ -> String "Task"
let convert_node_type nt =
let convert_node_type_string nt =
match nt with
| NRoot -> String "NRoot"
| NFile -> String "NFile"
| NTheory -> String "NTheory"
| NTransformation -> String "NTransformation"
| NGoal -> String "NGoal"
| NProofAttempt -> String "NProofAttempt"
| NRoot -> "NRoot"
| NFile -> "NFile"
| NTheory -> "NTheory"
| NTransformation -> "NTransformation"
| NGoal -> "NGoal"
| NProofAttempt -> "NProofAttempt"
let convert_node_type nt =
String (convert_node_type_string nt)
let convert_request_constructor (r: ide_request) =
match r with
......@@ -122,7 +125,7 @@ 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.value =
let print_request_to_json (r: ide_request): Json_base.value =
let cc = convert_request_constructor in
match r with
| Command_req (nid, s) ->
......@@ -233,7 +236,7 @@ let convert_message (m: message_notification) =
Obj ["mess_notif", cc m;
"open_error", String s]
let print_notification_to_json (n: notification): Json.value =
let print_notification_to_json (n: notification): Json_base.value =
let cc = convert_notification_constructor in
match n with
| New_node (nid, parent, node_type, name, detached) ->
......@@ -266,17 +269,21 @@ let print_notification_to_json (n: notification): Json.value =
"node_ID", Int nid;
"task", String s]
let print_notification fmt (n: notification) =
Format.fprintf fmt "%a" Json.print (print_notification_to_json n)
Format.fprintf fmt "%a" Json_base.print (print_notification_to_json n)
let print_request fmt (r: ide_request) =
Format.fprintf fmt "%a" Json.print (print_request_to_json r)
Format.fprintf fmt "%a" Json_base.print (print_request_to_json r)
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
exception NotProver
let parse_prover_from_json (j: Json.value) =
let parse_prover_from_json (j: Json_base.value) =
match j with
| Obj ["prover_name", String pn;
"prover_version", String pv;
......@@ -286,7 +293,7 @@ let parse_prover_from_json (j: Json.value) =
exception NotLimit
let parse_limit_from_json (j: Json.value) =
let parse_limit_from_json (j: Json_base.value) =
match j with
| Obj ["limit_time", Int t;
"limit_mem", Int m;
......@@ -342,11 +349,11 @@ let parse_request (constr: string) l =
Exit_req
| _ -> raise (NotRequest "")
let parse_request (j: Json.value): ide_request =
let parse_request_json (j: Json_base.value): ide_request =
match j with
| Obj (("ide_request", String constr) :: l) ->
parse_request constr l
| _ -> let s =Pp.string_of Json.print j in
| _ -> let s =Pp.string_of Json_base.print j in
begin Format.eprintf "BEGIN \n %s \nEND\n@." s; raise (NotRequest s); end
exception NotNodeType
......@@ -524,7 +531,7 @@ let parse_notification constr l =
Task (nid, s)
| _ -> raise NotNotification
let parse_notification j =
let parse_notification_json j =
match j with
| Obj (("notification", String constr) :: l) ->
parse_notification constr l
......@@ -532,13 +539,26 @@ let parse_notification j =
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
let x = Json_parser.value (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
parse_notification_json json
let parse_request (s: string) : ide_request =
let json = parse_json_object s in
parse_request json
parse_request_json json
let parse_list_notification (s: string): notification list =
let json = parse_json_object s in
match json with
| Array l -> List.map parse_notification_json l
| _ -> raise NotNotification
let parse_list_request (s: string): ide_request list =
let json = parse_json_object s in
match json with
| Array l -> List.map parse_request_json l
| _ -> raise (NotRequest "Not list")
src/session/json_util.mli
View file @ a478fd6d
open Itp_server
open Itp_communication
(** Useful functions for printing *)
val convert_node_type_string: node_type -> string
(** Print in Json format *)
val print_request: Format.formatter -> ide_request -> unit
val print_notification: Format.formatter -> notification -> unit
val print_list_request: Format.formatter -> ide_request list -> unit
val print_list_notification: Format.formatter -> notification list -> unit
(** Parse from Json format *)
val parse_request: string -> ide_request
val parse_notification: string -> notification
val parse_list_request: string -> ide_request list
val parse_list_notification: string -> notification list
src/util/json.ml → src/util/json_base.ml
View file @ a478fd6d
......@@ -40,7 +40,7 @@ let print_json_field key value_pr fmt value =
fprintf fmt "%a:%a" string key value_pr value
let list pr fmt l =
if l = [] then fprintf fmt "[]"
if l = [] then fprintf fmt "[null]"
else
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.comma
pr fmt l
......@@ -49,8 +49,11 @@ let print_map_binding key_to_str value_pr fmt binding =
let (key, value) = binding in
print_json_field (key_to_str key) value_pr fmt value
(* TODO document this exception *)
exception Bad_value
let map_bindings key_to_str value_pr fmt map_bindings =
if map_bindings = [] then fprintf fmt "{}"
if map_bindings = [] then raise Bad_value
else
Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.comma
(print_map_binding key_to_str value_pr) fmt map_bindings
......
src/util/json_lexer.mll
View file @ a478fd6d
......@@ -28,6 +28,7 @@ rule read =
| float { FLOAT (float_of_string (Lexing.lexeme lexbuf)) }
| "true" { TRUE }
| "false" { FALSE }
| "null" { NULL }
| '"' { read_string (Buffer.create 17) lexbuf }
| '{' { LEFTBRC }
| '}' { RIGHTBRC }
......
src/util/json_parser.mly
View file @ a478fd6d
......@@ -3,12 +3,14 @@
by Yaron Minsky, Anil Madhavapeddy, and Jason Hickey. Their 'unlicence' allows
it. *)
(****************************************************************************)
%start <Json.value> json_object
(* A JSON text can actually be any JSON value *)
%start <Json_base.value> value
%token <int> INT
%token <float> FLOAT
%token <string> STRING
%token TRUE
%token FALSE
%token NULL
%token LEFTBRC RIGHTBRC
%token LEFTSQ
%token RIGHTSQ
......@@ -18,18 +20,18 @@ it. *)
%%
json_object:
| EOF { Json.Null }
| LEFTBRC RIGHTBRC { Json.Null }
| EOF { Json_base.Null }
| LEFTBRC RIGHTBRC { Json_base.Null }
(* Left recursive rule are more efficient *)
| LEFTBRC members RIGHTBRC { Json.Obj (List.rev $2) }
| LEFTBRC members RIGHTBRC { Json_base.Obj (List.rev $2) }
members:
| json_pair { [ $1 ] }
| members COMMA json_pair { $3 :: $1 }
array:
| LEFTSQ RIGHTSQ { Json.Array [] }
| LEFTSQ elements RIGHTSQ { Json.Array (List.rev $2) }
| LEFTSQ RIGHTSQ { Json_base.Array [] }
| LEFTSQ elements RIGHTSQ { Json_base.Array (List.rev $2) }
elements:
| value { [$1] }
......@@ -39,10 +41,11 @@ json_pair:
| STRING COLON value { ($1, $3) }
value:
| STRING { Json.String $1 }
| INT { Json.Int $1 }
| FLOAT { Json.Float $1 }
| STRING { Json_base.String $1 }
| INT { Json_base.Int $1 }
| FLOAT { Json_base.Float $1 }
| json_object { $1 }
| array { $1 }
| TRUE { Json.Bool true}
| FALSE { Json.Bool false }
| TRUE { Json_base.Bool true}
| FALSE { Json_base.Bool false }
| NULL { Json_base.Null }
src/why3shell/why3shell.ml
View file @ a478fd6d
......@@ -6,6 +6,7 @@
open Why3
open Unix_scheduler
open Format