Commit ce820d49 authored by Robbert Krebbers's avatar Robbert Krebbers

Intro pattern for next.

parent 17970986
......@@ -47,12 +47,12 @@ Section client.
wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
- (* The two spawned threads, the waiters. *)
iSplitL; [|iIntros {_ _} "_"; by iNext].
iSplitL; [|by iIntros {_ _} "_ >"].
iDestruct recv_weaken "[] Hr" as "Hr".
{ iIntros "?". by iApply y_inv_split "-". }
{ iIntros "Hy". by iApply y_inv_split "Hy". }
iPvs recv_split "Hr" as "[H1 H2]"; first done.
iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); eauto.
iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|iIntros {_ _} "_"; by iNext]];
iFrame "Hh"; iSplitL "H1"; [|iSplitL "H2"; [|by iIntros {_ _} "_ >"]];
iApply worker_safe; by iSplit.
Qed.
End client.
......
......@@ -105,7 +105,7 @@ Proof.
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}))
"-" as {γ'} "[#? Hγ']"; eauto.
{ iNext. iFrame "Hl". iExists (const P). rewrite !big_sepS_singleton /=.
iSplit; [|done]. by iNext; iIntros "?". }
iSplit; [|done]. by iIntros "> ?". }
iAssert (barrier_ctx γ' l P)%I as "#?".
{ rewrite /barrier_ctx. by repeat iSplit. }
iPvsAssert (sts_ownS γ' (i_states γ) {[Change γ]}
......@@ -116,7 +116,7 @@ Proof.
auto using sts.closed_op, i_states_closed, low_states_closed;
set_solver. }
iPvsIntro. rewrite /recv /send. iSplitL "Hr".
- iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. iNext; by iIntros "?".
- iExists γ', P, P, γ. iFrame "Hr". repeat iSplit; auto. by iIntros "> ?".
- iExists γ'. by iSplit.
Qed.
......@@ -132,7 +132,7 @@ Proof.
iSplitR "HΦ"; [iNext|by iIntros "?"].
rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
iDestruct "Hr" as {Ψ} "[? Hsp]"; iExists Ψ; iFrame "Hsp".
iNext; iIntros "_"; by iApply "Hr".
iIntros "> _"; by iApply "Hr".
Qed.
Lemma wait_spec l P (Φ : val iProp) :
......@@ -160,7 +160,7 @@ Proof.
{ iNext. iApply (big_sepS_delete _ _ i); first done. by iApply "HΨ". }
iSplitL "HΨ' Hl Hsp"; [iNext|].
+ rewrite {2}/barrier_inv /=; iFrame "Hl".
iExists Ψ; iFrame "Hsp". iNext; by iIntros "_".
iExists Ψ; iFrame "Hsp". by iIntros "> _".
+ iPoseProof (saved_prop_agree i Q (Ψ i)) "#" as "Heq"; first by iSplit.
iIntros "_". wp_op=> ?; simplify_eq/=; wp_if.
iPvsIntro. iApply "HΦ". iApply "HQR". by iRewrite "Heq".
......@@ -191,9 +191,9 @@ Proof.
set_solver. }
iPvsIntro; iSplitL "Hγ1"; rewrite /recv /barrier_ctx.
+ iExists γ, P, R1, i1. iFrame "Hγ1 Hi1". repeat iSplit; auto.
by iNext; iIntros "?".
by iIntros "> ?".
+ iExists γ, P, R2, i2. iFrame "Hγ2 Hi2". repeat iSplit; auto.
by iNext; iIntros "?".
by iIntros "> ?".
Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) (recv l P1 - recv l P2).
......@@ -201,7 +201,7 @@ Proof.
rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
iExists γ, P, Q, i; iFrame "Hctx Hγ Hi".
iNext; iIntros "HQ". by iApply "HP"; iApply "HP1".
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 :
......
......@@ -33,8 +33,7 @@ Proof.
ef = None e' = Loc l σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_head_step (Alloc e) φ σ) // /φ;
last (by intros; inv_head_step; eauto 8); last (by simpl; eauto).
iIntros "[$ HΦ]". iNext.
iIntros {v2 σ2 ef} "[% HP]".
iIntros "[$ HΦ] >"; iIntros {v2 σ2 ef} "[% HP]".
(* FIXME: I should not have to refer to "H0". *)
destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
iSplit; last done. iApply "HΦ"; by iSplit.
......
......@@ -9,7 +9,8 @@ Inductive intro_pat :=
| IPersistent : intro_pat intro_pat
| IList : list (list intro_pat) intro_pat
| ISimpl : intro_pat
| IAlways : intro_pat.
| IAlways : intro_pat
| INext : intro_pat.
Module intro_pat.
Inductive token :=
......@@ -26,7 +27,8 @@ Inductive token :=
| TParenL : token
| TParenR : token
| TSimpl : token
| TAlways : token.
| TAlways : token
| TNext : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end.
......@@ -46,6 +48,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
| String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
| String "!" s => tokenize_go s (TAlways :: cons_name kn k) ""
| String ">" s => tokenize_go s (TNext :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn)
end.
......@@ -112,6 +115,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
| TParenR :: ts => close_conj_list k None [] = parse_go ts
| TSimpl :: ts => parse_go ts (SPat ISimpl :: k)
| TAlways :: ts => parse_go ts (SPat IAlways :: k)
| TNext :: ts => parse_go ts (SPat INext :: k)
end.
Definition parse (s : string) : option (list intro_pat) :=
match k parse_go (tokenize s) [SList]; close_list k [] [] with
......
......@@ -683,6 +683,13 @@ Tactic Notation "iAlways":=
apply tac_always_intro;
[reflexivity || fail "iAlways: spatial context non-empty"|].
(** * Later *)
Tactic Notation "iNext":=
eapply tac_next;
[apply _
|let P := match goal with |- upred_tactics.StripLaterL ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].
(** * Introduction tactic *)
Tactic Notation "iIntros" constr(pat) :=
let rec go pats :=
......@@ -690,6 +697,7 @@ Tactic Notation "iIntros" constr(pat) :=
| [] => idtac
| ISimpl :: ?pats => simpl; go pats
| IAlways :: ?pats => iAlways; go pats
| INext :: ?pats => iNext; go pats
| IPersistent (IName ?H) :: ?pats => iIntro #H; go pats
| IName ?H :: ?pats => iIntro H; go pats
| IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
......@@ -759,13 +767,6 @@ Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
"}" constr(p) :=
iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }; iIntros p.
(** * Later *)
Tactic Notation "iNext":=
eapply tac_next;
[apply _
|let P := match goal with |- upred_tactics.StripLaterL ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
Ltac iLöbCore IH tac_before tac_after :=
......
......@@ -75,7 +75,7 @@ Proof.
iSplit; [done|]; iSplitL "H1"; [|iSplitL "H2"].
+ by iApply worker_spec; iSplitL "H1".
+ by iApply worker_spec; iSplitL "H2".
+ iIntros {v1 v2} "?". by iNext.
+ by iIntros {v1 v2} "? >".
- iIntros {_ v} "[_ H]"; iPoseProof Q_res_join "H". by iNext; iExists γ.
Qed.
End 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