Commit 08540ed7 authored by Dan Frumin's avatar Dan Frumin

Simplify swap

parent f0967467
...@@ -4,9 +4,9 @@ Section tests_vcg. ...@@ -4,9 +4,9 @@ Section tests_vcg.
Context `{amonadG Σ}. Context `{amonadG Σ}.
Definition swap : val := λ: "a", Definition swap : val := λ: "a",
let: "l1" := Fst "a" in "l1" ←ᶜ a_ret (Fst "a");
let: "l2" := Fst (Snd "a") in "l2" ←ᶜ a_ret (Fst (Snd "a"));
let: "r" := Snd (Snd "a") in "r" ←ᶜ a_ret (Snd (Snd "a"));
(a_ret "r") = ∗ᶜ (a_ret "l1") ; (a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ; (a_ret "l1") = ∗ᶜ (a_ret "l2") ;
(a_ret "l2") = ∗ᶜ (a_ret "r") ; (a_ret "l2") = ∗ᶜ (a_ret "r") ;
...@@ -18,13 +18,13 @@ Section tests_vcg. ...@@ -18,13 +18,13 @@ Section tests_vcg.
{{ _, l2 C v1 l1 C v2 }}. {{ _, l2 C v1 l1 C v2 }}.
Proof. Proof.
iIntros "Hr [Hl1 Hl2]". iIntros "Hr [Hl1 Hl2]".
awp_pures. awp_lam. do 11 (awp_pure _). awp_pures. awp_lam.
vcg. eauto with iFrame. vcg. eauto with iFrame.
Qed. Qed.
Definition swap_with_alloc : val := λ: "a", Definition swap_with_alloc : val := λ: "a",
let: "l1" := Fst "a" in "l1" ←ᶜ a_ret (Fst "a");
let: "l2" := Snd "a" in "l2" ←ᶜ a_ret (Snd "a");
"r" ←ᶜ alloc (1, 0); "r" ←ᶜ alloc (1, 0);
(a_ret "r") = ∗ᶜ (a_ret "l1") ; (a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ; (a_ret "l1") = ∗ᶜ (a_ret "l2") ;
...@@ -36,8 +36,8 @@ Section tests_vcg. ...@@ -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 }}. AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2) @ R {{ _, l1 C v2 l2 C v1 }}.
Proof. Proof.
iIntros "Hl1 Hl2". iIntros "Hl1 Hl2".
awp_pures. awp_lam. do 6 (awp_pure _). awp_pures. awp_lam. vcg.
vcg. iIntros (l3) "? l1 l2 l3". eauto with iFrame. iIntros (l3) "? l1 l2 l3". eauto with iFrame.
Qed. Qed.
End tests_vcg. End tests_vcg.
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