Commit a1e93de9 by Robbert Krebbers

### Use option in spawn.

parent 98d7ce9b
 ... ... @@ -5,13 +5,13 @@ Import uPred. Definition spawn : val := λ: "f", let: "c" := ref (InjL #0) in Fork ("c" <- InjR ("f" #())) ;; "c". let: "c" := ref NONE in Fork ("c" <- SOME ("f" #())) ;; "c". Definition join : val := rec: "join" "c" := match: !"c" with InjR "x" => "x" | InjL <> => "join" "c" SOME "x" => "x" | NONE => "join" "c" end. Global Opaque spawn join. ... ... @@ -33,8 +33,8 @@ Context (heapN N : namespace). Local Notation iProp := (iPropG heap_lang Σ). Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp) : iProp := (∃ lv, l ↦ lv ★ (lv = InjLV #0 ∨ ∃ v, lv = InjRV v ★ (Ψ v ∨ own γ (Excl ()))))%I. (∃ lv, l ↦ lv ★ (lv = NONEV ∨ ∃ v, lv = SOMEV v ★ (Ψ v ∨ own γ (Excl ()))))%I. Definition join_handle (l : loc) (Ψ : val → iProp) : iProp := (heapN ⊥ N ★ ∃ γ, heap_ctx heapN ★ own γ (Excl ()) ★ ... ... @@ -60,13 +60,13 @@ Proof. wp_let. wp_alloc l as "Hl". wp_let. iPvs (own_alloc (Excl ())) as (γ) "Hγ"; first done. iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done. { iNext. iExists (InjLV #0). iFrame; eauto. } { iNext. iExists NONEV. iFrame; eauto. } wp_apply wp_fork. iSplitR "Hf". - iPvsIntro. wp_seq. iPvsIntro. iApply "HΦ". rewrite /join_handle. eauto. - wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv". iInv N as (v') "[Hl _]"; first wp_done. wp_store. iPvsIntro. iSplit; [iNext|done]. iExists (InjRV v). iFrame. eauto. iExists (SOMEV v). iFrame. eauto. Qed. Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!