Data.SBV.List

A collection of list utilities, useful when working with symbolic lists. To the extent possible, the functions in this module follow those of Data.List so importing qualified is the recommended workflow. Also, it is recommended you use the OverloadedLists extension to allow literal lists to be used as symbolic-lists.

Length, emptiness

length :: SymVal a => SList a -> SInteger

Length of a list.

>>> sat $ \(l :: SList Word16) -> length l .== 2
Satisfiable. Model:
  s0 = [0,0] :: [Word16]
>>> sat $ \(l :: SList Word16) -> length l .< 0
Unsatisfiable
>>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 ++ l2)
Q.E.D.

null :: SymVal a => SList a -> SBool

null s is True iff the list is empty

>>> prove $ \(l :: SList Word16) -> null l .<=> length l .== 0
Q.E.D.
>>> prove $ \(l :: SList Word16) -> null l .<=> l .== []
Q.E.D.

Deconstructing/Reconstructing

head :: SymVal a => SList a -> SBV a

head returns the first element of a list. Unspecified if the list is empty.

>>> prove $ \c -> head (singleton c) .== (c :: SInteger)
Q.E.D.

tail :: SymVal a => SList a -> SList a

tail returns the tail of a list. Unspecified if the list is empty.

>>> prove $ \(h :: SInteger) t -> tail (singleton h ++ t) .== t
Q.E.D.
>>> prove $ \(l :: SList Integer) -> length l .> 0 .=> length (tail l) .== length l - 1
Q.E.D.
>>> prove $ \(l :: SList Integer) -> sNot (null l) .=> singleton (head l) ++ tail l .== l
Q.E.D.

uncons :: SymVal a => SList a -> (SBV a, SList a)

uncons returns the pair of the head and tail. Unspecified if the list is empty.

init :: SymVal a => SList a -> SList a

init returns all but the last element of the list. Unspecified if the list is empty.

>>> prove $ \(h :: SInteger) t -> init (t ++ singleton h) .== t
Q.E.D.

singleton :: SymVal a => SBV a -> SList a

singleton x is the list of length 1 that contains the only value x.

>>> prove $ \(x :: SInteger) -> head (singleton x) .== x
Q.E.D.
>>> prove $ \(x :: SInteger) -> length (singleton x) .== 1
Q.E.D.

listToListAt :: SymVal a => SList a -> SInteger -> SList a

listToListAt l offset. List of length 1 at offset in l. Unspecified if index is out of bounds.

>>> prove $ \(l1 :: SList Integer) l2 -> listToListAt (l1 ++ l2) (length l1) .== listToListAt l2 0
Q.E.D.
>>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1)
Satisfiable. Model:
  s0 = [0,64] :: [Word16]

elemAt :: SymVal a => SList a -> SInteger -> SBV a

elemAt l i is the value stored at location i, starting at 0. Unspecified if index is out of bounds.

>>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
Q.E.D.

(!!) :: SymVal a => SList a -> SInteger -> SBV a

Short cut for elemAt

implode :: SymVal a => [SBV a] -> SList a

implode es is the list of length |es| containing precisely those elements. Note that there is no corresponding function explode, since we wouldn't know the length of a symbolic list.

>>> prove $ \(e1 :: SInteger) e2 e3 -> length (implode [e1, e2, e3]) .== 3
Q.E.D.
>>> prove $ \(e1 :: SInteger) e2 e3 -> P.map (elemAt (implode [e1, e2, e3])) (P.map literal [0 .. 2]) .== [e1, e2, e3]
Q.E.D.

concat :: SymVal a => SList [a] -> SList a

Concatenate list of lists.

NB. Concat is typically defined in terms of foldr. Here we prefer foldl, since the underlying solver primitive is foldl: Otherwise, we'd induce an extra call to reverse.

>>> concat [[1..3::Integer], [4..7], [8..10]]
[1,2,3,4,5,6,7,8,9,10] :: [SInteger]

(.:) :: SymVal a => SBV a -> SList a -> SList a infixr 5

Prepend an element, the traditional cons.

snoc :: SymVal a => SList a -> SBV a -> SList a

Append an element

nil :: SymVal a => SList a

Empty list. This value has the property that it's the only list with length 0:

>>> prove $ \(l :: SList Integer) -> length l .== 0 .<=> l .== nil
Q.E.D.

(++) :: SymVal a => SList a -> SList a -> SList a infixr 5

Append two lists.

>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== [1 .. 12]
Satisfiable. Model:
  s0 =      [1,2,3,4,5] :: [Integer]
  s1 =              [6] :: [Integer]
  s2 = [7,8,9,10,11,12] :: [Integer]

Containment

elem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool

elem e l. Does l contain the element e?

notElem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool

notElem e l. Does l not contain the element e?

isInfixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool

