[ derive ] Implements data types fusion

.github/workflows/ci-deptycheck.yml

@@ -138,7 +138,7 @@ jobs:
   ###################
 
   get-test-sets:
-    name: Aquire test sets
+    name: Acquire test sets
     needs:
       - deptycheck-build-lib
     runs-on: ubuntu-latest
@@ -187,7 +187,7 @@ jobs:
   #################
 
   get-examples:
-    name: Aquire examples
+    name: Acquire examples
     needs:
       - deptycheck-build-lib
     runs-on: ubuntu-latest

.github/workflows/ci-non-primary-os.yml

@@ -0,0 +1,30 @@
+---
+name: Non-primary OS
+
+on:
+  push:
+    branches:
+      - main
+      - master
+    tags:
+      - '*'
+  pull_request:
+    branches:
+      - main
+      - master
+
+permissions:
+  statuses: write
+
+concurrency:
+  group: ${{ github.workflow }}@${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: Clone on Windows
+    runs-on: windows-latest
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4

README.md

@@ -301,12 +301,6 @@ You can read more on the design of generators in [documentation](https://deptych
 
 ## Derivation of generators
 
-<!-- idris
-%hint
-UsedConstructorDerivator : ConstructorDerivator
-UsedConstructorDerivator = LeastEffort
--->
-
 DepTyCheck supports automatic derivation of generators using the datatype definition.
 
 For now, it is not tunable at all, however, it is planned to be added.

deptycheck.ipkg

@@ -9,7 +9,7 @@ license = "MPL-2.0"
 sourcedir = "src"
 builddir = ".build"
 
-version = 0.0.240616
+version = 0.0.240909
 
 modules = Deriving.DepTyCheck
         , Deriving.DepTyCheck.Gen
@@ -20,6 +20,7 @@ modules = Deriving.DepTyCheck
         , Deriving.DepTyCheck.Gen.Core.ConsEntry
         , Deriving.DepTyCheck.Gen.Core.Util
         , Deriving.DepTyCheck.Gen.Checked
+        , Deriving.DepTyCheck.Util.Fusion
         , Deriving.DepTyCheck.Util.Logging
         , Deriving.DepTyCheck.Util.Reflection
         , Language.Reflection.Compat

docs/source/conf.py

@@ -68,7 +68,6 @@
 #
 html_theme = "sphinx_rtd_theme"
 html_theme_options = {
-    "display_version": True,
     "prev_next_buttons_location": "bottom",
 }
 html_logo = "../../icons/deptycheck-lib-html-logo.png"

docs/source/explanation/derivation/design/single-con.md

@@ -298,7 +298,7 @@ genD_idx_generated @{data_Nat} @{data_String} fuel b = data_D_giv_b fuel b
 -->
 
 In this case, generation of non-recursive constructors `JJ` and `TL` is straightforward,
-the only difference is that `b` is a function argument, not a result of subgeneration.
+the only difference is that `b` is a function parameter, not a result of subgeneration.
 
 Recursive cases are not so easy.
 Surely, we can first generate value `b` using derived `data_Bool` generator (as we did before for `JJ` constructor)

docs/source/explanation/derivation/design/when-derivation-happens.md

@@ -62,7 +62,9 @@ thus inapplicable directly for dependent types.
 Since, we focus on total generators for dependent types, we cannot rely on common hybrid approach.
 Considering all said above, it is decided to go the hard way and to do derivation of generators directly,
 using metaprogramming facility if Idris called *elaboration scripts*.
-% TODO to add a link to Idris documentation as soon as elaboration scripts are documented.
+<!--
+TODO to add a link to Idris documentation as soon as elaboration scripts are documented.
+-->
 
 Thus, DepTyCheck's derivation mechanism is a fully compile-time metaprogram that analyses generated datatype and
 produces generator's code which is checked for type correctness and totality right after.

examples/README.md

@@ -16,6 +16,7 @@ The examples are the following:
 
 - [sorted lists](sorted-list/) of natural numbers
 - list and vector of strings, [both with unique elements](uniq-list/) implemented using `So` and usual `Eq` comparison
+- a sequence of [unique mentions of a given subset](covering-seq/) of elements interleaved with unrelated elements
 - naive possibly empty [sorted binary trees](sorted-tree-naive/) of natural numbers, implemented as if without dependent types
   with added limitations on sortedness
 - [indexed non-empty sorted binary trees](sorted-tree-indexed/) of natural numbers, with type indices for value bounds

examples/covering-seq/covering-seq.ipkg

@@ -0,0 +1,13 @@
+package covering-seq
+
+version = 0.1
+
+authors = "Denis Buzdalov"
+
+sourcedir = "src"
+builddir = ".build"
+
+depends = deptycheck
+
+modules = Data.List.Covering
+        , Data.List.Covering.Gen

examples/covering-seq/src/Data/List/Covering.idr

@@ -0,0 +1,64 @@
+module Data.List.Covering
+
+import public Data.Fin
+import Data.String
+
+%default total
+
+namespace BitMask
+
+  -- BitMask n ~~ Vect n Bool
+  public export
+  data BitMask : (bits : Nat) -> Type where
+    Nil  : BitMask 0
+    (::) : Bool -> BitMask n -> BitMask (S n)
+
+  export
+  Interpolation (BitMask n) where
+    interpolate []          = ""
+    interpolate (True ::bs) = "1\{bs}"
+    interpolate (False::bs) = "0\{bs}"
+
+  public export
+  update : Fin n -> (newValue : Bool) -> BitMask n -> BitMask n
+  update FZ     v (_::bs) = v::bs
+  update (FS n) v (b::bs) = b :: update n v bs
+
+  namespace Index
+
+    public export
+    data AtIndex : (n : Nat) -> Fin n -> BitMask n -> Bool -> Type where
+      Here  : AtIndex (S n) FZ (b::bs) b
+      There : AtIndex n i bs v -> AtIndex (S n) (FS i) (b::bs) v
+
+    public export
+    data AllBitsAre : (n : Nat) -> Bool -> BitMask n -> Type where
+      Finish   : AllBitsAre Z b []
+      Continue : AllBitsAre n b bs -> AllBitsAre (S n) b (b::bs)
+
+  export
+  setBits : BitMask n -> List $ Fin n
+  setBits []         = []
+  setBits $ True ::bs = FZ :: (FS <$> setBits bs)
+  setBits $ False::bs = FS <$> setBits bs
+
+-- Contains all and only mentions (hits) of values enabled in the given bitmask in any order interleaved with some arbitrary numbers (misses).
+public export
+data CoveringSequence : (n : Nat) -> BitMask n -> Type where
+  End  : AllBitsAre n False bs => CoveringSequence n bs
+  Miss : Nat -> CoveringSequence n bs -> CoveringSequence n bs
+  Hit  : (i : Fin n) -> AtIndex n i bs True => CoveringSequence n (update i False bs) -> CoveringSequence n bs
+
+public export
+hits : CoveringSequence n bs -> List $ Fin n
+hits End         = []
+hits $ Miss k xs = hits xs
+hits $ Hit i xs  = i :: hits xs
+
+export
+Interpolation (CoveringSequence n bs) where
+  interpolate = joinBy " " . asList where
+    asList : forall n, bs. CoveringSequence n bs -> List String
+    asList End         = []
+    asList $ Miss k xs = show k :: asList xs
+    asList $ Hit i xs  = "[\{show i}]" :: asList xs

examples/covering-seq/src/Data/List/Covering/Gen.idr

@@ -0,0 +1,14 @@
+module Data.List.Covering.Gen
+
+import public Data.List.Covering
+
+import public Test.DepTyCheck.Gen
+import Deriving.DepTyCheck.Gen
+
+%default total
+
+%logging "deptycheck.derive" 5
+
+export
+genCoveringSequence : Fuel -> {n : Nat} -> (bs : BitMask n) -> Gen MaybeEmpty $ CoveringSequence n bs
+genCoveringSequence = deriveGen

examples/covering-seq/tests/.clean-names

@@ -0,0 +1 @@
+../../../tests/.clean-names

examples/covering-seq/tests/Tests.idr

@@ -0,0 +1,9 @@
+module Tests
+
+import Test.Golden.RunnerHelper
+
+main : IO ()
+main = goldenRunner
+  [ "Covering sequence data structure" `atDir` "data"
+  , "Generator for covering sequences" `atDir` "gens"
+  ]

examples/covering-seq/tests/data/simple-seqs/Main.idr

@@ -0,0 +1,35 @@
+import Data.List.Covering
+
+%default total
+
+MaskIIII : BitMask ?
+MaskIIII = [True, True, True, True]
+
+x0123 : CoveringSequence ? MaskIIII
+x0123 = Hit 0 $ Hit 1 $ Hit 2 $ Hit 3 $ End
+
+x0123' : CoveringSequence ? MaskIIII
+x0123' = Hit 0 $ Hit 1 $ Miss 20 $ Hit 2 $ Hit 3 $ Miss 30 $ End
+
+x2301 : CoveringSequence ? MaskIIII
+x2301 = Hit 2 $ Hit 3 $ Hit 0 $ Hit 1 $ End
+
+x2301' : CoveringSequence ? MaskIIII
+x2301' = Hit 2 $ Hit 3 $ Miss 20 $ Hit 0 $ Hit 1 $ Miss 30 $ End
+
+failing "Can't find an implementation for AtIndex"
+  x23012 : CoveringSequence ? MaskIIII
+  x23012 = Hit 2 $ Hit 3 $ Hit 0 $ Hit 1 $ Hit 2 $ End
+
+MaskIIOI : BitMask ?
+MaskIIOI = [True, True, False, True]
+
+x013 : CoveringSequence ? MaskIIOI
+x013 = Hit 0 $ Hit 1 $ Hit 3 $ End
+
+x103 : CoveringSequence ? MaskIIOI
+x103 = Hit 1 $ Hit 0 $ Hit 3 $ End
+
+failing "Can't find an implementation for AtIndex"
+  badx0123 : CoveringSequence ? MaskIIOI
+  badx0123 = Hit 0 $ Hit 1 $ Hit 2 $ Hit 3 $ End

examples/covering-seq/tests/data/simple-seqs/expected

@@ -0,0 +1 @@
+1/1: Building Main (Main.idr)

examples/covering-seq/tests/data/simple-seqs/run

@@ -0,0 +1,6 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+idris2 --find-ipkg --check Main.idr
+
+rm -rf build

examples/covering-seq/tests/data/simple-seqs/test.ipkg

@@ -0,0 +1,3 @@
+package a-test
+
+depends = covering-seq

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

@@ -0,0 +1,27 @@
+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]
+  submain [True, False, True, True]
+  submain [False, False, True, False]
+  submain [False, False, False, False]

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

@@ -0,0 +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)
+-----------------------
+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)
+-----------------------
+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)
+-----------------------
+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)

examples/covering-seq/tests/gens/covering-seqs/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/test.ipkg

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

examples/covering-seq/tests/gens/print/DerivedGen.idr

@@ -0,0 +1,12 @@
+module DerivedGen
+
+import Data.List.Covering
+
+import Deriving.DepTyCheck.Gen
+
+%default total
+
+%language ElabReflection
+
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter $ Fuel -> {n : Nat} -> (bs : BitMask n) -> Gen MaybeEmpty $ CoveringSequence n bs

examples/covering-seq/tests/gens/print/derive.ipkg

@@ -0,0 +1,6 @@
+package derive-test
+
+authors = "Denis Buzdalov"
+
+depends = deptycheck
+        , covering-seq