Commit ab69de42 authored by Dan Frumin's avatar Dan Frumin

Stop loosing all of them locations in vcgen binop case.

parent 98432a2e
......@@ -140,8 +140,8 @@ Section vcg.
(m : denv) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match dcbin_op_eval E op dv1 dv2 with
| dSome dw => Φ E m dw
| mdw => dw, doption_interp mdw = Some dw
vcg_wp_continuation E Φ (dval_interp E dw)
| mdw => v, dval_interp E <$> (doption_interp mdw) = Some v
mapsto_wand_list E m (vcg_wp_continuation E Φ v)
end%I.
Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
......@@ -633,15 +633,19 @@ Section vcg_spec.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dcbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin.
* iDestruct "Hwp" as (dw Hopt) "Hcont"; simplify_eq.
* iExists (dval_interp E dw); iSplit.
* iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
apply dcbin_op_eval_dSome_wf in Hbin; try done.
rewrite -denv_merge_interp //. eauto with iFrame.
* iDestruct "Hwp" as (dw0 Hopt) "Hcont"; simplify_eq.
* iDestruct "Hwp" as (w0 Hopt) "Hcont"; simplify_eq.
destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E dw0); iSplit; last done.
iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin.
iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
rewrite mapsto_wand_list_spec. iSpecialize ("Hcont" with "Hm").
iExists w0; iSplit; last done.
iPureIntro. rewrite -Hbin in Hopt.
destruct (doption_interp (dcbin_op_eval E b dv1 dv2)) as [dw0|] eqn:Hdw0; simplify_eq/=.
apply dcbin_op_eval_correct. by rewrite Hdw0.
Qed.
Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ :
......
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