fix for #2415, support for negative literals in match

ocaml/fstar-lib/FStar_Parser_Parse.mly

@@ -621,6 +621,18 @@ atomicPattern:
       { mk_pattern (PatWild (Some Implicit, [])) (rr $loc) }
   | c=constant
       { mk_pattern (PatConst c) (rr $loc(c)) }
+  | tok=MINUS c=constant
+      { let r = rr2 $loc(tok) $loc(c) in
+        let c =
+          match c with
+          | Const_int (s, swopt) ->
+            (match swopt with
+             | None
+             | Some (Signed, _) -> Const_int ("-" ^ s, swopt)
+             | _ -> raise_error (Fatal_SyntaxError, "Syntax_error: negative integer constant with unsigned width") r)
+          | _ -> raise_error (Fatal_SyntaxError, "Syntax_error: negative constant that is not an integer") r
+        in
+        mk_pattern (PatConst c) r }
   | BACKTICK_PERC q=atomicTerm
       { mk_pattern (PatVQuote q) (rr $loc) }
   | qual_id=aqualifiedWithAttrs(lident)

tests/bug-reports/Bug2415.fst

@@ -0,0 +1,32 @@
+module Bug2415
+
+let sign = (z:int{z = 0 \/ z = (-1) \/ z = 1})
+
+let example_1 (s:sign) : string =
+ match s with
+ | -1 -> "negative"
+ | 1 -> "positive"
+ | 0 -> "zero"
+ | -2 -> assert False; ""
+
+open FStar.Int32
+open FStar.Int8
+open FStar.UInt32
+open FStar.UInt8
+
+type i8 = FStar.Int8.t
+type i32 = FStar.Int32.t
+type u8 = FStar.UInt8.t
+type u32 = FStar.UInt32.t
+
+let test1 (n:i32) =
+  match n with
+  | -1l -> assert (Int32.v n == -1)
+  | 1l -> assert (Int32.v n == 1)
+  | _ -> ()
+
+[@@ expect_failure [114]]  // type of pattern (Int32.t) does not match the type of scrutinee (Int8.t)
+let test2 (n:i8) =
+  match n with
+  | -0l -> ()
+  | _ -> ()

tests/bug-reports/Makefile

@@ -50,7 +50,8 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2635.fst Bug2637.fst Bug2641.fst Bug1486.fst PropProofs.fst \
   Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\
   Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\
-  Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst
+  Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \
+	Bug2415.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst