[ unfinished ] Add a relative weight distribution test

examples/sorted-tree-indexed/tests/gens/_common/DistrCheckCommon.idr

@@ -0,0 +1,28 @@
+module DistrCheckCommon
+
+import Data.List.Lazy
+
+import public Test.DepTyCheck.Gen
+
+import public Statistics.Norm.Precise
+import public Statistics.Confidence
+
+import System.Random.Pure.StdGen
+
+%default total
+
+find : LazyList (Vect n SignificantBounds) -> Maybe $ Vect n SignificantBounds
+find [] = Nothing
+find (x::xs) = case force xs of
+                 [] => Just x
+                 xs => if all isOk x then Just x else assert_total $ find xs
+
+verdict : Vect n (CoverageTest a) -> Gen em a -> Maybe $ Vect n SignificantBounds
+verdict conds = find . mapMaybe sequence .
+                  checkCoverageConditions conds . unGenTryN 10000000 someStdGen
+
+Show SignificantBounds where show = interpolate
+
+export
+printVerdict : HasIO m => Gen em a -> Vect n (CoverageTest a) -> m ()
+printVerdict = putStrLn .: show .: flip verdict

examples/sorted-tree-indexed/tests/gens/_common/run

@@ -0,0 +1,6 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+pack exec CheckDistribution.idr
+
+rm -rf build

examples/sorted-tree-indexed/tests/gens/_common/test.ipkg

@@ -0,0 +1,5 @@
+package test
+
+main = CheckDistribution
+
+depends = deptycheck, summary-stat

examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/CheckDistribution.idr

@@ -0,0 +1,24 @@
+module CheckDistribution
+
+import Data.SortedBinTree.Gen
+
+import Deriving.DepTyCheck.Gen
+
+import DistrCheckCommon
+
+%default total
+
+%language ElabReflection
+
+-- Check how weights of subtrees are related between left and right subtree of a root
+
+mainFor : (depth : Nat) -> IO ()
+mainFor depth = printVerdict (genSortedBinTree1 $ limit depth) $ fromList
+                  $ [ coverWith (ratio 1 $ S depth) ((== n) . length) | n <- [0 .. depth] ]
+
+main : IO ()
+main = do
+  mainFor 0
+  mainFor 1
+  mainFor 2
+  mainFor 7

examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr

examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/expected

@@ -0,0 +1,4 @@
+Just [ok]
+Just [ok, ok]
+Just [ok, ok, ok]
+Just [ok, ok, ok, ok, ok, ok, ok, ok]

examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/run

@@ -0,0 +1 @@
+../_common/run

examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/test.ipkg

@@ -0,0 +1,5 @@
+package test
+
+main = CheckDistribution
+
+depends = deptycheck, sorted-tree-indexed, summary-stat