Commit c4682b81 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove broken file.

parent bfa32cfe
......@@ -24,4 +24,3 @@ theories/tests/fact.v
# theories/tests/lists.v
(** TODO: this file should be updated to not break the C-language abstraction *)
From iris_c.vcgen Require Import proofmode.
Definition a_list_nil : val := λ:<>, c_ret NONEV.
Definition a_list_data : val := λ: "x",
c_bind (λ: "s",
match: "s" with
NONE => assert: #false
| SOME "l" => (c_bind (λ: "p", c_ret (Fst "p")) (c_load (c_ret "l")))
end) "x".
Definition a_list_next : val := λ: "x",
c_bind (λ: "s",
match: "s" with
NONE => assert: #false
| SOME "l" => (c_bind (λ: "p", c_ret (Snd "p")) (c_load (c_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",
c_bind (λ: "xs",
match: "xs" with
NONE => assert: #false
| SOME "l" =>
c_bind (λ:"p",
c_bind ( λ: "r",
c_store (c_ret "l") (c_ret (Fst "p", "r")))
(c_load "y"))
(c_load (c_ret "l"))
end) "x".
Definition a_list_store_next : val := λ: "x1" "x2",
c_bind (λ: "p",
match: Fst "p" with
NONE => assert: #false
| SOME "l" => c_bind (λ:"m", c_store (c_ret "l") (c_ret (Fst "m", Snd "p")))
(c_load (c_ret "l"))
(c_par "x1" "x2").
Definition in_place_reverse : val := λ: "hd",
c_bind (λ: "i", a_bind (λ: "j",
(λ:<>, a_un_op NegOp (c_bin_op EqOp (c_load (c_ret "i")) (c_ret NONEV)))
(λ:<>, c_bind (λ: "k",
a_list_store_next (c_load (c_ret "i")) (a_load (c_ret "j")) ;
c_store (c_ret "j") (c_load (c_ret "i")) ;
c_store (c_ret "i") (c_load (c_ret "k")))
(a_alloc 1 (a_list_next (c_load (c_ret "i"))))) ;
(c_load (c_ret "j"))
) (a_alloc 1 (c_ret NONEV))) (a_alloc 1 (c_ret "hd")).
Section list_spec.
Context `{cmonadG Σ}.
Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
match xs with
| [] => hd = NONEV
| x :: xs => (l:cloc) hd', hd = SOMEV (cloc_to_val l) l C (x,hd') is_list hd' xs
Lemma a_list_nil_spec R Φ:
Φ NONEV - cwp (a_list_nil #()) R Φ.
Proof. iIntros "H"; cwp_lam; by cwp_ret_value. Qed.
Lemma a_list_next_spec (e: expr) R Φ :
cwp e R (λ v,
(l:cloc) hd x xs, v = SOMEV (cloc_to_val l) l C (x, hd) is_list hd xs
(l C (x, hd) - is_list hd xs - Φ hd)) -
cwp (a_list_next e) R Φ.
iIntros "H". rewrite/ a_list_next.
cwp_apply (cwp_cwp R with "H").
- iIntros (v) "H". cwp_lam. iApply cwp_bind. iApply (cwp_wand with "H").
iIntros (v0) "H". iDestruct "H" as (i hd x xs) "[-> [Hi [Hlst HΦ]]]".
cwp_let. cwp_match. iApply cwp_bind.
cwp_load_ret i. iIntros "Hi". iSpecialize ("HΦ" with "Hi Hlst").
cwp_let. iApply cwp_ret. wp_proj. iFrame.
End list_spec.
Section in_place_reversal.
Context `{cmonadG Σ}.
Lemma a_list_store_next_spec e1 e2 Ψ1 Ψ2 R Φ :
cwp e1 R (λ v, (hd:cloc) x old,
v = SOMEV (cloc_to_val hd) hd C (x, old) Ψ1 (x, SOMEV (cloc_to_val hd))) -
cwp e2 R Ψ2 -
( (hd : cloc) x new, Ψ1 (x, SOMEV (cloc_to_val hd)) - Ψ2 new -
(hd C[LLvl] (x, new) - Φ (x, new)%V)) -
cwp (a_list_store_next e1 e2) R Φ.
iIntros "H1 H2 HΦ".
cwp_apply (cwp_cwp with "H1"); iIntros (v1) "H1"; cwp_lam.
cwp_apply (cwp_cwp with "H2"); iIntros (v2) "H2"; cwp_lam.
iApply cwp_bind. iApply (cwp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>".
iDestruct "H1" as (hd x nxt ->) "(Hhd & HΨ1)".
do 4 cwp_pure _. iApply cwp_bind. cwp_load_ret hd. iIntros "Hd".
cwp_let. iApply c_store_ret. do 2 cwp_proj; cwp_ret_value.
iExists (x, nxt)%V. iFrame. iIntros "Hd".
iSpecialize ("HΦ" $! hd x with "HΨ1 H2"). by iApply "HΦ".
Lemma in_place_reverse_spec (hd:val) xs R:
is_list hd xs -
cwp (in_place_reverse hd) R (λ v, is_list v (reverse xs)).
iIntros "Hlst". cwp_lam.
iApply cwp_bind; cwp_alloc_ret i "[Hi _]".
iApply cwp_bind; cwp_alloc_ret j "[Hj _]".
compute[cloc_add]. rewrite !Nat.add_0_r.
assert ((i.1, i.2) = i) as -> by (destruct i; auto).
assert ((j.1, j.2) = j) as -> by (destruct j; auto).
iApply a_sequence_spec'. iNext.
iApply (a_while_inv_spec ( ls rs rhd hd, i C hd is_list hd ls
j C rhd is_list rhd rs (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
- 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 (c_bin_op_spec _ _
(λ x, x = hd i C hd)%I (λ x, x = NONEV)%I with "[Hi] [] [-]").
{ cwp_load_ret i. } { cwp_ret_value. }
iNext. 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. cwp_load_ret j.
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 cwp_bind.
iNext. iApply (a_alloc_spec _ _ (λ v, v = #1) with "[] [-]")%I.
{ iApply cwp_ret. by wp_value_head. }
iApply a_list_next_spec.
cwp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
iSplit; first done. iFrame. iIntros "Hl Hls".
iNext. iIntros (? ->). iExists 1%nat; iSplit; eauto.
iIntros (k) "[Hk _]". cwp_let. iApply a_sequence_spec'; iNext.
compute[cloc_add]. rewrite !Nat.add_0_r.
assert ((k.1, k.2) = k) as -> by (destruct k; auto).
iApply (a_list_store_next_spec _ _
(λ z, z = (v, SOMEV (cloc_to_val l)) i C (SOMEV (cloc_to_val l)) )%I
(λ v, v = rhd j C rhd)%I with "[Hi Hl] [Hj]").
{ cwp_load_ret i. eauto 42 with iFrame. }
{ cwp_load_ret j. }
iIntros (a0 ? ?) "(% & Hi) (% & Hj)". simplify_eq/=.
(* TODO: this is annoying *)
assert (a0 = l) as ->. { by destruct l,a0; simplify_eq/=. }
iIntros "Hl". iModIntro. iApply a_sequence_spec'; iNext.
iApply (a_move_spec with "[$Hj $Hi Hls Hrs Hk Hl]").
iIntros "Hi Hj". iModIntro.
iApply (a_move_spec with "[$Hi $Hk Hls Hrs Hj Hl]").
iIntros "Hk Hi". iModIntro. iExists ls, (v :: rs), (InjRV (cloc_to_val l)), lnxt.
iFrame. iSplit.
* iExists l, rhd; iSplit; first done; iFrame.
* iPureIntro. simplify_eq. by rewrite cons_middle assoc -reverse_cons.
End in_place_reversal.
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