Commit 7c4416b6 authored by Robbert Krebbers's avatar Robbert Krebbers

Let wp_store to a wp_seq if possible.

parent e78a78ab
...@@ -148,7 +148,7 @@ Tactic Notation "wp_store" := ...@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity |env_cbv; reflexivity
|wp_finish] |wp_finish; try wp_seq]
| _ => fail "wp_store: not a 'wp'" | _ => fail "wp_store: not a 'wp'"
end. end.
......
...@@ -45,7 +45,7 @@ Section client. ...@@ -45,7 +45,7 @@ Section client.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done. iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
iFrame "Hh". iSplitL "Hy Hs". iFrame "Hh". iSplitL "Hy Hs".
- (* The original thread, the sender. *) - (* The original thread, the sender. *)
wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done]. wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op. iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
- (* The two spawned threads, the waiters. *) - (* The two spawned threads, the waiters. *)
iSplitL; [|by iIntros {_ _} "_ >"]. iSplitL; [|by iIntros {_ _} "_ >"].
......
...@@ -27,7 +27,7 @@ Section LiftingTests. ...@@ -27,7 +27,7 @@ Section LiftingTests.
nclose N E heap_ctx N WP heap_e @ E {{ v, v = #2 }}. nclose N E heap_ctx N WP heap_e @ E {{ v, v = #2 }}.
Proof. Proof.
iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done. iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load. wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
Qed. Qed.
Definition heap_e2 : expr [] := Definition heap_e2 : expr [] :=
...@@ -39,7 +39,7 @@ Section LiftingTests. ...@@ -39,7 +39,7 @@ Section LiftingTests.
Proof. Proof.
iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done. iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
wp_alloc l. wp_let. wp_alloc l'. wp_let. wp_alloc l. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_seq. wp_load. done. wp_load. wp_op. wp_store. wp_load. done.
Qed. Qed.
Definition FindPred : val := Definition FindPred : val :=
......
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