Data.SBV.String

A collection of string/character utilities, useful when working with symbolic strings. 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 OverloadedStrings extension to allow literal strings to be used as symbolic-strings.

Length, emptiness

length :: SString -> SInteger

Length of a string.

>>> sat $ \s -> length s .== 2
Satisfiable. Model:
  s0 = "AB" :: String
>>> sat $ \s -> length s .< 0
Unsatisfiable
>>> prove $ \s1 s2 -> length s1 + length s2 .== length (s1 .++ s2)
Q.E.D.

null :: SString -> SBool

null s is True iff the string is empty

>>> prove $ \s -> null s .<=> length s .== 0
Q.E.D.
>>> prove $ \s -> null s .<=> s .== ""
Q.E.D.

Deconstructing/Reconstructing

head :: SString -> SChar

head returns the head of a string. Unspecified if the string is empty.

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

tail :: SString -> SString

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

>>> prove $ \h s -> tail (singleton h .++ s) .== s
Q.E.D.
>>> prove $ \s -> length s .> 0 .=> length (tail s) .== length s - 1
Q.E.D.
>>> prove $ \s -> sNot (null s) .=> singleton (head s) .++ tail s .== s
Q.E.D.

uncons :: SString -> (SChar, SString)

@uncons returns the pair of the first character and tail. Unspecified if the string is empty.

init :: SString -> SString

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

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

singleton :: SChar -> SString

singleton c is the string of length 1 that contains the only character whose value is the 8-bit value c.

>>> prove $ \c -> c .== literal 'A' .=> singleton c .== "A"
Q.E.D.
>>> prove $ \c -> length (singleton c) .== 1
Q.E.D.

strToStrAt :: SString -> SInteger -> SString

strToStrAt s offset. Substring of length 1 at offset in s. Unspecified if offset is out of bounds.

>>> prove $ \s1 s2 -> strToStrAt (s1 .++ s2) (length s1) .== strToStrAt s2 0
Q.E.D.
>>> sat $ \s -> length s .>= 2 .&& strToStrAt s 0 ./= strToStrAt s (length s - 1)
Satisfiable. Model:
  s0 = "ABC" :: String

strToCharAt :: SString -> SInteger -> SChar

strToCharAt s i is the 8-bit value stored at location i. Unspecified if index is out of bounds.

>>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A'
Q.E.D.

• >>> prove $ s i c -> i inRange (0, length s - 1) .&& s strToCharAt i .== c .=> indexOf s (singleton c) .<= i Q.E.D.

(.!!) :: SString -> SInteger -> SChar

Short cut for strToCharAt

implode :: [SChar] -> SString

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

>>> prove $ \c1 c2 c3 -> length (implode [c1, c2, c3]) .== 3
Q.E.D.
>>> prove $ \c1 c2 c3 -> map (strToCharAt (implode [c1, c2, c3])) (map literal [0 .. 2]) .== [c1, c2, c3]
Q.E.D.

concat :: SString -> SString -> SString

Concatenate two strings. See also .++.

(.:) :: SChar -> SString -> SString infixr 5

Prepend an element, the traditional cons.

snoc :: SString -> SChar -> SString

Append an element

nil :: SString

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

>>> prove $ \l -> length l .== 0 .<=> l .== nil
Q.E.D.

(.++) :: SString -> SString -> SString infixr 5

Short cut for concat.

>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x .++ y .++ z .== "Hello world!"
Satisfiable. Model:
  s0 =  "Hello" :: String
  s1 =      " " :: String
  s2 = "world!" :: String

Containment

isInfixOf :: SString -> SString -> SBool

isInfixOf sub s. Does s contain the substring sub?

>>> prove $ \s1 s2 s3 -> s2 `isInfixOf` (s1 .++ s2 .++ s3)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isInfixOf` s2 .&& s2 `isInfixOf` s1 .<=> s1 .== s2
Q.E.D.

isSuffixOf :: SString -> SString -> SBool

isSuffixOf suf s. Is suf a suffix of s?

>>> prove $ \s1 s2 -> s2 `isSuffixOf` (s1 .++ s2)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isSuffixOf` s2 .=> subStr s2 (length s2 - length s1) (length s1) .== s1
Q.E.D.

isPrefixOf :: SString -> SString -> SBool

isPrefixOf pre s. Is pre a prefix of s?

>>> prove $ \s1 s2 -> s1 `isPrefixOf` (s1 .++ s2)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isPrefixOf` s2 .=> subStr s2 0 (length s1) .== s1
Q.E.D.

Substrings

take :: SInteger -> SString -> SString

take len s. Corresponds to Haskell's take on symbolic-strings.

>>> prove $ \s i -> i .>= 0 .=> length (take i s) .<= i
Q.E.D.

drop :: SInteger -> SString -> SString

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

>>> prove $ \s i -> length (drop i s) .<= length s
Q.E.D.
>>> prove $ \s i -> take i s .++ drop i s .== s
Q.E.D.

subStr :: SString -> SInteger -> SInteger -> SString

subStr s offset len is the substring 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 $ \s i -> i .>= 0 .&& i .< length s .=> subStr s 0 i .++ subStr s i (length s - i) .== s
Q.E.D.
>>> sat  $ \i j -> subStr "hello" i j .== "ell"
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subStr "hell" i j .== "no"
Unsatisfiable

replace :: SString -> SString -> SString -> SString

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

>>> prove $ \s -> replace "hello" s "world" .== "world" .=> s .== "hello"
Q.E.D.
>>> prove $ \s1 s2 s3 -> length s2 .> length s1 .=> replace s1 s2 s3 .== s1
Q.E.D.

indexOf :: SString -> SString -> SInteger

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

• >>> prove $ s i -> i .> 0 .&& i .s .= indexOf s (subStr s i 1) .<= i Q.E.D.

>>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1
Q.E.D.

offsetIndexOf :: SString -> SString -> SInteger -> SInteger

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

>>> prove $ \s sub -> offsetIndexOf s sub 0 .== indexOf s sub
Q.E.D.
>>> prove $ \s sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1
Q.E.D.
>>> prove $ \s sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
Q.E.D.

Conversion to/from naturals

strToNat :: SString -> 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 :: SInteger -> SString

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.