Commit 04e3e8e1 authored by Martin Clochard's avatar Martin Clochard

WhyML: Relaxation of conditions on variants

This commits enable the possibility to use variants
with different types/well-founded relations for
mutually recursive functions. This is useful if the
termination of sub-groups of those functions requires
a finer termination argument.

Example use case:
Suppose for example the following mutually recursive
function structure:

type t = A (list t)
let rec f (x:t) (...other args...)
  variant { x , other variants }
= ... f x (...different args...)...
with g (l:list t) (...other args...)
  variant { l }
= ...

The global termination argument is structural descent
trough the type t. However, as it is not enough for f
which perform a non-structural recursive calls, we add
other variants. Such variants were forbidden under the
previous behavior because f and g variants were
considered incompatible: As x and l have different
types, it was impossible to write the lexicographic
comparison of both n-uplets (even when completing g's
list).

The new behavior for mutual recursive calls is the
following: We first scan both variants to find the
longest compatible common prefix, e.g prefixes for
which types and relations are the same. Additionally,
we allow the last elements of such prefix to have
different types if their well-founded relation is
structural descent. Then, we generate a lexicographic
descent obligation on those prefixes only.

We still enforce that in a mutually recursive group,
the first component of each variant must corresponds
to the same well-founded relation. This event is much
more likely to be symptomatic of an error, as functions
with such fully mismatched variants cannot call each
other anyway. Moreover, one can always break them in
different recursive groups.
parent ceec4a68
......@@ -952,19 +952,15 @@ and subst_fd psm fdl =
until the effects are stabilized. TODO: prove correctness *)
let create_rec_defn = let letrec = ref 1 in fun defl ->
if defl = [] then invalid_arg "Mlw_expr.create_rec_defn";
(* check that the all variants use the same order *)
(* Check that all variants use compatible orders for their
first component. *)
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
with Invalid_argument _ -> false in
if not res then Loc.errorm
"All functions in a recursive definition \
must use the same well-founded order for variant"
match variant1 , vl with
| [] , [] -> ()
| (_,r1) :: _, (_,r2) :: _ when Opt.equal ls_equal r1 r2 -> ()
| _ -> Loc.errorm "All functions in a recursive definition \
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 *)
......
......@@ -235,7 +235,7 @@ type wp_env = {
ps_int_gt : Term.lsymbol;
fs_int_pl : Term.lsymbol;
fs_int_mn : Term.lsymbol;
letrec_var : term list Mint.t;
letrec_var : variant list Mint.t;
}
let decrease_alg ?loc env old_t t =
......@@ -258,30 +258,25 @@ let decrease_alg ?loc env old_t t =
t_close_branch (pat_app cs pl oty) f in
t_case old_t (List.map add_cs csl)
let decrease_rel ?loc env old_t t = function
| Some ls -> ps_app ls [t; old_t]
| 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])
| None -> decrease_alg ?loc env old_t t
let decrease_def ?loc env old_t t =
if ty_equal (t_type old_t) ty_int && ty_equal (t_type t) ty_int
then t_and (ps_app env.ps_int_le [t_nat_const 0;old_t])
(ps_app env.ps_int_lt [t;old_t])
else decrease_alg ?loc env old_t t
let decrease loc lab env olds varl =
let rec decr pr olds varl = match olds, varl with
| [], [] -> (* empty variant *)
t_true
| [old_t], [t, rel] ->
t_and_simp pr (decrease_rel ?loc env old_t t rel)
| old_t::_, (t,_)::_ when not (oty_equal old_t.t_ty t.t_ty) ->
Loc.errorm ?loc "cannot use lexicographic ordering"
| old_t::olds, (t,rel)::varl ->
let dt = t_and_simp pr (decrease_rel ?loc env old_t t rel) in
let pr = t_and_simp pr (t_equ old_t t) in
t_or_simp dt (decr pr olds varl)
| _ -> assert false
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))
| _ -> t_false
in
t_label ?loc lab (decr t_true olds varl)
t_label ?loc lab (decr olds varl)
let expl_variant = Slab.add Split_goal.stop_split (Slab.singleton expl_variant)
let expl_loopvar = Slab.add Split_goal.stop_split (Slab.singleton expl_loopvar)
......@@ -845,7 +840,7 @@ and wp_desc env e q xq = match e.e_node with
| Eloop (inv, varl, e1) ->
(* TODO: what do we do about well-foundness? *)
let i = wp_expl expl_loop_keep inv in
let olds = List.map (fun (t,_) -> t_at_old t) varl in
let olds = List.map (fun (t,r) -> t_at_old t , r) varl in
let i = if varl = [] then i else
let d = decrease e.e_loc expl_loopvar env olds varl in
wp_and ~sym:true i d in
......@@ -945,7 +940,7 @@ and wp_fun_defn ?eff env { fun_ps = ps ; fun_lambda = l } =
let env =
if c.c_letrec = 0 || c.c_variant = [] then env else
let lab = t_var lab in
let t_at_lab (t,_) = t_app fs_at [t; lab] t.t_ty in
let t_at_lab (t,r) = t_app fs_at [t; lab] t.t_ty , r in
let tl = List.map t_at_lab c.c_variant in
let lrv = Mint.add c.c_letrec tl env.letrec_var in
{ env with letrec_var = lrv } in
......@@ -1890,7 +1885,8 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr)
I => (OK /\ (NE => I' /\ V))
*)
let variant =
let old_vars = List.map (fun (t,_) -> Subst.term havoc_state t) varl in
let old_vars = List.map (fun (t,r) ->
Subst.term havoc_state t,r) varl in
let new_vars =
List.map (fun (t,rel) -> Subst.term wp1.post.s t,rel) varl in
decrease e.e_loc expl_loopvar env old_vars new_vars
......@@ -2044,7 +2040,7 @@ and fast_wp_fun_defn env { fun_lambda = l } =
let prestate = Subst.save_label lab prestate in
let env =
if c.c_letrec = 0 || c.c_variant = [] then env else
let tl = List.map (fun (t,_) -> Subst.term prestate t) c.c_variant in
let tl = List.map (fun (t,r) -> Subst.term prestate t,r) c.c_variant in
let lrv = Mint.add c.c_letrec tl env.letrec_var in
{ env with letrec_var = lrv } in
(* generate the initial state, using the overall effect of the function *)
......
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