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,32] :: [Word16]

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

elemAt l i is the value stored at location i. 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 $ (l :: SList Integer) i e -> i inRange (0, length l - 1) .&& l elemAt i .== e .=> indexOf l (singleton e) .<= i 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 -> map (elemAt (implode [e1, e2, e3])) (map literal [0 .. 2]) .== [e1, e2, e3]
Q.E.D.

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

Concatenate two lists. See also ++.

(.:) :: 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

Short cut for concat.

>>> 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 $ (l :: SList Int8) i -> i .> 0 .&& i .l .= indexOf l (subList l i 1) .<= i Q.E.D.

>>> 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. >>> 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.