From 4ef6a9d8daf3bdd198ca92ea0b9a4e9c0ee9dc51 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 11 Nov 2024 20:38:06 +0300 Subject: [PATCH 1/2] [ test ] Add tests for laziness with weak memoisation --- .../gen-monad/laziness000-weakmemo/UseGen.idr | 20 ++++++++++++ .../gen-monad/laziness000-weakmemo/expected | 3 ++ tests/lib/gen-monad/laziness000-weakmemo/run | 6 ++++ .../laziness000-weakmemo/use-gen.ipkg | 6 ++++ tests/lib/gen-monad/laziness000/UseGen.idr | 18 +++++++++++ tests/lib/gen-monad/laziness000/expected | 3 ++ tests/lib/gen-monad/laziness000/run | 6 ++++ tests/lib/gen-monad/laziness000/use-gen.ipkg | 6 ++++ .../gen-monad/laziness001-weakmemo/UseGen.idr | 22 +++++++++++++ .../gen-monad/laziness001-weakmemo/expected | 4 +++ tests/lib/gen-monad/laziness001-weakmemo/run | 6 ++++ .../laziness001-weakmemo/use-gen.ipkg | 6 ++++ tests/lib/gen-monad/laziness001/use-gen.ipkg | 2 -- .../gen-monad/laziness002-weakmemo/UseGen.idr | 26 ++++++++++++++++ .../gen-monad/laziness002-weakmemo/expected | 7 +++++ tests/lib/gen-monad/laziness002-weakmemo/run | 6 ++++ .../laziness002-weakmemo/use-gen.ipkg | 6 ++++ tests/lib/gen-monad/laziness002/use-gen.ipkg | 2 -- .../gen-monad/laziness003-weakmemo/UseGen.idr | 31 +++++++++++++++++++ .../gen-monad/laziness003-weakmemo/expected | 11 +++++++ tests/lib/gen-monad/laziness003-weakmemo/run | 6 ++++ .../laziness003-weakmemo/use-gen.ipkg | 6 ++++ tests/lib/gen-monad/laziness003/use-gen.ipkg | 2 -- .../ne-laziness000-weakmemo/UseGen.idr | 19 ++++++++++++ .../ne-laziness000-weakmemo/expected | 3 ++ .../lib/gen-monad/ne-laziness000-weakmemo/run | 6 ++++ .../ne-laziness000-weakmemo/use-gen.ipkg | 6 ++++ tests/lib/gen-monad/ne-laziness000/UseGen.idr | 17 ++++++++++ tests/lib/gen-monad/ne-laziness000/expected | 13 ++++++++ tests/lib/gen-monad/ne-laziness000/run | 6 ++++ .../lib/gen-monad/ne-laziness000/use-gen.ipkg | 6 ++++ .../ne-laziness001-weakmemo/UseGen.idr | 20 ++++++++++++ .../ne-laziness001-weakmemo/expected | 4 +++ .../lib/gen-monad/ne-laziness001-weakmemo/run | 6 ++++ .../ne-laziness001-weakmemo/use-gen.ipkg | 6 ++++ .../lib/gen-monad/ne-laziness001/use-gen.ipkg | 2 -- .../ne-laziness002-weakmemo/UseGen.idr | 23 ++++++++++++++ .../ne-laziness002-weakmemo/expected | 6 ++++ .../lib/gen-monad/ne-laziness002-weakmemo/run | 6 ++++ .../ne-laziness002-weakmemo/use-gen.ipkg | 6 ++++ .../lib/gen-monad/ne-laziness002/use-gen.ipkg | 2 -- tests/lib/gen-monad/pick-001/use-gen.ipkg | 2 -- tests/lib/gen-monad/use-gen-000/use-gen.ipkg | 2 -- tests/lib/gen-monad/use-gen-001/use-gen.ipkg | 2 -- .../use-gen-002/deptycheck-usage.ipkg | 2 -- 45 files changed, 358 insertions(+), 18 deletions(-) create mode 100644 tests/lib/gen-monad/laziness000-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/laziness000-weakmemo/expected create mode 100755 tests/lib/gen-monad/laziness000-weakmemo/run create mode 100644 tests/lib/gen-monad/laziness000-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/laziness000/UseGen.idr create mode 100644 tests/lib/gen-monad/laziness000/expected create mode 100755 tests/lib/gen-monad/laziness000/run create mode 100644 tests/lib/gen-monad/laziness000/use-gen.ipkg create mode 100644 tests/lib/gen-monad/laziness001-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/laziness001-weakmemo/expected create mode 100755 tests/lib/gen-monad/laziness001-weakmemo/run create mode 100644 tests/lib/gen-monad/laziness001-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/laziness002-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/laziness002-weakmemo/expected create mode 100755 tests/lib/gen-monad/laziness002-weakmemo/run create mode 100644 tests/lib/gen-monad/laziness002-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/laziness003-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/laziness003-weakmemo/expected create mode 100755 tests/lib/gen-monad/laziness003-weakmemo/run create mode 100644 tests/lib/gen-monad/laziness003-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/ne-laziness000-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/ne-laziness000-weakmemo/expected create mode 100755 tests/lib/gen-monad/ne-laziness000-weakmemo/run create mode 100644 tests/lib/gen-monad/ne-laziness000-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/ne-laziness000/UseGen.idr create mode 100644 tests/lib/gen-monad/ne-laziness000/expected create mode 100755 tests/lib/gen-monad/ne-laziness000/run create mode 100644 tests/lib/gen-monad/ne-laziness000/use-gen.ipkg create mode 100644 tests/lib/gen-monad/ne-laziness001-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/ne-laziness001-weakmemo/expected create mode 100755 tests/lib/gen-monad/ne-laziness001-weakmemo/run create mode 100644 tests/lib/gen-monad/ne-laziness001-weakmemo/use-gen.ipkg create mode 100644 tests/lib/gen-monad/ne-laziness002-weakmemo/UseGen.idr create mode 100644 tests/lib/gen-monad/ne-laziness002-weakmemo/expected create mode 100755 tests/lib/gen-monad/ne-laziness002-weakmemo/run create mode 100644 tests/lib/gen-monad/ne-laziness002-weakmemo/use-gen.ipkg diff --git a/tests/lib/gen-monad/laziness000-weakmemo/UseGen.idr b/tests/lib/gen-monad/laziness000-weakmemo/UseGen.idr new file mode 100644 index 000000000..0c17428d9 --- /dev/null +++ b/tests/lib/gen-monad/laziness000-weakmemo/UseGen.idr @@ -0,0 +1,20 @@ +module UseGen + +import Data.List.Lazy + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen MaybeEmpty Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 ] + +main : IO Unit +main = putStrLn $ show $ unGenTryN 10 someStdGen g diff --git a/tests/lib/gen-monad/laziness000-weakmemo/expected b/tests/lib/gen-monad/laziness000-weakmemo/expected new file mode 100644 index 000000000..6c5e09eba --- /dev/null +++ b/tests/lib/gen-monad/laziness000-weakmemo/expected @@ -0,0 +1,3 @@ +pure 6 +--- outmost gen --- +[6, 6, 6, 6, 6, 6, 6, 6, 6, 6] diff --git a/tests/lib/gen-monad/laziness000-weakmemo/run b/tests/lib/gen-monad/laziness000-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/laziness000-weakmemo/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/gen-monad/laziness000-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/laziness000-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/laziness000-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/laziness000/UseGen.idr b/tests/lib/gen-monad/laziness000/UseGen.idr new file mode 100644 index 000000000..a1bda7261 --- /dev/null +++ b/tests/lib/gen-monad/laziness000/UseGen.idr @@ -0,0 +1,18 @@ +module UseGen + +import Data.List.Lazy + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +g : Gen MaybeEmpty Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 ] + +main : IO Unit +main = putStrLn $ show $ unGenTryN 10 someStdGen g diff --git a/tests/lib/gen-monad/laziness000/expected b/tests/lib/gen-monad/laziness000/expected new file mode 100644 index 000000000..6c5e09eba --- /dev/null +++ b/tests/lib/gen-monad/laziness000/expected @@ -0,0 +1,3 @@ +pure 6 +--- outmost gen --- +[6, 6, 6, 6, 6, 6, 6, 6, 6, 6] diff --git a/tests/lib/gen-monad/laziness000/run b/tests/lib/gen-monad/laziness000/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/laziness000/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/gen-monad/laziness000/use-gen.ipkg b/tests/lib/gen-monad/laziness000/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/laziness000/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/laziness001-weakmemo/UseGen.idr b/tests/lib/gen-monad/laziness001-weakmemo/UseGen.idr new file mode 100644 index 000000000..9d08f6247 --- /dev/null +++ b/tests/lib/gen-monad/laziness001-weakmemo/UseGen.idr @@ -0,0 +1,22 @@ +module UseGen + +import Data.List.Lazy + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen MaybeEmpty Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 + , pure $ trace "pure 5" 5 + ] + +main : IO Unit +main = putStrLn $ show $ unGenTryN 10 someStdGen g diff --git a/tests/lib/gen-monad/laziness001-weakmemo/expected b/tests/lib/gen-monad/laziness001-weakmemo/expected new file mode 100644 index 000000000..5f83da579 --- /dev/null +++ b/tests/lib/gen-monad/laziness001-weakmemo/expected @@ -0,0 +1,4 @@ +pure 6 +--- outmost gen --- +pure 5 +[5, 6, 6, 6, 6, 5, 5, 5, 5, 5] diff --git a/tests/lib/gen-monad/laziness001-weakmemo/run b/tests/lib/gen-monad/laziness001-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/laziness001-weakmemo/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/gen-monad/laziness001-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/laziness001-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/laziness001-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/laziness001/use-gen.ipkg b/tests/lib/gen-monad/laziness001/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/laziness001/use-gen.ipkg +++ b/tests/lib/gen-monad/laziness001/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/laziness002-weakmemo/UseGen.idr b/tests/lib/gen-monad/laziness002-weakmemo/UseGen.idr new file mode 100644 index 000000000..9d41404e4 --- /dev/null +++ b/tests/lib/gen-monad/laziness002-weakmemo/UseGen.idr @@ -0,0 +1,26 @@ +module UseGen + +import Data.List.Lazy + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen MaybeEmpty Nat +g = trace "--- outmost gen ---" $ oneOf + [ oneOf $ trace "-- list with pure 4, 5, 6 --" + [ pure $ trace "pure 4" 4 + , pure $ trace "pure 5" 5 + , pure $ trace "pure 6" 6 + ] + , pure $ trace "pure 7" 7 + ] + +main : IO Unit +main = putStrLn $ show $ unGenTryN 10 someStdGen g diff --git a/tests/lib/gen-monad/laziness002-weakmemo/expected b/tests/lib/gen-monad/laziness002-weakmemo/expected new file mode 100644 index 000000000..a9116734e --- /dev/null +++ b/tests/lib/gen-monad/laziness002-weakmemo/expected @@ -0,0 +1,7 @@ +-- list with pure 4, 5, 6 -- +pure 4 +--- outmost gen --- +pure 7 +pure 5 +pure 6 +[7, 4, 4, 7, 7, 7, 7, 7, 5, 7] diff --git a/tests/lib/gen-monad/laziness002-weakmemo/run b/tests/lib/gen-monad/laziness002-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/laziness002-weakmemo/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/gen-monad/laziness002-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/laziness002-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/laziness002-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/laziness002/use-gen.ipkg b/tests/lib/gen-monad/laziness002/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/laziness002/use-gen.ipkg +++ b/tests/lib/gen-monad/laziness002/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/laziness003-weakmemo/UseGen.idr b/tests/lib/gen-monad/laziness003-weakmemo/UseGen.idr new file mode 100644 index 000000000..ea8852b52 --- /dev/null +++ b/tests/lib/gen-monad/laziness003-weakmemo/UseGen.idr @@ -0,0 +1,31 @@ +module UseGen + +import Data.List.Lazy + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen MaybeEmpty Nat +g = trace "--- outmost gen ---" $ oneOf + [ oneOf $ trace "-- list with pure 4, 5 --" + [ pure $ trace "pure 4" 4 + , pure $ trace "pure 5" 5 + , oneOf $ trace "- inner actually empty list -" + [ trace "1st empty" empty + , trace "2nd empty" empty + , trace "3rd empty" empty + , trace "4th empty" empty + ] + ] + , pure $ trace "pure 7" 7 + ] + +main : IO Unit +main = putStrLn $ show $ unGenTryN 10 someStdGen g diff --git a/tests/lib/gen-monad/laziness003-weakmemo/expected b/tests/lib/gen-monad/laziness003-weakmemo/expected new file mode 100644 index 000000000..462e0432b --- /dev/null +++ b/tests/lib/gen-monad/laziness003-weakmemo/expected @@ -0,0 +1,11 @@ +-- list with pure 4, 5 -- +pure 4 +--- outmost gen --- +pure 7 +pure 5 +- inner actually empty list - +1st empty +2nd empty +3rd empty +4th empty +[7, 4, 4, 7, 7, 7, 7, 7, 5, 7] diff --git a/tests/lib/gen-monad/laziness003-weakmemo/run b/tests/lib/gen-monad/laziness003-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/laziness003-weakmemo/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/gen-monad/laziness003-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/laziness003-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/laziness003-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/laziness003/use-gen.ipkg b/tests/lib/gen-monad/laziness003/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/laziness003/use-gen.ipkg +++ b/tests/lib/gen-monad/laziness003/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/ne-laziness000-weakmemo/UseGen.idr b/tests/lib/gen-monad/ne-laziness000-weakmemo/UseGen.idr new file mode 100644 index 000000000..141019eec --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000-weakmemo/UseGen.idr @@ -0,0 +1,19 @@ +module UseGen + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen1 Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 + ] + +main : IO Unit +main = putStrLn $ show $ take 10 $ unGenAll someStdGen g diff --git a/tests/lib/gen-monad/ne-laziness000-weakmemo/expected b/tests/lib/gen-monad/ne-laziness000-weakmemo/expected new file mode 100644 index 000000000..f77a19036 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000-weakmemo/expected @@ -0,0 +1,3 @@ +--- outmost gen --- +pure 6 +[6, 6, 6, 6, 6, 6, 6, 6, 6, 6] diff --git a/tests/lib/gen-monad/ne-laziness000-weakmemo/run b/tests/lib/gen-monad/ne-laziness000-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000-weakmemo/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/gen-monad/ne-laziness000-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness000-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/ne-laziness000/UseGen.idr b/tests/lib/gen-monad/ne-laziness000/UseGen.idr new file mode 100644 index 000000000..35d25a725 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000/UseGen.idr @@ -0,0 +1,17 @@ +module UseGen + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +g : Gen1 Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 + ] + +main : IO Unit +main = putStrLn $ show $ take 10 $ unGenAll someStdGen g diff --git a/tests/lib/gen-monad/ne-laziness000/expected b/tests/lib/gen-monad/ne-laziness000/expected new file mode 100644 index 000000000..777d19609 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000/expected @@ -0,0 +1,13 @@ +--- outmost gen --- +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +pure 6 +[6, 6, 6, 6, 6, 6, 6, 6, 6, 6] diff --git a/tests/lib/gen-monad/ne-laziness000/run b/tests/lib/gen-monad/ne-laziness000/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000/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/gen-monad/ne-laziness000/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness000/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness000/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/ne-laziness001-weakmemo/UseGen.idr b/tests/lib/gen-monad/ne-laziness001-weakmemo/UseGen.idr new file mode 100644 index 000000000..5992c70c7 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness001-weakmemo/UseGen.idr @@ -0,0 +1,20 @@ +module UseGen + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen1 Nat +g = trace "--- outmost gen ---" $ oneOf + [ pure $ trace "pure 6" 6 + , pure $ trace "pure 5" 5 + ] + +main : IO Unit +main = putStrLn $ show $ take 10 $ unGenAll someStdGen g diff --git a/tests/lib/gen-monad/ne-laziness001-weakmemo/expected b/tests/lib/gen-monad/ne-laziness001-weakmemo/expected new file mode 100644 index 000000000..885368ff6 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness001-weakmemo/expected @@ -0,0 +1,4 @@ +--- outmost gen --- +pure 5 +pure 6 +[5, 6, 6, 6, 6, 5, 5, 5, 5, 5] diff --git a/tests/lib/gen-monad/ne-laziness001-weakmemo/run b/tests/lib/gen-monad/ne-laziness001-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness001-weakmemo/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/gen-monad/ne-laziness001-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness001-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness001-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/ne-laziness001/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness001/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/ne-laziness001/use-gen.ipkg +++ b/tests/lib/gen-monad/ne-laziness001/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/ne-laziness002-weakmemo/UseGen.idr b/tests/lib/gen-monad/ne-laziness002-weakmemo/UseGen.idr new file mode 100644 index 000000000..310302237 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness002-weakmemo/UseGen.idr @@ -0,0 +1,23 @@ +module UseGen + +import Debug.Trace + +import Test.DepTyCheck.Gen + +import System.Random.Pure.StdGen + +%default total + +%cg chez lazy=weakMemo + +g : Gen1 Nat +g = trace "--- outmost gen ---" $ oneOf + [ oneOf $ trace "list with pure 4 and 5" + [ pure $ trace "pure 4" 4 + , pure $ trace "pure 5" 5 + ] + , pure $ trace "pure 6" 6 + ] + +main : IO Unit +main = putStrLn $ show $ take 10 $ unGenAll someStdGen g diff --git a/tests/lib/gen-monad/ne-laziness002-weakmemo/expected b/tests/lib/gen-monad/ne-laziness002-weakmemo/expected new file mode 100644 index 000000000..0af078bb7 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness002-weakmemo/expected @@ -0,0 +1,6 @@ +--- outmost gen --- +pure 6 +list with pure 4 and 5 +pure 4 +pure 5 +[6, 4, 4, 6, 6, 6, 6, 6, 5, 6] diff --git a/tests/lib/gen-monad/ne-laziness002-weakmemo/run b/tests/lib/gen-monad/ne-laziness002-weakmemo/run new file mode 100755 index 000000000..55f2037b5 --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness002-weakmemo/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/gen-monad/ne-laziness002-weakmemo/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness002-weakmemo/use-gen.ipkg new file mode 100644 index 000000000..5bdbbaa8e --- /dev/null +++ b/tests/lib/gen-monad/ne-laziness002-weakmemo/use-gen.ipkg @@ -0,0 +1,6 @@ +package dummy + +main = UseGen +executable = use-gen + +depends = deptycheck diff --git a/tests/lib/gen-monad/ne-laziness002/use-gen.ipkg b/tests/lib/gen-monad/ne-laziness002/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/ne-laziness002/use-gen.ipkg +++ b/tests/lib/gen-monad/ne-laziness002/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/pick-001/use-gen.ipkg b/tests/lib/gen-monad/pick-001/use-gen.ipkg index d71bc8f30..5bdbbaa8e 100644 --- a/tests/lib/gen-monad/pick-001/use-gen.ipkg +++ b/tests/lib/gen-monad/pick-001/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = use-gen diff --git a/tests/lib/gen-monad/use-gen-000/use-gen.ipkg b/tests/lib/gen-monad/use-gen-000/use-gen.ipkg index f74ca0fda..29bedee79 100644 --- a/tests/lib/gen-monad/use-gen-000/use-gen.ipkg +++ b/tests/lib/gen-monad/use-gen-000/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - modules = UseGen opts = "--no-color --console-width 0" diff --git a/tests/lib/gen-monad/use-gen-001/use-gen.ipkg b/tests/lib/gen-monad/use-gen-001/use-gen.ipkg index ccb837730..7faf00c5f 100644 --- a/tests/lib/gen-monad/use-gen-001/use-gen.ipkg +++ b/tests/lib/gen-monad/use-gen-001/use-gen.ipkg @@ -1,7 +1,5 @@ package dummy -authors = "Denis Buzdalov" - main = UseGen executable = a-test diff --git a/tests/lib/gen-monad/use-gen-002/deptycheck-usage.ipkg b/tests/lib/gen-monad/use-gen-002/deptycheck-usage.ipkg index 4e61381aa..60c18fdeb 100644 --- a/tests/lib/gen-monad/use-gen-002/deptycheck-usage.ipkg +++ b/tests/lib/gen-monad/use-gen-002/deptycheck-usage.ipkg @@ -1,7 +1,5 @@ package deptycheck-usage -authors = "Denis Buzdalov" - sourcedir = "src" depends = deptycheck From 85e23c7c400cc595a8440649e40110049d8e70ee Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 11 Nov 2024 21:49:53 +0300 Subject: [PATCH 2/2] [ breaking, cleanup ] Remove now unused `simplificationHack` derivator's option --- docs/source/explanation/specifications/experiments.md | 5 ++++- examples/pil-fun/src/Language/PilFun/Derived.idr | 2 -- examples/pil-fun/src/Language/PilFun/Pretty/Derived.idr | 2 -- examples/sorted-list-so-comp/src/Data/List/Sorted/Gen.idr | 4 ---- examples/sorted-list-so-full/src/Data/List/Sorted/Gen.idr | 4 ---- examples/sorted-list-tl-pred/src/Data/List/Sorted/Gen.idr | 4 ---- examples/sorted-tree-indexed/src/Data/SortedBinTree/Gen.idr | 4 ---- examples/sorted-tree-naive/src/Data/SortedBinTree/Gen.idr | 4 ---- examples/uniq-list/src/Data/List/Uniq/Gen.idr | 4 ---- examples/uniq-list/src/Data/Vect/Uniq/Gen.idr | 4 ---- src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr | 2 +- tests/derivation/_common/derive.ipkg | 2 -- .../distribution/dependent-rec-sh-001/CheckDistribution.idr | 2 -- .../distribution/dependent-rec-sh-002/CheckDistribution.idr | 2 -- tests/derivation/inputvalidation/_common/validate-input.ipkg | 2 -- tests/derivation/utils/arg-deps/_common/arg-deps.ipkg | 2 -- tests/derivation/utils/canonicsig/_common/canonic-sig.ipkg | 2 -- .../utils/cons-analysis/_common-deep-cons-app/cons.ipkg | 2 -- .../utils/involved-types/_common-involved-types/inv-ty.ipkg | 2 -- .../up-to-renaming-ttimp-eq/_common/renaming-ttimp-eq.ipkg | 2 -- tests/docs/readme/test.ipkg | 2 -- 21 files changed, 5 insertions(+), 54 deletions(-) diff --git a/docs/source/explanation/specifications/experiments.md b/docs/source/explanation/specifications/experiments.md index 299371030..6fab13f93 100644 --- a/docs/source/explanation/specifications/experiments.md +++ b/docs/source/explanation/specifications/experiments.md @@ -14,7 +14,8 @@ import Deriving.DepTyCheck.Gen deriveGen : a --> -```idris + +``` idris %language ElabReflection %hint @@ -24,6 +25,8 @@ UsedConstructorDerivator = LeastEffort {simplificationHack = True} The version of the compiler used is `https://github.com/buzden/Idris2/commit/9ab96dacd4f855674028d68de0a013ac7926c73d`. +Please, notice that used settings may fail typechecking with the most recent versions of the compiler and library. + ## Constructors In the first experiment, it is found out how the number of constructors affects the derivation time. diff --git a/examples/pil-fun/src/Language/PilFun/Derived.idr b/examples/pil-fun/src/Language/PilFun/Derived.idr index 0885aa2c1..d365a1775 100644 --- a/examples/pil-fun/src/Language/PilFun/Derived.idr +++ b/examples/pil-fun/src/Language/PilFun/Derived.idr @@ -8,6 +8,4 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint LE : ConstructorDerivator; LE = LeastEffort {simplificationHack = True} - Language.PilFun.genStmts = deriveGen diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Derived.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Derived.idr index b2322bbf9..99945a6a2 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Derived.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Derived.idr @@ -8,6 +8,4 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint LE : ConstructorDerivator; LE = LeastEffort {simplificationHack = True} - Language.PilFun.Pretty.rawNewName = deriveGen diff --git a/examples/sorted-list-so-comp/src/Data/List/Sorted/Gen.idr b/examples/sorted-list-so-comp/src/Data/List/Sorted/Gen.idr index ca0e5d33a..52c55e147 100644 --- a/examples/sorted-list-so-comp/src/Data/List/Sorted/Gen.idr +++ b/examples/sorted-list-so-comp/src/Data/List/Sorted/Gen.idr @@ -9,10 +9,6 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - export genSortedList : Fuel -> Gen MaybeEmpty SortedList genSortedList = deriveGen diff --git a/examples/sorted-list-so-full/src/Data/List/Sorted/Gen.idr b/examples/sorted-list-so-full/src/Data/List/Sorted/Gen.idr index ca0e5d33a..52c55e147 100644 --- a/examples/sorted-list-so-full/src/Data/List/Sorted/Gen.idr +++ b/examples/sorted-list-so-full/src/Data/List/Sorted/Gen.idr @@ -9,10 +9,6 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - export genSortedList : Fuel -> Gen MaybeEmpty SortedList genSortedList = deriveGen diff --git a/examples/sorted-list-tl-pred/src/Data/List/Sorted/Gen.idr b/examples/sorted-list-tl-pred/src/Data/List/Sorted/Gen.idr index ca0e5d33a..52c55e147 100644 --- a/examples/sorted-list-tl-pred/src/Data/List/Sorted/Gen.idr +++ b/examples/sorted-list-tl-pred/src/Data/List/Sorted/Gen.idr @@ -9,10 +9,6 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - export genSortedList : Fuel -> Gen MaybeEmpty SortedList genSortedList = deriveGen diff --git a/examples/sorted-tree-indexed/src/Data/SortedBinTree/Gen.idr b/examples/sorted-tree-indexed/src/Data/SortedBinTree/Gen.idr index 9f42c73c0..99cfa87be 100644 --- a/examples/sorted-tree-indexed/src/Data/SortedBinTree/Gen.idr +++ b/examples/sorted-tree-indexed/src/Data/SortedBinTree/Gen.idr @@ -9,10 +9,6 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - export genSortedBinTree1 : Fuel -> Gen MaybeEmpty (mi ** ma ** SortedBinTree1 mi ma) genSortedBinTree1 = deriveGen diff --git a/examples/sorted-tree-naive/src/Data/SortedBinTree/Gen.idr b/examples/sorted-tree-naive/src/Data/SortedBinTree/Gen.idr index ae6c2baed..18abe3342 100644 --- a/examples/sorted-tree-naive/src/Data/SortedBinTree/Gen.idr +++ b/examples/sorted-tree-naive/src/Data/SortedBinTree/Gen.idr @@ -9,10 +9,6 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - export genSortedBinTree : Fuel -> Gen MaybeEmpty SortedBinTree genSortedBinTree = deriveGen diff --git a/examples/uniq-list/src/Data/List/Uniq/Gen.idr b/examples/uniq-list/src/Data/List/Uniq/Gen.idr index f409e21d1..5546fa5a1 100644 --- a/examples/uniq-list/src/Data/List/Uniq/Gen.idr +++ b/examples/uniq-list/src/Data/List/Uniq/Gen.idr @@ -9,8 +9,4 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - Data.List.Uniq.genUniqStrList = deriveGen diff --git a/examples/uniq-list/src/Data/Vect/Uniq/Gen.idr b/examples/uniq-list/src/Data/Vect/Uniq/Gen.idr index 0c8d080ac..d1e52f9ef 100644 --- a/examples/uniq-list/src/Data/Vect/Uniq/Gen.idr +++ b/examples/uniq-list/src/Data/Vect/Uniq/Gen.idr @@ -9,8 +9,4 @@ import Deriving.DepTyCheck.Gen %logging "deptycheck.derive" 5 -%hint -UsedConstructorDerivator : ConstructorDerivator -UsedConstructorDerivator = LeastEffort {simplificationHack = True} - Data.Vect.Uniq.genUniqStrVect = deriveGen diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index c2da91cee..9da3811c5 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -201,7 +201,7 @@ namespace NonObligatoryExts ||| It is seemingly most simple to implement, maybe the fastest and ||| fits well when external generators are provided for non-dependent types. export - [LeastEffort] {default False simplificationHack : Bool} -> ConstructorDerivator where + [LeastEffort] ConstructorDerivator where consGenExpr sig con givs fuel = do -- Prepare local search context diff --git a/tests/derivation/_common/derive.ipkg b/tests/derivation/_common/derive.ipkg index 829660105..6a01abc87 100644 --- a/tests/derivation/_common/derive.ipkg +++ b/tests/derivation/_common/derive.ipkg @@ -1,7 +1,5 @@ package derive-test -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/distribution/dependent-rec-sh-001/CheckDistribution.idr b/tests/derivation/distribution/dependent-rec-sh-001/CheckDistribution.idr index 8e607986d..37e9de804 100644 --- a/tests/derivation/distribution/dependent-rec-sh-001/CheckDistribution.idr +++ b/tests/derivation/distribution/dependent-rec-sh-001/CheckDistribution.idr @@ -6,8 +6,6 @@ import DistrCheckCommon %default total -%hint DA : ConstructorDerivator; DA = LeastEffort {simplificationHack=True} - data ListNat : Type data Constraint : ListNat -> Type diff --git a/tests/derivation/distribution/dependent-rec-sh-002/CheckDistribution.idr b/tests/derivation/distribution/dependent-rec-sh-002/CheckDistribution.idr index c72076850..e9e899319 100644 --- a/tests/derivation/distribution/dependent-rec-sh-002/CheckDistribution.idr +++ b/tests/derivation/distribution/dependent-rec-sh-002/CheckDistribution.idr @@ -6,8 +6,6 @@ import DistrCheckCommon %default total -%hint DA : ConstructorDerivator; DA = LeastEffort {simplificationHack=True} - data ListNat : Type data Constraint : Nat -> ListNat -> Type diff --git a/tests/derivation/inputvalidation/_common/validate-input.ipkg b/tests/derivation/inputvalidation/_common/validate-input.ipkg index f477a9c94..438e03ad7 100644 --- a/tests/derivation/inputvalidation/_common/validate-input.ipkg +++ b/tests/derivation/inputvalidation/_common/validate-input.ipkg @@ -1,7 +1,5 @@ package validate-input -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/utils/arg-deps/_common/arg-deps.ipkg b/tests/derivation/utils/arg-deps/_common/arg-deps.ipkg index 7e2c850f4..32599e2f3 100644 --- a/tests/derivation/utils/arg-deps/_common/arg-deps.ipkg +++ b/tests/derivation/utils/arg-deps/_common/arg-deps.ipkg @@ -1,7 +1,5 @@ package arg-deps -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/utils/canonicsig/_common/canonic-sig.ipkg b/tests/derivation/utils/canonicsig/_common/canonic-sig.ipkg index cfdc1c590..0b2820f23 100644 --- a/tests/derivation/utils/canonicsig/_common/canonic-sig.ipkg +++ b/tests/derivation/utils/canonicsig/_common/canonic-sig.ipkg @@ -1,7 +1,5 @@ package canonic-sig -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/utils/cons-analysis/_common-deep-cons-app/cons.ipkg b/tests/derivation/utils/cons-analysis/_common-deep-cons-app/cons.ipkg index 7e2c850f4..32599e2f3 100644 --- a/tests/derivation/utils/cons-analysis/_common-deep-cons-app/cons.ipkg +++ b/tests/derivation/utils/cons-analysis/_common-deep-cons-app/cons.ipkg @@ -1,7 +1,5 @@ package arg-deps -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/utils/involved-types/_common-involved-types/inv-ty.ipkg b/tests/derivation/utils/involved-types/_common-involved-types/inv-ty.ipkg index 0fa9a8dca..5839e0fa5 100644 --- a/tests/derivation/utils/involved-types/_common-involved-types/inv-ty.ipkg +++ b/tests/derivation/utils/involved-types/_common-involved-types/inv-ty.ipkg @@ -1,7 +1,5 @@ package inv-tys -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/derivation/utils/up-to-renaming-ttimp-eq/_common/renaming-ttimp-eq.ipkg b/tests/derivation/utils/up-to-renaming-ttimp-eq/_common/renaming-ttimp-eq.ipkg index c25163c73..cbbdf8b44 100644 --- a/tests/derivation/utils/up-to-renaming-ttimp-eq/_common/renaming-ttimp-eq.ipkg +++ b/tests/derivation/utils/up-to-renaming-ttimp-eq/_common/renaming-ttimp-eq.ipkg @@ -1,7 +1,5 @@ package renaming-ttimp-eq -authors = "Denis Buzdalov" - opts = "--no-color --console-width 0" depends = deptycheck diff --git a/tests/docs/readme/test.ipkg b/tests/docs/readme/test.ipkg index d9db1f696..5feb1f608 100644 --- a/tests/docs/readme/test.ipkg +++ b/tests/docs/readme/test.ipkg @@ -1,5 +1,3 @@ package test -authors = "Denis Buzdalov" - depends = deptycheck