Merge branch 'fix-iEval-precedence' into 'master'

Fix parsing precedence for iEval

See merge request iris/iris!269

tests/proofmode.ref

@@ -126,7 +126,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iSimpl in (constr)",
-"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
+"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
 last call failed.
 Tactic failure: iEval: %: unsupported selection pattern.
 "test_iFrame_later_1"
@@ -443,8 +443,8 @@ Tactic failure: iModIntro: spatial context is non-empty.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic)" and
-"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
+"iDestructCore (open_constr) as (constr) (tactic3)" and
+"iDestructCore (open_constr) as (constr) (tactic3)", last call failed.
 Tactic failure: iDestruct: "HQ" not found.
 "iIntros_dup_name"
      : string
@@ -553,14 +553,14 @@ Tactic failure: iStartProof: not a BI assertion.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)" and
 "<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
 Tactic failure: iPoseProof: not a BI assertion.
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)", 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to fun H => iDestructHyp H as pat),
@@ -573,15 +573,15 @@ Tactic failure: iRename: "H" not fresh.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)" and
 "iPoseProofCoreHyp (constr) as (constr)", last call failed.
 Tactic failure: iPoseProof: "Hx" not found.
 "iPoseProof_not_found_fail2"
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
-"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)",
+"iPoseProofCoreLem (constr) as (constr) before_tc (tactic3)", 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
 "spec_tac" (bound to
@@ -616,9 +616,9 @@ Tactic failure: iElaborateSelPat: "H" not found.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)", 
+"iDestructCore (open_constr) as (constr) (tactic3)",
+"iDestructCore (open_constr) as (constr) (tactic3)",
+"iDestructCore (open_constr) as (constr) (tactic3)", 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
@@ -627,9 +627,9 @@ Tactic failure: iDestruct: "{HP}"
 should contain exactly one proper introduction pattern.
 The command has indeed failed with message:
 In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)",
-"iDestructCore (open_constr) as (constr) (tactic)", 
+"iDestructCore (open_constr) as (constr) (tactic3)",
+"iDestructCore (open_constr) as (constr) (tactic3)",
+"iDestructCore (open_constr) as (constr) (tactic3)", 
 "tac" (bound to fun H => iDestructHyp H as pat),
 "iDestructHyp (constr) as (constr)",
 "<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
@@ -648,7 +648,7 @@ Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: cannot apply P.
@@ -656,7 +656,7 @@ Tactic failure: iApply: cannot apply P.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: Q
@@ -665,7 +665,7 @@ not absorbing and the remaining hypotheses not affine.
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
+"iPoseProofCore (open_constr) as (constr) (constr) (tactic3)", 
 "tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
 failed.
 Tactic failure: iApply: Q

tests/proofmode.v

@@ -480,6 +480,13 @@ Proof.
   done.
 Qed.
 
+Lemma test_iEval_precedence : True ⊢ True : PROP.
+Proof.
+  iIntros.
+  (* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
+  iEval (rewrite /=); iPureIntro; exact I.
+Qed.
+
 Check "test_iSimpl_in".
 Lemma test_iSimpl_in x y : ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H". iSimpl in "H". Show. done. Qed.

tests/proofmode_iris.ref

@@ -111,20 +111,20 @@
      : string
 The command has indeed failed with message:
 In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+"iInvCore (constr) in (tactic3)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
 failed.
 Tactic failure: iInv: selector 34 is not of the right type .
 The command has indeed failed with message:
 In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+"iInvCore (constr) in (tactic3)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
 failed.
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
+"iInvCore (constr) in (tactic3)" and
+"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
 failed.
 Tactic failure: iInv: invariant "H2" not found.
 "test_iInv"

theories/proofmode/ltac_tactics.v

@@ -195,7 +195,7 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
   iClear Hs; clear xs.
 
 (** ** Simplification *)
-Tactic Notation "iEval" tactic(t) :=
+Tactic Notation "iEval" tactic3(t) :=
   iStartProof;
   eapply tac_eval;
     [let x := fresh in intros x; t; unfold x; reflexivity
@@ -212,7 +212,7 @@ Local Ltac iEval_go t Hs :=
       |pm_reduce; iEval_go t Hs]
   end.
 
-Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
+Tactic Notation "iEval" tactic3(t) "in" constr(Hs) :=
   iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
 
 Tactic Notation "iSimpl" := iEval (simpl).
@@ -726,7 +726,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
     end.
 
 Tactic Notation "iPoseProofCoreLem"
-    constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
+    constr(lem) "as" constr(Hnew) "before_tc" tactic3(tac) :=
   eapply tac_pose_proof with Hnew _; (* (j:=H) *)
     [iIntoEmpValid lem
     |pm_reduce;
@@ -1015,7 +1015,7 @@ Both variants of [lazy_tc] are used in other tactics that build on top of
   because it may be not possible to eliminate logical connectives before all
   type class constraints have been resolved. *)
 Tactic Notation "iPoseProofCore" open_constr(lem)
-    "as" constr(p) constr(lazy_tc) tactic(tac) :=
+    "as" constr(p) constr(lazy_tc) tactic3(tac) :=
   iStartProof;
   let Htmp := iFresh in
   let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
@@ -1032,7 +1032,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
      | true =>
         iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
      | false =>
-        iPoseProofCoreLem t as Htmp before_tc (spec_tac ()); [..|tac Htmp]
+        iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
      end
   end.
 
@@ -1634,7 +1634,7 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
 
 
 (* Used for generalization in iInduction and iLöb *)
-Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
+Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
   let rec go Hs :=
     lazymatch Hs with
     | [] => tac
@@ -1643,56 +1643,56 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
     end in
   try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
 
-Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic(tac):=
+Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ")" constr(Hs)
-    "with" tactic(tac):=
+    "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2); tac; iIntros (x1 x2)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ")" constr(Hs)
-    "with" tactic(tac):=
+    "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3); tac; iIntros (x1 x2 x3)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
-    constr(Hs) "with" tactic(tac):=
+    constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4); tac; iIntros (x1 x2 x3 x4)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ")" constr(Hs) "with" tactic(tac):=
+    ident(x5) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5); tac; iIntros (x1 x2 x3 x4 x5)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ")" constr(Hs) "with" tactic(tac):=
+    ident(x5) ident(x6) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6);
     tac; iIntros (x1 x2 x3 x4 x5 x6)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ")" constr(Hs) "with" tactic(tac):=
