On typing errors, the arguments is printed colored on the location which

is indicated by the error.

Changes in constructor Transf_error to add arguments: transformation,
location and specific argument.
Changes in callback for transformations because we need to pass the
information of the transformation name/arguments.

src/ide/why3ide.ml

@@ -1328,17 +1328,35 @@ let open_session: GMenu.menu_item =
 
 let treat_message_notification msg = match msg with
   (* TODO: do something ! *)
-  | Proof_error (_id, s)         -> print_message "%s" s
-  | Transf_error (_id, s)        -> print_message "%s" s
-  | Strat_error (_id, s)         -> print_message "%s" s
-  | Replay_Info s                -> print_message "%s" s
-  | Query_Info (_id, s)          -> print_message "%s" s
-  | Query_Error (_id, s)         -> print_message "%s" s
-  | Help s                       -> print_message "%s" s
-  | Information s                -> print_message "%s" s
-  | Task_Monitor (t, s, r)       -> update_monitor t s r
-  | Open_File_Error s            -> print_message "%s" s
-  | Parse_Or_Type_Error (loc, s) ->
+  | Proof_error (_id, s)                        -> print_message "%s" s
+  | Transf_error (_id, tr_name, arg, loc, msg) ->
+      if arg = "" then
+        print_message "%s\nTransformation failed: \n%s" msg tr_name
+      else
+        begin
+          let buf = message_zone#buffer in
+          (* Redefines the new tag for this buffer every time. I think this is
+             needed because we clear it often. *)
+          let _error = buf#create_tag
+              ~name:"error" [`BACKGROUND gconfig.neg_premise_color] in
+          print_message "%s\nTransformation failed. \nOn argument: \n%s \n%s" tr_name arg msg;
+          let color = "error" in
+          let _, _, beg_char, end_char = Loc.get loc in
+          let start = buf#start_iter#forward_lines 3 in
+          buf#apply_tag_by_name
+            ~start:(start#forward_chars beg_char)
+            ~stop:(start#forward_chars end_char)
+            color
+        end
+  | Strat_error (_id, s)                        -> print_message "%s" s
+  | Replay_Info s                               -> print_message "%s" s
+  | Query_Info (_id, s)                         -> print_message "%s" s
+  | Query_Error (_id, s)                        -> print_message "%s" s
+  | Help s                                      -> print_message "%s" s
+  | Information s                               -> print_message "%s" s
+  | Task_Monitor (t, s, r)                      -> update_monitor t s r
+  | Open_File_Error s                           -> print_message "%s" s
+  | Parse_Or_Type_Error (loc, s)                ->
     begin
       (* TODO find a new color *)
       color_loc ~color:Goal_color loc;

src/session/controller_itp.ml

@@ -561,7 +561,7 @@ let run_strategy_on_goal
          schedule_proof_attempt c g p ~counterexmp ~limit ~callback ~notification
       | Itransform(trname,pcsuccess) ->
          let callback ntr =
-           callback_tr ntr;
+           callback_tr trname [] ntr;
            match ntr with
            | TSfailed _e -> (* transformation failed *)
               callback (STSgoto (g,pc+1));
@@ -596,6 +596,7 @@ let schedule_tr_with_same_arguments
   let s = c.controller_session in
   let args = get_transf_args s tr in
   let name = get_transf_name s tr in
+  let callback = callback name args in
   schedule_transformation c pn name args ~callback ~notification
 
 let clean_session c ~removed =
@@ -655,7 +656,7 @@ let rec copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
       List.iter (fun x -> schedule_pa_with_same_arguments c x to_pn ~counterexmp:false
           ~callback:callback_pa ~notification) from_pa_list;
       let from_tr_list = get_transformations s from_pn in
-      let callback x st = callback_tr st;
+      let callback x tr args st = callback_tr tr args st;
         match st with
         | TSdone tid ->
           copy_paste c (ATn x) (ATn tid) ~notification ~callback_pa ~callback_tr

src/session/controller_itp.mli

@@ -207,7 +207,7 @@ val run_strategy_on_goal :
   Strategy.t ->
   counterexmp:bool ->
   callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
-  callback_tr:(transformation_status -> unit) ->
+  callback_tr:(string -> string list -> transformation_status -> unit) ->
   callback:(strategy_status -> unit) ->
   notification:notifier -> unit
 (** [run_strategy_on_goal c id strat] executes asynchronously the
@@ -230,7 +230,7 @@ val mark_as_obsolete:
 val copy_paste:
     notification:notifier ->
     callback_pa:(proofAttemptID -> proof_attempt_status -> unit) ->
-    callback_tr:(transformation_status -> unit) ->
+    callback_tr:(string -> string list -> transformation_status -> unit) ->
     controller -> any -> any -> unit
 
 val copy_detached:

src/session/itp_communication.ml

@@ -24,7 +24,8 @@ type global_information =
 
 type message_notification =
   | Proof_error           of node_ID * string
-  | Transf_error          of node_ID * string
+  | Transf_error          of node_ID * string * string * Loc.position * string
+  (* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg *)
   | Strat_error           of node_ID * string
   | Replay_Info           of string
   | Query_Info            of node_ID * string

src/session/itp_communication.mli

@@ -25,7 +25,8 @@ type global_information =
 
 type message_notification =
   | Proof_error           of node_ID * string
-  | Transf_error          of node_ID * string
+  | Transf_error          of node_ID * string * string * Loc.position * string
+  (* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg *)
   | Strat_error           of node_ID * string
   | Replay_Info           of string
   | Query_Info            of node_ID * string

src/session/itp_server.ml

@@ -221,29 +221,29 @@ let bypass_pretty s id =
   | _ -> Format.fprintf fmt "Uncaught: %a" Exn_printer.exn_printer exn
   end
 
-let get_exception_message ses id fmt e =
+let get_exception_message ses id e =
   match e with
   | Controller_itp.Noprogress ->
-      Format.fprintf fmt "Transformation made no progress\n"
+      Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
-      Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %a \n %a"
-        s (print_type ses id) ty1 (print_type ses id) ty2
+      Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
+        s (print_type ses id) ty1 (print_type ses id) ty2, Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
-      Format.fprintf fmt "Error in transformation %s during unification of following two terms:\n %a \n %a" s
-        (print_term ses id) t1 (print_term ses id) t2
+      Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a \n %a" s
+        (print_term ses id) t1 (print_term ses id) t2, Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans (s) ->
-      Format.fprintf fmt "Error in transformation function: %s \n" s
+      Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
   | Args_wrapper.Arg_hyp_not_found (s) ->
-      Format.fprintf fmt "Following hypothesis was not found: %s \n" s
+      Pp.sprintf "Following hypothesis was not found: %s \n" s, Loc.dummy_position, ""
   | Args_wrapper.Arg_theory_not_found (s) ->
-      Format.fprintf fmt "Theory not found: %s" s
-  | Loc.Located (loc, s) ->
-      Format.fprintf fmt "Parsing error at %a: %a" Loc.report_position loc Exn_printer.exn_printer s
+      Pp.sprintf "Theory not found: %s" s, Loc.dummy_position, ""
+  | Args_wrapper.Arg_parse_type_error(loc, arg, e) ->
+      Pp.sprintf "Parsing error: %a" Exn_printer.exn_printer e, loc, arg
   | Args_wrapper.Unnecessary_arguments l ->
-      Format.fprintf fmt "First arguments were parsed and typed correcly but the last following are useless:\n%a"
-        (Pp.print_list Pp.newline (fun fmt s -> Format.fprintf fmt "%s" s)) l
+      Pp.sprintf "First arguments were parsed and typed correcly but the last following are useless:\n%a"
+        (Pp.print_list Pp.newline (fun fmt s -> Format.fprintf fmt "%s" s)) l, Loc.dummy_position, ""
   | e ->
-      bypass_pretty ses id fmt e
+      (Pp.sprintf "%a" (bypass_pretty ses id) e), Loc.dummy_position, ""
 
 
 (* Debugging functions *)
@@ -279,19 +279,19 @@ 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, s)     -> fprintf fmt "transf error %s" 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
-  | Query_Error (_ids, s)      -> fprintf fmt "query error %s" s
-  | Help _s                    -> fprintf fmt "help"
-  | Information s              -> fprintf fmt "info %s" s
-  | Task_Monitor _             -> fprintf fmt "task montor"
-  | Parse_Or_Type_Error (_, s) -> fprintf fmt "parse_or_type_error:\n %s" s
-  | File_Saved s               -> fprintf fmt "file saved %s" s
-  | Error s                    -> fprintf fmt "%s" s
-  | Open_File_Error s          -> fprintf fmt "%s" s
+  | Proof_error (_ids, s)                    -> fprintf fmt "proof error %s" s
+  | Transf_error (_ids, _tr, _args, _loc, s) -> fprintf fmt "transf error %s" 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
+  | Query_Error (_ids, s)                    -> fprintf fmt "query error %s" s
+  | Help _s                                  -> fprintf fmt "help"
+  | Information s                            -> fprintf fmt "info %s" s
+  | Task_Monitor _                           -> fprintf fmt "task montor"
+  | Parse_Or_Type_Error (_, s)               -> fprintf fmt "parse_or_type_error:\n %s" s
+  | File_Saved s                             -> fprintf fmt "file saved %s" s
+  | Error s                                  -> fprintf fmt "%s" s
+  | Open_File_Error s                        -> fprintf fmt "%s" s
 
 (* TODO ad hoc printing. Should reuse print_loc. *)
 let print_loc fmt (loc: Loc.position) =
@@ -1034,8 +1034,10 @@ end
 
   (* ----------------- Schedule transformation -------------------- *)
 
-  (* Callback of a transformation *)
-  let callback_update_tree_transform status =
+  (* Callback of a transformation.
+     This contains arguments of the transformation only for pretty printing of
+     errors*)
+  let callback_update_tree_transform tr args status =
     let d = get_server_data () in
     match status with
     | TSdone trans_id ->
@@ -1044,17 +1046,16 @@ end
       let nid = node_ID_from_pn id in
       init_and_send_subtree_from_trans nid trans_id
     | TSfailed (id, e) ->
-      let msg =
-        Pp.sprintf "%a" (get_exception_message d.cont.controller_session id) e
-      in
-      P.notify (Message (Transf_error (node_ID_from_pn id, msg)))
+      let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
+      let tr_applied = tr ^ " " ^ (List.fold_left (fun acc x -> x ^ " " ^ acc) "" args) in
+      P.notify (Message (Transf_error (node_ID_from_pn id, tr_applied, arg_opt, loc, msg)))
     | _ -> ()
 
   let rec apply_transform nid t args =
     let d = get_server_data () in
     match any_from_node_ID nid with
     | APn id ->
-      let callback = callback_update_tree_transform in
+      let callback = callback_update_tree_transform t args in
       C.schedule_transformation d.cont id t args ~callback ~notification:(notify_change_proved d.cont)
     | APa panid ->
       let parent_id = get_proof_attempt_parent d.cont.controller_session panid in
@@ -1080,7 +1081,7 @@ end
          Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
        in
        let callback_pa = callback_update_tree_proof d.cont in
-       let callback_tr st = callback_update_tree_transform st in
+       let callback_tr tr args st = callback_update_tree_transform tr args st in
        List.iter (fun id ->
                   C.run_strategy_on_goal d.cont id st ~counterexmp
                     ~callback_pa ~callback_tr ~callback ~notification:(notify_change_proved d.cont))

src/session/json_util.ml

@@ -264,9 +264,12 @@ let convert_message (m: message_notification) =
       convert_record ["mess_notif", cc m;
            "node_ID", Int nid;
            "error", String s]
-  | Transf_error (nid, s) ->
+  | Transf_error (nid, tr, arg, loc, s) ->
       convert_record ["mess_notif", cc m;
            "node_ID", Int nid;
+           "tr_name", String tr;
+           "failing_arg", String arg;
+           "loc", convert_loc loc;
            "error", String s]
   | Strat_error (nid, s) ->
       convert_record ["mess_notif", cc m;
@@ -651,8 +654,11 @@ let parse_message constr j =
 
   | "Transf_error" ->
     let nid = get_int (get_field j "node_ID") 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 s = get_string (get_field j "error") in
-    Transf_error (nid, s)
+    Transf_error (nid, tr_name, arg, loc, s)
 
   | "Strat_error" ->
     let nid = get_int (get_field j "node_ID") in

src/tools/why3shell.ml

@@ -94,14 +94,14 @@ 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, 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
-  | Query_Error (_id, s)   -> fprintf fmt "%s@." s
-  | File_Saved s           -> fprintf fmt "%s@." s
-  | Help s                 -> fprintf fmt "%s@. Additionally for shell:\n\
+  | Proof_error (_id, s)                        -> fprintf fmt "%s@." s
+  | Transf_error (_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
+  | Query_Error (_id, s)                        -> fprintf fmt "%s@." s
+  | File_Saved s                                -> fprintf fmt "%s@." s
+  | Help s                                      -> fprintf fmt "%s@. Additionally for shell:\n\
 goto n -> focuse on n\n\
 ng -> next node\n\
 g -> print the current task\n\

src/transform/args_wrapper.ml

@@ -260,15 +260,20 @@ let type_ptree ~as_fmla t tables =
   then Typing.type_fmla_in_namespace ns km (fun _ -> None) t
   else Typing.type_term_in_namespace ns km (fun _ -> None) t
 
+exception Arg_parse_type_error of Loc.position * string * exn
+
 let parse_and_type ~as_fmla s task =
-  let lb = Lexing.from_string s in
-  let t =
+  try
+    let lb = Lexing.from_string s in
+    let t =
       Lexer.parse_term lb
-  in
-  let t =
+    in
+    let t =
       type_ptree ~as_fmla:as_fmla t task
-  in
-  t
+    in
+    t
+  with
+  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
 
 let parse_list_ident s =
   let lb = Lexing.from_string s in

src/transform/args_wrapper.mli

@@ -38,6 +38,7 @@ type (_, _) trans_typ =
   | Topt        : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
   | Toptbool    : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
 
+exception Arg_parse_type_error of Loc.position * string * exn
 exception Unnecessary_arguments of string list
 
 (** wrap arguments of transformations, turning string arguments into