Commit 4084c886 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Generalize clear/frame patterns in introduction patterns.

Now they can also be used to clear/frame the whole pure/persistent/spatial
context.
parent facc4127
Pipeline #4195 passed with stage
in 2 minutes and 35 seconds
...@@ -198,9 +198,9 @@ _introduction patterns_: ...@@ -198,9 +198,9 @@ _introduction patterns_:
Apart from this, there are the following introduction patterns that can only Apart from this, there are the following introduction patterns that can only
appear at the top level: appear at the top level:
- `{H1 ... Hn}` : clear `H1 ... Hn`. - `{selpat}` : clear the hypotheses given by the selection pattern `selpat`.
- `{$H1 ... $Hn}` : frame `H1 ... Hn` (this pattern can be mixed with the Items of the selection pattern can be prefixed with `$`, which cause them to
previous pattern, e.g., `{$H1 H2 $H3}`). be framed instead of cleared.
- `!%` : introduce a pure goal (and leave the proof mode). - `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality and clear the spatial context. - `!#` : introduce an always modality and clear the spatial context.
- `!>` : introduce a modality. - `!>` : introduce a modality.
......
From stdpp Require Export strings. From stdpp Require Export strings.
From iris.proofmode Require Import tokens. From iris.proofmode Require Import tokens sel_patterns.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Inductive intro_pat := Inductive intro_pat :=
...@@ -18,8 +18,8 @@ Inductive intro_pat := ...@@ -18,8 +18,8 @@ Inductive intro_pat :=
| IDone : intro_pat | IDone : intro_pat
| IForall : intro_pat | IForall : intro_pat
| IAll : intro_pat | IAll : intro_pat
| IClear : string intro_pat | IClear : sel_pat intro_pat
| IClearFrame : string intro_pat. | IClearFrame : sel_pat intro_pat.
Module intro_pat. Module intro_pat.
Inductive stack_item := Inductive stack_item :=
...@@ -96,8 +96,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack := ...@@ -96,8 +96,14 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
end end
with parse_clear (ts : list token) (k : stack) : option stack := with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with match ts with
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame s) :: k) | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear 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 | TBraceR :: ts => parse_go ts k
| _ => None | _ => None
end. end.
......
...@@ -30,6 +30,7 @@ Definition parse (s : string) : option (list sel_pat) := ...@@ -30,6 +30,7 @@ Definition parse (s : string) : option (list sel_pat) :=
Ltac parse s := Ltac parse s :=
lazymatch type of s with lazymatch type of s with
| sel_pat => constr:([s])
| list sel_pat => s | list sel_pat => s
| list string => eval vm_compute in (SelName <$> s) | list string => eval vm_compute in (SelName <$> s)
| string => | string =>
......
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