Set package:leancheck

Lists representing sets. The Listable tiers enumeration will not have repeated sets.

> take 6 (list :: [Set Nat])
[Set [],Set [0],Set [1],Set [0,1],Set [2],Set [0,2]]

Given a constructor that takes a set of elements (as a list), lists tiers of applications of this constructor. A naive Listable instance for the Set (of Data.Set) would read:

instance Listable a => Listable (Set a) where
tiers  =  cons0 empty \/ cons2 insert

The above instance has a problem: it generates repeated sets. A more efficient implementation that does not repeat sets is given by:

tiers  =  setCons fromList

Alternatively, you can use setsOf direclty.

Takes as argument tiers of element values; returns tiers of size-ordered lists of elements without repetition.

setsOf [[0],[1],[2],...] =
[ [[]]
, [[0]]
, [[1]]
, [[0,1],[2]]
, [[0,2],[3]]
, [[0,3],[1,2],[4]]
, [[0,1,2],[0,4],[1,3],[5]]
, ...
]

Can be used in the constructor of specialized Listable instances. For Set (from Data.Set), we would have:

instance Listable a => Listable (Set a) where
tiers  =  mapT fromList $ setsOf tiers

Like choices but lists tiers of strictly ascending choices. Used to construct setsOf values.

setChoices [[False,True]] == [[(False,[[True]]),(True,[[]])]]
setChoices [[1],[2],[3]]
== [ [(1,[[],[2],[3]])]
, [(2,[[],[],[3]])]
, [(3,[[],[],[]])]
]

Resets any delays in a list-of tiers. Conceptually this function makes a constructor "weightless", assuring the first tier is non-empty.

reset [[], [], ..., xs, ys, zs, ...]  =  [xs, ys, zs, ...]

reset [[], xs, ys, zs, ...]  =  [xs, ys, zs, ...]

reset [[], [], ..., [x], [y], [z], ...]  =  [[x], [y], [z], ...]

Typically used when defining Listable instances:

instance Listable <Type> where
tiers  =  ...
\/ reset (cons<N> <Constructor>)
\/ ...

Be careful: do not apply reset to recursive data structure constructors. In general this will make the list of size 0 infinite, breaking the tiers invariant (each tier must be finite).