examples: add several regression tests for pattern matching

For issues #829, #1121, #1228, #1903 and #1954. The PatternMatch.fst
file also constains some various examples. While at it, also add a check
for #1956 (even if it never manifested).

examples/bug-reports/Bug1121.fst

@@ -0,0 +1,17 @@
+module Bug1121
+
+[@(expect_failure [138])]
+let foo () : Tot int =
+  match (1,2) with
+  | (x,x) -> x
+
+[@(expect_failure [138])]
+let foo2 x = match x with (x,x) -> 1
+
+[@(expect_failure [138])]
+let foo3 x x = 42
+
+[@(expect_failure [138])]
+let foo4 (x:int) =
+    let inner_foo x x = x + x in
+    inner_foo x x

examples/bug-reports/Bug1228.fst

@@ -0,0 +1,36 @@
+module Bug1228
+
+[@(expect_failure [19])]
+let 2 = 4  // Incomplete pattern (ok in OCaml)
+
+[@(expect_failure [19])]
+let [] = [1]  // idem
+
+[@(expect_failure [178])]
+let 2: int = 4  // Incomplete pattern (ok in OCaml)
+
+[@(expect_failure [178])]
+let []: list int = [1]  // idem
+
+[@(expect_failure [178])]
+let (): int = 4  // int to unit?
+
+let foo (x: int): int = x
+
+[@(expect_failure [114])]
+let () = foo  // function to unit?
+
+[@(expect_failure [114])]
+let 3 = foo  // function to int?
+
+[@(expect_failure [114])]
+let 4 = [1; 2; 3]  // list int to int?
+
+[@(expect_failure [178])]
+let (): int -> int = foo  // function to unit?
+
+[@(expect_failure [178])]
+let 3: int -> int = foo  // function to int?
+
+[@(expect_failure [178])]
+let 4: list int = [1; 2; 3]  // list int to int?

examples/bug-reports/Bug1903.fst

