Fix `forall` parsing. using the stdpp change

tests/proofmode_ascii.ref

@@ -148,3 +148,74 @@ Tactic failure: iInv: invariant "H2" not found.
   --------------------------------------∗
   |={E ∖ ↑N,E}=> emp
   
+"p1"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (P : PROP) (_ : True), bi_entails P P
+"p2"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall P : PROP, and True (bi_entails P P)
+"p3"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  ex (fun P : PROP => bi_entails P P)
+"p4"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
+"p5"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
+"p6"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  ex
+    (unique
+       (fun z : nat =>
+        bi_emp_valid
+          (bi_exist
+             (fun _ : nat =>
+              bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
+"p7"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (y : nat),
+  bi_entails (bi_pure True) (bi_pure (ge y O))
+"p8"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
+"p9"
+     : string
+1 subgoal
+  
+  PROP : bi
+  ============================
+  forall (a : nat) (_ : eq a O) (_ : nat),
+  bi_emp_valid (bi_forall (fun z : nat => bi_pure (ge z O)))

tests/proofmode_ascii.v

@@ -4,6 +4,8 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 
 From iris.bi Require Import ascii.
 
+Set Default Proof Using "Type".
+
 Section base_logic_tests.
   Context {M : ucmraT}.
   Implicit Types P Q R : uPred M.
@@ -294,4 +296,62 @@ Lemma test_entails_annot_sections_space_close P :
   (P |--@{PROP} P ) /\ (|--@{PROP} ) P P /\
   (P -|-@{PROP} P ) /\ (-|-@{PROP} ) P P.
 Proof. naive_solver. Qed.
+
+
+Check "p1".
+Lemma p1 : forall P, True -> P |-- P.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p2".
+Lemma p2 : forall P, True /\ (P |-- P).
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p3".
+Lemma p3 : exists P, P |-- P.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p4".
+Lemma p4 : |--@{PROP} exists (x : nat), ⌜x = 0⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p5".
+Lemma p5 : |--@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p6".
+Lemma p6 : exists! (z : nat), |--@{PROP} exists (x : nat), ⌜forall y : nat, y = y⌝ ** ⌜z = 0⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p7".
+Lemma p7 : forall (a : nat), a = 0 -> forall y, True |--@{PROP} ⌜y >= 0⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p8".
+Lemma p8 : forall (a : nat), a = 0 -> forall y, |--@{PROP} ⌜y >= 0⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Check "p9".
+Lemma p9 : forall (a : nat), a = 0 -> forall y : nat, |--@{PROP} forall z : nat, ⌜z >= 0⌝.
+Proof.
+  Unset Printing Notations. Show. Set Printing Notations.
+Abort.
+
+Set Printing Notations.
+
 End parsing_tests.

theories/bi/ascii.v

@@ -6,7 +6,9 @@ From iris.algebra Require Export ofe.
  *)
 Notation "P |-- Q" := (P ⊢ Q)
   (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
-Notation "P '|--@{' PROP } Q" := (P ⊢@{PROP} Q) (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
+Notation "P '|--@{' PROP } Q" := (P ⊢@{PROP} Q)
+  (at level 99, Q at level 200, right associativity, only parsing)
+  : stdpp_scope.
 Notation "(|--)" := (⊢) (only parsing) : stdpp_scope.
 Notation "'(|--@{' PROP } )" := (⊢@{PROP}) (only parsing) : stdpp_scope.
 
@@ -16,11 +18,14 @@ Notation "'|--@{' PROP } Q" := (⊢@{PROP} Q) (at level 20, Q at level 200, only
 Notation "'(|--@{' PROP } Q )" := (⊢@{PROP} Q) (only parsing) : stdpp_scope.
 
 Notation "P -|- Q" := (P ⊣⊢ Q) (at level 95, no associativity, only parsing) : stdpp_scope.
-Notation "P '-|-@{' PROP } Q" := (P ⊣⊢@{PROP} Q) (at level 95, no associativity, only parsing) : stdpp_scope.
+Notation "P '-|-@{' PROP } Q" := (P ⊣⊢@{PROP} Q)
+  (at level 95, no associativity, only parsing) : stdpp_scope.
 Notation "(-|-)" := (⊣⊢) (only parsing) : stdpp_scope.
 Notation "'(-|-@{' PROP } )" := (⊣⊢@{PROP}) (only parsing) : stdpp_scope.
 
-Notation "P -* Q" := (P ⊢ Q)%stdpp (at level 99, Q at level 200, right associativity, only parsing) : stdpp_scope.
+Notation "P -* Q" := (P ⊢ Q)%stdpp
+  (at level 99, Q at level 200, right associativity, only parsing)
+  : stdpp_scope.
 
 (* FIXME: Notation "'⌜' φ '⌝'" := (bi_pure φ%type%stdpp) : bi_scope. *)
 Notation "P /\ Q" := (P ∧ Q)%I (only parsing) : bi_scope.
@@ -28,56 +33,83 @@ Notation "(/\)" := bi_and (only parsing) : bi_scope.
 Notation "P \/ Q" := (P ∨ Q)%I (only parsing) : bi_scope.
 Notation "(\/)" := bi_or (only parsing) : bi_scope.
 Notation "P -> Q" := (P → Q)%I (only parsing) : bi_scope.
-Notation "P ** Q" := (P ∗ Q)%I (at level 80, right associativity, only parsing) : bi_scope.
+Notation "P ** Q" := (P ∗ Q)%I
+  (at level 80, right associativity, only parsing) : bi_scope.
 Notation "(**)" := bi_sep (only parsing) : bi_scope.
 Notation "P -* Q" := (P -∗ Q)%I
   (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
 
 (* ∀ x .. y , P *)
 Notation "'forall' x .. y , P" :=
-  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) (at level 200, x binder, right associativity, only parsing) : bi_scope.
+  (bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..))
+  (at level 200, x binder, right associativity, only parsing) : bi_scope.
 (* ∃ x .. y , P *)
 Notation "'exists' x .. y , P" :=
-  (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) (at level 200, x binder, right associativity, only parsing) : bi_scope.
+  (bi_exist (fun x => .. (bi_exist (fun y => P%I)) ..))
+  (at level 200, x binder, right associativity, only parsing) : bi_scope.
 
-Notation "|> P" := (▷ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "|> P" := (▷ P)%I
+  (at level 20, right associativity, only parsing) : bi_scope.
 Notation "|>? p P" := (▷?p P)%I (at level 20, p at level 9, P at level 20,
    only parsing) : bi_scope.
 Notation "|>^ n P" := (▷^n P)%I (at level 20, n at level 9, P at level 20,
    only parsing) : bi_scope.
 
-Notation "P <-> Q" := (P ↔ Q)%I (at level 95, no associativity, only parsing) : bi_scope.
+Notation "P <-> Q" := (P ↔ Q)%I
+  (at level 95, no associativity, only parsing) : bi_scope.
 
-Notation "P *-* Q" := (P ∗-∗ Q)%I (at level 95, no associativity, only parsing) : bi_scope.
+Notation "P *-* Q" := (P ∗-∗ Q)%I
+  (at level 95, no associativity, only parsing) : bi_scope.
 
-Notation "'<#>' P" := (□ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "'<#>' P" := (□ P)%I
+  (at level 20, right associativity, only parsing) : bi_scope.
 Notation "'<#>?' p P" := (□?p P)%I (at level 20, p at level 9, P at level 20,
    right associativity, only parsing) : bi_scope.
 
-Notation "'<except_0>' P" := (◇ P)%I (at level 20, right associativity, only parsing) : bi_scope.
+Notation "'<except_0>' P" := (◇ P)%I
+  (at level 20, right associativity, only parsing) : bi_scope.
 
 Notation "mP -*? Q" := (mP -∗? Q)%I
   (at level 99, Q at level 200, right associativity, only parsing) : bi_scope.
 
-Notation "P ==* Q" := (P ==∗ Q)%stdpp (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==* Q" := (P ==∗ Q)%I (at level 99, Q at level 200, only parsing) : bi_scope.
+Notation "P ==* Q" := (P ==∗ Q)%stdpp
+  (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==* Q" := (P ==∗ Q)%I
+  (at level 99, Q at level 200, only parsing) : bi_scope.
 
-Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q) (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E1 , E2 }=* Q" := (P ={E1,E2}=∗ Q)
+  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
 
-Notation "P ={ E }=* Q" := (P ={E}=∗ Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E }=* Q" := (P ={E}=∗ Q) (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
+Notation "P ={ E }=* Q" := (P ={E}=∗ Q)%I
+  (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E }=* Q" := (P ={E}=∗ Q)
+  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
 .
 
-Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}▷=> Q)%I (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}▷=∗ Q)%I (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=> Q" := (|={E1,E2}▷=> Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
-
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q) (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)%I (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
-
-Notation "|={ E }|>=> Q" := (|={E}▷=> Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E }|>=* Q" := (P ={E}▷=∗ Q)%I (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=>^ n Q" := (|={E1,E2}▷=>^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing) : bi_scope.
+Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}▷=> Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}▷=∗ Q)%I
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "|={ E1 , E2 }|>=> Q" := (|={E1,E2}▷=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+
+Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)
+  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
+
+Notation "|={ E }|>=> Q" := (|={E}▷=> Q)%I
+  (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "P ={ E }|>=* Q" := (P ={E}▷=∗ Q)%I
+  (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
+Notation "|={ E1 , E2 }|>=>^ n Q" := (|={E1,E2}▷=>^n Q)%I
+  (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
+  : bi_scope.
+Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+  (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
+   : stdpp_scope.
+Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+  (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
+  : bi_scope.