Commit 4fde9aa2 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

fixed in-place list reversal

parent 328c1d73
......@@ -20,6 +20,40 @@ Definition a_list_next : val := λ: "x",
| SOME "l" => (a_bind (λ: "p", a_ret (Snd "p")) (a_load (a_ret "l")))
end) "x".
(*TODO: generalize the function below to set an arbitrary node in the list *)
Definition a_list_set_next : val := λ: "x" "y",
a_bind (λ: "xs",
match: "xs" with
NONE => assert: #false
| SOME "l" =>
a_bind (λ:"p",
a_bind ( λ: "r",
a_store (a_ret "l") (a_ret (Fst "p", "r")))
(a_load "y"))
(a_load (a_ret "l"))
end) "x".
Definition a_list_store_next : val := λ: "x1" "x2",
a_bind (λ: "p",
match: Fst "p" with
NONE => assert: #false
| SOME "l" => a_bind (λ:"m", a_store (a_ret "l") (a_ret (Fst "m", Snd "p")))
(a_load (a_ret "l"))
end)
(a_par "x1" "x2").
Definition in_place_reverse : val := λ: "hd",
a_bind (λ: "i", a_bind (λ: "j",
a_while
(λ:<>, a_un_op NegOp (a_bin_op EqOp (a_load (a_ret "i")) (a_ret NONEV)))
(λ:<>, a_bind (λ: "k",
a_list_store_next (a_load (a_ret "i")) (a_load (a_ret "j")) ;;;;
a_store (a_ret "j") (a_load (a_ret "i")) ;;;;
a_store (a_ret "i") (a_load (a_ret "k")))
(a_alloc (a_list_next (a_load (a_ret "i"))))) ;;;;
(a_load (a_ret "j"))
) (a_alloc (a_ret NONEV))) (a_alloc (a_ret "hd")).
Section list_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
......@@ -54,47 +88,25 @@ End list_spec.
Section InPlaceReversal.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
(*TODO: generalize the function below to set an arbitrary node in the list *)
Definition a_list_set_next : val := λ: "x" "y",
a_bind (λ: "xs",
match: "xs" with
NONE => assert: #false
| SOME "l" =>
a_bind (λ:"p",
a_bind ( λ: "r",
a_store (a_ret "l") (a_ret (Fst "p", "r")))
(a_load (a_ret "y")))
(a_load (a_ret "l"))
end)
(a_load (a_ret "x")).
Definition in_place_reverse : val := λ: "hd",
a_bind (λ: "i", a_bind (λ: "j",
a_while
(λ:<>, a_un_op NegOp (a_bin_op EqOp (a_load (a_ret "i")) (a_ret NONEV)))
(λ:<>, a_bind (λ: "k",
a_list_set_next "i" "j" ;;;;
a_store (a_ret "j") (a_load (a_ret "i")) ;;;;
a_store (a_ret "i") (a_load (a_ret "k")))
(a_alloc (a_list_next (a_load (a_ret "i"))))) ;;;;
(a_load (a_ret "j"))
) (a_alloc (a_ret NONEV))) (a_alloc (a_ret "hd")).
Lemma a_list_set_next_spec (i j hd : loc) (x v w: val) R Φ :
i U (SOMEV #hd) hd U (x, v) j U w
(i U (SOMEV #hd) - hd L (x, w) - j U w - Φ (x, w)%V) -
awp (a_list_set_next #i #j) R Φ.
Lemma a_list_store_next_spec e1 e2 Ψ1 Ψ2 R Φ :
awp e1 R (λ v, (hd:loc) x old,
v = SOMEV #hd hd U (x, old) Ψ1 (x, SOMEV #hd)) -
awp e2 R Ψ2 -
( (hd : loc) x new, Ψ1 (x, SOMEV #hd) - Ψ2 new -
(hd L (x, new) - Φ (x, new)%V)) -
awp (a_list_store_next e1 e2) R Φ.
Proof.
iIntros "(Hi & Hhd & Hj & HΦ)". rewrite/ a_list_set_next. do 2 awp_lam.
iApply awp_bind. awp_load_ret i. iIntros "Hi". awp_let. awp_match.
iApply awp_bind. awp_load_ret hd. iIntros "Hd". awp_let.
iApply awp_bind. awp_load_ret j. iIntros "Hj". awp_let.
iApply (a_store_spec _ _ (λ v, v = hd)%I (λ z, z = (x, w)%V )%I).
- awp_ret_value.
- awp_proj; awp_ret_value.
- iIntros (? ?) "-> ->". iExists (x, v)%V; iFrame. iIntros "Hd".
iApply ("HΦ" with "[$Hi] [$Hd] [$Hj]").
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1"; awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2"; awp_lam.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>".
iDestruct "H1" as (hd x nxt ->) "(Hhd & HΨ1)".
do 4 awp_pure _. iApply awp_bind. awp_load_ret hd. iIntros "Hd".
awp_let. iApply a_store_ret. do 2 awp_proj; awp_ret_value.
iExists (x, nxt)%V. iFrame. iIntros "Hd".
iSpecialize ("HΦ" $! hd x with "HΨ1 H2"). by iApply "HΦ".
Qed.
Lemma in_place_reverse_spec (hd:val) xs R:
......@@ -110,16 +122,14 @@ Section InPlaceReversal.
- iExists xs, [], (InjLV #()), hd; eauto with iFrame.
- iModIntro; iIntros "H". clear hd.
iDestruct "H" as (ls rs rhd hd) "(Hi & Hls & Hj & Hrs & %)".
iApply a_un_op_spec.
iApply (a_bin_op_spec _ _
(λ x, x = hd i U hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ awp_load_ret i. } { awp_ret_value. }
iIntros (? ?) "[-> Hi ] ->".
destruct ls.
iApply a_un_op_spec. iApply (a_bin_op_spec _ _
(λ x, x = hd i U hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ awp_load_ret i. } { awp_ret_value. }
iIntros (? ?) "[-> Hi ] ->". destruct ls.
+ rewrite{1}/ is_list. iDestruct "Hls" as "->".
iExists #true; iSplit; first done. iExists #false; iSplit; first done.
iLeft; iSplit; first done. do 2 iModIntro. awp_seq. awp_load_ret j.
iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
+ iDestruct "Hls" as (l lnxt) "(-> & Hl & Hls)". fold is_list.
iExists #false; iSplit; first done; iExists #true; iSplit; first done.
iRight. iSplit; first done. iApply awp_bind.
......@@ -127,8 +137,13 @@ Section InPlaceReversal.
awp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
iSplit; first done. iFrame. iIntros "Hl Hls".
iIntros (k) "Hk". awp_let. iApply a_sequence_spec.
iApply (a_list_set_next_spec with "[$Hi $Hl $Hj Hls Hrs Hk]").
iIntros "Hi Hl Hj". iModIntro. awp_seq. iApply a_sequence_spec.
iApply (a_list_store_next_spec _ _
(λ z, z = (v, SOMEV #l) i U (SOMEV #l) )%I
(λ v, v = rhd j U rhd )%I with "[Hi Hl] [Hj]").
{ awp_load_ret i. eauto 42 with iFrame. }
{ awp_load_ret j. }
iIntros (? ? ?) "(% & Hi) (% & Hj)". simplify_eq.
iIntros "Hl". iModIntro. awp_seq. iApply a_sequence_spec.
iApply (a_move_spec with "[$Hj $Hi Hls Hrs Hk Hl]").
iIntros "Hi Hj". iModIntro. awp_seq.
iApply (a_move_spec with "[$Hi $Hk Hls Hrs Hj Hl]").
......@@ -138,4 +153,4 @@ Section InPlaceReversal.
* iPureIntro. simplify_eq. by rewrite cons_middle assoc -reverse_cons.
Qed.
End InPlaceReversal.
\ No newline at end of file
End InPlaceReversal.
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