Commit ead51b74 authored by Sylvain Dailler's avatar Sylvain Dailler

fix #274

When applying a transformation without arguments, this checks that
arguments are indeed not provided. If they are, it now raises the same
exception as transformation with too many arguments.

Also update CHANGES with recent changes.
parent 8a86e6dd
: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
--------------------------------
......
......@@ -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 *)
......
......@@ -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.*)
......
......@@ -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) ->
......
......@@ -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 ->
......
......@@ -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
......
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