Commit de0c3057 authored by Andrei Paskevich's avatar Andrei Paskevich

provide a transformation working exclusively on the goal

parent c59b0dda
......@@ -103,6 +103,37 @@ let decl_l = gen_decl_l add_decl
let tdecl = gen_decl add_tdecl
let tdecl_l = gen_decl_l add_tdecl
let apply_to_goal fn d = match d.d_node with
| Dprop (Pgoal,pr,f) -> fn pr f
| _ -> assert false
let gen_goal add fn =
let fn = WHdecl.memoize 5 (apply_to_goal fn) in
let rec pass task = match task with
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.fold_left add prev (fn d)
| Some { task_decl = td; task_prev = prev } ->
add_tdecl (pass prev) td
| _ -> assert false
in
pass
let gen_goal_l add fn =
let fn = WHdecl.memoize 5 (apply_to_goal fn) in
let rec pass task = match task with
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.rev_map (List.fold_left add prev) (fn d)
| Some { task_decl = td; task_prev = prev } ->
List.rev_map (fun task -> add_tdecl task td) (pass prev)
| _ -> assert false
in
pass
let goal = gen_goal add_decl
let goal_l = gen_goal_l add_decl
let tgoal = gen_goal add_tdecl
let tgoal_l = gen_goal_l add_tdecl
let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
(** dependent transformations *)
......
......@@ -59,6 +59,12 @@ val decl_l : (decl -> decl list list) -> task -> task tlist
val tdecl : (decl -> tdecl list ) -> task -> task trans
val tdecl_l : (decl -> tdecl list list) -> task -> task tlist
val goal : (prsymbol -> fmla -> decl list ) -> task trans
val goal_l : (prsymbol -> fmla -> decl list list) -> task tlist
val tgoal : (prsymbol -> fmla -> tdecl list ) -> task trans
val tgoal_l : (prsymbol -> fmla -> tdecl list list) -> task tlist
val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
(* dependent transformatons *)
......
......@@ -143,23 +143,9 @@ let simplify_trivial_quantification =
let () = Trans.register_transform
"simplify_trivial_quantification" simplify_trivial_quantification
let on_goal fn_prop =
let rec fn task = match task with
| Some { Task.task_decl = {Theory.td_node =
Theory.Decl ({d_node = Decl.Dprop (Pgoal,pr,fmla)})};
Task.task_prev = task_prev } ->
(List.fold_left Task.add_decl) task_prev (fn_prop pr fmla)
| Some { Task.task_decl = ({Theory.td_node = Theory.Meta _} as td);
Task.task_prev = task_prev } ->
Task.add_tdecl (fn task_prev) td
| _ -> assert false
in
Trans.store fn
let simplify_trivial_quantification_in_goal =
on_goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
let () = Trans.register_transform
"simplify_trivial_quantification_in_goal"
simplify_trivial_quantification_in_goal
simplify_trivial_quantification_in_goal
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