From 4084c886324414900173f51a750da7333f50bac0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 27 Apr 2017 15:33:29 +0200
Subject: [PATCH] Generalize clear/frame patterns in introduction patterns.

Now they can also be used to clear/frame the whole pure/persistent/spatial
context.
---
 ProofMode.md                        |  6 +++---
 theories/proofmode/intro_patterns.v | 16 +++++++++++-----
 theories/proofmode/sel_patterns.v   |  1 +
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index dbbe030f4..d178f52f0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -198,9 +198,9 @@ _introduction patterns_:
 Apart from this, there are the following introduction patterns that can only
 appear at the top level:
 
-- `{H1 ... Hn}` : clear `H1 ... Hn`.
-- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the
-  previous pattern, e.g., `{$H1 H2 $H3}`).
+- `{selpat}` : clear the hypotheses given by the selection pattern `selpat`.
+  Items of the selection pattern can be prefixed with `$`, which cause them to
+  be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
 - `!#` : introduce an always modality and clear the spatial context.
 - `!>` : introduce a modality.
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 39a28f98b..7d1c308a4 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-From iris.proofmode Require Import tokens.
+From iris.proofmode Require Import tokens sel_patterns.
 Set Default Proof Using "Type".
 
 Inductive intro_pat :=
@@ -18,8 +18,8 @@ Inductive intro_pat :=
   | IDone : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
-  | IClear : string → intro_pat
-  | IClearFrame : string → intro_pat.
+  | IClear : sel_pat → intro_pat
+  | IClearFrame : sel_pat → intro_pat.
 
 Module intro_pat.
 Inductive stack_item :=
@@ -96,8 +96,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
-  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k)
-  | TName s :: ts => parse_clear ts (SPat (IClear s) :: k)
+  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
+  | TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
+  | TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
+  | TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
+  | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
+  | TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
+  | TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
+  | TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
   | TBraceR :: ts => parse_go ts k
   | _ => None
   end.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 01581650c..5578d17e2 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -30,6 +30,7 @@ Definition parse (s : string) : option (list sel_pat) :=
 
 Ltac parse s :=
   lazymatch type of s with
+  | sel_pat => constr:([s])
   | list sel_pat => s
   | list string => eval vm_compute in (SelName <$> s)
   | string =>
-- 
GitLab