Commit e2c493dd by Ralf Jung

### avoid clash of notations between disjunction and parallel composition

parent e7ecf91e
 ... @@ -10,7 +10,7 @@ Definition par : val := ... @@ -10,7 +10,7 @@ Definition par : val := let: "v2" := Snd "fs" #() in let: "v2" := Snd "fs" #() in let: "v1" := join "handle" in let: "v1" := join "handle" in ("v1", "v2"). ("v1", "v2"). Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Global Opaque par. Global Opaque par. Section proof. Section proof. ... @@ -39,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) ... @@ -39,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) : (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) : (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗ (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) ⊢ WP e1 || e2 {{ Φ }}. ⊢ WP e1 ||| e2 {{ Φ }}. Proof. Proof. iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- \$Hh \$H]"); try wp_done. iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- \$Hh \$H]"); try wp_done. iSplitL "H1"; by wp_let. iSplitL "H1"; by wp_let. ... ...
 ... @@ -9,8 +9,8 @@ Definition worker (n : Z) : val := ... @@ -9,8 +9,8 @@ Definition worker (n : Z) : val := Definition client : expr := Definition client : expr := let: "y" := ref #0 in let: "y" := ref #0 in let: "b" := newbarrier #() in let: "b" := newbarrier #() in ("y" <- (λ: "z", "z" + #42) ;; signal "b") || ("y" <- (λ: "z", "z" + #42) ;; signal "b") ||| (worker 12 "b" "y" || worker 17 "b" "y"). (worker 12 "b" "y" ||| worker 17 "b" "y"). Global Opaque worker client. Global Opaque worker client. Section client. Section client. ... ...
 ... @@ -20,7 +20,7 @@ Proof. apply subG_inG. Qed. ... @@ -20,7 +20,7 @@ Proof. apply subG_inG. Qed. Definition client eM eW1 eW2 : expr := Definition client eM eW1 eW2 : expr := let: "b" := newbarrier #() in let: "b" := newbarrier #() in (eM ;; signal "b") || ((wait "b" ;; eW1) || (wait "b" ;; eW2)). (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)). Global Opaque client. Global Opaque client. Section proof. Section proof. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!