Commit 589890aa authored by Guillaume Melquiond's avatar Guillaume Melquiond

In the Gappa printer, perform a pseudo-congruence on the goal and move the...

In the Gappa printer, perform a pseudo-congruence on the goal and move the introduce_premises transformation after abstraction.

Goal
  h (f x) = 1 /\ f x = g y -> h (g y) = 1
is now transformed by fmla_cond_subst into
  h (g y) = 1 /\ f x = g y -> h (g y) = 1
which can now be abstracted to
  abstr = 1 /\ abstr1 = abstr2 -> abstr = 1.
parent 3f154567
......@@ -22,7 +22,6 @@ transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "introduce_premises"
theory BuiltIn
syntax type int "int"
......
......@@ -325,11 +325,18 @@ let print_goal info fmt g =
let print_task env pr thpr ?old:_ fmt task =
forget_all ident_printer;
let info = get_info env task in
let task = Trans.apply (Trans.goal (fun pr f ->
[create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
(fun t _ -> match t.t_node with
| Tconst _ | Tapp(_,[]) -> false
| Tapp(ls,_) -> not (Sid.mem ls.ls_name info.info_symbols)
| _ -> true) true f)
])) task in
let task =
Abstraction.abstraction
(fun ls -> Sid.mem ls.ls_name info.info_symbols)
task
in
task in
let task = Trans.apply (Trans.lookup_transform "introduce_premises" env) task in
(*
eprintf "Abstraction: @\n%a@." Pretty.print_task task;
*)
......
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