[ derive ] Implement a multi-stage (layered) algorithm of order search

deptycheck.ipkg

@@ -31,6 +31,7 @@ modules = Deriving.DepTyCheck
 depends = ansi
         , best-alternative
         , collection-utils
+        , cozippable
         , dependent-vect
         , elab-pretty
         , elab-util

examples/covering-seq/tests/gens/covering-seqs-long/Main.idr

@@ -0,0 +1,28 @@
+import Data.Fuel
+import Data.List
+import Data.List.Lazy
+import Data.List.Covering.Gen
+import Data.String
+
+import System.Random.Pure.StdGen
+
+%default total
+
+submain : {n : _} -> BitMask n -> IO ()
+submain bs = do
+  putStrLn "-----------------------"
+  putStrLn "bitmask: \{bs}"
+  putStrLn "-----------------------"
+  let vals = unGenTryN 10 someStdGen $ genCoveringSequence (limit $ 2 * n) bs
+  Lazy.for_ vals $ \v => do
+    let hits = hits v
+    let verdict = if sort hits == setBits bs then "ok" else "fail, hits are: \{show hits}, expected: \{show $ setBits bs}"
+    putStrLn "\{v} (\{verdict})"
+
+main : IO ()
+main = do
+  submain [True, True, True, True, True, True, True, True]
+  submain [True, False, True, True, True, True, True, True]
+  submain [True, False, True, False, True, False, True, False]
+  submain [False, False, True, False, False, False, False, False]
+  submain [False, False, False, False, False, False, False, False]

examples/covering-seq/tests/gens/covering-seqs-long/expected

@@ -0,0 +1,65 @@
+-----------------------
+bitmask: 11111111
+-----------------------
+10 0 [7] 14 [6] 7 6 13 [0] 5 8 [5] [4] [3] [2] [1] (ok)
+[6] [7] 3 16 2 11 [5] [4] 2 [3] [2] 1 [1] [0] 3 (ok)
+3 10 [7] 15 [6] 2 [5] [4] [3] 5 16 16 13 [2] [1] [0] (ok)
+10 [7] 11 7 [3] 6 1 8 2 12 [6] [5] [4] [2] [1] [0] (ok)
+[4] [7] [6] 2 [5] [3] [2] 1 [1] 14 15 6 13 3 3 [0] (ok)
+[6] [0] [7] [5] 10 [4] [3] [2] [1] 14 7 16 4 15 7 (ok)
+[5] [7] 7 7 9 [4] 3 [2] 2 6 [6] [3] 16 9 [1] [0] (ok)
+7 3 12 0 [4] [2] 13 [1] 8 4 [0] 2 [6] [7] [5] [3] (ok)
+9 [7] 4 [6] [5] [4] 12 12 14 [3] [2] 8 4 [1] [0] 6 (ok)
+2 [7] 4 8 11 [3] [6] 13 [5] [4] 10 [2] 0 2 [1] [0] (ok)
+-----------------------
+bitmask: 10111111
+-----------------------
+6 10 [7] 0 [6] 14 7 6 [0] 13 5 [5] [4] 11 [3] [2] (ok)
+[7] 16 [6] [5] 2 [4] [3] [2] [0] 11 2 (ok)
+16 3 10 15 2 5 16 [7] [4] [6] [5] [3] [2] 16 [0] 13 (ok)
+15 4 10 [7] 11 [6] [5] [4] [3] [2] 7 6 1 8 2 [0] (ok)
+[7] 1 [6] 14 15 [5] [4] [3] 6 [2] [0] 6 (ok)
+10 14 7 [6] [0] [7] [5] 16 [4] 4 15 7 0 [3] [2] 4 (ok)
+[5] [7] 0 7 7 [4] 9 [2] 3 2 [6] [3] 6 16 9 [0] (ok)
+12 [6] [3] 0 [5] [7] [4] 13 8 [2] 3 [0] (ok)
+4 [0] [7] 12 12 [6] 14 [3] 8 4 5 [5] 11 15 [4] [2] (ok)
+8 [7] [6] 11 13 10 [3] [5] [4] [2] 0 3 [0] 4 (ok)
+-----------------------
+bitmask: 10101010
+-----------------------
+7 6 [6] 13 5 [4] [2] 11 6 [0] 15 (ok)
+1 [6] [4] 6 [2] [0] 5 12 2 11 13 (ok)
+[2] [6] 2 5 [4] [0] 16 16 13 14 13 3 15 (ok)
+6 1 8 2 12 [6] [4] 12 16 [2] [0] 11 6 (ok)
+6 2 [4] 1 14 15 [6] 6 13 [2] 3 6 [0] 14 16 15 (ok)
+[0] [6] [4] 15 [2] 7 0 6 6 (ok)
+8 16 [0] 12 [6] [4] [2] 4 0 4 2 8 5 14 (ok)
+3 [6] 8 [4] [2] [0] 0 7 3 12 (ok)
+12 [6] 0 [4] 13 8 4 8 [2] 6 [0] (ok)
+14 [0] [6] 8 4 5 [4] 12 [2] 15 9 (ok)
+-----------------------
+bitmask: 00100000
+-----------------------
+7 6 [2] 13 5 11 13 14 0 (ok)
+16 [2] 2 11 2 1 6 5 12 2 11 14 7 (ok)
+16 11 1 16 3 10 15 [2] 2 5 16 16 13 14 13 (ok)
+[2] 6 14 16 15 4 10 11 7 6 1 8 5 (ok)
+[2] 6 (ok)
+6 [2] 2 1 14 5 (ok)
+[2] 15 7 0 6 4 14 6 (ok)
+3 2 [2] 6 16 8 16 12 4 0 4 2 8 5 10 13 (ok)
+8 8 [2] 15 7 3 4 0 3 8 0 2 (ok)
+16 13 15 [2] 10 7 3 12 8 (ok)
+-----------------------
+bitmask: 00000000
+-----------------------
+14 7 6 13 5 11 13 14 5 2 (ok)
+ (ok)
+1 6 5 12 2 0 16 (ok)
+2 1 (ok)
+16 11 1 16 3 10 15 2 5 16 16 13 14 13 0 16 (ok)
+6 14 16 15 4 10 11 7 6 1 8 5 (ok)
+15 6 6 (ok)
+14 7 16 4 15 7 0 6 4 14 13 6 0 1 (ok)
+6 16 8 16 12 4 0 4 2 7 (ok)
+7 7 (ok)

