Commit c056a95c authored by Ralf Jung's avatar Ralf Jung

more types, less inference

parent ca3c807e
......@@ -12,6 +12,7 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
Notation irisG Λ Σ := (irisG' (state Λ) Σ).
Inductive stuckness := not_stuck | maybe_stuck.
Definition stuckness_le (s1 s2 : stuckness) : bool :=
match s1, s2 with
| maybe_stuck, not_stuck => false
......@@ -22,6 +23,9 @@ Proof.
split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
if s is maybe_stuck then strongly_atomic else weakly_atomic.
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
......@@ -244,9 +248,6 @@ Qed.
Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} WP e @ s; E {{ Φ }}.
Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
Definition stuckness_to_atomicity s :=
if s is maybe_stuck then strongly_atomic else weakly_atomic.
Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
(|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) WP e @ s; E1 {{ Φ }}.
Proof.
......
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