Commit 328c1d73 authored by Léon Gondelman's avatar Léon Gondelman

fix 1 in-place list reversal

parent 44cb36aa
......@@ -58,14 +58,11 @@ Section Derived.
iApply ("HΦ" with "[$Hl] [$Hr]").
Qed.
Definition a_move: val := λ: "x" "y",
a_store (a_ret "x") (a_load (a_ret "y")).
Lemma a_move_spec (s t :loc) (v w: val) R Φ :
s U v t U w ( t U w - s L w - Φ w) -
awp (a_move #s #t) R Φ.
awp (a_store (a_ret #s) (a_load (a_ret #t))) R Φ.
Proof.
iIntros "(Hs & Ht & H)". do 2 awp_lam.
iIntros "(Hs & Ht & H)".
iApply a_store_ret. awp_load_ret t. iIntros "Ht".
iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
Qed.
......
......@@ -75,8 +75,8 @@ Section InPlaceReversal.
(λ:<>, 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_move "j" "i" ;;;;
a_move "i" "k")
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")).
......
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