Commit 4b163a42 authored by MARCHE Claude's avatar MARCHE Claude Committed by David Hauzar

trace goal change in transformation

parent 8db8a6d5
......@@ -53,6 +53,21 @@ let store fn = let tr = Wtask.memoize_option 63 fn in fun t -> match t with
let bind f g = store (fun task -> g (f task) task)
let trace_goal msg tr =
fun task ->
begin match task with
| Some { task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,t)}}} ->
Debug.dprintf debug "[%s (before)] task goal is %a@." msg Pretty.print_term t
| _ -> Debug.dprintf debug "[%s (before)] task has non goal@." msg
end;
let new_task = tr task in
begin match new_task with
| Some { task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,t)}}} ->
Debug.dprintf debug "[%s (after)] task goal is %a@." msg Pretty.print_term t
| _ -> Debug.dprintf debug "[%s (after)] task has non goal@." msg
end;
new_task
let fold fn v =
let h = Wtask.create 63 in
let rewind acc task =
......
......@@ -31,6 +31,8 @@ val singleton : 'a trans -> 'a tlist
val return : 'a -> 'a trans
val bind : 'a trans -> ('a -> 'b trans) -> 'b trans
val trace_goal : string -> task trans -> task trans
(** Compose transformation *)
val compose : task trans -> 'a trans -> 'a trans
val compose_l : task tlist -> 'a tlist -> 'a tlist
......
......@@ -69,7 +69,7 @@ let encoding_smt env = Trans.seq [
Libencoding.monomorphise_goal;
select_kept def_enco_select_smt env;
Trans.print_meta Libencoding.debug Libencoding.meta_kept;
Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env;
Trans.trace_goal "meta_enco_kept" (Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env);
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
let encoding_tptp env = Trans.seq [
......
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