Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

proofmode/intro_patterns.v

@@ -13,7 +13,7 @@ Inductive intro_pat :=
   | INext : intro_pat
   | IForall : intro_pat
   | IAll : intro_pat
-  | IClear : list string → intro_pat.
+  | IClear : list (bool * string) → intro_pat. (* true = frame, false = clear *)
 
 Module intro_pat.
 Inductive token :=
@@ -71,8 +71,7 @@ Inductive stack_item :=
   | SList : stack_item
   | SConjList : stack_item
   | SBar : stack_item
-  | SAmp : stack_item
-  | SClear : stack_item.
+  | SAmp : stack_item.
 Notation stack := (list stack_item).
 
 Fixpoint close_list (k : stack)
@@ -108,13 +107,6 @@ Fixpoint close_conj_list (k : stack)
   | _ => None
   end.
 
-Fixpoint close_clear (k : stack) (ss : list string) : option stack :=
-  match k with
-  | SPat (IName s) :: k => close_clear k (s :: ss)
-  | SClear :: k => Some (SPat (IClear (reverse ss)) :: k)
-  | _ => None
-  end.
-
 Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
@@ -135,9 +127,18 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TNext :: ts => parse_go ts (SPat INext :: k)
   | TAll :: ts => parse_go ts (SPat IAll :: k)
   | TForall :: ts => parse_go ts (SPat IForall :: k)
-  | TClearL :: ts => parse_go ts (SClear :: k)
-  | TClearR :: ts => close_clear k [] ≫= parse_go ts
+  | TClearL :: ts => parse_clear ts [] k
+  | _ => None
+  end
+with parse_clear (ts : list token)
+    (ss : list (bool * string)) (k : stack) : option stack :=
+  match ts with
+  | TFrame :: TName s :: ts => parse_clear ts ((true,s) :: ss) k
+  | TName s :: ts => parse_clear ts ((false,s) :: ss) k
+  | TClearR :: ts => parse_go ts (SPat (IClear (reverse ss)) :: k)
+  | _ => None
   end.
+
 Definition parse (s : string) : option (list intro_pat) :=
   match k ← parse_go (tokenize s) [SList]; close_list k [] [] with
   | Some [SPat (IList [ps])] => Some ps

proofmode/spec_patterns.v

@@ -42,32 +42,29 @@ Inductive state :=
   | StTop : state
   | StAssert : spec_goal_kind → bool → list string → state.
 
-Fixpoint parse_go (ts : list token) (s : state)
-    (k : list spec_pat) : option (list spec_pat) :=
-  match s with
-  | StTop =>
-     match ts with
-     | [] => Some (rev k)
-     | TName s :: ts => parse_go ts StTop (SName false s :: k)
-     | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts StTop (SGoalPersistent :: k)
-     | TBracketL :: TPure :: TBracketR :: ts => parse_go ts StTop (SGoalPure :: k)
-     | TBracketL :: ts => parse_go ts (StAssert GoalStd false []) k
-     | TPvs :: TBracketL :: ts => parse_go ts (StAssert GoalPvs false []) k
-     | TPvs :: ts => parse_go ts StTop (SGoal GoalPvs true [] :: k)
-     | TPersistent :: TName s :: ts => parse_go ts StTop (SName true s :: k)
-     | TForall :: ts => parse_go ts StTop (SForall :: k)
-     | _ => None
-     end
-  | StAssert kind neg ss =>
-     match ts with
-     | TMinus :: ts => guard (¬neg ∧ ss = []); parse_go ts (StAssert kind true ss) k
-     | TName s :: ts => parse_go ts (StAssert kind neg (s :: ss)) k
-     | TBracketR :: ts => parse_go ts StTop (SGoal kind neg (rev ss) :: k)
-     | _ => None
-     end
+Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
+  match ts with
+  | [] => Some (rev k)
+  | TName s :: ts => parse_go ts (SName false s :: k)
+  | TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
+  | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
+  | TBracketL :: ts => parse_goal ts GoalStd false [] k
+  | TPvs :: TBracketL :: ts => parse_goal ts GoalPvs false [] k
+  | TPvs :: ts => parse_go ts (SGoal GoalPvs true [] :: k)
+  | TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
+  | TForall :: ts => parse_go ts (SForall :: k)
+  | _ => None
+  end
+with parse_goal (ts : list token) (kind : spec_goal_kind)
+    (neg : bool) (ss : list string) (k : list spec_pat) : option (list spec_pat) :=
+  match ts with
+  | TMinus :: ts => guard (¬neg ∧ ss = []); parse_goal ts kind true ss k
+  | TName s :: ts => parse_goal ts kind neg (s :: ss) k
+  | TBracketR :: ts => parse_go ts (SGoal kind neg (reverse ss) :: k)
+  | _ => None
   end.
 Definition parse (s : string) : option (list spec_pat) :=
-  parse_go (tokenize s) StTop [].
+  parse_go (tokenize s) [].
 
 Ltac parse s :=
   lazymatch type of s with

proofmode/tactics.v

@@ -560,7 +560,13 @@ Tactic Notation "iIntros" constr(pat) :=
     | ISimpl :: ?pats => simpl; go pats
     | IAlways :: ?pats => iAlways; go pats
     | INext :: ?pats => iNext; go pats
-    | IClear ?Hs :: ?pats => iClear Hs; go pats
+    | IClear ?cpats :: ?pats =>
+       let rec clr cpats :=
+         match cpats with
+         | [] => go pats
+         | (false,?H) :: ?cpats => iClear H; clr cpats
+         | (true,?H) :: ?cpats => iFrame H; clr cpats
+         end in clr cpats
     | 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

tests/proofmode.v

@@ -28,7 +28,7 @@ Proof.
   iRevert {a b} "Ha Hb". iIntros {b a} "Hb {foo} Ha".
   iAssert (uPred_ownM (a ⋅ core a)) with "[Ha]" as "[Ha #Hac]".
   { by rewrite cmra_core_r. }
-  iFrame "Ha Hac".
+  iIntros "{$Hac $Ha}".
   iExists (S j + z1), z2.
   iNext.
   iApply ("H3" $! _ 0 with "H1 []").