Merge branch 'issue_274' into 'master'

fix #274

Closes #274

See merge request !96

CHANGES.md

 :x: marks a potential source of incompatibility
 
+Tools
+  * why3prove counterexamples output is not JSON by default. To restore previous
+   behavior, pass the argument --json
+
+API
+  * function Call_provers.print_prover_result now takes an additional boolean
+  argument ~json_model which state if the counterexamples are printed with json
+  format :x:
+
+Transformations
+  * Improvement of apply/rewrite in presence of let. Solve a bug that prevents
+  applying hypothesis with nested let-bindings :x:
+  * Adding arguments to transformations without arguments is now forbidden
+  (previously ignored):x:
+
+Counterexamples
+  * Improved display of counterexamples in Task view
+
+
 Version 1.2.0, February 11, 2019
 --------------------------------
 

src/core/trans.ml

@@ -499,6 +499,8 @@ let list_trans () =
   in
     Hstr.fold (fun k _ acc -> k::acc) transforms_with_args_l l
 
+exception Unnecessary_arguments of string list
+
 let apply_transform tr_name env task =
    match lookup_trans env tr_name with
     | Trans_one t -> [apply t task]
@@ -507,11 +509,13 @@ let apply_transform tr_name env task =
     | Trans_with_args_l _ -> assert false (* apply (t []) task *)
 
 let apply_transform_args tr_name env args tables task =
-   match lookup_trans env tr_name with
-    | Trans_one t -> [apply t task]
-    | Trans_list t -> apply t task
-    | Trans_with_args t -> [apply (t args) env tables task]
-    | Trans_with_args_l t -> apply (t args) env tables task
+   match lookup_trans env tr_name, args with
+    | Trans_one t, [] -> [apply t task]
+    | Trans_list t, [] -> apply t task
+    | Trans_one _, l | Trans_list _, l ->
+        raise (Unnecessary_arguments l)
+    | Trans_with_args t, _ -> [apply (t args) env tables task]
+    | Trans_with_args_l t, _ -> apply (t args) env tables task
 
 (** Flag-dependent transformations *)
 

src/core/trans.mli

@@ -261,6 +261,8 @@ val lookup_trans_desc: string -> Pp.formatted
 
 val list_trans : unit -> string list
 
+exception Unnecessary_arguments of string list
+
 val apply_transform : string -> Env.env -> task -> task list
 (** apply a registered 1-to-1 or a 1-to-n, directly.*)
 

src/session/controller_itp.ml

@@ -752,7 +752,7 @@ let schedule_transformation c id name args ~callback ~notification =
         | 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 _
+        | Arg_parse_type_error _ | Trans.Unnecessary_arguments _
         | Reflection.NoReification ) as e ->
           callback (TSfailed (id, e))
       | e when not (Debug.test_flag Debug.stack_trace) ->

src/session/itp_server.ml

@@ -242,7 +242,7 @@ let get_exception_message ses id e =
       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 ->
+  | Trans.Unnecessary_arguments l ->
       Pp.sprintf "First arguments were parsed and typed correctly 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, ""
   | Generic_arg_trans_utils.Unnecessary_terms l ->

src/transform/args_wrapper.mli

@@ -27,7 +27,6 @@ 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