Allow overloading exists and forall similar to let operators

ocaml/fstar-lib/FStar_Parser_LexFStar.ml

@@ -60,10 +60,10 @@ let () =
   Hashtbl.add keywords "end"           END         ;
   Hashtbl.add keywords "ensures"       ENSURES     ;
   Hashtbl.add keywords "exception"     EXCEPTION   ;
-  Hashtbl.add keywords "exists"        EXISTS      ;
+  Hashtbl.add keywords "exists"        (EXISTS false);
   Hashtbl.add keywords "false"         FALSE       ;
   Hashtbl.add keywords "friend"        FRIEND      ;
-  Hashtbl.add keywords "forall"        FORALL      ;
+  Hashtbl.add keywords "forall"        (FORALL false);
   Hashtbl.add keywords "fun"           FUN         ;
   Hashtbl.add keywords "λ"             FUN         ;
   Hashtbl.add keywords "function"      FUNCTION    ;
@@ -191,8 +191,8 @@ let () =
    "}", RBRACE;
    "$", DOLLAR;
      (* New Unicode equivalents *)
-   "∀", FORALL;
-   "∃", EXISTS;
+   "∀", (FORALL false);
+   "∃", (EXISTS false);
    "⊤", NAME "True";
    "⊥", NAME "False";
    "⟹", IMPLIES;
@@ -490,6 +490,34 @@ match%sedlex lexbuf with
         | s  -> LET_OP s
       )
 
+ | "exists", Plus op_char ->
+    ensure_no_comment lexbuf (fun s ->
+        match BatString.lchop ~n:6 s with
+        | "" -> EXISTS false
+        | s  -> EXISTS_OP s
+      )
+
+ | "∃", Plus op_char ->
+    ensure_no_comment lexbuf (fun s ->
+        match BatString.lchop ~n:1 s with
+        | "" -> EXISTS false
+        | s  -> EXISTS_OP s
+      )
+
+ | "forall", Plus op_char ->
+    ensure_no_comment lexbuf (fun s ->
+        match BatString.lchop ~n:6 s with
+        | "" -> FORALL false
+        | s  -> FORALL_OP s
+      )
+
+ | "∀", Plus op_char ->
+    ensure_no_comment lexbuf (fun s ->
+        match BatString.lchop ~n:1 s with
+        | "" -> FORALL false
+        | s  -> FORALL_OP s
+      )
+
  | "and", Plus op_char ->
     ensure_no_comment lexbuf (fun s ->
         match BatString.lchop ~n:3 s with

ocaml/fstar-lib/FStar_Parser_Parse.mly

@@ -86,13 +86,19 @@ let parse_extension_blob (extension_name:string)
 %token <string> AND_OP
 %token <string> MATCH_OP
 %token <string> IF_OP
+%token <bool> EXISTS
+%token <string> EXISTS_OP
+%token <bool> FORALL
+%token <string> FORALL_OP
+
+
 /* [SEMICOLON_OP] encodes either:
 - [;;], which used to be SEMICOLON_SEMICOLON, or
 - [;<OP>], with <OP> a sequence of [op_char] (see FStar_Parser_LexFStar).
 */
 %token <string option> SEMICOLON_OP
 
-%token FORALL EXISTS ASSUME NEW LOGIC ATTRIBUTES
+%token ASSUME NEW LOGIC ATTRIBUTES
 %token IRREDUCIBLE UNFOLDABLE INLINE OPAQUE UNFOLD INLINE_FOR_EXTRACTION
 %token NOEXTRACT
 %token NOEQUALITY UNOPTEQUALITY PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH
@@ -1074,6 +1080,16 @@ typ:
 %inline quantifier:
   | FORALL { fun x -> QForall x }
   | EXISTS { fun x -> QExists x}
+  | op=FORALL_OP
+    { 
+      let op = mk_ident("forall" ^ op, rr $loc(op)) in
+      fun (x,y,z) -> QuantOp (op, x, y, z)
+    }
+  | op=EXISTS_OP
+    { 
+      let op = mk_ident("exists" ^ op, rr $loc(op)) in
+      fun (x,y,z) -> QuantOp (op, x, y, z)
+    }
 
 trigger:
   |   { [] }
@@ -1541,6 +1557,11 @@ string:
   | op=TILDE        { mk_ident (op, rr $loc) }
   | op=and_op       {op}
   | op=let_op       {op}
+  | op=quantifier_op {op}
+
+%inline quantifier_op:
+  | op=EXISTS_OP    { mk_ident ("exists" ^ op, rr $loc) }
+  | op=FORALL_OP    { mk_ident ("forall" ^ op, rr $loc) }
 
 %inline and_op:
   | op=AND_OP { mk_ident ("and" ^ op, rr $loc) }