Commit 101b1f51 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: harden 04e3e8e1 against polymorphic relations

parent 8cc4efb8
......@@ -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 *)
......
......@@ -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)
......
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