@@ -0,0 +1,18 @@
+module Bug1903
+
+[@(expect_failure [178])] (* bad ascription *)
+let None : option unit = Some ()
+
+[@(expect_failure [19])] (* incomplete match *)
+let None = Some ()
+
+[@(expect_failure [72])] (* X unbound *)
+let X = 42
+
+[@(expect_failure [114])] (* type doesn't match *)
+let None = 42
+
+[@(expect_failure [19])] (* incomplete match *)
+let 0 = 1
+
+let 0 = 0 (* OK *)

examples/bug-reports/Bug1954.fst

@@ -0,0 +1,26 @@
+module Bug1954
+
+(* disable warning about needless let rec *)
+#set-options "--warn_error -328"
+
+[@(expect_failure [178])]
+let blah = match None with | (None : option int) -> ()
+
+let         addp ((x, y) : int & int) : int = x + y
+let rec rec_addp ((x, y) : int & int) : int = x + y
+
+let         addp' = fun ((x,y) : int & int) -> x + y <: int
+let rec rec_addp' = fun ((x,y) : int & int) -> x + y <: int
+
+type box a = | Box of a
+
+let unbox (Box x) : int = x
+
+let unbox' (Box x : box int) : int = x
+
+let unbox'' (Box (x : int) : box int) : int = x
+
+[@(expect_failure [178])]
+let g b =
+    match b with
+    | (Box x : box int) -> x

examples/bug-reports/Bug1956.fst

@@ -0,0 +1,8 @@
+module Bug1956
+
+[@expect_failure]
+let xx : squash False = ()
+
+// This can succeed if `xx` leaks into the SMT context for this query
+[@expect_failure]
+let _ = assert False

examples/bug-reports/Bug829.fst

@@ -0,0 +1,20 @@
+module Bug829
+
+type r = { x : int }
+
+[@(expect_failure [114])]
+let true = 2
+
+[@(expect_failure [114])]
+let { x = true } = { x = 2 }
+
+[@(expect_failure [19])]
+let (x, true) = (2, false)
+
+let (x, true)  = (2, true)
+
+[@(expect_failure [19])]
+let (false, false, xx) = (true, true, 9)
+
+[@(expect_failure [114])]
+let (true, true) = (2, false)

examples/bug-reports/Makefile

@@ -38,7 +38,8 @@ SHOULD_VERIFY_CLOSED=bug022.fst bug024.fst bug025.fst bug026.fst bug026b.fst bug
   Bug1622.fst bug1540.fst Bug1784.fst Bug1802.fst Bug1055.fst Bug1818.fst Bug1640.fst Bug1243.fst Bug1841.fst \
   Bug1847.fst Bug1855.fst Bug1812.fst Bug1840.fst Bug1866.fst Bug811.fst Bug841.fst Bug1060.fst Bug1070.fst \
   Bug1130.fst Bug1170.fst Bug1191.fst Bug1799.fst Bug1900.fst Bug1908.fst Bug1913.fst BugLexTop.fst Bug1940a.fst \
-  Bug1940b.fst Bug1940c.fst Bug1936.fst Bug1952a.fst Bug1952b.fst Bug1953.fst Bug1074.fst
+  Bug1940b.fst Bug1940c.fst Bug1936.fst Bug1952a.fst Bug1952b.fst Bug1953.fst Bug1074.fst Bug1954.fst Bug1903.fst \
+  Bug1121.fst Bug1956.fst Bug1228.fst Bug829.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=bug771.fsti bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=bug016.fst

examples/micro-benchmarks/Makefile

@@ -33,7 +33,7 @@ all-pos: Unit1.Basic.uver Unit1.Projectors2.uver Unit1.WPsAndTriples.uver Unit1.
 	 PatAnnot.uver TupleSyntax.uver Test.FunctionalExtensionality.uver ArgsAndQuals.uver Test.Printf.uver \
 	 MustEraseForExtraction.uver UnifyReify.uver NestedLemma.uver NormTypesForSMT.uver \
 	 StrictUnfolding.uver GhostImplicits.uver Erasable.ml-cmp Coercions.uver Coercions1Phase.uver \
-	 Inference.uver
+	 Inference.uver PatternMatch.uver
 
 Coercions1Phase.uver: OTHERFLAGS += --use_two_phase_tc false
 Coercions1Phase.fst: Coercions.fst

examples/micro-benchmarks/PatternMatch.fst

@@ -0,0 +1,73 @@
+module PatternMatch
+
+(* Error 19: assertion failed (from incomplete pattern matching in this case
+ * Error 114: Type of pattern __ does not match type of scrutinee __
+ * Error 178: Type ascriptions within patterns are only allowed on variables [2 times]
+ *)
+
+let _ = (=)
+
+let pair_on_arg ((x,y) : int & int) : int = x + y
+
+type ab = | A | B
+
+[@(expect_failure [178])]
+let oops2 = match A with | (A : _) -> ()
+
+[@(expect_failure [178])]
+let blah = match None with | (None : option int) -> ()
+
+[@(expect_failure [19])]
+let None = Some 42
+
+[@(expect_failure [19])]
+let Some () = None
+
+let true = true
+
+[@(expect_failure [19])]
+let true = false
+
+[@(expect_failure [114])]
+let false = 1
+
+[@(expect_failure [114])]
+let A = 2
+
+[@(expect_failure [19])]
+let A = B
+
+[@(expect_failure [178])]
+let None : option unit = Some 42
+
+let x1, y1 = 42, true
+let ((x2 : int), (y2 : bool)) = (42, true)
+
+let _ = assert (x1 == 42)
+let _ = assert (y1 == true)
+let _ = assert (x2 == 42)
+let _ = assert (y2 == true)
+
+
+type r = { x : int }
+
+[@(expect_failure [114])]
+let true = 2
+
+[@(expect_failure [114])]
+let { x = true } = { x = 2 }
+
+[@(expect_failure [19])]
+let (x, true) = (2, false)
+
+[@(expect_failure [19])]
+let (false, false, x) = (true, true, 9)
+
+let (x, true)  = (2, true)
+
+[@(expect_failure [114])]
+let (true, true) = (2, false)
+
+let (z, 0) = (42, 0)
+
+let () = ()