prop_curry.ml 533 Bytes
Newer Older
1

Léon Gondelman's avatar
Léon Gondelman committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15
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

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 () =
16 17 18 19
  Trans.register_transform "prop_curry" curry
    ~desc:"Transform@ conjunctions@ in@ implication@ premises@ into@ \
      sequences@ of@ premises."