ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

WhyML: harden 04e3e8e against polymorphic relations

Browse Source
This commit is contained in:
Andrei Paskevich
2015-07-02 21:05:48 +02:00
parent 8cc4efb82e
commit 101b1f5117
2 changed files with 17 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/whyml/mlw_expr.ml
View File

@@ -956,11 +956,13 @@ let create_rec_defn = let letrec = ref 1 in fun defl ->
first component. *)
let variant1 = (snd (List.hd defl)).l_spec.c_variant in
let check_variant (_, { l_spec = { c_variant = vl }}) =
match variant1 , vl with
| [] , [] -> ()
| (_,r1) :: _, (_,r2) :: _ when Opt.equal ls_equal r1 r2 -> ()
match variant1, vl with
| [], []
| (_,None)::_, (_,None)::_ -> ()
| (t1, Some r1)::_, (t2, Some r2)::_
when oty_equal t1.t_ty t2.t_ty && ls_equal r1 r2 -> ()
| _ -> Loc.errorm "All functions in a recursive definition \
must use the same well-founded order for the first variant component"
must use the same well-founded order for the first variant component"
in
List.iter check_variant (List.tl defl);
(* create the first list of fun_defns *)

20
src/whyml/mlw_wp.ml
View File

@@ -265,15 +265,17 @@ let decrease_def ?loc env old_t t =
else decrease_alg ?loc env old_t t
let decrease loc lab env olds varl =
let rec decr olds varl = match olds , varl with
| (old_t,None)::olds, (t,None)::varl ->
let dt = decrease_def ?loc env old_t t in
if oty_equal old_t.t_ty t.t_ty
then t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds varl))
else dt
| (old_t,Some old_r)::olds, (t,Some r)::varl when ls_equal old_r r ->
let dt = ps_app r [t; old_t] in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds varl))
let rec decr olds varl = match olds, varl with
| (old_t, Some old_r)::olds, (t, Some r)::varl
when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
let dt = ps_app r [t; old_t] in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds varl))
| (old_t, None)::olds, (t, None)::varl
when oty_equal old_t.t_ty t.t_ty ->
let dt = decrease_def ?loc env old_t t in
t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds varl))
| (old_t, None)::_, (t, None)::_ ->
decrease_def ?loc env old_t t
| _ -> t_false
in
t_label ?loc lab (decr olds varl)