Commit 6628e772 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (`iSpecialize` changes).

parent 771f5a3e
Pipeline #23469 passed with stage
in 14 minutes and 41 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-11-21.4.d1787db2") | (= "dev") }
"coq-iris" { (= "dev.2020-02-01.2.dba20c7f") | (= "dev") }
]
......@@ -210,7 +210,7 @@ Section forward_spec.
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]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 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'".
{ 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.
......@@ -237,9 +237,9 @@ Section forward_spec.
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 "H []") as "H'".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
iApply (denv_stack_interp_wand with "H'"); iIntros "{H1 H2 H H'} [[H1 H2] H]".
iApply (cwp_store with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
......@@ -254,7 +254,7 @@ Section forward_spec.
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]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 H} [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.
......@@ -268,9 +268,9 @@ Section forward_spec.
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 "H []") as "H'".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
iApply (denv_stack_interp_wand with "H'"); iIntros "{H1 H2 H 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]".
......@@ -282,7 +282,7 @@ Section forward_spec.
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
destruct (dun_op_eval _ _ _) as [dw|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} H".
iApply cwp_un_op. iApply (cwp_wand with "H"); iIntros (v1) "[-> $]"; eauto.
- (* par *)
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
......@@ -290,7 +290,7 @@ Section forward_spec.
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]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H1 H2 H} [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