[ test ] Add tests inspired by John Hughes' RGen example

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"

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

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]

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

tests/lib/john-hughes/rgen-001/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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

tests/lib/john-hughes/rgen-002/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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

tests/lib/john-hughes/rgen-003/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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

tests/lib/john-hughes/rgen-004/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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

tests/lib/john-hughes/rgen-005/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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

tests/lib/john-hughes/rgen-006/use-gen.ipkg

@@ -0,0 +1,6 @@
+package test
+
+main = UseGen
+executable = use-gen
+
+depends = deptycheck

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

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]

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