Commit 3c006d28 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

fixes #19

Merged apply and apply_with (resp. rewrite and rewrite_with). Typo in
error returned by apply. Also adding session for 19.
parent 6e1471e0
......@@ -5,7 +5,7 @@
<file name="../19_apply_with.mlw">
<theory name="I19_simplint" sum="7bce20e61a5551a6af73d2355b15c709">
<goal name="g">
<transf name="apply_with" arg1="H" arg2="1">
<transf name="apply" arg1="H" arg2="with" arg3="1">
<goal name="g.0">
</goal>
<goal name="g.1">
......@@ -15,7 +15,7 @@
</theory>
<theory name="I19_simplpoly" sum="a0862dae57e5acda121e6fa4f7b5e82d">
<goal name="test">
<transf name="apply_with" arg1="trans" arg2="b">
<transf name="apply" arg1="trans" arg2="with" arg3="b">
<goal name="test.0">
</goal>
<goal name="test.1">
......@@ -25,11 +25,21 @@
</theory>
<theory name="I19_simplpoly2" sum="5f0342147f8467ab584bf33b21a6a483">
<goal name="test">
<transf name="apply_with" arg1="trans" arg2="42,b">
<transf name="apply" arg1="trans" arg2="with" arg3="42,b">
<goal name="test.0">
</goal>
<goal name="test.1">
</goal>
</transf>
<transf name="rewrite" arg1="trans_eq" arg2="with" arg3="b,a,a">
<goal name="test.0">
</goal>
<goal name="test.1">
</goal>
<goal name="test.2">
</goal>
</transf>
</goal>
</theory>
\ No newline at end of file
</theory>
</file>
</why3session>
......@@ -243,10 +243,10 @@ let get_exception_message ses id e =
| 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 ->
Pp.sprintf "First arguments were parsed and typed correcly but the last following are useless:\n%a"
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 ->
Pp.sprintf "First arguments were parsed and typed correcly but the last following are useless:\n%a"
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 "%a" (print_term ses id) s)) l, Loc.dummy_position, ""
| Args_wrapper.Arg_expected_none s ->
......
......@@ -77,7 +77,7 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
| _ when diff < 0 ->
Debug.dprintf debug_matching "Too many withed terms@.";
raise (Arg_trans (trans_name ^ ": the last " ^
string_of_int diff
string_of_int (-diff)
^ " terms in with are useless"))
| _ when diff > 0 ->
Debug.dprintf debug_matching "Not enough withed terms@.";
......@@ -563,29 +563,10 @@ let () = wrap_and_register
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l)))) replace
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) (rewrite None)
let _ = wrap_and_register
~desc:"rewrite_with [<-] <name> [in] <name2> with <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite_with"
~desc:"rewrite [<-] <name> [in] <name2> [with] <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol (Topt ("with", Ttermlist Ttrans_l))))))) (fun rev h h1opt term_list -> rewrite term_list rev h h1opt)
(* register_transform_with_args_l *)
(* ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
(* "rewrite" *)
(* (wrap_l (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite) *)
let () = wrap_and_register
~desc:"apply <prop> applies prop to the goal" "apply"
(Tprsymbol Ttrans_l) (fun x -> apply x None)
let () = wrap_and_register
~desc:"apply_with <prop> <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply_with"
(* TODO ideally apply and apply_with should be the same tactic but with an
(Toptbool "with") inside it. This cannot currently be done because the change
would probably makes proof using apply detached. And detached are not handled
yet.
*)
(Tprsymbol (Ttermlist Ttrans_l)) (fun x y -> apply x (Some y))
~desc:"apply <prop> [with] <list term> applies prop to the goal and \
uses the list of terms to instantiate the variables that are not found." "apply"
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y)
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