parser: allow nested quantifiers at the top level

Note: the parser is spitting out a lot of conflicts.

	Warning: 28 states have shift/reduce conflicts.
	Warning: one state has reduce/reduce conflicts.
	Warning: 338 shift/reduce conflicts were arbitrarily resolved.
	Warning: one reduce/reduce conflict was arbitrarily resolved.
	Warning: 232 end-of-stream conflicts were arbitrarily resolved.

These are not introduced (nor fixed) by this patch.

Author: mtzguido

src/ml/pulseparser.mly

@@ -359,10 +359,10 @@ mutOrRefQualifier:
   | MUT { MUT }
   | REF { REF }
 
-typX(X,Y):
-  | t=Y { t }
+typX(X):
+  | t=X { t }
 
-  | q=quantifier bs=binders DOT trigger=trigger e=X
+  | q=quantifier bs=binders DOT trigger=trigger e=typX(X)
       {
         match bs with
         | [] ->
@@ -373,5 +373,5 @@ typX(X,Y):
       }
 
 pulseSLProp:
-  | p=typX(tmEqWith(appTermNoRecordExp), tmEqWith(appTermNoRecordExp))
+  | p=typX(tmEqWith(appTermNoRecordExp))
     { p }

test/nolib/QuantifierOps.fst

@@ -0,0 +1,26 @@
+module QuantifierOps
+
+#lang-pulse
+open Pulse.Nolib
+
+let ( exists* ) : #a:Type -> (a -> slprop) -> slprop = admit()
+let ( forall+ ) : #a:Type -> (a -> slprop) -> slprop = admit()
+
+let test =
+  forall+ (x : int).
+    exists* (y : int).
+      emp
+
+let test2 =
+  exists* (y : int).
+    forall+ (x : int).
+      emp
+
+fn def ()
+  preserves
+    forall+ (x : int).
+      exists* (y : int).
+        emp
+{
+  ()
+}