allow quantifiers \forall and \exists in addition to \A and \E

Signed-off-by: Damien Doligez <[email protected]>

Author: damiendoligez

src/alexer.mll

@@ -93,7 +93,8 @@ and token = parse
       { [ ST (`Num (int_of_string num), lab, String.length dots) ] }
 
   | (","|"."|"_"|"("|")"|"["|"]"|"{"|"}"|"<<"|">>"|"]_"|">>_"|"=="|"!"
-    |"@"|":"|"::"|";"|"->"|"<-"|"|->"|"\\A"|"\\AA"|"\\E"|"\\EE"|'_' as p)
+    |"@"|":"|"::"|";"|"->"|"<-"|"|->"|"\\A"|"\\AA"|"\\E"|"\\EE"|'_'
+    |"\\forall"|"\\exists" as p)
       { [ PUNCT p ] }
 
   (* numbers *)

src/expr/e_parser.ml

@@ -549,6 +549,8 @@ and complex_expr b = lazy begin
     locate begin
       choice [ punct "\\A" <!> Forall ;
                punct "\\E" <!> Exists ;
+               punct "\\forall" <!> Forall ;
+               punct "\\exists" <!> Exists ;
              ]
       <**> (quantifier_boundeds b)
       <**> (colon_expr b)

test/parser/parser_tests.ml

@@ -95,9 +95,6 @@ let expect_failure (test : syntax_test) : bool =
     "Conjlist with RECURSIVE in LET/IN";
     "Disjlist with RECURSIVE in LET/IN";
 
-    (* https://github.com/tlaplus/tlapm/issues/160 *)
-    "Verbose Bounded Quantification";
-
     (* https://github.com/tlaplus/tlapm/issues/161 *)
     "Infix Minus as Parameter";
     "Prefix Operator References";