examples/covering-seq/tests/gens/covering-seqs-long/run

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

examples/covering-seq/tests/gens/covering-seqs-long/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+
+depends = covering-seq
+
+executable = a-test
+main = Main

examples/covering-seq/tests/gens/covering-seqs/expected

@@ -1,52 +1,52 @@
 -----------------------
 bitmask: 1111
 -----------------------
-3 3 [1] [3] [2] [0] 5 (ok)
-[2] [3] [1] [0] (ok)
-[3] [2] [1] 1 [0] 2 (ok)
-5 3 3 4 [3] [2] [1] [0] (ok)
-1 6 4 2 [3] [0] [2] [1] (ok)
-0 1 [3] [2] 7 [1] [0] (ok)
-8 5 [3] 5 [2] 7 [1] [0] (ok)
-[3] 7 [2] [1] 5 [0] 6 (ok)
-[3] [2] 5 [1] [0] (ok)
-[3] 4 [2] 3 [1] [0] 2 8 (ok)
+5 [2] 7 6 5 [1] [3] [0] (ok)
+4 [2] [3] [1] 0 [0] 6 6 (ok)
+4 [3] 3 [0] [2] 0 3 [1] (ok)
+1 [3] 0 8 1 [1] [2] [0] (ok)
+4 [3] [2] [1] 1 0 [0] (ok)
+[3] [2] 7 7 3 8 [1] [0] (ok)
+7 3 7 8 [3] [2] [1] [0] (ok)
+[3] 2 6 6 5 [2] [1] [0] (ok)
+1 [0] 1 5 7 [3] [2] [1] (ok)
+[3] 3 [2] [1] [0] 4 2 (ok)
 -----------------------
 bitmask: 1011
 -----------------------
-3 3 [3] 4 [2] [0] 5 (ok)
-[2] [3] [0] (ok)
-8 6 [0] [3] 2 [2] 6 (ok)
-[3] 3 4 6 1 8 [2] [0] (ok)
-[3] 5 0 [2] [0] 3 (ok)
-[3] 7 7 [2] [0] (ok)
-7 [3] 8 3 7 [2] [0] 7 (ok)
-[3] 8 [2] 0 0 5 [0] (ok)
-7 [3] [2] 3 8 8 [0] 4 (ok)
-[3] 4 [2] 5 [0] 4 2 6 (ok)
+7 [2] 6 7 5 [3] 0 [0] (ok)
+3 0 [3] [2] [0] (ok)
+[3] [2] 8 [0] 6 1 4 0 (ok)
+[3] 2 [0] 6 [2] 4 0 4 (ok)
+1 6 5 1 [3] 4 [2] [0] (ok)
+3 7 7 7 [3] 5 [2] [0] (ok)
+[3] [2] 5 7 [0] 6 8 (ok)
+1 [3] 0 2 6 [2] [0] 5 (ok)
+5 1 [3] 1 [2] [0] 5 3 (ok)
+8 4 [3] 8 [2] [0] 3 2 (ok)
 -----------------------
 bitmask: 0010
 -----------------------
-3 3 [2] 1 4 (ok)
-8 7 5 2 [2] 0 3 8 (ok)
-[2] 0 4 (ok)
-0 8 [2] (ok)
-[2] 4 (ok)
-6 1 8 1 6 4 2 [2] (ok)
-7 1 [2] 5 7 (ok)
-8 5 [2] 7 8 7 3 (ok)
-8 5 7 8 [2] 8 6 (ok)
-[2] 7 5 5 (ok)
+7 [2] 6 7 5 4 (ok)
+6 8 [2] 3 3 (ok)
+[2] 4 3 0 5 8 1 (ok)
+8 [2] 2 6 (ok)
+7 [2] 4 1 6 5 1 (ok)
+5 [2] 3 7 7 7 (ok)
+6 2 5 7 [2] 6 8 (ok)
+1 0 2 [2] 6 (ok)
+5 1 [2] 1 5 3 7 (ok)
+4 8 [2] 3 4 2 (ok)
 -----------------------
 bitmask: 0000
 -----------------------
-3 3 1 4 4 (ok)
-8 7 5 2 2 1 3 8 (ok)
-0 4 6 8 5 (ok)
-3 4 (ok)
-6 1 8 (ok)
-4 2 1 2 5 1 2 7 (ok)
-5 7 7 7 0 (ok)
-7 5 8 6 7 5 (ok)
-8 7 6 2 (ok)
-8 7 3 5 (ok)
+2 (ok)
+0 (ok)
+5 5 7 6 3 (ok)
+0 6 8 3 (ok)
+0 5 8 1 (ok)
+0 7 2 (ok)
+1 0 8 4 (ok)
+7 4 1 6 5 1 (ok)
+7 5 (ok)
+7 6 8 5 7 5 5 (ok)