From 5629870ab01d85fa41a7bf66dde5e4dc046b06e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 05:49:21 -0800 Subject: [PATCH] test: news tests --- tests/compiler/closure_bug2.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug2.lean.expected.out | 1 + tests/compiler/closure_bug3.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug3.lean.expected.out | 1 + tests/compiler/closure_bug4.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug4.lean.expected.out | 1 + tests/compiler/closure_bug5.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug5.lean.expected.out | 1 + tests/compiler/closure_bug6.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug6.lean.expected.out | 1 + tests/compiler/closure_bug7.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug7.lean.expected.out | 1 + tests/compiler/closure_bug8.lean | 22 +++++++++++++++++++ tests/compiler/closure_bug8.lean.expected.out | 1 + 14 files changed, 161 insertions(+) create mode 100644 tests/compiler/closure_bug2.lean create mode 100644 tests/compiler/closure_bug2.lean.expected.out create mode 100644 tests/compiler/closure_bug3.lean create mode 100644 tests/compiler/closure_bug3.lean.expected.out create mode 100644 tests/compiler/closure_bug4.lean create mode 100644 tests/compiler/closure_bug4.lean.expected.out create mode 100644 tests/compiler/closure_bug5.lean create mode 100644 tests/compiler/closure_bug5.lean.expected.out create mode 100644 tests/compiler/closure_bug6.lean create mode 100644 tests/compiler/closure_bug6.lean.expected.out create mode 100644 tests/compiler/closure_bug7.lean create mode 100644 tests/compiler/closure_bug7.lean.expected.out create mode 100644 tests/compiler/closure_bug8.lean create mode 100644 tests/compiler/closure_bug8.lean.expected.out diff --git a/tests/compiler/closure_bug2.lean b/tests/compiler/closure_bug2.lean new file mode 100644 index 0000000000..dbd040f16b --- /dev/null +++ b/tests/compiler/closure_bug2.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug2.lean.expected.out b/tests/compiler/closure_bug2.lean.expected.out new file mode 100644 index 0000000000..20c8b030a5 --- /dev/null +++ b/tests/compiler/closure_bug2.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17] diff --git a/tests/compiler/closure_bug3.lean b/tests/compiler/closure_bug3.lean new file mode 100644 index 0000000000..95b79d0e65 --- /dev/null +++ b/tests/compiler/closure_bug3.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug3.lean.expected.out b/tests/compiler/closure_bug3.lean.expected.out new file mode 100644 index 0000000000..8a50612c31 --- /dev/null +++ b/tests/compiler/closure_bug3.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] diff --git a/tests/compiler/closure_bug4.lean b/tests/compiler/closure_bug4.lean new file mode 100644 index 0000000000..316a1c5204 --- /dev/null +++ b/tests/compiler/closure_bug4.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug4.lean.expected.out b/tests/compiler/closure_bug4.lean.expected.out new file mode 100644 index 0000000000..6191717be4 --- /dev/null +++ b/tests/compiler/closure_bug4.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15] diff --git a/tests/compiler/closure_bug5.lean b/tests/compiler/closure_bug5.lean new file mode 100644 index 0000000000..524a455422 --- /dev/null +++ b/tests/compiler/closure_bug5.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug5.lean.expected.out b/tests/compiler/closure_bug5.lean.expected.out new file mode 100644 index 0000000000..9db7211ab9 --- /dev/null +++ b/tests/compiler/closure_bug5.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14] diff --git a/tests/compiler/closure_bug6.lean b/tests/compiler/closure_bug6.lean new file mode 100644 index 0000000000..a3f8ac43f2 --- /dev/null +++ b/tests/compiler/closure_bug6.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7, x8]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug6.lean.expected.out b/tests/compiler/closure_bug6.lean.expected.out new file mode 100644 index 0000000000..7ab4e1500a --- /dev/null +++ b/tests/compiler/closure_bug6.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7, 8] diff --git a/tests/compiler/closure_bug7.lean b/tests/compiler/closure_bug7.lean new file mode 100644 index 0000000000..f403e64f3d --- /dev/null +++ b/tests/compiler/closure_bug7.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6, x7]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug7.lean.expected.out b/tests/compiler/closure_bug7.lean.expected.out new file mode 100644 index 0000000000..9dfba65da5 --- /dev/null +++ b/tests/compiler/closure_bug7.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6, 7] diff --git a/tests/compiler/closure_bug8.lean b/tests/compiler/closure_bug8.lean new file mode 100644 index 0000000000..5e53b8b36e --- /dev/null +++ b/tests/compiler/closure_bug8.lean @@ -0,0 +1,22 @@ +def f (x : Nat) : Nat × (Nat → String) := +let x1 := x + 1; +let x2 := x + 2; +let x3 := x + 3; +let x4 := x + 4; +let x5 := x + 5; +let x6 := x + 6; +let x7 := x + 7; +let x8 := x + 8; +let x9 := x + 9; +let x10 := x + 10; +let x11 := x + 11; +let x12 := x + 12; +let x13 := x + 13; +let x14 := x + 14; +let x15 := x + 15; +let x16 := x + 16; +let x17 := x + 17; +(x, fun y => toString [x1, x2, x3, x4, x5, x6]) + +def main (xs : List String) : IO Unit := +IO.println ((f (xs.headD "0").toNat).2 (xs.headD "0").toNat) diff --git a/tests/compiler/closure_bug8.lean.expected.out b/tests/compiler/closure_bug8.lean.expected.out new file mode 100644 index 0000000000..73ee80fd4b --- /dev/null +++ b/tests/compiler/closure_bug8.lean.expected.out @@ -0,0 +1 @@ +[1, 2, 3, 4, 5, 6]