Commit d5229693 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use SOME/NONE in tests/one_shot.

parent 2966b4da
...@@ -5,17 +5,17 @@ From iris.proofmode Require Import invariants ghost_ownership. ...@@ -5,17 +5,17 @@ From iris.proofmode Require Import invariants ghost_ownership.
Import uPred. Import uPred.
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref (InjL #0) in ( let: "x" := ref NONE in (
(* tryset *) (λ: "n", (* tryset *) (λ: "n",
CAS "x" (InjL #0) (InjR "n")), CAS "x" NONE (SOME "n")),
(* check *) (λ: <>, (* check *) (λ: <>,
let: "y" := !"x" in λ: <>, let: "y" := !"x" in λ: <>,
match: "y" with match: "y" with
InjL <> => #() NONE => #()
| InjR "n" => | SOME "n" =>
match: !"x" with match: !"x" with
InjL <> => assert: #false NONE => assert: #false
| InjR "m" => assert: "n" = "m" | SOME "m" => assert: "n" = "m"
end end
end)). end)).
Global Opaque one_shot_example. Global Opaque one_shot_example.
...@@ -35,8 +35,8 @@ Context (heapN N : namespace) (HN : heapN ⊥ N). ...@@ -35,8 +35,8 @@ Context (heapN N : namespace) (HN : heapN ⊥ N).
Local Notation iProp := (iPropG heap_lang Σ). Local Notation iProp := (iPropG heap_lang Σ).
Definition one_shot_inv (γ : gname) (l : loc) : iProp := Definition one_shot_inv (γ : gname) (l : loc) : iProp :=
(l InjLV #0 own γ Pending (l NONEV own γ Pending
n : Z, l InjRV #n own γ (Cinr (DecAgree n)))%I. n : Z, l SOMEV #n own γ (Cinr (DecAgree n)))%I.
Lemma wp_one_shot (Φ : val iProp) : Lemma wp_one_shot (Φ : val iProp) :
heap_ctx heapN ( f1 f2 : val, heap_ctx heapN ( f1 f2 : val,
...@@ -58,14 +58,14 @@ Proof. ...@@ -58,14 +58,14 @@ Proof.
iPvsIntro; iRight; iExists n; by iSplitL "Hl". iPvsIntro; iRight; iExists n; by iSplitL "Hl".
+ wp_cas_fail. rewrite /one_shot_inv; eauto 10. + wp_cas_fail. rewrite /one_shot_inv; eauto 10.
- iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ". - iIntros "!". wp_seq. wp_focus (! _)%E. iInv> N as "Hγ".
iAssert ( v, l v ((v = InjLV #0 own γ Pending) iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = InjRV #n own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv". n : Z, v = SOMEV #n own γ (Cinr (DecAgree n))))%I with "[-]" as "Hv".
{ iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]". { iDestruct "Hγ" as "[[Hl Hγ]|Hl]"; last iDestruct "Hl" as (m) "[Hl Hγ]".
+ iExists (InjLV #0). iFrame. eauto. + iExists NONEV. iFrame. eauto.
+ iExists (InjRV #m). iFrame. eauto. } + iExists (SOMEV #m). iFrame. eauto. }
iDestruct "Hv" as (v) "[Hl Hv]". wp_load; iPvsIntro. iDestruct "Hv" as (v) "[Hl Hv]". wp_load; iPvsIntro.
iAssert (one_shot_inv γ l (v = InjLV #0 n : Z, iAssert (one_shot_inv γ l (v = NONEV n : Z,
v = InjRV #n own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]". v = SOMEV #n own γ (Cinr (DecAgree n))))%I with "[-]" as "[$ #Hv]".
{ iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst. { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
+ iSplit. iLeft; by iSplitL "Hl". eauto. + iSplit. iLeft; by iSplitL "Hl". eauto.
+ iSplit. iRight; iExists m; by iSplitL "Hl". eauto. } + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
......
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