Commit 22d11b93 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'f_equal' into 'master'

congruence transformation

See merge request !20
parents 2e437378 5973d2b5
......@@ -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\
......
(********************************************************************)
(* *)
(* 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."
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