From 5973d2b5464f57c0ae2971f87ea10ec0e88b03e3 Mon Sep 17 00:00:00 2001 From: Raphael Rieu-Helft Date: Wed, 12 Sep 2018 17:20:39 +0200 Subject: [PATCH] Add congruence transformation --- Makefile.in | 2 +- src/transform/congruence.ml | 31 +++++++++++++++++++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 src/transform/congruence.ml diff --git a/Makefile.in b/Makefile.in index 63d3246d3..642752c6c 100644 --- a/Makefile.in +++ b/Makefile.in @@ -222,7 +222,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal \ instantiate_predicate smoke_detector \ prop_curry eliminate_literal \ generic_arg_trans_utils case apply subst \ - introduction ind_itp destruct cut \ + introduction ind_itp destruct cut congruence \ induction induction_pr matching reflection LIB_PRINTER = cntexmp_printer alt_ergo why3printer smtv1 smtv2 coq\ diff --git a/src/transform/congruence.ml b/src/transform/congruence.ml new file mode 100644 index 000000000..7cb1144c5 --- /dev/null +++ b/src/transform/congruence.ml @@ -0,0 +1,31 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + +open Term +open Decl + +let congruence pr f = + match f.t_node with + | Tapp (eq, [{ t_node = Tapp (f1, l1) }; { t_node = Tapp (f2, l2) }]) + when ls_equal eq ps_equ && ls_equal f1 f2 -> + (* f a1 b1 c1... = f a2 b2 c2... *) + let ts = List.map2 t_equ_simp l1 l2 in + (* a1 = a2, b1 = b2... *) + let goal_of_t t = + let pr = create_prsymbol (Ident.id_fresh "G") in + [create_prop_decl Pgoal pr t] in + List.map goal_of_t ts + | _ -> [[create_prop_decl Pgoal pr f]] (* no progress *) + +let t = Trans.goal_l congruence + +let () = Trans.register_transform_l "congruence" t + ~desc:"Replace@ equality@ between@ two@ results@ of@ a@ function@ by@ equalities@ between@ parameters." -- 2.22.0