Skip to content

GitLab

why3
why3
Commit 3dcca8d3 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

whyml: reuse Mlw_ty.spec in lambdas and Eabstr

parent 6ae9985c
Hide whitespace changes
Inline Side-by-side
Showing with 71 additions and 95 deletions
src/whyml/mlw_expr.ml
View file @ 3dcca8d3
......@@ -468,7 +468,7 @@ and expr_node =
| Efor of pvsymbol * for_bounds * invariant * expr
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eabstr of expr * post * xpost
| Eabstr of expr * spec
| Eassert of assertion_kind * term
| Eabsurd
......@@ -484,12 +484,9 @@ and fun_defn = {
}
and lambda = {
l_args : pvsymbol list;
l_variant : variant list; (* lexicographic order *)
l_pre : pre;
l_expr : expr;
l_post : post;
l_xpost : xpost;
l_args : pvsymbol list;
l_expr : expr;
l_spec : spec;
}
(* base tools *)
......@@ -530,29 +527,11 @@ let ps_pvset pvs ps = varmap_pvset pvs ps.ps_varm
let e_pvset pvs e = varmap_pvset pvs e.e_varm
let spec_of_lambda lam = {
c_pre = lam.l_pre;
c_effect = lam.l_expr.e_effect;
c_post = lam.l_post;
c_xpost = lam.l_xpost;
c_variant = lam.l_variant; }
let l_pvset pvs lam =
let pvs = e_pvset pvs lam.l_expr in
let pvs = spec_pvset pvs (spec_of_lambda lam) in
let pvs = spec_pvset pvs lam.l_spec in
List.fold_right Spv.remove lam.l_args pvs
let spec_of_abstract e q xq = {
c_pre = t_true;
c_post = q;
c_xpost = xq;
c_effect = e.e_effect;
c_variant = []; }
let abstr_pvset pvs e q xq =
let pvs = e_pvset pvs e in
spec_pvset pvs (spec_of_abstract e q xq)
(* check admissibility of consecutive events *)
exception StaleRegion of expr * ident
......@@ -965,11 +944,13 @@ let e_any spec vty =
vta_check (vars_merge varm vars_empty) vta;
mk_expr (Eany spec) vty spec.c_effect varm
let e_abstract e q xq =
let spec = spec_of_abstract e q xq in
let e_abstract e spec =
if spec.c_variant <> [] then
Loc.errorm "variants are not allowed in `abstract'";
let spec = { spec with c_effect = e.e_effect } in
spec_check spec e.e_vty;
let varm = spec_varmap e.e_varm spec in
mk_expr (Eabstr (e,q,xq)) e.e_vty e.e_effect varm
mk_expr (Eabstr (e,spec)) e.e_vty e.e_effect varm
let e_assert ak f =
let varm = add_t_vars f.t_vars Mid.empty in
......@@ -983,7 +964,7 @@ let e_absurd ity =
(* simple functional definitions *)
let create_fun_defn id lam recsyms =
let spec = spec_of_lambda lam in
let spec = { lam.l_spec with c_effect = lam.l_expr.e_effect } in
let varm = spec_varmap lam.l_expr.e_varm spec in
let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
let varm = List.fold_left del_pv varm lam.l_args in
......@@ -993,7 +974,7 @@ let create_fun_defn id lam recsyms =
| vty -> vty in
let vta = vty_arrow lam.l_args ~spec vty in
{ fun_ps = create_psymbol_poly id vta varm_ps;
fun_lambda = lam;
fun_lambda = { lam with l_spec = spec };
fun_varm = varm; }
let e_rec fdl e =
......@@ -1062,8 +1043,8 @@ let rec expr_subst psm e = e_label_copy e (match e.e_node with
e_assign_real (expr_subst psm e) pv
| Eghost e ->
e_ghost (expr_subst psm e)
| Eabstr (e,q,xq) ->
e_abstract (expr_subst psm e) q xq
| Eabstr (e,spec) ->
e_abstract (expr_subst psm e) spec
| Eraise (xs,e0) ->
e_raise xs (expr_subst psm e0) (vtv_of_expr e).vtv_ity
| Etry (e,bl) ->
......@@ -1103,8 +1084,8 @@ and subst_fd psm fdl =
let create_rec_defn defl =
if defl = [] then invalid_arg "Mlw_expr.create_rec_defn";
(* check that the all variants use the same order *)
let variant1 = (snd (List.hd defl)).l_variant in
let check_variant (_, { l_variant = vl }) =
let variant1 = (snd (List.hd defl)).l_spec.c_variant in
let check_variant (_, { l_spec = { c_variant = vl }}) =
let res = try List.for_all2 (fun (_,r1) (_,r2) ->
Util.option_eq ls_equal r1 r2) vl variant1
with Invalid_argument _ -> false in
......@@ -1126,7 +1107,7 @@ let create_rec_defn defl =
subst_fd m fdl
let create_fun_defn id lam =
if lam.l_variant <> [] then
if lam.l_spec.c_variant <> [] then
Loc.errorm "variants are not allowed in a non-recursive definition";
create_fun_defn id lam Sid.empty
......@@ -1146,6 +1127,6 @@ let e_fold fn acc e = match e.e_node with
| Eif (e1,e2,e3) -> fn (fn (fn acc e1) e2) e3
| Eapp (e,_,_) | Eassign (e,_,_) | Eghost e
| Eloop (_,_,e) | Efor (_,_,_,e) | Eraise (_,e)
| Eabstr (e,_,_) -> fn acc e
| Eabstr (e,_) -> fn acc e
| Elogic _ | Evalue _ | Earrow _
| Eany _ | Eassert _ | Eabsurd -> acc
src/whyml/mlw_expr.mli
View file @ 3dcca8d3
......@@ -162,7 +162,7 @@ and expr_node = private
| Efor of pvsymbol * for_bounds * invariant * expr
| Eraise of xsymbol * expr
| Etry of expr * (xsymbol * pvsymbol * expr) list
| Eabstr of expr * post * xpost
| Eabstr of expr * spec
| Eassert of assertion_kind * term
| Eabsurd
......@@ -178,17 +178,13 @@ and fun_defn = private {
}
and lambda = {
l_args : pvsymbol list;
l_variant : variant list; (* lexicographic order *)
l_pre : pre;
l_expr : expr;
l_post : post;
l_xpost : xpost;
l_args : pvsymbol list;
l_expr : expr;
l_spec : spec;
}
val e_pvset : Spv.t -> expr -> Spv.t
val l_pvset : Spv.t -> lambda -> Spv.t
val abstr_pvset : Spv.t -> expr -> post -> xpost -> Spv.t
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
......@@ -248,7 +244,7 @@ val e_for :
pvsymbol -> expr -> for_direction -> expr -> invariant -> expr -> expr
val e_any : spec -> vty -> expr
val e_abstract : expr -> post -> xpost -> expr
val e_abstract : expr -> spec -> expr
val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
......
src/whyml/mlw_ocaml.ml
View file @ 3dcca8d3
......@@ -749,7 +749,7 @@ and print_lexpr pri info fmt e =
| Etry (e,bl) ->
fprintf fmt "@[(try %a with@\n@[<hov>%a@])@]"
(print_expr info) e (print_list newline (print_xbranch info)) bl
| Eabstr (e,_,_) ->
| Eabstr (e,_) ->
print_lexpr pri info fmt e
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
......
src/whyml/mlw_pretty.ml
View file @ 3dcca8d3
......@@ -311,9 +311,9 @@ and print_enode pri fmt e = match e.e_node with
fprintf fmt "absurd"
| Eassert (ak,f) ->
fprintf fmt "%a { %a }" print_ak ak print_term f
| Eabstr (e,q,_xq) ->
(* TODO: print_xpost *)
fprintf fmt "abstract %a@ { %a }" print_expr e print_post q
| Eabstr (e,spec) ->
(* TODO: print_spec *)
fprintf fmt "abstract %a@ { %a }" print_expr e print_post spec.c_post
| Eghost e ->
fprintf fmt "ghost@ %a" print_expr e
| Eany spec ->
......@@ -333,11 +333,11 @@ and print_rec lr fst fmt { fun_ps = ps ; fun_lambda = lam } =
(if fst then if lr then "let rec" else "let" else "with")
print_psty ps
(print_list space print_arg) lam.l_args
print_term lam.l_pre
print_variant lam.l_variant
print_term lam.l_spec.c_pre
print_variant lam.l_spec.c_variant
print_expr lam.l_expr
print_post lam.l_post
(* TODO: print_xpost *)
print_post lam.l_spec.c_post
(* TODO: print_spec *)
(*
and print_tl fmt tl =
......
src/whyml/mlw_typing.ml
View file @ 3dcca8d3
......@@ -721,25 +721,18 @@ let spec_invariant lenv pvs vty spec =
c_post = post_inv ity spec.c_post;
c_xpost = Mexn.mapi xpost_inv spec.c_xpost }
let abstr_invariant lenv e q xq =
let ity = ity_or_unit e.e_vty in
let pvs = abstr_pvset Spv.empty e q xq in
let rvs = reset_vars e.e_effect pvs in
let _,qinv = env_invariant lenv e.e_effect pvs in
let post_inv = post_invariant lenv rvs qinv in
let xpost_inv xs q = post_inv xs.xs_ity q in
post_inv ity q, Mexn.mapi xpost_inv xq
let abstr_invariant lenv e spec0 =
let pvs = e_pvset Spv.empty e in
let spec = { spec0 with c_effect = e.e_effect } in
let spec = spec_invariant lenv pvs e.e_vty spec in
(* we do not require invariants on free variables *)
{ spec with c_pre = spec0.c_pre }
let lambda_invariant lenv pvs eff lam =
let ity = ity_or_unit lam.l_expr.e_vty in
let pvs = List.fold_right Spv.add lam.l_args pvs in
let rvs = reset_vars eff pvs in
let pinv,qinv = env_invariant lenv eff pvs in
let post_inv = post_invariant lenv rvs qinv in
let xpost_inv xs q = post_inv xs.xs_ity q in
{ lam with l_pre = t_and_simp lam.l_pre pinv;
l_post = post_inv ity lam.l_post;
l_xpost = Mexn.mapi xpost_inv lam.l_xpost }
let spec = { lam.l_spec with c_effect = eff } in
let spec = spec_invariant lenv pvs lam.l_expr.e_vty spec in
{ lam with l_spec = spec }
let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
......@@ -1081,8 +1074,11 @@ and expr_desc lenv loc de = match de.de_desc with
let e1 = expr lenv de1 in
let q = create_post lenv "result" e1.e_vty q in
let xq = complete_xpost lenv e1.e_effect xq in
let q, xq = abstr_invariant lenv e1 q xq in
e_abstract e1 q xq
let spec = {
c_pre = t_true; c_post = q; c_xpost = xq;
c_effect = eff_empty; c_variant = [] } in
let spec = abstr_invariant lenv e1 spec in
e_abstract e1 spec
| DEassert (ak, f) ->
let ak = match ak with
| Ptree.Aassert -> Aassert
......@@ -1162,12 +1158,14 @@ and expr_lam lenv gh pvl (var, p, de, q, xq) =
let e = e_ghostify gh (expr lenv de) in
if not gh && vty_ghost e.e_vty then
errorm ~loc:de.de_loc "ghost body in a non-ghost function";
{ l_args = pvl;
l_variant = List.map (create_variant lenv) var;
l_pre = create_pre lenv p;
l_expr = e;
l_post = create_post lenv "result" e.e_vty q;
l_xpost = complete_xpost lenv e.e_effect xq }
let spec = {
c_pre = create_pre lenv p;
c_post = create_post lenv "result" e.e_vty q;
c_xpost = complete_xpost lenv e.e_effect xq;
c_effect = e.e_effect;
c_variant = List.map (create_variant lenv) var; }
in
{ l_args = pvl; l_expr = e; l_spec = spec }
(** Type declaration *)
......
src/whyml/mlw_wp.ml
View file @ 3dcca8d3
......@@ -725,10 +725,11 @@ and wp_desc env e q xq = match e.e_node with
let w = wp_and ~sym:false (wp_and ~sym:true d p) w in (* FIXME? ~sym? *)
let q = create_unit_post w in
wp_expr env e1 q xq (* FIXME? should (wp_label e) rather be here? *)
| Eabstr (e1, c_q, c_xq) ->
let w1 = backstep (wp_expr env e1) c_q c_xq in
let w2 = wp_abstract env e1.e_effect c_q c_xq q xq in
wp_and ~sym:true (wp_label e w1) w2
| Eabstr (e1, spec) ->
let p = wp_label e (wp_expl expl_pre spec.c_pre) in
let w1 = backstep (wp_expr env e1) spec.c_post spec.c_xpost in
let w2 = wp_abstract env e1.e_effect spec.c_post spec.c_xpost q xq in
wp_and ~sym:false p (wp_and ~sym:true (wp_label e w1) w2)
| Eassign (e1, reg, pv) ->
let rec get_term d = match d.e_node with
| Elogic t -> t
......@@ -819,23 +820,23 @@ and wp_abstract env c_eff c_q c_xq q xq =
backstep proceed c_q c_xq
and wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
let lab = fresh_mark () in
let lab = fresh_mark () and c = l.l_spec in
let add_arg sbs pv = ity_match sbs pv.pv_vtv.vtv_ity pv.pv_vtv.vtv_ity in
let subst = List.fold_left add_arg ps.ps_subst l.l_args in
let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
let args = List.map (fun pv -> pv.pv_vs) l.l_args in
let env = if l.l_variant = [] then env else
let env = if 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 tl = List.map t_at_lab l.l_variant in
let tl = List.map t_at_lab c.c_variant in
let add_family lrv fam = Mint.add fam tl lrv in
let lrv = List.fold_left add_family env.letrec_var faml in
{ env with letrec_var = lrv }
in
let q = old_mark lab (wp_expl expl_post l.l_post) in
let q = old_mark lab (wp_expl expl_post c.c_post) in
let conv p = old_mark lab (wp_expl expl_xpost p) in
let f = wp_expr env l.l_expr q (Mexn.map conv l.l_xpost) in
let f = wp_implies l.l_pre (erase_mark lab f) in
let f = wp_expr env l.l_expr q (Mexn.map conv c.c_xpost) in
let f = wp_implies c.c_pre (erase_mark lab f) in
wp_forall args (quantify env regs f)
and wp_rec_defn env fdl =
......@@ -1054,7 +1055,7 @@ and fast_wp_desc env s r e =
let ok = if kind = Aassume then t_true else f in
let ne = if kind = Acheck then t_true else f in
ok, ((ne, s), Mexn.empty)
| Eabstr (_, _, _) -> assert false (*TODO*)
| Eabstr (_, _) -> assert false (*TODO*)
| Etry (_, _) -> assert false (*TODO*)
| Eraise (_, _) -> assert false (*TODO*)
| Efor (_, _, _, _) -> assert false (*TODO*)
......@@ -1084,28 +1085,28 @@ and fast_wp_desc env s r e =
and fast_wp_fun_defn env faml { fun_ps = ps ; fun_lambda = l } =
(* OK: forall bl. pl => ok(e)
NE: true *)
let lab = fresh_mark () in
let lab = fresh_mark () and c = l.l_spec in
let add_arg sbs pv = ity_match sbs pv.pv_vtv.vtv_ity pv.pv_vtv.vtv_ity in
let subst = List.fold_left add_arg ps.ps_subst l.l_args in
let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
let args = List.map (fun pv -> pv.pv_vs) l.l_args in
let env = if l.l_variant = [] then env else
let env = if 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 tl = List.map t_at_lab l.l_variant in
let tl = List.map t_at_lab c.c_variant in
let add_family lrv fam = Mint.add fam tl lrv in
let lrv = List.fold_left add_family env.letrec_var faml in
{ env with letrec_var = lrv }
in
let q = old_mark lab (wp_expl expl_post l.l_post) in
let q = old_mark lab (wp_expl expl_post c.c_post) in
let result, _ as q = open_post q in
let conv p = old_mark lab (wp_expl expl_xpost p) in
let xq = Mexn.map conv l.l_xpost in
let xq = Mexn.map conv c.c_xpost in
let xq = Mexn.map open_post xq in
let xresult = Mexn.map fst xq in
let ok, n = fast_wp_expr env Subst.empty (result, xresult) l.l_expr in
let f = wp_and ~sym:true ok (wp_nimplies n (q, xq)) in
let f = wp_implies l.l_pre (erase_mark lab f) in
let f = wp_implies c.c_pre (erase_mark lab f) in
wp_forall args (quantify env regs f)
and fast_wp_rec_defn env fdl =
......
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