From c0080884d0c6760a789491f2f639a12f0978b674 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 29 Nov 2024 11:16:58 +0300
Subject: [PATCH] [ unfinished ] Add a relative weight distribution test

---
 .../tests/gens/_common/DistrCheckCommon.idr   | 28 +++++++++++++++++++
 .../tests/gens/_common/run                    |  6 ++++
 .../tests/gens/_common/test.ipkg              |  5 ++++
 .../CheckDistribution.idr                     | 24 ++++++++++++++++
 .../DistrCheckCommon.idr                      |  1 +
 .../distribution-relative-weight/expected     |  4 +++
 .../gens/distribution-relative-weight/run     |  1 +
 .../distribution-relative-weight/test.ipkg    |  5 ++++
 8 files changed, 74 insertions(+)
 create mode 100644 examples/sorted-tree-indexed/tests/gens/_common/DistrCheckCommon.idr
 create mode 100755 examples/sorted-tree-indexed/tests/gens/_common/run
 create mode 100644 examples/sorted-tree-indexed/tests/gens/_common/test.ipkg
 create mode 100644 examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/CheckDistribution.idr
 create mode 120000 examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/DistrCheckCommon.idr
 create mode 100644 examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/expected
 create mode 120000 examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/run
 create mode 100644 examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/test.ipkg

diff --git a/examples/sorted-tree-indexed/tests/gens/_common/DistrCheckCommon.idr b/examples/sorted-tree-indexed/tests/gens/_common/DistrCheckCommon.idr
new file mode 100644
index 000000000..b66f524ca
--- /dev/null
+++ b/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
diff --git a/examples/sorted-tree-indexed/tests/gens/_common/run b/examples/sorted-tree-indexed/tests/gens/_common/run
new file mode 100755
index 000000000..cda0cf801
--- /dev/null
+++ b/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
diff --git a/examples/sorted-tree-indexed/tests/gens/_common/test.ipkg b/examples/sorted-tree-indexed/tests/gens/_common/test.ipkg
new file mode 100644
index 000000000..b77b23f30
--- /dev/null
+++ b/examples/sorted-tree-indexed/tests/gens/_common/test.ipkg
@@ -0,0 +1,5 @@
+package test
+
+main = CheckDistribution
+
+depends = deptycheck, summary-stat
diff --git a/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/CheckDistribution.idr b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/CheckDistribution.idr
new file mode 100644
index 000000000..6e214cbf6
--- /dev/null
+++ b/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
diff --git a/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/DistrCheckCommon.idr b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/DistrCheckCommon.idr
new file mode 120000
index 000000000..97b34ad55
--- /dev/null
+++ b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/DistrCheckCommon.idr
@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr
\ No newline at end of file
diff --git a/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/expected b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/expected
new file mode 100644
index 000000000..2742003f6
--- /dev/null
+++ b/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]
diff --git a/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/run b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/run
new file mode 120000
index 000000000..805165988
--- /dev/null
+++ b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/run
@@ -0,0 +1 @@
+../_common/run
\ No newline at end of file
diff --git a/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/test.ipkg b/examples/sorted-tree-indexed/tests/gens/distribution-relative-weight/test.ipkg
new file mode 100644
index 000000000..c02bdac39
--- /dev/null
+++ b/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