Commit 29d5c925 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: relax type checking on the last term in the variant list

parent 371db739
......@@ -970,6 +970,9 @@ let create_rec_defn = let letrec = ref 1 in fun defl ->
(* check that the all variants use the same order *)
let variant1 = (snd (List.hd defl)).l_spec.c_variant in
let check_variant (_, { l_spec = { c_variant = vl }}) =
let vl, variant1 = match List.rev vl, List.rev variant1 with
| (_, None)::vl, (_, None)::variant1 -> vl, variant1
| _, _ -> vl, variant1 in
let res = try List.for_all2 (fun (t1,r1) (t2,r2) ->
Opt.equal ty_equal t1.t_ty t2.t_ty &&
Opt.equal ls_equal r1 r2) vl variant1
......
......@@ -247,7 +247,8 @@ let decrease_alg ?loc env old_t t =
let decrease_rel ?loc env old_t t = function
| Some ls -> ps_app ls [t; old_t]
| None when ty_equal (t_type t) ty_int ->
| None when ty_equal (t_type old_t) ty_int
&& ty_equal (t_type t) ty_int ->
t_and
(ps_app env.ps_int_le [t_nat_const 0; old_t])
(ps_app env.ps_int_lt [t; old_t])
......
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