Commit 42886abb authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: admit (and ignore) useless variants in the core API

Now, any reference to an external variable in an effect is stored
in a fake variant. This is better than to create a fake exceptional
postcondition, because then Mlw_typing can reject useless xposts.
parent f0fcfab7
......@@ -409,9 +409,8 @@ let vtv_check vars eff vtv =
let rec vta_check vars vta =
let add_arg vars pv = vars_union vars pv.pv_vars in
let vars = List.fold_left add_arg vars vta.vta_args in
if vta.vta_spec.c_variant <> [] || vta.vta_spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in a parameter declaration";
eff_check vars vta.vta_result vta.vta_spec.c_effect;
if vta.vta_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.vta_check";
match vta.vta_result with
| VTarrow a -> vta_check vars a
| VTvalue v -> vtv_check vars vta.vta_spec.c_effect v
......@@ -939,16 +938,14 @@ let e_try e0 bl =
let pv_dummy = create_pvsymbol (id_fresh "dummy") (vty_value ity_unit)
let e_any spec vty =
if spec.c_variant <> [] || spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in `any'";
if spec.c_letrec <> 0 then invalid_arg "Mlw_expr.e_any";
let vta = vty_arrow [pv_dummy] ~spec vty in
let varm = vta_varmap vta in
vta_check (vars_merge varm vars_empty) vta;
mk_expr (Eany spec) vty spec.c_effect varm
let e_abstract e spec =
if spec.c_variant <> [] || spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in `abstract'";
if spec.c_letrec <> 0 then invalid_arg "Mlw_expr.e_abstract";
spec_check { spec with c_effect = e.e_effect } e.e_vty;
let varm = spec_varmap e.e_varm spec in
mk_expr (Eabstr (e,spec)) e.e_vty e.e_effect varm
......@@ -1112,6 +1109,7 @@ let create_rec_defn = let letrec = ref 1 in fun defl ->
| VTarrow _ -> Loc.errorm ?loc:lam.l_expr.e_loc
"The body of a recursive function must be a first-order value"
| VTvalue _ ->
if lam.l_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.create_rec_defn";
let spec = { lam.l_spec with c_letrec = !letrec } in
let lam = { lam with l_spec = spec } in
let fd = create_fun_defn (id_clone ps.ps_name) lam recsyms in
......@@ -1121,8 +1119,7 @@ let create_rec_defn = let letrec = ref 1 in fun defl ->
subst_fd m fdl
let create_fun_defn id lam =
if lam.l_spec.c_variant <> [] || lam.l_spec.c_letrec <> 0 then
Loc.errorm "variants are not allowed in a non-recursive definition";
if lam.l_spec.c_letrec <> 0 then invalid_arg "Mlw_expr.create_fun_defn";
create_fun_defn id lam Sid.empty
(* fold *)
......
......@@ -451,12 +451,13 @@ let clone_export uc m inst =
Mreg.fold conv eff.eff_resets e in
let conv_term mv t = t_gen_map (ty_s_map conv_ts) conv_ls mv t in
let addx mv xs t q = Mexn.add (conv_xs xs) (conv_term mv t) q in
let conv_vari mv (t,r) = conv_term mv t, Util.option_map conv_ls r in
let conv_spec mv c = {
c_pre = conv_term mv c.c_pre;
c_post = conv_term mv c.c_post;
c_xpost = Mexn.fold (addx mv) c.c_xpost Mexn.empty;
c_effect = conv_eff c.c_effect;
c_variant = [];
c_variant = List.map (conv_vari mv) c.c_variant;
c_letrec = 0; } in
let rec conv_vta mv a =
let args = List.map conv_pv a.vta_args in
......
......@@ -721,11 +721,9 @@ let reset_vars eff pvs =
(* add dummy postconditions for uncovered exceptions *)
let complete_xpost eff xq =
let xe = Sexn.union eff.eff_raises eff.eff_ghostx in
(*
let check xs _ = Loc.errorm
"this expression does not raise exception %a" print_xs xs in
Mexn.iter check (Mexn.set_diff xq xe);
*)
let dummy { xs_ity = ity } () =
let v = create_vsymbol (id_fresh "dummy") (ty_of_ity ity) in
Mlw_ty.create_post v t_true in
......@@ -911,29 +909,20 @@ let rec type_c lenv gh pvs vars (dtyv, dsp) =
reg_fold on_reg u.reg_ity.ity_vars eff in
let eff = Sreg.fold check writes eff in
let spec = spec_of_dspec lenv eff vty dsp in
(* we add an exception postcondition for %Exit that mentions
every external variable in effect expressions which also
does not occur in pre/post/xpost. In this way, we keep
the variable in the specification in order to preserve
the effect in [Mlw_ty.spec_filter]. The exception %Exit
cannot be raised by an abstract parameter, so this xpost
will never appear in WP *)
(* we add a fake variant term for every external variable in effect
expressions which also does not occur in pre/post/xpost. In this
way, we store the variable in the specification in order to keep
the effect from being erased by Mlw_ty.spec_filter. Variants are
ignored outside of "let rec" definitions, so WP are not affected. *)
let del_pv pv s = Svs.remove pv.pv_vs s in
let esvs = Spv.fold del_pv pvs esvs in
let drop _ t s = Mvs.set_diff s t.t_vars in
let esvs = drop () spec.c_pre esvs in
let esvs = drop () spec.c_post esvs in
let esvs = Mexn.fold drop spec.c_xpost esvs in
let xpost = if Svs.is_empty esvs then spec.c_xpost else
let exn = Invalid_argument "Mlw_typing.type_c" in
let res = create_vsymbol (id_fresh "dummy") ty_unit in
let t_old = t_var pv_old.pv_vs in
let add vs f = (* put under 'old' in case of reset *)
let t = fs_app fs_at [t_var vs; t_old] vs.vs_ty in
t_and_simp (t_equ t t) f in
let xq = Mlw_ty.create_post res (Svs.fold add esvs t_true) in
Mexn.add_new exn xs_exit xq spec.c_xpost in
let spec = { spec with c_xpost = xpost } in
let add_vs vs varl = (t_var vs, None) :: varl in
let varl = Svs.fold add_vs esvs spec.c_variant in
let spec = { spec with c_variant = varl } in
(* add the invariants *)
spec_invariant lenv pvs vty spec, vty
......
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