[ test, distr ] Add a relative weight distribution test

examples/sorted-tree-indexed/src/Data/SortedBinTree.idr

@@ -15,6 +15,11 @@ toList : SortedBinTree1 mi ma -> List Nat
 toList (Leaf x)          = [x]
 toList (Node left right) = toList left ++ toList right
 
+export
+weight : SortedBinTree1 mi ma -> Nat
+weight $ Leaf x = 1
+weight $ Node l r = 1 + weight l + weight r
+
 export
 Interpolation (SortedBinTree1 mi ma) where
   interpolate $ Leaf x = "\{show x}"

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

@@ -0,0 +1,34 @@
+module CheckDistribution
+
+import Data.DPair
+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
+
+getLR : (mi ** ma ** SortedBinTree1 mi ma) -> Maybe $ let t = Exists $ Exists . SortedBinTree1 in (t, t)
+getLR (_ ** _ ** Leaf {}) = Nothing
+getLR (_ ** _ ** Node l r) = Just (Evidence _ $ Evidence _ l, Evidence _ $ Evidence _ r)
+
+mainFor : (depth : Nat) -> IO ()
+mainFor depth = printVerdict' getLR (genSortedBinTree1 $ limit depth) $ fromList
+                  $ [ coverWith 1 (\(l, r) => weight l.snd.snd `f` weight r.snd.snd)
+                    | (r, f) <-
+                      [ (ratio 1 2, (>))
+                      , (ratio 1 10, (==))
+                      , (ratio 1 2, (<))
+                      ]
+                    ]
+
+main : IO ()
+main = do
+  mainFor 2
+  mainFor 4
+  mainFor 6

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,3 @@
+Just [ok, ok, ok]
+Just [ok, ok, ok]
+Just [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