From 179dba781fa6f54c87f34e8cc1b975ffce94a09e Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 9 Sep 2024 18:57:05 +0300 Subject: [PATCH] [ test ] Add tests inspired by John Hughes' RGen example --- tests/Tests.idr | 1 + tests/lib/john-hughes/rgen-001/UseGen.idr | 25 +++++++++++++++ tests/lib/john-hughes/rgen-001/expected | 10 ++++++ tests/lib/john-hughes/rgen-001/run | 6 ++++ tests/lib/john-hughes/rgen-001/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-002/UseGen.idr | 30 ++++++++++++++++++ tests/lib/john-hughes/rgen-002/expected | 10 ++++++ tests/lib/john-hughes/rgen-002/run | 6 ++++ tests/lib/john-hughes/rgen-002/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-003/UseGen.idr | 31 +++++++++++++++++++ tests/lib/john-hughes/rgen-003/expected | 10 ++++++ tests/lib/john-hughes/rgen-003/run | 6 ++++ tests/lib/john-hughes/rgen-003/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-004/UseGen.idr | 32 +++++++++++++++++++ tests/lib/john-hughes/rgen-004/expected | 10 ++++++ tests/lib/john-hughes/rgen-004/run | 6 ++++ tests/lib/john-hughes/rgen-004/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-005/UseGen.idr | 30 ++++++++++++++++++ tests/lib/john-hughes/rgen-005/expected | 10 ++++++ tests/lib/john-hughes/rgen-005/run | 6 ++++ tests/lib/john-hughes/rgen-005/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-006/UseGen.idr | 33 ++++++++++++++++++++ tests/lib/john-hughes/rgen-006/expected | 10 ++++++ tests/lib/john-hughes/rgen-006/run | 6 ++++ tests/lib/john-hughes/rgen-006/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-007/UseGen.idr | 30 ++++++++++++++++++ tests/lib/john-hughes/rgen-007/expected | 10 ++++++ tests/lib/john-hughes/rgen-007/run | 6 ++++ tests/lib/john-hughes/rgen-007/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-008/UseGen.idr | 32 +++++++++++++++++++ tests/lib/john-hughes/rgen-008/expected | 10 ++++++ tests/lib/john-hughes/rgen-008/run | 6 ++++ tests/lib/john-hughes/rgen-008/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-009/UseGen.idr | 32 +++++++++++++++++++ tests/lib/john-hughes/rgen-009/expected | 10 ++++++ tests/lib/john-hughes/rgen-009/run | 6 ++++ tests/lib/john-hughes/rgen-009/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-010/UseGen.idr | 32 +++++++++++++++++++ tests/lib/john-hughes/rgen-010/expected | 10 ++++++ tests/lib/john-hughes/rgen-010/run | 6 ++++ tests/lib/john-hughes/rgen-010/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-011/UseGen.idr | 32 +++++++++++++++++++ tests/lib/john-hughes/rgen-011/expected | 10 ++++++ tests/lib/john-hughes/rgen-011/run | 6 ++++ tests/lib/john-hughes/rgen-011/use-gen.ipkg | 6 ++++ tests/lib/john-hughes/rgen-012/UseGen.idr | 34 +++++++++++++++++++++ tests/lib/john-hughes/rgen-012/expected | 10 ++++++ tests/lib/john-hughes/rgen-012/run | 6 ++++ tests/lib/john-hughes/rgen-012/use-gen.ipkg | 6 ++++ 49 files changed, 638 insertions(+) create mode 100644 tests/lib/john-hughes/rgen-001/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-001/expected create mode 100755 tests/lib/john-hughes/rgen-001/run create mode 100644 tests/lib/john-hughes/rgen-001/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-002/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-002/expected create mode 100755 tests/lib/john-hughes/rgen-002/run create mode 100644 tests/lib/john-hughes/rgen-002/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-003/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-003/expected create mode 100755 tests/lib/john-hughes/rgen-003/run create mode 100644 tests/lib/john-hughes/rgen-003/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-004/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-004/expected create mode 100755 tests/lib/john-hughes/rgen-004/run create mode 100644 tests/lib/john-hughes/rgen-004/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-005/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-005/expected create mode 100755 tests/lib/john-hughes/rgen-005/run create mode 100644 tests/lib/john-hughes/rgen-005/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-006/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-006/expected create mode 100755 tests/lib/john-hughes/rgen-006/run create mode 100644 tests/lib/john-hughes/rgen-006/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-007/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-007/expected create mode 100755 tests/lib/john-hughes/rgen-007/run create mode 100644 tests/lib/john-hughes/rgen-007/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-008/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-008/expected create mode 100755 tests/lib/john-hughes/rgen-008/run create mode 100644 tests/lib/john-hughes/rgen-008/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-009/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-009/expected create mode 100755 tests/lib/john-hughes/rgen-009/run create mode 100644 tests/lib/john-hughes/rgen-009/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-010/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-010/expected create mode 100755 tests/lib/john-hughes/rgen-010/run create mode 100644 tests/lib/john-hughes/rgen-010/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-011/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-011/expected create mode 100755 tests/lib/john-hughes/rgen-011/run create mode 100644 tests/lib/john-hughes/rgen-011/use-gen.ipkg create mode 100644 tests/lib/john-hughes/rgen-012/UseGen.idr create mode 100644 tests/lib/john-hughes/rgen-012/expected create mode 100755 tests/lib/john-hughes/rgen-012/run create mode 100644 tests/lib/john-hughes/rgen-012/use-gen.ipkg diff --git a/tests/Tests.idr b/tests/Tests.idr index e1bc7268d..2f6fa7fd8 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -7,6 +7,7 @@ main = goldenRunner $ [ "The `Gen` monad" `atDir` "lib/gen-monad" , "Distribution of generators" `atDir` "lib/distribution" , "Model coverage" `atDir` "lib/coverage" + , "John Hughes-style tests" `atDir` "lib/john-hughes" , "The library documentation" `atDir` "docs" , "Derivation utils: TTImp equality up to renaming" `atDir` "derivation/utils/up-to-renaming-ttimp-eq" , "Derivation utils: canonic signature" `atDir` "derivation/utils/canonicsig" diff --git a/tests/lib/john-hughes/rgen-001/UseGen.idr b/tests/lib/john-hughes/rgen-001/UseGen.idr new file mode 100644 index 000000000..a87b84188 --- /dev/null +++ b/tests/lib/john-hughes/rgen-001/UseGen.idr @@ -0,0 +1,25 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-001/expected b/tests/lib/john-hughes/rgen-001/expected new file mode 100644 index 000000000..db414ea77 --- /dev/null +++ b/tests/lib/john-hughes/rgen-001/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 57, 6, 66] +[68, 94, 42, 45, 8, 25] +[75, 58, 86, 80, 74, 38] +[33, 69, 37, 18, 1, 21] +[99, 74, 42, 24, 41, 48] +[46, 64, 2, 60, 35, 72] +[75, 54, 46, 85, 76, 35] +[75, 39, 3, 51, 15, 78] +[14, 87, 51, 33, 19, 80] +[42, 21, 20, 56, 99, 29] diff --git a/tests/lib/john-hughes/rgen-001/run b/tests/lib/john-hughes/rgen-001/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-001/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-001/use-gen.ipkg b/tests/lib/john-hughes/rgen-001/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-001/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-002/UseGen.idr b/tests/lib/john-hughes/rgen-002/UseGen.idr new file mode 100644 index 000000000..18ab33b6f --- /dev/null +++ b/tests/lib/john-hughes/rgen-002/UseGen.idr @@ -0,0 +1,30 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-002/expected b/tests/lib/john-hughes/rgen-002/expected new file mode 100644 index 000000000..a63c4778e --- /dev/null +++ b/tests/lib/john-hughes/rgen-002/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 57, 6, 2] +[68, 94, 42, 45, 8, 68] +[75, 58, 86, 80, 74, 75] +[33, 69, 37, 18, 1, 33] +[99, 74, 42, 24, 41, 99] +[46, 64, 2, 60, 35, 46] +[75, 54, 46, 85, 76, 75] +[75, 39, 3, 51, 15, 75] +[14, 87, 51, 33, 19, 14] +[80, 42, 21, 20, 56, 80] diff --git a/tests/lib/john-hughes/rgen-002/run b/tests/lib/john-hughes/rgen-002/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-002/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-002/use-gen.ipkg b/tests/lib/john-hughes/rgen-002/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-002/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-003/UseGen.idr b/tests/lib/john-hughes/rgen-003/UseGen.idr new file mode 100644 index 000000000..7d585192d --- /dev/null +++ b/tests/lib/john-hughes/rgen-003/UseGen.idr @@ -0,0 +1,31 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f + guard $ b == e + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-003/expected b/tests/lib/john-hughes/rgen-003/expected new file mode 100644 index 000000000..42e4daf8a --- /dev/null +++ b/tests/lib/john-hughes/rgen-003/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 57, 73, 2] +[68, 94, 42, 45, 94, 68] +[75, 58, 86, 80, 58, 75] +[33, 69, 37, 18, 69, 33] +[99, 74, 42, 24, 74, 99] +[41, 48, 46, 64, 48, 41] +[60, 35, 72, 75, 35, 60] +[85, 76, 35, 75, 76, 85] +[51, 15, 78, 14, 15, 51] +[33, 19, 80, 42, 19, 33] diff --git a/tests/lib/john-hughes/rgen-003/run b/tests/lib/john-hughes/rgen-003/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-003/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-003/use-gen.ipkg b/tests/lib/john-hughes/rgen-003/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-003/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-004/UseGen.idr b/tests/lib/john-hughes/rgen-004/UseGen.idr new file mode 100644 index 000000000..4a609a0ca --- /dev/null +++ b/tests/lib/john-hughes/rgen-004/UseGen.idr @@ -0,0 +1,32 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f + guard $ b == e + guard $ c == d + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-004/expected b/tests/lib/john-hughes/rgen-004/expected new file mode 100644 index 000000000..50e323cfd --- /dev/null +++ b/tests/lib/john-hughes/rgen-004/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 21, 73, 2] +[66, 68, 94, 94, 68, 66] +[8, 25, 75, 75, 25, 8] +[74, 38, 33, 33, 38, 74] +[18, 1, 21, 21, 1, 18] +[42, 24, 41, 41, 24, 42] +[64, 2, 60, 60, 2, 64] +[75, 54, 46, 46, 54, 75] +[76, 35, 75, 75, 35, 76] +[15, 78, 14, 14, 78, 15] diff --git a/tests/lib/john-hughes/rgen-004/run b/tests/lib/john-hughes/rgen-004/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-004/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-004/use-gen.ipkg b/tests/lib/john-hughes/rgen-004/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-004/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-005/UseGen.idr b/tests/lib/john-hughes/rgen-005/UseGen.idr new file mode 100644 index 000000000..e0bf943d9 --- /dev/null +++ b/tests/lib/john-hughes/rgen-005/UseGen.idr @@ -0,0 +1,30 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f && b == e && c == d + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-005/expected b/tests/lib/john-hughes/rgen-005/expected new file mode 100644 index 000000000..50e323cfd --- /dev/null +++ b/tests/lib/john-hughes/rgen-005/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 21, 73, 2] +[66, 68, 94, 94, 68, 66] +[8, 25, 75, 75, 25, 8] +[74, 38, 33, 33, 38, 74] +[18, 1, 21, 21, 1, 18] +[42, 24, 41, 41, 24, 42] +[64, 2, 60, 60, 2, 64] +[75, 54, 46, 46, 54, 75] +[76, 35, 75, 75, 35, 76] +[15, 78, 14, 14, 78, 15] diff --git a/tests/lib/john-hughes/rgen-005/run b/tests/lib/john-hughes/rgen-005/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-005/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-005/use-gen.ipkg b/tests/lib/john-hughes/rgen-005/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-005/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-006/UseGen.idr b/tests/lib/john-hughes/rgen-006/UseGen.idr new file mode 100644 index 000000000..f727b4710 --- /dev/null +++ b/tests/lib/john-hughes/rgen-006/UseGen.idr @@ -0,0 +1,33 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f + guard $ b == e + guard $ c == d + guard $ c == 2 + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-006/expected b/tests/lib/john-hughes/rgen-006/expected new file mode 100644 index 000000000..988ae4adc --- /dev/null +++ b/tests/lib/john-hughes/rgen-006/expected @@ -0,0 +1,10 @@ +[2, 73, 2, 2, 73, 2] +[66, 68, 2, 2, 68, 66] +[45, 8, 2, 2, 8, 45] +[80, 74, 2, 2, 74, 80] +[18, 1, 2, 2, 1, 18] +[42, 24, 2, 2, 24, 42] +[46, 64, 2, 2, 64, 46] +[72, 75, 2, 2, 75, 72] +[76, 35, 2, 2, 35, 76] +[15, 78, 2, 2, 78, 15] diff --git a/tests/lib/john-hughes/rgen-006/run b/tests/lib/john-hughes/rgen-006/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-006/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-006/use-gen.ipkg b/tests/lib/john-hughes/rgen-006/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-006/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-007/UseGen.idr b/tests/lib/john-hughes/rgen-007/UseGen.idr new file mode 100644 index 000000000..084169833 --- /dev/null +++ b/tests/lib/john-hughes/rgen-007/UseGen.idr @@ -0,0 +1,30 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f && b == e && c == d && c == 2 + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-007/expected b/tests/lib/john-hughes/rgen-007/expected new file mode 100644 index 000000000..988ae4adc --- /dev/null +++ b/tests/lib/john-hughes/rgen-007/expected @@ -0,0 +1,10 @@ +[2, 73, 2, 2, 73, 2] +[66, 68, 2, 2, 68, 66] +[45, 8, 2, 2, 8, 45] +[80, 74, 2, 2, 74, 80] +[18, 1, 2, 2, 1, 18] +[42, 24, 2, 2, 24, 42] +[46, 64, 2, 2, 64, 46] +[72, 75, 2, 2, 75, 72] +[76, 35, 2, 2, 35, 76] +[15, 78, 2, 2, 78, 15] diff --git a/tests/lib/john-hughes/rgen-007/run b/tests/lib/john-hughes/rgen-007/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-007/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-007/use-gen.ipkg b/tests/lib/john-hughes/rgen-007/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-007/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-008/UseGen.idr b/tests/lib/john-hughes/rgen-008/UseGen.idr new file mode 100644 index 000000000..09c8d7246 --- /dev/null +++ b/tests/lib/john-hughes/rgen-008/UseGen.idr @@ -0,0 +1,32 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ c == f + guard $ c == e + guard $ c == d + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-008/expected b/tests/lib/john-hughes/rgen-008/expected new file mode 100644 index 000000000..4fa6241ef --- /dev/null +++ b/tests/lib/john-hughes/rgen-008/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 21, 21, 21] +[66, 68, 94, 94, 94, 94] +[8, 25, 75, 75, 75, 75] +[74, 38, 33, 33, 33, 33] +[18, 1, 21, 21, 21, 21] +[42, 24, 41, 41, 41, 41] +[64, 2, 60, 60, 60, 60] +[75, 54, 46, 46, 46, 46] +[76, 35, 75, 75, 75, 75] +[15, 78, 14, 14, 14, 14] diff --git a/tests/lib/john-hughes/rgen-008/run b/tests/lib/john-hughes/rgen-008/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-008/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-008/use-gen.ipkg b/tests/lib/john-hughes/rgen-008/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-008/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-009/UseGen.idr b/tests/lib/john-hughes/rgen-009/UseGen.idr new file mode 100644 index 000000000..076f0cfba --- /dev/null +++ b/tests/lib/john-hughes/rgen-009/UseGen.idr @@ -0,0 +1,32 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ b == f + guard $ b == e + guard $ b == d + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-009/expected b/tests/lib/john-hughes/rgen-009/expected new file mode 100644 index 000000000..165b29aa4 --- /dev/null +++ b/tests/lib/john-hughes/rgen-009/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 73, 73, 73] +[66, 68, 94, 68, 68, 68] +[8, 25, 75, 25, 25, 25] +[74, 38, 33, 38, 38, 38] +[18, 1, 21, 1, 1, 1] +[42, 24, 41, 24, 24, 24] +[64, 2, 60, 2, 2, 2] +[75, 54, 46, 54, 54, 54] +[76, 35, 75, 35, 35, 35] +[15, 78, 14, 78, 78, 78] diff --git a/tests/lib/john-hughes/rgen-009/run b/tests/lib/john-hughes/rgen-009/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-009/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-009/use-gen.ipkg b/tests/lib/john-hughes/rgen-009/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-009/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-010/UseGen.idr b/tests/lib/john-hughes/rgen-010/UseGen.idr new file mode 100644 index 000000000..c0d8c7fdf --- /dev/null +++ b/tests/lib/john-hughes/rgen-010/UseGen.idr @@ -0,0 +1,32 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + guard $ b == d + e <- nums + guard $ b == e + f <- nums + guard $ b == f + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-010/expected b/tests/lib/john-hughes/rgen-010/expected new file mode 100644 index 000000000..165b29aa4 --- /dev/null +++ b/tests/lib/john-hughes/rgen-010/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 73, 73, 73] +[66, 68, 94, 68, 68, 68] +[8, 25, 75, 25, 25, 25] +[74, 38, 33, 38, 38, 38] +[18, 1, 21, 1, 1, 1] +[42, 24, 41, 24, 24, 24] +[64, 2, 60, 2, 2, 2] +[75, 54, 46, 54, 54, 54] +[76, 35, 75, 35, 35, 35] +[15, 78, 14, 78, 78, 78] diff --git a/tests/lib/john-hughes/rgen-010/run b/tests/lib/john-hughes/rgen-010/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-010/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-010/use-gen.ipkg b/tests/lib/john-hughes/rgen-010/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-010/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-011/UseGen.idr b/tests/lib/john-hughes/rgen-011/UseGen.idr new file mode 100644 index 000000000..e691626f3 --- /dev/null +++ b/tests/lib/john-hughes/rgen-011/UseGen.idr @@ -0,0 +1,32 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + c <- nums + d <- nums + e <- nums + f <- nums + guard $ a == f + guard $ a == e + guard $ a == d + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-011/expected b/tests/lib/john-hughes/rgen-011/expected new file mode 100644 index 000000000..c91b13303 --- /dev/null +++ b/tests/lib/john-hughes/rgen-011/expected @@ -0,0 +1,10 @@ +[2, 73, 21, 2, 2, 2] +[66, 68, 94, 66, 66, 66] +[8, 25, 75, 8, 8, 8] +[74, 38, 33, 74, 74, 74] +[18, 1, 21, 18, 18, 18] +[42, 24, 41, 42, 42, 42] +[64, 2, 60, 64, 64, 64] +[75, 54, 46, 75, 75, 75] +[76, 35, 75, 76, 76, 76] +[15, 78, 14, 15, 15, 15] diff --git a/tests/lib/john-hughes/rgen-011/run b/tests/lib/john-hughes/rgen-011/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-011/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-011/use-gen.ipkg b/tests/lib/john-hughes/rgen-011/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-011/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/john-hughes/rgen-012/UseGen.idr b/tests/lib/john-hughes/rgen-012/UseGen.idr new file mode 100644 index 000000000..08821e4ce --- /dev/null +++ b/tests/lib/john-hughes/rgen-012/UseGen.idr @@ -0,0 +1,34 @@ +module UseGen + +import Data.List.Lazy + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +guard : Bool -> Gen0 () +guard True = pure () +guard False = empty + +fun : Gen0 $ List Int +fun = do + let nums = elements [1 .. 100] + a <- nums + b <- nums + guard $ a == b + c <- nums + guard $ a == c + d <- nums + guard $ a == d + e <- nums + guard $ a == e + f <- nums + guard $ a == f + pure [a, b, c, d, e, f] + +main : IO Unit +main = Lazy.traverse_ printLn $ unGenTryN 10 someStdGen fun diff --git a/tests/lib/john-hughes/rgen-012/expected b/tests/lib/john-hughes/rgen-012/expected new file mode 100644 index 000000000..4f201218b --- /dev/null +++ b/tests/lib/john-hughes/rgen-012/expected @@ -0,0 +1,10 @@ +[2, 2, 2, 2, 2, 2] +[66, 66, 66, 66, 66, 66] +[42, 42, 42, 42, 42, 42] +[58, 58, 58, 58, 58, 58] +[69, 69, 69, 69, 69, 69] +[21, 21, 21, 21, 21, 21] +[41, 41, 41, 41, 41, 41] +[2, 2, 2, 2, 2, 2] +[54, 54, 54, 54, 54, 54] +[35, 35, 35, 35, 35, 35] diff --git a/tests/lib/john-hughes/rgen-012/run b/tests/lib/john-hughes/rgen-012/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/john-hughes/rgen-012/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps use-gen.ipkg && \ +pack exec UseGen.idr + +rm -rf build diff --git a/tests/lib/john-hughes/rgen-012/use-gen.ipkg b/tests/lib/john-hughes/rgen-012/use-gen.ipkg new file mode 100644 index 000000000..7735f2ddb --- /dev/null +++ b/tests/lib/john-hughes/rgen-012/use-gen.ipkg @@ -0,0 +1,6 @@ +package test + +main = UseGen +executable = use-gen + +depends = deptycheck