diff --git a/src/ide/why3_js.ml b/src/ide/why3_js.ml
index b184ae46221ff29cef093830e669e25d37e9892b..3fb4ea00f6e568860603d741fd59e6bab501cc94 100644
--- a/src/ide/why3_js.ml
+++ b/src/ide/why3_js.ml
@@ -567,7 +567,7 @@ let interpNotif (n: notification) =
| Proof_error (_nid, s) ->
PE.error_print_msg
(Format.asprintf "Proof error on selected node: \"%s\"" s)
- | Transf_error (_ids, _tr, _args, _loc, s, _d) ->
+ | Transf_error (_b, _ids, _tr, _args, _loc, s, _d) ->
PE.error_print_msg
(Format.asprintf "Transformation error on selected node: \"%s\"" s)
| Strat_error (_nid, s) ->
diff --git a/src/ide/why3ide.ml b/src/ide/why3ide.ml
index 0bf9726fd721aa2a36f061bf160410a4a2acd0d8..02dd70d4e653ae1fc9788b06ffa0a15d355f86e2 100644
--- a/src/ide/why3ide.ml
+++ b/src/ide/why3ide.ml
@@ -1465,7 +1465,12 @@ let treat_message_notification msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) ->
print_message ~kind:1 ~notif_kind:"Proof_error" "%s" s
- | Transf_error (_id, tr_name, arg, loc, msg, doc) ->
+ | Transf_error (true, _id, tr_name, _arg, _loc, msg, _doc) ->
+ (* When the error reported by the transformation is fatal, we notify the
+ user with a popup. *)
+ let msg = Format.sprintf "Please report:\nTransformation %s failed: \n%s\n" tr_name msg in
+ GToolbox.message_box ~title:"Why3 fatal error" msg
+ | Transf_error (false, _id, tr_name, arg, loc, msg, doc) ->
if arg = "" then
print_message ~kind:1 ~notif_kind:"Transformation Error"
"%s\nTransformation failed: \n%s\n\n%s" msg tr_name doc
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index ea1615c44a3bf77ecf00f8a8443e243dc074205f..df2bdcd9dfee9685b8433079cb390d8013fc615c 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -12,6 +12,8 @@
open Format
open Wstdlib
open Session_itp
+open Generic_arg_trans_utils
+open Args_wrapper
let debug_sched = Debug.register_info_flag "scheduler"
~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \
@@ -53,20 +55,24 @@ let print_status fmt st =
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
+ | TSfatal of (proofNodeID * exn)
let print_trans_status fmt st =
match st with
| TSscheduled -> fprintf fmt "TScheduled"
| TSdone _tid -> fprintf fmt "TSdone" (* TODO print tid *)
| TSfailed _e -> fprintf fmt "TSfailed"
+ | TSfatal _e -> fprintf fmt "TSfatal"
type strategy_status = STSgoto of proofNodeID * int | STShalt
+ | STSfatal of string * proofNodeID * exn
let print_strategy_status fmt st =
match st with
| STSgoto(id,n) ->
fprintf fmt "goto step %d in proofNode %a" n print_proofNodeID id
| STShalt -> fprintf fmt "halt"
+ | STSfatal _ -> fprintf fmt "fatal"
type controller =
@@ -716,7 +722,7 @@ let schedule_transformation c id name args ~callback ~notification =
begin match s with
| TSdone tid -> update_trans_node notification c.controller_session tid
| TSscheduled
- | TSfailed _ -> ()
+ | TSfailed _ | TSfatal _ -> ()
end;
callback s
in
@@ -733,10 +739,18 @@ let schedule_transformation c id name args ~callback ~notification =
| NoProgress ->
(* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, NoProgress))
+ | (Arg_trans _ | Arg_trans_decl _
+ | Arg_trans_term _ | Arg_trans_term2 _
+ | Arg_trans_pattern _ | Arg_trans_type _ | Arg_bad_hypothesis _
+ | Cannot_infer_type _ | Unnecessary_terms _ | Parse_error _
+ | Arg_expected _ | Arg_theory_not_found _ | Arg_expected_none _
+ | Arg_qid_not_found _ | Arg_pr_not_found _ | Arg_error _
+ | Arg_parse_type_error _ | Unnecessary_arguments _) as e ->
+ callback (TSfailed (id, e))
| e when not (Debug.test_flag Debug.stack_trace) ->
(* "@[Exception raised in Session_itp.apply_trans_to_goal %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *)
- callback (TSfailed (id, e))
+ callback (TSfatal (id, e))
end;
false
in
@@ -782,6 +796,8 @@ let run_strategy_on_goal
let callback ntr =
callback_tr trname [] ntr;
match ntr with
+ | TSfatal (id, e) ->
+ callback (STSfatal (trname, id, e))
| TSfailed _e -> (* transformation failed *)
callback (STSgoto (g,pc+1));
let run_next () = exec_strategy (pc+1) strat g; false in
@@ -1184,6 +1200,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
begin match st with
| TSscheduled -> ()
| TSfailed _ -> assert false
+ | TSfatal _ -> assert false
| TSdone trid ->
match get_sub_tasks ses trid with
| [pn] ->
@@ -1230,6 +1247,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
debug
"[Bisect] transformation 'remove' scheduled@.";
callback_tr "remove" [rem] st;
+ | TSfatal (_, exn)
| TSfailed(_,exn) ->
(* may happen if removing a type or a lsymbol that is used
later on. We do has if proof fails. *)
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 21e7c44fae2ccfcf89be457af7e37a4d1137dbdf..c4205eecd947c4f2f8811458fc5df9a3e77e8614 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -34,10 +34,17 @@ type transformation_status =
TSscheduled
| TSdone of transID
| TSfailed of (proofNodeID * exn)
+ (* We distinguish normal usage exception of transformation from fatal
+ exception like assertion failure that should not be raised *)
+ | TSfatal of (proofNodeID * exn)
val print_trans_status : Format.formatter -> transformation_status -> unit
type strategy_status = STSgoto of proofNodeID * int | STShalt
+ (* When a transformation fatally returns, we have to
+ fatally fail the strategy
+ [transformation_name, pid, exn] *)
+ | STSfatal of string * proofNodeID * exn
val print_strategy_status : Format.formatter -> strategy_status -> unit
diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml
index e0f85166f5168bb3d621531fdfc9459b8603f9a8..64e309e1c3c76a9c796f2c4cb98f71bb23e62d17 100644
--- a/src/session/itp_communication.ml
+++ b/src/session/itp_communication.ml
@@ -36,7 +36,7 @@ type global_information =
type message_notification =
| Proof_error of node_ID * string
- | Transf_error of node_ID * string * string * Loc.position * string * string
+ | Transf_error of bool * node_ID * string * string * Loc.position * string * string
(* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_trans *)
| Strat_error of node_ID * string
| Replay_Info of string
@@ -155,7 +155,8 @@ let print_request fmt r =
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
- | Transf_error (_ids, _tr, _args, _loc, s, _d) -> fprintf fmt "transf error %s" s
+ | Transf_error (b, _ids, _tr, _args, _loc, s, _d) ->
+ fprintf fmt "transf error (is fatal = %b) %s" b s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli
index 10de2a128d4513d9b71608600b8ca521954a6616..4d9e41cd3f3e3e817bb63fbfae0d895e1fc48df4 100644
--- a/src/session/itp_communication.mli
+++ b/src/session/itp_communication.mli
@@ -40,8 +40,8 @@ type global_information =
type message_notification =
| Proof_error of node_ID * string
- | Transf_error of node_ID * string * string * Loc.position * string * string
- (** Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf *)
+ | Transf_error of bool * node_ID * string * string * Loc.position * string * string
+ (** Transf_error (is_fatal, nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf *)
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 39b748530bd02ea7309805fbc41d09bd142dd6c9..12f01043f3c574e6919b2759e9205f6d55f187c4 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -1138,8 +1138,15 @@ end
with | _ -> "" in
let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
- P.notify (Message (Transf_error (node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
- | _ -> ()
+ P.notify (Message (Transf_error (false, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
+ | TSscheduled -> ()
+ | TSfatal (id, e) ->
+ let doc = try
+ Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
+ with | _ -> "" in
+ let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
+ let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
+ P.notify (Message (Transf_error (true, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
let apply_transform node_id t args =
let d = get_server_data () in
diff --git a/src/session/json_util.ml b/src/session/json_util.ml
index 2bd660d761e117a48a30e4ea2097c4d13e3e5a99..b7f86bb293b0e39c762688298554bca3b988129d 100644
--- a/src/session/json_util.ml
+++ b/src/session/json_util.ml
@@ -261,8 +261,9 @@ let convert_message (m: message_notification) =
convert_record ["mess_notif", cc m;
"node_ID", Int nid;
"error", String s]
- | Transf_error (nid, tr, arg, loc, s, doc) ->
+ | Transf_error (is_fatal, nid, tr, arg, loc, s, doc) ->
convert_record ["mess_notif", cc m;
+ "is_fatal", Bool is_fatal;
"node_ID", Int nid;
"tr_name", String tr;
"failing_arg", String arg;
@@ -665,12 +666,13 @@ let parse_message constr j =
| "Transf_error" ->
let nid = get_int (get_field j "node_ID") in
+ let is_fatal = get_bool (get_field j "is_fatal") in
let tr_name = get_string (get_field j "tr_name") in
let arg = get_string (get_field j "failing_arg") in
let loc = parse_loc (get_field j "loc") in
let error = get_string (get_field j "error") in
let doc = get_string (get_field j "doc") in
- Transf_error (nid, tr_name, arg, loc, error, doc)
+ Transf_error (is_fatal, nid, tr_name, arg, loc, error, doc)
| "Strat_error" ->
let nid = get_int (get_field j "node_ID") in
diff --git a/src/tools/why3shell.ml b/src/tools/why3shell.ml
index 38511eadf6cc4a48af414fcc6cea8822c30ac01e..5cb35ca795ab99bd4977e1cf0348f3010f5e8e37 100644
--- a/src/tools/why3shell.ml
+++ b/src/tools/why3shell.ml
@@ -105,7 +105,7 @@ module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
let treat_message_notification fmt msg = match msg with
(* TODO: do something ! *)
| Proof_error (_id, s) -> fprintf fmt "%s@." s
- | Transf_error (_id, _tr_name, _arg, _loc, s, _) -> fprintf fmt "%s@." s
+ | Transf_error (_b, _id, _tr_name, _arg, _loc, s, _) -> fprintf fmt "%s@." s
| Strat_error (_id, s) -> fprintf fmt "%s@." s
| Replay_Info s -> fprintf fmt "%s@." s
| Query_Info (_id, s) -> fprintf fmt "%s@." s
diff --git a/src/transform/args_wrapper.mli b/src/transform/args_wrapper.mli
index 1133993d973278fbfd3a9aefb767e38884c8c92f..7cb8e93cfbc63b0e59eee5ba176c315a5d733342 100644
--- a/src/transform/args_wrapper.mli
+++ b/src/transform/args_wrapper.mli
@@ -26,6 +26,8 @@ exception Arg_expected_none of string
exception Arg_pr_not_found of Decl.prsymbol
exception Arg_qid_not_found of Ptree.qualid
exception Arg_error of string
+exception Arg_parse_type_error of Loc.position * string * exn
+exception Unnecessary_arguments of string list
val build_naming_tables : Task.task -> Trans.naming_table
@@ -98,9 +100,6 @@ type (_, _) trans_typ =
string is the keyword for that optional argument, its presence
meaning "true" *)
-exception Arg_parse_type_error of Loc.position * string * exn
-exception Unnecessary_arguments of string list
-
(** {2 parsing and typing of arguments}
the functions below wrap arguments of transformations, turning string