Commit 2cc2993e authored by Dan Frumin's avatar Dan Frumin
Browse files

Clean up spacing a bit

parent 51a28faa
......@@ -16,7 +16,6 @@ Definition gcd : val := λ: "a" "b",
((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
;;;; a_load (a_ret "a").
Section gcd_spec.
Context `{amonadG Σ}.
......
......@@ -20,7 +20,7 @@ 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 *)
(* 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
......@@ -82,13 +82,11 @@ Section list_spec.
awp_load_ret i. iIntros "Hi". iSpecialize ("HΦ" with "Hi Hlst").
awp_let. iApply awp_ret. wp_proj. iFrame.
Qed.
End list_spec.
Section InPlaceReversal.
Section in_place_reversal.
Context `{amonadG Σ}.
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)) -
......@@ -152,5 +150,4 @@ Section InPlaceReversal.
* iExists l, rhd; iSplit; first done; iFrame.
* iPureIntro. simplify_eq. by rewrite cons_middle assoc -reverse_cons.
Qed.
End InPlaceReversal.
End in_place_reversal.
......@@ -19,7 +19,6 @@ Section test.
awp_load_ret l.
Qed.
Lemma test2 (l r : loc) R :
l U #3 - r L #0 -
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => v = #1).
......@@ -35,7 +34,6 @@ Section test.
awp_load_ret l.
Qed.
Definition swap : val := λ: "l1" "l2",
a_bind (λ: "r",
(a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
......@@ -63,5 +61,4 @@ Section test.
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
End test.
......@@ -26,5 +26,4 @@ Section test.
- iIntros (? ? ->) "[% Hx]"; simplify_eq/=.
iExists _; iFrame. eauto.
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