Commit 5f59febf authored by Sylvain Dailler's avatar Sylvain Dailler

Merge branch 'master' into rebase_collecting_counterex

parents 9c269141 57259417
......@@ -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\
......
VERSION=1.1.0+git
VERSION=1.2.0+git
(********************************************************************)
(* *)
(* 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."
......@@ -190,6 +190,15 @@ let () = Trans.register_transform "introduce_premises" introduce_premises
~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
goal@ into@ constant@ symbol@ and@ axioms."
(* In this file t_replace is used to substitute vsymbol with lsymbols. This is
done in [set_vs]; but in cases where the attribute is directly on the lsymbol
term application (Tapp), the substitution may not work resulting in an error
of the transformation. That's why we check for equality modulo attributes and
then copy attributes back on the term again.
*)
let rec t_replace t1 t2 t =
if t_equal_nt_na t t1 then t_attr_copy t t2 else t_map (t_replace t1 t2) t
let rec generalize hd =
match hd.Task.task_decl.Theory.td_node with
| Theory.Decl {d_node = Dprop (Pgoal,pr,f)} ->
......
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