isInfixOf sub l. Does l contain the subsequence sub?

>>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 ++ l2 ++ l3)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 .&& l2 `isInfixOf` l1 .<=> l1 .== l2
Q.E.D.

isSuffixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool

isSuffixOf suf l. Is suf a suffix of l?

>>> prove $ \(l1 :: SList Word16) l2 -> l2 `isSuffixOf` (l1 ++ l2)
Q.E.D.
>>> prove $ \(l1 :: SList Word16) l2 -> l1 `isSuffixOf` l2 .=> subList l2 (length l2 - length l1) (length l1) .== l1
Q.E.D.

isPrefixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool

isPrefixOf pre l. Is pre a prefix of l?

>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` (l1 ++ l2)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` l2 .=> subList l2 0 (length l1) .== l1
Q.E.D.

Sublists

take :: SymVal a => SInteger -> SList a -> SList a

take len l. Corresponds to Haskell's take on symbolic lists.

>>> prove $ \(l :: SList Integer) i -> i .>= 0 .=> length (take i l) .<= i
Q.E.D.

drop :: SymVal a => SInteger -> SList a -> SList a

drop len s. Corresponds to Haskell's drop on symbolic-lists.

>>> prove $ \(l :: SList Word16) i -> length (drop i l) .<= length l
Q.E.D.
>>> prove $ \(l :: SList Word16) i -> take i l ++ drop i l .== l
Q.E.D.

subList :: SymVal a => SList a -> SInteger -> SInteger -> SList a

subList s offset len is the sublist of s at offset offset with length len. This function is under-specified when the offset is outside the range of positions in s or len is negative or offset+len exceeds the length of s.

>>> prove $ \(l :: SList Integer) i -> i .>= 0 .&& i .< length l .=> subList l 0 i ++ subList l i (length l - i) .== l
Q.E.D.
>>> sat  $ \i j -> subList [1..5] i j .== ([2..4] :: SList Integer)
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subList [1..5] i j .== ([6..7] :: SList Integer)
Unsatisfiable

replace :: (Eq a, SymVal a) => SList a -> SList a -> SList a -> SList a

replace l src dst. Replace the first occurrence of src by dst in s

>>> prove $ \l -> replace [1..5] l [6..10] .== [6..10] .=> l .== ([1..5] :: SList Word8)
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 .=> replace l1 l2 l3 .== l1
Q.E.D.

indexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger

indexOf l sub. Retrieves first position of sub in l, -1 if there are no occurrences. Equivalent to offsetIndexOf l sub 0.

>>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1
Q.E.D.

offsetIndexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger -> SInteger

offsetIndexOf l sub offset. Retrieves first position of sub at or after offset in l, -1 if there are no occurrences.

>>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub
Q.E.D.
>>> prove $ \(l :: SList Int8) sub i -> i .>= length l .&& length sub .> 0 .=> offsetIndexOf l sub i .== -1
Q.E.D.
>>> prove $ \(l :: SList Int8) sub i -> i .> length l .=> offsetIndexOf l sub i .== -1
Q.E.D.

Reverse

reverse :: SymVal a => SList a -> SList a

reverse s reverses the sequence.

NB. We can define reverse in terms of foldl as: foldl (soFar elt -> singleton elt ++ soFar) [] But in my experiments, I found that this definition performs worse instead of the recursive definition SBV generates for reverse calls. So we're keeping it intact.

>>> sat $ \(l :: SList Integer) -> reverse l .== literal [3, 2, 1]
Satisfiable. Model:
  s0 = [1,2,3] :: [Integer]
>>> prove $ \(l :: SList Word32) -> reverse l .== [] .<=> null l
Q.E.D.

Mapping

map :: (SymVal a, SymVal b) => (SBV a -> SBV b) -> SList a -> SList b

map op s maps the operation on to sequence.

>>> map (+1) [1 .. 5 :: Integer]
[2,3,4,5,6] :: [SInteger]
>>> map (+1) [1 .. 5 :: WordN 8]
[2,3,4,5,6] :: [SWord8]
>>> map singleton [1 .. 3 :: Integer]
[[1],[2],[3]] :: [[SInteger]]
>>> import Data.SBV.Tuple
>>> import GHC.Exts (fromList)
>>> map (\t -> t^._1 + t^._2) (fromList [(x, y) | x <- [1..3], y <- [4..6]] :: SList (Integer, Integer))
[5,6,7,6,7,8,7,8,9] :: [SInteger]

Of course, SBV's map can also be reused in reverse:

>>> sat $ \l -> map (+1) l .== [1,2,3 :: Integer]
Satisfiable. Model:
  s0 = [0,1,2] :: [Integer]

