Merge pull request #465 from mtzguido/pars

parser: allow nested quantifiers at the top level

Author: mtzguido

src/ml/FStarC_Parser_Parse.mly

@@ -419,8 +419,8 @@ rawDecl:
       {
         let r = rr $loc in
         let lbs = focusLetBindings lbs r in
-        if q <> Rec && List.length lbs <> 1
-        then raise_error_text r Fatal_MultipleLetBinding "Unexpected multiple let-binding (Did you forget some rec qualifier ?)";
+        if q <> Rec && FStarC_List.length lbs > Prims.parse_int "1"
+        then raise_error_text (fst (nth lbs (Prims.parse_int "1"))).prange Fatal_MultipleLetBinding "Unexpected multiple let-binding (Did you forget some rec qualifier ?)";
         TopLevelLet(q, lbs)
       }
   | VAL c=constant

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
+{
+  ()
+}