sbv-7.13: 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 | None
Language | Haskell2010

Data.SBV.List

Contents

- Length, emptiness
- Deconstructing/Reconstructing
- Containment
- Sublists

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 :: SymWord a => SList a -> SInteger
- null :: SymWord a => SList a -> SBool
- head :: SymWord a => SList a -> SBV a
- tail :: SymWord a => SList a -> SList a
- uncons :: SymWord a => SList a -> (SBV a, SList a)
- init :: SymWord a => SList a -> SList a
- singleton :: SymWord a => SBV a -> SList a
- listToListAt :: SymWord a => SList a -> SInteger -> SList a
- elemAt :: forall a. SymWord a => SList a -> SInteger -> SBV a
- (.!!) :: SymWord a => SList a -> SInteger -> SBV a
- implode :: SymWord a => [SBV a] -> SList a
- concat :: SymWord a => SList a -> SList a -> SList a
- (.:) :: SymWord a => SBV a -> SList a -> SList a
- (.++) :: SymWord a => SList a -> SList a -> SList a
- isInfixOf :: SymWord a => SList a -> SList a -> SBool
- isSuffixOf :: SymWord a => SList a -> SList a -> SBool
- isPrefixOf :: SymWord a => SList a -> SList a -> SBool
- take :: SymWord a => SInteger -> SList a -> SList a
- drop :: SymWord a => SInteger -> SList a -> SList a
- subList :: SymWord a => SList a -> SInteger -> SInteger -> SList a
- replace :: SymWord a => SList a -> SList a -> SList a -> SList a
- indexOf :: SymWord a => SList a -> SList a -> SInteger
- offsetIndexOf :: SymWord a => SList a -> SList a -> SInteger -> SInteger

# Length, emptiness

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

Length of a list.

    >>> sat $ \(l :: SList Word16) -> length l .== 2
    Satisfiable. Model:
      s0 = [0,0] :: [SWord16]
    >>> 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 :: SymWord 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 :: SymWord 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 :: SymWord 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) -> bnot (null l) ==> singleton (head l) .++ tail l .== l
    Q.E.D.

uncons :: SymWord a => SList a -> (SBV a, SList a) Source #

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

init :: SymWord 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 :: SymWord 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 :: SymWord 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,0,32] :: [SWord16]

elemAt :: forall a. SymWord a => SList a -> SInteger -> SBV a Source #

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

    >>> prove $ \i -> i .>= 0 &&& i .<= 4 ==> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
    Q.E.D.
    >>> prove $ \(l :: SList Integer) i e -> l `elemAt` i .== e ==> indexOf l (singleton e) .<= i
    Q.E.D.

(.!!) :: SymWord a => SList a -> SInteger -> SBV a Source #

Short cut for `elemAt`

implode :: SymWord 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 -> map (elemAt (implode [e1, e2, e3])) (map literal [0 .. 2]) .== [e1, e2, e3]
    Q.E.D.

concat :: SymWord a => SList a -> SList a -> SList a Source #

Concatenate two lists. See also `.++`.

(.:) :: SymWord a => SBV a -> SList a -> SList a infixr 5 Source #

Prepend an element, the traditional `cons`.

(.++) :: SymWord a => SList a -> SList a -> SList a infixr 5 Source #

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] :: [SInteger]
      s1 =              [6] :: [SInteger]
      s2 = [7,8,9,10,11,12] :: [SInteger]

# Containment

isInfixOf :: SymWord 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 :: SymWord 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 :: SymWord 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 :: SymWord 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 :: SymWord 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 :: SymWord 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 :: SymWord 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 :: SymWord 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 .< length l ==> indexOf l (subList l i 1) .<= i
    Q.E.D.
    >>> prove $ \(l :: SList Word16) i -> i .> 0 &&& i .< length l ==> indexOf l (subList l i 1) .== i
    Falsifiable. Counter-example:
      s0 = [32,0,0] :: [SWord16]
      s1 =        2 :: Integer
    >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 ==> indexOf l1 l2 .== -1
    Q.E.D.

offsetIndexOf :: SymWord 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.