Commit 4ae19de7 authored by Robbert Krebbers's avatar Robbert Krebbers

Let `lcons` return unit.

parent 58a96a4a
......@@ -65,7 +65,7 @@ Definition par_map_reduce_reduce_server : val :=
send "cred" #false;; "go" ("n" - #1) "csort" "cred" NONE "zs"
| SOME "acc" =>
(* Read subsequent items with the same key *)
let: "ys" := lcons (Snd "acc") (lnil #()) in
let: "ys" := lnil #() in lcons (Snd "acc") "ys";;
let: "new_acc" := par_map_reduce_collect "csort" (Fst "acc") "ys" in
send "cred" #true;;
send "cred" (Fst "acc", "ys");;
......
......@@ -10,8 +10,8 @@ Definition lmerge : val :=
let: "y" := lhead "ys" in
let: "z" := lhead "zs" in
if: "cmp" "y" "z"
then lpop "ys";; "go" "cmp" "ys" "zs";; lcons "y" "ys";; #()
else lpop "zs";; "go" "cmp" "ys" "zs";; lcons "z" "ys";; #().
then lpop "ys";; "go" "cmp" "ys" "zs";; lcons "y" "ys"
else lpop "zs";; "go" "cmp" "ys" "zs";; lcons "z" "ys".
Definition sort_service : val :=
rec: "go" "c" :=
......@@ -69,14 +69,12 @@ Section sort.
wp_apply (lpop_spec with "Hl1"); iIntros "Hl1".
wp_apply ("IH" $! _ _ (x2 :: _) with "Hl1 Hl2 HI1' [$HI2 $HI2']").
iIntros (ws) "[Hl1 HI]".
wp_apply (lcons_spec with "Hl1"); iIntros "Hl1".
wp_pures. iApply "HΨ". iFrame.
wp_apply (lcons_spec with "Hl1"); iIntros "Hl1". iApply "HΨ". iFrame.
- rewrite decide_False //.
wp_apply (lpop_spec with "Hl2"); iIntros "Hl2".
wp_apply ("IH" $! _ (x1 :: _) with "Hl1 Hl2 [$HI1 $HI1'] HI2'").
iIntros (ws) "[Hl1 HI]".
wp_apply (lcons_spec with "Hl1"); iIntros "Hl1".
wp_pures. iApply "HΨ". iFrame.
wp_apply (lcons_spec with "Hl1"); iIntros "Hl1". iApply "HΨ". iFrame.
Qed.
Lemma sort_service_spec p c :
......@@ -84,8 +82,7 @@ Section sort.
sort_service c
{{{ RET #(); c p @ N }}}.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ).
wp_lam.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (p c Ψ). wp_lam.
wp_recv (A I R ?? cmp) as "#Hcmp".
wp_recv (xs l vs) as "[Hl HI]".
wp_apply (llength_spec with "Hl"); iIntros "Hl".
......
......@@ -13,7 +13,8 @@ Definition send_all : val :=
Definition recv_all : val :=
rec: "go" "c" :=
if: ~recv "c" then lnil #() else
let: "x" := recv "c" in lcons "x" ("go" "c").
let: "x" := recv "c" in
let: "l" := "go" "c" in lcons "x" "l";; "l".
Definition sort_elem_client : val :=
λ: "cmp" "xs",
......@@ -57,7 +58,7 @@ Section sort_elem_client.
- wp_recv (y v) as (Htl) "HIxv".
wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
iIntros (l ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "(Hl & Hc & HI)".
wp_apply (lcons_spec with "Hl"); iIntros "Hl".
wp_apply (lcons_spec with "Hl"); iIntros "Hl"; wp_pures.
iApply ("HΦ" $! _ (y :: ys)); simpl; eauto with iFrame.
- wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
iApply ("HΦ" $! _ [] []); rewrite /= right_id_L; by iFrame.
......
......@@ -10,7 +10,7 @@ Fixpoint llist `{heapG Σ} (l : loc) (vs : list val) : iProp Σ :=
Arguments llist : simpl never.
Definition lnil : val := λ: <>, ref NONE.
Definition lcons : val := λ: "x" "l", "l" <- SOME ("x", ref (!"l"));; "l".
Definition lcons : val := λ: "x" "l", "l" <- SOME ("x", ref (!"l")).
Definition lisnil : val := λ: "l",
match: !"l" with
......@@ -83,7 +83,7 @@ Lemma lnil_spec :
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_alloc l. by iApply "HΦ". Qed.
Lemma lcons_spec l v vs :
{{{ llist l vs }}} lcons v #l {{{ RET #l; llist l (v :: vs) }}}.
{{{ llist l vs }}} lcons v #l {{{ RET #(); llist l (v :: vs) }}}.
Proof.
iIntros (Φ) "Hll HΦ". wp_lam. destruct vs as [|v' vs]; simpl; wp_pures.
- wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
......
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