Commit 0337bba4 authored by Dan Frumin's avatar Dan Frumin

Thunk the arguments for a_sequence

parent 53d00192
......@@ -39,7 +39,10 @@ Definition a_seq : val := λ: <>,
a_atomic_env (λ: "env", mset_clear "env").
Definition a_sequence : val := λ: "e1" "e2",
a_bind (λ: <>, a_bind (λ: <>, "e2") (a_seq #())) "e1".
("e1" #());;; a_seq #();;;("e2" #()).
Notation "a ;;;; b"
:= (a_sequence (λ: <>, a) (λ: <>, b))%E (at level 80, right associativity).
Definition a_if : val := λ: "cnd" "e1" "e2",
a_bind (λ: "c", if: "c" then "e1" else "e2") "cnd".
......@@ -88,14 +91,16 @@ Section proofs.
{ rewrite -big_sepM_insert_override; eauto. }
Qed.
Lemma a_sequence_spec R (v1 v2: val) Φ :
awp v1 R (λ _, U (awp v2 R Φ)) - awp (a_sequence v1 v2) R Φ.
Lemma a_sequence_spec R (e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} Φ :
awp e1 R (λ _, U (awp e2 R Φ)) -
awp (e1 ;;;; e2) R Φ.
Proof.
iIntros "HΦ". do 2 awp_lam. iApply awp_bind.
awp_lam.
iApply (awp_wand with "[HΦ]"); first done.
iIntros (v) "H". awp_lam. iApply awp_bind. iApply a_seq_spec.
iUnlock. by awp_pure _.
Qed.
iUnlock. by do 2 awp_lam.
Qed.
Lemma a_load_spec R (l : loc) (v : val) Φ :
l U v -
......@@ -129,10 +134,12 @@ Section proofs.
- by iApply "HΦ".
Qed.
Lemma a_alloc_spec R (v : val) Φ :
Lemma a_alloc_spec R (ev : expr) (v : val) Φ :
IntoVal ev v
( l, l U v - Φ #l) -
awp (a_alloc (a_ret v)) R Φ.
awp (a_alloc (a_ret ev)) R Φ.
Proof.
intros <-%of_to_val.
unfold a_alloc. iIntros "HΦ".
rewrite /a_ret.
do 2 awp_lam.
......@@ -141,7 +148,8 @@ Section proofs.
iApply awp_atomic_env.
iIntros (env) "Henv HR".
rewrite {2}/env_inv.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)". iDestruct "Hlocks" as %Hlocks.
iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
iDestruct "Hlocks" as %Hlocks.
iApply wp_fupd.
wp_let. wp_alloc l as "Hl".
iAssert (⌜σ !! l = None)%I with "[Hl Hls]" as %Hl.
......@@ -237,7 +245,7 @@ Section proofs.
iIntros "HΦ". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "HΦ").
iIntros (v) "[[% H] | [% H]]"; subst; by repeat awp_pure _.
Qed.
Qed.
End proofs.
......@@ -70,27 +70,43 @@ Section test.
by iFrame.
Qed.
Definition swap (l1 l2 : loc) : val := λ: <>,
Definition swap : val := λ: "l1" "l2",
a_bind (λ: "r",
a_sequence
(a_bind (λ: "v", (a_store (a_ret "r") (a_ret "v"))) (a_load (a_ret #l1)))
(a_sequence
(a_store (a_ret #l1) (a_load (a_ret #l2)))
(a_store (a_ret #l2) (a_load (a_ret "r")))) ;;; a_seq #() )
((a_bind (λ: "v", (a_store (a_ret "r")) (a_ret "v"))) (a_load (a_ret "l1")));;;;
((a_bind (λ: "v", (a_store (a_ret "l1")) (a_ret "v"))) (a_load (a_ret "l2")));;;;
((a_bind (λ: "v", (a_store (a_ret "l2")) (a_ret "v"))) (a_load (a_ret "r")));;;
a_seq #())
(a_alloc (a_ret #0%V)).
Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
l1 U v1 - l2 U v2 -
awp (swap l1 l2 #()) R (λ _, l1 U v2 l2 U v1).
awp (swap #l1 #l2) R (λ _, l1 U v2 l2 U v1).
Proof.
iIntros "Hl1 Hl2".
awp_lam.
do 2 awp_lam.
iApply awp_bind.
iApply (a_alloc_spec R #0 ).
iApply a_alloc_spec.
iIntros (r) "Hr".
awp_lam. iApply awp_bind.
Admitted.
awp_lam.
iApply a_sequence_spec.
iApply awp_bind.
iApply (a_load_spec with "Hl1"). iIntros "Hl1".
awp_lam.
iApply (a_store_spec with "Hr"). iIntros "Hr".
iUnlock.
iApply a_sequence_spec.
iApply awp_bind.
iApply (a_load_spec with "Hl2"). iIntros "Hl2".
awp_lam.
iApply (a_store_spec with "Hl1"). iIntros "Hl1".
iUnlock.
iApply awp_bind.
iApply awp_bind.
iApply (a_load_spec with "Hr"). iIntros "Hr".
awp_lam.
iApply (a_store_spec with "Hl2"). iIntros "Hl2".
awp_lam.
iApply a_seq_spec. iUnlock; iFrame.
Qed.
End test.
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