Merge branch 'buzden:master' into remove-maybe-empty-deep

docs/source/explanation/specifications/experiments.md

@@ -14,7 +14,8 @@ import Deriving.DepTyCheck.Gen
 deriveGen : a
 -->
 
-```idris
+<!-- The code block above uses ```<space>idris intentionally, now this code does not compile and it's okay -->
+``` 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.

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

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

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

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

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

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

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

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

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

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

tests/derivation/_common/derive.ipkg

@@ -1,7 +1,5 @@
 package derive-test
 
-authors = "Denis Buzdalov"
-
 opts = "--no-color --console-width 0"
 
 depends = deptycheck

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
 

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
 

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

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

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

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

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

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

tests/docs/readme/test.ipkg

@@ -1,5 +1,3 @@
 package test
 
-authors = "Denis Buzdalov"
-
 depends = deptycheck

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

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]

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

tests/lib/gen-monad/laziness000-weakmemo/use-gen.ipkg

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

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

tests/lib/gen-monad/laziness000/expected

@@ -0,0 +1,3 @@
+pure 6
+--- outmost gen ---
+[6, 6, 6, 6, 6, 6, 6, 6, 6, 6]

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

tests/lib/gen-monad/laziness000/use-gen.ipkg

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

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

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]

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

tests/lib/gen-monad/laziness001-weakmemo/use-gen.ipkg

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

tests/lib/gen-monad/laziness001/use-gen.ipkg

@@ -1,7 +1,5 @@
 package dummy
 
-authors = "Denis Buzdalov"
-
 main = UseGen
 executable = use-gen
 

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

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]

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

tests/lib/gen-monad/laziness002-weakmemo/use-gen.ipkg

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

tests/lib/gen-monad/laziness002/use-gen.ipkg

@@ -1,7 +1,5 @@
 package dummy
 
-authors = "Denis Buzdalov"
-
 main = UseGen
 executable = use-gen