Commit 1975bbfd authored by Léon Gondelman's avatar Léon Gondelman

New transformation curry

parent 2c86281f
......@@ -150,7 +150,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
reduction_engine compute induction_pr curry
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
......
open Ident
open Term
open Decl
open Theory
open Task
let rec curry t = match t.t_node with
| Tbinop (Timplies, lhs, rhs) -> expand t lhs (curry rhs)
| _ -> t_map curry t
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."
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