diff --git a/Makefile.in b/Makefile.in index b9c3a757a9cf208653a146ac5a39612b7aa0aa22..4682e40bb39a272bb15067b536a795a0de79846e 100644 --- a/Makefile.in +++ b/Makefile.in @@ -156,7 +156,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \ introduction abstraction close_epsilon lift_epsilon \ eliminate_epsilon \ eval_match instantiate_predicate smoke_detector \ - reduction_engine compute induction_pr curry + reduction_engine compute induction_pr prop_curry LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \ simplify gappa cvc3 yices mathematica diff --git a/src/transform/curry.ml b/src/transform/prop_curry.ml similarity index 72% rename from src/transform/curry.ml rename to src/transform/prop_curry.ml index 5fb09b03c39761bfe3213e3b89dc2ad4682e0128..87e199fbeaee590ef938200b95ba5a1cfbc11500 100644 --- a/src/transform/curry.ml +++ b/src/transform/prop_curry.ml @@ -1,7 +1,7 @@ + open Term open Decl - let rec curry t = match t.t_node with | Tbinop (Timplies, lhs, rhs) -> expand t lhs (curry rhs) | _ -> t_map curry t @@ -10,11 +10,10 @@ and expand orig l r = match l.t_node with | Tbinop (Tand, a, b) -> expand orig a (expand orig b r) | _ -> t_label_copy orig (t_implies (curry l) r) - let curry = Trans.goal (fun pr t -> [create_prop_decl Pgoal pr (curry t)]) - - let () = - Trans.register_transform "curry" curry - ~desc:"Currify." + Trans.register_transform "prop_curry" curry + ~desc:"Transform@ conjunctions@ in@ implication@ premises@ into@ \ + sequences@ of@ premises." +