mapi :: (SymVal a, SymVal b) => (SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b

mapi op s maps the operation on to sequence, with the counter given at each element, starting at the given value. In Haskell terms, it is:

   mapi :: (Integer -> a -> b) -> Integer -> [a] -> [b]
   mapi f i xs = zipWith f [i..] xs

Note that mapi is definable in terms of zipWith, with extra coding. The reason why SBV provides this function natively is because it maps to a native function in the underlying solver. So, hopefully it'll perform better in terms being decidable.

>>> mapi (+) 10 [1 .. 5 :: Integer]
[11,13,15,17,19] :: [SInteger]

Folding

foldl :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b

foldl op base s folds the from the left.

>>> foldl (+) 0 [1 .. 5 :: Integer]
15 :: SInteger
>>> foldl (*) 1 [1 .. 5 :: Integer]
120 :: SInteger
>>> foldl (\soFar elt -> singleton elt ++ soFar) ([] :: SList Integer) [1 .. 5 :: Integer]
[5,4,3,2,1] :: [SInteger]

Again, we can use foldl in the reverse too:

>>> sat $ \l -> foldl (\soFar elt -> singleton elt ++ soFar) ([] :: SList Integer) l .== [5, 4, 3, 2, 1 :: Integer]
Satisfiable. Model:
  s0 = [1,2,3,4,5] :: [Integer]

foldr :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b

foldr op base s folds the sequence from the right.

>>> foldr (+) 0 [1 .. 5 :: Integer]
15 :: SInteger
>>> foldr (*) 1 [1 .. 5 :: Integer]
120 :: SInteger
>>> foldr (\elt soFar -> soFar ++ singleton elt) ([] :: SList Integer) [1 .. 5 :: Integer]
[5,4,3,2,1] :: [SInteger]

foldli :: (SymVal a, SymVal b) => (SInteger -> SBV b -> SBV a -> SBV b) -> SInteger -> SBV b -> SList a -> SBV b

foldli op i base s folds the sequence, with the counter given at each element, starting at the given value. In Haskell terms, it is:

  foldli :: (Integer -> b -> a -> b) -> Integer -> b -> [a] -> b
  foldli f c e xs = foldl (b (i, a) -> f i b a) e (zip [c..] xs)

While this function is rather odd looking, it maps directly to the implementation in the underlying solver, and proofs involving it might have better decidability.

>>> foldli (\i b a -> i+b+a) 10 0 [1 .. 5 :: Integer]
75 :: SInteger

foldri :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SInteger -> SBV b) -> SBV b -> SInteger -> SList a -> SBV b

foldri op base i s folds the sequence from the right, with the counter given at each element, starting at the given value. This function is provided as a parallel to foldli.

Zipping

zip :: (SymVal a, SymVal b) => SList a -> SList b -> SList (a, b)

zip xs ys zips the lists to give a list of pairs. The length of the final list is the minumum of the lengths of the given lists.

>>> zip [1..10::Integer] [11..20::Integer]
[(1,11),(2,12),(3,13),(4,14),(5,15),(6,16),(7,17),(8,18),(9,19),(10,20)] :: [(SInteger, SInteger)]
>>> import Data.SBV.Tuple
>>> foldr (+) 0 (map (\t -> t^._1+t^._2::SInteger) (zip [1..10::Integer] [10, 9..1::Integer]))
110 :: SInteger

zipWith :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c

zipWith f xs ys zips the lists to give a list of pairs, applying the function to each pair of elements. The length of the final list is the minumum of the lengths of the given lists.

>>> zipWith (+) [1..10::Integer] [11..20::Integer]
[12,14,16,18,20,22,24,26,28,30] :: [SInteger]
>>> foldr (+) 0 (zipWith (+) [1..10::Integer] [10, 9..1::Integer])
110 :: SInteger

Filtering

filter :: SymVal a => (SBV a -> SBool) -> SList a -> SList a

filter f xs filters the list with the given predicate.

>>> filter (\x -> x `sMod` 2 .== 0) [1 .. 10 :: Integer]
[2,4,6,8,10] :: [SInteger]
>>> filter (\x -> x `sMod` 2 ./= 0) [1 .. 10 :: Integer]
[1,3,5,7,9] :: [SInteger]

Other list functions

all :: SymVal a => (SBV a -> SBool) -> SList a -> SBool

Check all elements satisfy the predicate.

>>> let isEven x = x `sMod` 2 .== 0
>>> all isEven [2, 4, 6, 8, 10 :: Integer]
True
>>> all isEven [2, 4, 6, 1, 8, 10 :: Integer]
False

any :: SymVal a => (SBV a -> SBool) -> SList a -> SBool

Check some element satisfies the predicate. -- >>> let isEven x = x sMod 2 .== 0 >>> any (sNot . isEven) [2, 4, 6, 8, 10 :: Integer] False >>> any isEven [2, 4, 6, 1, 8, 10 :: Integer] True