[ example ] Sorted tree examples improvements

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

@@ -1,6 +1,7 @@
 module Data.SortedBinTree
 
 import public Data.Nat
+import Data.String
 
 %default total
 
@@ -13,3 +14,22 @@ export
 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}"
+  interpolate $ Node l r = """
+    .
+    \{ind "|" $ interpolate l}
+    \{ind " " $ interpolate r}
+    """
+    where
+      ind : (pref : String) -> String -> String
+      ind k s = do
+        let f::fs = lines s | [] => ""
+        joinBy "\n" $ "|" :: ("|- " ++ f) :: (("\{k}  " ++) <$> fs)

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

examples/sorted-tree-indexed/tests/gens/sorted-big/Main.idr

@@ -0,0 +1,20 @@
+import Data.SortedBinTree.Gen
+import Data.Fuel
+import Data.List
+import Data.List.Lazy
+import Data.Primitives.Interpolation
+
+import System.Random.Pure.StdGen
+
+%default total
+
+main : IO ()
+main = do
+  let vals = unGenTryN 10 someStdGen $ genSortedBinTree1 $ limit 10
+  Lazy.for_ vals $ \(mi ** ma ** tree) => do
+    putStrLn "--------------"
+    let list = toList tree
+    putStrLn "min: \{mi}, max: \{ma}, length: \{length list}"
+    putStrLn "tree:\n\{tree}"
+    putStrLn "as list: \{show list}"
+    putStrLn "sorted: \{show $ sorted list}"