+    ident(x5) ident(x6) ident(x7) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7);
     tac; iIntros (x1 x2 x3 x4 x5 x6 x7)).
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) "with" tactic(tac):=
+    ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) "with" tactic3(tac):=
   iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8);
     tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8)).
 
-Tactic Notation "iRevertIntros" "with" tactic(tac) :=
+Tactic Notation "iRevertIntros" "with" tactic3(tac) :=
   iRevertIntros "" with tac.
-Tactic Notation "iRevertIntros" "(" ident(x1) ")" "with" tactic(tac):=
+Tactic Notation "iRevertIntros" "(" ident(x1) ")" "with" tactic3(tac):=
   iRevertIntros (x1) "" with tac.
-Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ")" "with" tactic(tac):=
+Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ")"
-    "with" tactic(tac):=
+    "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")"
-    "with" tactic(tac):=
+    "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ")" "with" tactic(tac):=
+    ident(x5) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ")" "with" tactic(tac):=
+    ident(x5) ident(x6) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5 x6) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ")" "with" tactic(tac):=
+    ident(x5) ident(x6) ident(x7) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7) "" with tac.
 Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
-    ident(x5) ident(x6) ident(x7) ident(x8) ")" "with" tactic(tac):=
+    ident(x5) ident(x6) ident(x7) ident(x8) ")" "with" tactic3(tac):=
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8) "" with tac.
 
 (** * Destruct tactic *)
@@ -1710,7 +1710,7 @@ Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
 Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
   CopyDestruct P → CopyDestruct (<pers> P) := {}.
 
-Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
   let ident :=
     lazymatch type of lem with
     | ident => constr:(Some lem)
@@ -1869,7 +1869,7 @@ result in the following actions:
 - Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 - Introduce the proofmode hypotheses [Hs]
 *)
-Tactic Notation "iInductionCore" tactic(tac) "as" constr(IH) :=
+Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
   let rec fix_ihs rev_tac :=
     lazymatch goal with
     | H : context [envs_entails _ _] |- _ =>
@@ -1901,7 +1901,7 @@ Ltac iHypsContaining x :=
   let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs _) _ => Γs end in
   let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
-Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
+Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic3(tac) :=
   iRevertIntros Hs with (
     iRevertIntros "∗" with (
       idtac;
@@ -2083,7 +2083,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      | _ => idtac
      end].
 
-Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=
+Tactic Notation "iLöbRevert" constr(Hs) "with" tactic3(tac) :=
   iRevertIntros Hs with (
     iRevertIntros "∗" with tac
   ).
@@ -2144,7 +2144,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
 Boolean or an introduction pattern, which will be coerced into [true] if it
 only contains `#` or `%` patterns at the top-level, and [false] otherwise. *)
 Tactic Notation "iAssertCore" open_constr(Q)
-    "with" constr(Hs) "as" constr(p) tactic(tac) :=
+    "with" constr(Hs) "as" constr(p) tactic3(tac) :=
   iStartProof;
   let pats := spec_pat.parse Hs in
   lazymatch pats with
@@ -2156,7 +2156,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
   [pm_reduce;
    iSpecializeCore H with hnil pats as p; [..|tac H]].
 
-Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
+Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic3(tac) :=
   let p := intro_pat_intuitionistic p in
   lazymatch p with
   | true => iAssertCore Q with "[#]" as p tac
@@ -2314,7 +2314,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
 
 (* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
 invariant. *)
-Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(Hclose) "in" tactic(tac) :=
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(Hclose) "in" tactic3(tac) :=
   iStartProof;
   let pats := spec_pat.parse pats in
   lazymatch pats with
@@ -2361,13 +2361,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
     )].
 
 (* Without closing view shift *)
-Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic(tac) :=
+Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic3(tac) :=
   iInvCore N with pats as (@None string) in ltac:(tac).
 (* Without pattern *)
-Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic(tac) :=
+Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic3(tac) :=
   iInvCore N with "[$]" as Hclose in ltac:(tac).
 (* Without both *)
-Tactic Notation "iInvCore" constr(N) "in" tactic(tac) :=
+Tactic Notation "iInvCore" constr(N) "in" tactic3(tac) :=
   iInvCore N with "[$]" as (@None string) in ltac:(tac).
 
 (* With everything *)