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.
>>> sat $ \(s :: SString) -> length s .== 2
Satisfiable. Model:
  s0 = "BA" :: String
>>> sat $ \(s :: SString) -> length s .< 0
Unsatisfiable
>>> prove $ \(s1 :: SString) s2 -> length s1 + length s2 .== length (s1 ++ s2)
Q.E.D.

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.
>>> prove $ \(s :: SString) -> null s .<=> length s .== 0
Q.E.D.
>>> prove $ \(s :: SString) -> null s .<=> s .== ""
Q.E.D.

Empty list. This value has the property that it's the only list with length 0. If you use OverloadedLists extension, you can write it as the familiar `[]`.

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

Prepend an element, the traditional cons.

>>> 1 .: 2 .: 3 .: [4, 5, 6 :: SInteger]
[1,2,3,4,5,6] :: [SInteger]

Append an element

>>> [1, 2, 3 :: SInteger] `snoc` 4 `snoc` 5 `snoc` 6
[1,2,3,4,5,6] :: [SInteger]

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

>>> prove $ \c -> head [c] .== (c :: SInteger)
Q.E.D.
>>> prove $ \c -> c .== literal 'A' .=> ([c] :: SString) .== "A"
Q.E.D.
>>> prove $ \(c :: SChar) -> length ([c] :: SString) .== 1
Q.E.D.
>>> prove $ \(c :: SChar) -> head ([c] :: SString) .== c
Q.E.D.

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

