sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Joel Burget Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.List

Contents

- Length, emptiness
- Deconstructing/Reconstructing
- Containment
- Sublists
- Reverse
- Mapping
- Folding
- Zipping
- Filtering
- Other list functions

Description

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.

Synopsis

- length :: SymVal a => SList a -> SInteger
- null :: SymVal a => SList a -> SBool
- head :: SymVal a => SList a -> SBV a
- tail :: SymVal a => SList a -> SList a
- uncons :: SymVal a => SList a -> (SBV a, SList a)
- init :: SymVal a => SList a -> SList a
- singleton :: SymVal a => SBV a -> SList a
- listToListAt :: SymVal a => SList a -> SInteger -> SList a
- elemAt :: SymVal a => SList a -> SInteger -> SBV a
- (!!) :: SymVal a => SList a -> SInteger -> SBV a
- implode :: SymVal a => [SBV a] -> SList a
- concat :: SymVal a => SList [a] -> SList a
- (.:) :: SymVal a => SBV a -> SList a -> SList a
- snoc :: SymVal a => SList a -> SBV a -> SList a
- nil :: SymVal a => SList a
- (++) :: SymVal a => SList a -> SList a -> SList a
- elem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
- notElem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
- isInfixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
- isSuffixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
- isPrefixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
- take :: SymVal a => SInteger -> SList a -> SList a
- drop :: SymVal a => SInteger -> SList a -> SList a
- subList :: SymVal a => SList a -> SInteger -> SInteger -> SList a
- replace :: (Eq a, SymVal a) => SList a -> SList a -> SList a -> SList a
- indexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger
- offsetIndexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger -> SInteger
- reverse :: SymVal a => SList a -> SList a
- map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SList a -> SList b
- mapi :: forall a b. (SymVal a, SymVal b) => (SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b
- foldl :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
- foldr :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
- foldli :: (SymVal a, SymVal b) => (SInteger -> SBV b -> SBV a -> SBV b) -> SInteger -> SBV b -> SList a -> SBV b
- foldri :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SInteger -> SBV b) -> SBV b -> SInteger -> SList a -> SBV b
- zip :: (SymVal a, SymVal b) => SList a -> SList b -> SList (a, b)
- zipWith :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
- filter :: SymVal a => (SBV a -> SBool) -> SList a -> SList a
- all :: SymVal a => (SBV a -> SBool) -> SList a -> SBool
- any :: SymVal a => (SBV a -> SBool) -> SList a -> SBool

# Length, emptiness

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

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 Source #

``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 Source #

``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 Source #

``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) Source #

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

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

``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 Source #

``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 Source #

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

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

``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 $ (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 Source #

Short cut for `elemAt`

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

``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 Source #

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 Source #

Prepend an element, the traditional `cons`.

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

Append an element

nil :: SymVal a => SList a Source #

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 Source #

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 Source #

``elem` e l`. Does `l` contain the element `e`?

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

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

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

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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 :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SList a -> SList b Source #

``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 :: forall a b. (SymVal a, SymVal b) => (SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b Source #

``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 Source #

``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 Source #

``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 Source #

``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 Source #

``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) Source #

``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 Source #

``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 Source #

`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 Source #

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 Source #

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