diff --git a/theories/tests/swap.v b/theories/tests/swap.v index 2125bf06fc66c8b2bc738be74171e3daf4afa802..cde79a79504a813f88ac8c762f766f2960cf2760 100644 --- a/theories/tests/swap.v +++ b/theories/tests/swap.v @@ -4,9 +4,9 @@ Section tests_vcg. Context `{amonadG Σ}. Definition swap : val := λ: "a", - let: "l1" := Fst "a" in - let: "l2" := Fst (Snd "a") in - let: "r" := Snd (Snd "a") in + "l1" ←ᶜ a_ret (Fst "a");ᶜ + "l2" ←ᶜ a_ret (Fst (Snd "a"));ᶜ + "r" ←ᶜ a_ret (Snd (Snd "a"));ᶜ (a_ret "r") =ᶜ ∗ᶜ (a_ret "l1") ;ᶜ (a_ret "l1") =ᶜ ∗ᶜ (a_ret "l2") ;ᶜ (a_ret "l2") =ᶜ ∗ᶜ (a_ret "r") ;ᶜ @@ -18,13 +18,13 @@ Section tests_vcg. {{ _, l2 ↦C v1 ∗ l1 ↦C v2 }}. Proof. iIntros "Hr [Hl1 Hl2]". - awp_pures. awp_lam. do 11 (awp_pure _). + awp_pures. awp_lam. vcg. eauto with iFrame. Qed. Definition swap_with_alloc : val := λ: "a", - let: "l1" := Fst "a" in - let: "l2" := Snd "a" in + "l1" ←ᶜ a_ret (Fst "a");ᶜ + "l2" ←ᶜ a_ret (Snd "a");ᶜ "r" ←ᶜ allocᶜ (♯1, ♯0);ᶜ (a_ret "r") =ᶜ ∗ᶜ (a_ret "l1") ;ᶜ (a_ret "l1") =ᶜ ∗ᶜ (a_ret "l2") ;ᶜ @@ -36,8 +36,8 @@ Section tests_vcg. AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2) @ R {{ _, l1 ↦C v2 ∗ l2 ↦C v1 }}. Proof. iIntros "Hl1 Hl2". - awp_pures. awp_lam. do 6 (awp_pure _). - vcg. iIntros (l3) "? l1 l2 l3". eauto with iFrame. + awp_pures. awp_lam. vcg. + iIntros (l3) "? l1 l2 l3". eauto with iFrame. Qed. End tests_vcg.