Commit 2b37af79 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: handle labels over proxy let-in in Expr rather than in Vc

parent 2942e4df
......@@ -1022,7 +1022,7 @@ let rec expr uloc env ({de_loc = loc} as de) =
let e = Loc.try3 ?loc try_expr uloc env de in
let loc = Opt.get_def loc uloc in
if loc = None && Slab.is_empty labs
then e else e_label ?loc labs e
then e else e_label_push ?loc labs e
and cexp uloc env ghost ({de_loc = loc} as de) vl =
let uloc, labs, de = strip uloc Slab.empty de in
......
......@@ -351,6 +351,18 @@ let e_label_copy { e_label = lab; e_loc = loc } e =
let loc = if e.e_loc = None then loc else e.e_loc in
{ e with e_label = lab; e_loc = loc }
let proxy_label = create_label "whyml_proxy_symbol"
let proxy_labels = Slab.singleton proxy_label
let rec e_label_push ?loc l e = match e.e_node with
| (Elet (LDvar ({pv_vs = {vs_name = id}},_) as ld, e1)
| Elet (LDsym ({rs_name = id},_) as ld, e1))
when Slab.mem proxy_label id.id_label ->
let e1 = e_label_push ?loc l e1 in
{ e with e_node = Elet (ld, e1); e_loc = loc }
| _ ->
{ e with e_label = l; e_loc = loc }
let e_ghost e = e.e_effect.eff_ghost
let c_ghost c = c.c_cty.cty_effect.eff_ghost
......@@ -728,9 +740,6 @@ let c_pur s vl ityl ity =
let cty = create_cty v_args [] [q] Mexn.empty Mpv.empty eff ity in
mk_cexp (Cpur (s,vl)) cty
let proxy_label = create_label "whyml_proxy_symbol"
let proxy_labels = Slab.singleton proxy_label
let mk_proxy e hd = match e.e_node with
| Evar v when Slab.is_empty e.e_label -> hd, v
| _ ->
......
......@@ -157,6 +157,7 @@ and rec_defn = private {
(** {2 Expressions} *)
val e_label : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_push : ?loc:Loc.position -> Slab.t -> expr -> expr
val e_label_add : label -> expr -> expr
val e_label_copy : expr -> expr -> expr
......
......@@ -634,11 +634,6 @@ let rec wp_expr env e res q xq = match e.e_node with
let w = bind_oldies c (wp_havoc env c.cty_effect w) in
vc_label e (wp_and (vc_cexp env true ce) (wp_and p w))
| Elet (LDvar ({pv_vs = v}, e0), e1) (* FIXME: what for? *)
when Slab.mem proxy_label v.vs_name.id_label ->
(* we push the label down, past the inserted "let" *)
let q = wp_expr env (e_label_copy e e1) res q xq in
wp_expr env e0 v q xq
| Elet (LDvar ({pv_vs = v}, e0), e1)
| Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
let q = wp_expr env e1 res q xq in
......@@ -748,12 +743,6 @@ and sp_expr env e res xres dst = match e.e_node with
let ok = wp_of_pre env e.e_loc expl_pre c.cty_pre in
out_label e (wp_and (vc_cexp env false ce) ok, ne, ex)
| Elet (LDvar ({pv_vs = v}, e0), e1) (* FIXME: what for? *)
when Slab.mem proxy_label v.vs_name.id_label ->
(* we push the label down, past the inserted "let" *)
let e1 = e_label_copy e e1 in
let out = sp_expr env e1 res xres dst in
sp_pred_let env e0 v xres out e1 eff_empty dst
| Elet (LDvar ({pv_vs = v}, e0), e1)
| Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
let out = sp_expr env e1 res xres dst in
......@@ -940,12 +929,6 @@ and sp_pred_seq env e0 res xres out e1 eff dst =
and sp_seq env e res xres out eff dst = match e.e_node with
| Eghost e1 ->
sp_seq env (e_label_copy e e1) res xres out eff dst
| Elet (LDvar ({pv_vs = v}, e0), e1) (* FIXME: what for? *)
when Slab.mem proxy_label v.vs_name.id_label ->
(* we push the label down, past the inserted "let" *)
let e1 = e_label_copy e e1 in
let out = sp_seq env e1 res xres out eff dst in
sp_pred_let env e0 v xres out e1 eff dst
| Elet (LDvar ({pv_vs = v}, e0), e1)
| Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
let out = sp_seq env e1 res xres out eff dst in
......@@ -1063,9 +1046,11 @@ and vc_let_sym env vc_wp ld {e_effect = eff} =
let sm = List.fold_left add_rd Mrs.empty rdl in
let add_rd d dl = add_rs sm d.rec_sym d.rec_fun dl in
List.fold_right add_rd rdl ([],[]) in
(* TODO: switch to sp_*_close when it handles multiple results *)
let close_wp wp =
wp_and ok (wp_forall vl (List.fold_right sp_implies ax wp)) in
let close_sp = if vc_wp then (fun _ -> assert false) else
(* replace pv with fresh vs so that sp_wp_close binds them *)
let sbs = List.fold_left (fun sbs v ->
Mvs.add v (t_var (clone_vs v)) sbs) Mvs.empty vl in
fun sp -> t_subst sbs (List.fold_right sp_and ax sp) in
......
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