>>> prove $ \(h :: SInteger) t -> tail ([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) .=> [head l] ++ tail l .== l
Q.E.D.
>>> prove $ \(h :: SChar) s -> tail ([h] ++ s) .== s
Q.E.D.
>>> prove $ \(s :: SString) -> length s .> 0 .=> length (tail s) .== length s - 1
Q.E.D.
>>> prove $ \(s :: SString) -> sNot (null s) .=> [head s] ++ tail s .== s
Q.E.D.

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

>>> prove $ \(x :: SInteger) xs -> uncons (x .: xs) .== (x, xs)
Q.E.D.

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

>>> prove $ \(h :: SInteger) t -> init (t ++ [h]) .== t
Q.E.D.
>>> prove $ \(c :: SChar) t -> init (t ++ [c]) .== t
Q.E.D.

last returns the last element of the list. Unspecified if the list is empty.

>>> prove $ \(l :: SInteger) i -> last (i ++ [l]) .== l
Q.E.D.

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

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

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 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.
>>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `elemAt` i .== literal 'A'
Q.E.D.

Short cut for elemAt

>>> prove $ \(xs :: SList Integer) i -> xs !! i .== xs `elemAt` i
Q.E.D.

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.
>>> prove $ \(c1 :: SChar) c2 c3 -> length (implode [c1, c2, c3]) .== 3
Q.E.D.
>>> prove $ \(c1 :: SChar) c2 c3 -> P.map (elemAt (implode [c1, c2, c3])) (P.map literal [0 .. 2]) .== [c1, c2, c3]
Q.E.D.

Concatenate list of lists.

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

Append two lists.

>>> sat $ \x y (z :: SList Integer) -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== [sEnum|1 .. 12|]
Satisfiable. Model:
  s0 =      [1,2,3,4,5] :: [Integer]
  s1 =              [6] :: [Integer]
  s2 = [7,8,9,10,11,12] :: [Integer]
>>> sat $ \(x :: SString) y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== "Hello world!"
Satisfiable. Model:
  s0 =  "Hello" :: String
  s1 =      " " :: String
  s2 = "world!" :: String

elem e l. Does l contain the element e?

>>> prove $ \(xs :: SList Integer) x -> x `elem` xs .=> length xs .>= 1
Q.E.D.

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

>>> prove $ \(x :: SList Integer) -> x `notElem` []
Q.E.D.

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.
>>> prove $ \(s1 :: SString) s2 s3 -> s2 `isInfixOf` (s1 ++ s2 ++ s3)
Q.E.D.
>>> prove $ \(s1 :: SString) s2 -> s1 `isInfixOf` s2 .&& s2 `isInfixOf` s1 .<=> s1 .== s2
Q.E.D.

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.
>>> prove $ \(s1 :: SString) s2 -> s2 `isSuffixOf` (s1 ++ s2)
Q.E.D.
>>> prove $ \(s1 :: SString) s2 -> s1 `isSuffixOf` s2 .=> subList s2 (length s2 - length s1) (length s1) .== s1
Q.E.D.

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.
>>> prove $ \(s1 :: SString) s2 -> s1 `isPrefixOf` (s1 ++ s2)
Q.E.D.
>>> prove $ \(s1 :: SString) s2 -> s1 `isPrefixOf` s2 .=> subList s2 0 (length s1) .== s1
Q.E.D.

listEq is a variant of equality that you can use for lists of floats. It respects NaN /= NaN. The reason we do not do this automatically is that it complicates proof objectives usually, as it does not simply resolve to the native equality check.

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.
>>> prove $ \(s :: SString) i -> i .>= 0 .=> length (take i s) .<= i
Q.E.D.

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.
>>> prove $ \(s :: SString) i -> length (drop i s) .<= length s
Q.E.D.
>>> prove $ \(s :: SString) i -> take i s ++ drop i s .== s
Q.E.D.

splitAt n xs = (take n xs, drop n xs)

>>> prove $ \n (xs :: SList Integer) -> let (l, r) = splitAt n xs in l ++ r .== xs
Q.E.D.

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 [sEnum|1..5|] i j .== [sEnum|2..4::SInteger|]
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subList [sEnum|1..5|] i j .== [sEnum|6..7::SInteger|]
Unsatisfiable
>>> prove $ \(s1 :: SString) (s2 :: SString) -> subList (s1 ++ s2) (length s1) 1 .== subList s2 0 1
Q.E.D.
>>> sat $ \(s :: SString) -> length s .>= 2 .&& subList s 0 1 ./= subList s (length s - 1) 1
Satisfiable. Model:
  s0 = "AB" :: String
>>> prove $ \(s :: SString) i -> i .>= 0 .&& i .< length s .=> subList s 0 i ++ subList s i (length s - i) .== s
Q.E.D.
>>> sat  $ \i j -> subList "hello" i j .== ("ell" :: SString)
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subList "hell" i j .== ("no" :: SString)
Unsatisfiable

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

>>> prove $ \l -> replace [sEnum|1..5|] l [sEnum|6..10|] .== [sEnum|6..10|] .=> l .== [sEnum|1..5::SWord8|]
Q.E.D.
>>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 .=> replace l1 l2 l3 .== l1
Q.E.D.
>>> prove $ \(s :: SString) -> replace "hello" s "world" .== "world" .=> s .== "hello"
Q.E.D.
>>> prove $ \(s1 :: SString) s2 s3 -> length s2 .> length s1 .=> replace s1 s2 s3 .== s1
Q.E.D.

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.
>>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1
Q.E.D.

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.
>>> prove $ \(s :: SString) sub -> offsetIndexOf s sub 0 .== indexOf s sub
Q.E.D.
>>> prove $ \(s :: SString) sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1
Q.E.D.
>>> prove $ \(s :: SString) sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
Q.E.D.

reverse s reverses the sequence.

NB. We can define reverse in terms of foldl as: foldl (soFar elt -> [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.
>>> sat $ \(l :: SString ) -> reverse l .== "321"
Satisfiable. Model:
  s0 = "123" :: String
>>> prove $ \(l :: SString) -> reverse l .== "" .<=> null l
Q.E.D.

Map a function (or a closure) over a symbolic list.

>>> map (+ (1 :: SInteger)) [sEnum|1 .. 5 :: SInteger|]
[2,3,4,5,6] :: [SInteger]
>>> map (+ (1 :: SWord 8)) [sEnum|1 .. 5 :: SWord 8|]
[2,3,4,5,6] :: [SWord8]
>>> map (\x -> [x] :: SList Integer) [sEnum|1 .. 3 :: SInteger|]
[[1],[2],[3]] :: [[SInteger]]
>>> import Data.SBV.Tuple
>>> map (\t -> t^._1 + t^._2) (literal [(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 :: SInteger)) l .== [1,2,3 :: SInteger]
Satisfiable. Model:
  s0 = [0,1,2] :: [Integer]

concatMap f xs maps f over elements and concats the result.

>>> concatMap (\x -> [x, x] :: SList Integer) [sEnum|1 .. 3|]
[1,1,2,2,3,3] :: [SInteger]

Difference.

>>> [1, 2] \\ [3, 4 :: SInteger]
[1,2] :: [SInteger]
>>> [1, 2] \\ [2, 4 :: SInteger]
[1] :: [SInteger]

foldl f base s folds the from the left.

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

Again, we can use foldl in the reverse too:

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

foldr f base s folds the from the right.

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

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 [sEnum|1..10 :: SInteger|] [sEnum|11..20 :: SInteger|]
[(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 ((+) @SInteger) 0 (map (\t -> t^._1+t^._2::SInteger) (zip [sEnum|1..10|] [sEnum|10, 9..1|]))
110 :: SInteger

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 ((+) @SInteger) ([sEnum|1..10::SInteger|]) ([sEnum|11..20::SInteger|])
[12,14,16,18,20,22,24,26,28,30] :: [SInteger]
>>> foldr ((+) @SInteger) 0 (zipWith ((+) @SInteger) [sEnum|1..10 :: SInteger|] [sEnum|10, 9..1 :: SInteger|])
110 :: SInteger

Lookup. If we can't find, then the result is unspecified.

>>> lookup (4 :: SInteger) (literal [(5, 12), (4, 3), (2, 6 :: Integer)])
3 :: SInteger
>>> prove  $ \(x :: SInteger) -> x .== lookup 9 (literal [(5, 12), (4, 3), (2, 6 :: Integer)])
Falsifiable. Counter-example:
  Data.SBV.List.lookup_notFound @Integer = 0 :: Integer
  s0                                     = 1 :: Integer

Filter a list via a predicate.

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

Partition a symbolic list according to a predicate.

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

Symbolic equivalent of takeWhile

>>> takeWhile (\(x :: SInteger) -> x `sMod` 2 .== 0) (literal [1..10])
[] :: [SInteger]
>>> takeWhile (\(x :: SInteger) -> x `sMod` 2 ./= 0) (literal [1..10])
[1] :: [SInteger]

Symbolic equivalent of dropWhile >>> dropWhile ((x :: SInteger) -> x sMod 2 .== 0) (literal [1..10]) [1,2,3,4,5,6,7,8,9,10] :: [SInteger] >>> dropWhile ((x :: SInteger) -> x sMod 2 ./= 0) (literal [1..10]) [2,3,4,5,6,7,8,9,10] :: [SInteger]

Check all elements satisfy the predicate.

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

Check some element satisfies the predicate.

>>> let isEven x = x `sMod` 2 .== 0
>>> any (sNot . isEven) [2, 4, 6, 8, 10 :: SInteger]
False
>>> any isEven [2, 4, 6, 1, 8, 10 :: SInteger]
True

Conjunction of all the elements.

>>> and []
True
>>> prove $ \s -> and [s, sNot s] .== sFalse
Q.E.D.

Disjunction of all the elements.

>>> or []
False
>>> prove $ \s -> or [s, sNot s]
Q.E.D.

Replicate an element a given number of times.

>>> replicate 3 (2 :: SInteger) .== [2, 2, 2 :: SInteger]
True
>>> replicate (-2) (2 :: SInteger) .== ([] :: SList Integer)
True

inits of a list.

>>> inits ([] :: SList Integer)
[[]] :: [[SInteger]]
>>> inits [1,2,3,4::SInteger]
[[],[1],[1,2],[1,2,3],[1,2,3,4]] :: [[SInteger]]

tails of a list.

>>> tails ([] :: SList Integer)
[[]] :: [[SInteger]]
>>> tails [1,2,3,4::SInteger]
[[1,2,3,4],[2,3,4],[3,4],[4],[]] :: [[SInteger]]

sum s. Sum the given sequence.

>>> sum [sEnum|1 .. 10::SInteger|]
55 :: SInteger

product s. Multiply out the given sequence.

>>> product [sEnum|1 .. 10::SInteger|]
3628800 :: SInteger

strToNat s. Retrieve integer encoded by string s (ground rewriting only). Note that by definition this function only works when s only contains digits, that is, if it encodes a natural number. Otherwise, it returns '-1'.

>>> prove $ \s -> let n = strToNat s in length s .== 1 .=> (-1) .<= n .&& n .<= 9
Q.E.D.

natToStr i. Retrieve string encoded by integer i (ground rewriting only). Again, only naturals are supported, any input that is not a natural number produces empty string, even though we take an integer as an argument.

>>> prove $ \i -> length (natToStr i) .== 3 .=> i .<= 999
Q.E.D.

A class of symbolic aware enumerations. This is similar to Haskell's Enum class, except some of the methods are generalized to work with symbolic values. Together with the sEnum quasiquoter, you can write symbolic arithmetic progressions, such as:

>>> [sEnum| 5, 7 .. 16::SInteger|]
[5,7,9,11,13,15] :: [SInteger]
>>> [sEnum| 4 ..|] :: SList (WordN 4)
[4,5,6,7,8,9,10,11,12,13,14,15] :: [SWord 4]
>>> [sEnum| 9, 12 ..|] :: SList (IntN 4)
[-7,-4,-1,2,5] :: [SInt 4]