Commit a054f077 authored by Robbert Krebbers's avatar Robbert Krebbers

More idiomatic fix: clear unused stuff asap.

parent 6628e772
Pipeline #24214 failed with stage
in 14 minutes and 34 seconds
......@@ -209,8 +209,8 @@ Section forward_spec.
{ apply (Forall_cons (denv_wf E)); eauto 10. }
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ (_ :: ms1) with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 H} [H1 H2]".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [H1 H2]".
iApply cwp_seq_bind. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
iDestruct (denv_unlock_interp with "Hm") as "Hm"; do 2 iModIntro.
iDestruct ("H2" with "Hm") as "[Hm2 H]". rewrite -dcexpr_interp_subst'.
......@@ -221,9 +221,9 @@ Section forward_spec.
destruct (dloc_var_of_dval _) as [i|] eqn:?; simplify_eq/=.
destruct (denv_delete_frac_2 i _ _) as [[[[ms2 mNew2] q] dv2]|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H'".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_frac_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H'"); iIntros "[H1 H2]".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply cwp_load. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
iDestruct ("H2" with "Hm") as "[Hm2 Hi]".
iIntros "$ !>". iExists _, _. iFrame "Hi". iSplit; first by eauto.
......@@ -236,10 +236,10 @@ Section forward_spec.
destruct (denv_delete_full_2 i ms2 _) as [[[ms3 mNew3] dv3]|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H'".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H'"); iIntros "{H1 H2 H H'} [[H1 H2] H]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [[H1 H2] H]".
iApply (cwp_store with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
......@@ -253,8 +253,8 @@ Section forward_spec.
destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 H} [H1 H2]".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply (cwp_bin_op with "H1 H2"); iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iExists _. repeat (iSplit; first by eauto).
iApply denv_merge_interp; eauto 10 with iFrame.
......@@ -267,10 +267,10 @@ Section forward_spec.
destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H'".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H'"); iIntros "{H1 H2 H H'} [[H1 H2] H]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [[H1 H2] H]".
iApply (cwp_pre_bin_op with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2] $ !>".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
......@@ -289,8 +289,8 @@ Section forward_spec.
destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 H} [H1 H2]".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply (cwp_par with "H1 H2"); iIntros "!>" (v1 v2) "[-> Hm1] [-> Hm2] !>".
iSplit; first done. iApply denv_merge_interp; eauto 10 with iFrame.
Qed.
......
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