From 97bd63aa38901c0f90d9f789bbc23d55e59d6061 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Mar 2017 23:38:59 +0100
Subject: [PATCH] More sane/consistent syntax for modal specialization
 patterns.

---
 ProofMode.md                           | 6 ++----
 theories/base_logic/lib/boxes.v        | 2 +-
 theories/heap_lang/lib/barrier/proof.v | 8 ++++----
 theories/program_logic/weakestpre.v    | 2 +-
 theories/proofmode/spec_patterns.v     | 5 ++---
 theories/tests/proofmode.v             | 4 ++--
 6 files changed, 12 insertions(+), 15 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index a1507dfba..79eca351a 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -242,12 +242,10 @@ _specification patterns_ to express splitting of hypotheses:
   consumed. Hypotheses may be prefixed with a `$`, which results in them being
   framed in the generated goal for the premise.
 - `[-H1 ... Hn]` : negated form of the above pattern.
-- `>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
+- `[> H1 ... Hn]` : same as the above pattern, but can only be used if the goal
   is a modality, in which case the modality will be kept in the generated goal
   for the premise will be wrapped into the modality.
-- `>[-H1 ... Hn]`  : negated form of the above pattern.
-- `>` : shorthand for `>[-]` (typically used for the last premise of an applied
-  lemma).
+- `[> -H1 ... Hn]`  : negated form of the above pattern.
 - `[#]` : This pattern can be used when eliminating `P -∗ Q` with `P` being
   persistent. Using this pattern, all hypotheses are available in the goal for
   `P`, as well the remaining goal. The pattern can optionally contain 
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 0722ee823..413fbdd5d 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -225,7 +225,7 @@ Lemma box_empty E f P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iAssert ([∗ map] γ↦b ∈ f, ▷ Φ γ ∗ box_own_auth γ (◯ Excl' false) ∗
-    box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with ">[Hf]" as "[HΦ ?]".
+    box_own_prop γ (Φ γ) ∗ inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { iApply (fupd_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
     assert (true = b) as <- by eauto.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 2bdce5c36..d06424595 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -93,7 +93,7 @@ Lemma newbarrier_spec (P : iProp Σ) :
 Proof.
   iIntros (Φ) "HΦ".
   rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
-  iApply ("HΦ" with ">[-]").
+  iApply ("HΦ" with "[> -]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
     as (γ') "[#? Hγ']"; eauto.
@@ -102,7 +102,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { done. }
   iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ∗ sts_ownS γ' low_states {[Send]})%I with ">[-]" as "[Hr Hs]".
+    ∗ sts_ownS γ' low_states {[Send]})%I with "[> -]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - set_solver.
     - iApply (sts_own_weaken with "Hγ'");
@@ -140,7 +140,7 @@ Proof.
   wp_load. destruct p.
   - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
     { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
-    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with ">[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     iModIntro. wp_if.
     iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
@@ -175,7 +175,7 @@ Proof.
     rewrite /barrier_inv /=. iNext. iFrame "Hl".
     by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
   iAssert (sts_ownS γ (i_states i1) {[Change i1]}
-    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with ">[-]" as "[Hγ1 Hγ2]".
+    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with "[> -]" as "[Hγ1 Hγ2]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     - abstract set_solver.
     - iApply (sts_own_weaken with "Hγ");
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 03b61878d..007063e76 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -129,7 +129,7 @@ Lemma wp_strong_mono E1 E2 e Φ Ψ :
 Proof.
   iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
-  { iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
+  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 92c215d55..691ba64d5 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -41,14 +41,13 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
      parse_go ts (SAutoFrame GPersistent :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GSpatial :: k)
-  | TModal :: TBracketL :: TFrame :: TBracketR :: ts =>
+  | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GModal :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
   | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
   | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
+  | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
   | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
-  | TModal :: TBracketL :: ts => parse_goal ts GModal false [] [] k
-  | TModal :: ts => parse_go ts (SGoal (SpecGoal GModal true [] [] false) :: k)
   | TForall :: ts => parse_go ts (SForall :: k)
   | _ => None
   end
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 13a85e4c5..c3a00b51c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -96,7 +96,7 @@ Section iris.
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
   Proof.
     iIntros (?) "H HP HQ".
-    iApply ("H" with "[% //] HP >[HQ] >[//]").
+    iApply ("H" with "[% //] [$] [> HQ] [> //]").
     by iApply inv_alloc.
   Qed.
 End iris.
@@ -124,7 +124,7 @@ Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
 
 Lemma demo_13 (M : ucmraT) (P : uPred M) : (|==> False) -∗ |==> P.
-Proof. iIntros. iAssert False%I with ">[-]" as "[]". done. Qed.
+Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
 
 Lemma demo_14 (M : ucmraT) (P : uPred M) : False -∗ P.
 Proof. iIntros "H". done. Qed.
-- 
GitLab