    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.String
    -- Copyright : (c) Joel Burget
    --                 Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- 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.
    -----------------------------------------------------------------------------

    {-# LANGUAGE OverloadedStrings   #-}
    {-# LANGUAGE Rank2Types          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications    #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.String (
            -- * Length, emptiness
              length, null
            -- * Deconstructing/Reconstructing
            , head, tail, uncons, init, singleton, strToStrAt, strToCharAt, (.!!), implode, concat, (.:), snoc, nil, (.++)
            -- * Containment
            , isInfixOf, isSuffixOf, isPrefixOf
            -- * Substrings
            , take, drop, subStr, replace, indexOf, offsetIndexOf
            -- * Conversion to\/from naturals
            , strToNat, natToStr
            ) where

    import Prelude hiding (head, tail, init, length, take, drop, concat, null)
    import qualified Prelude as P

    import Data.SBV.Core.Data hiding (SeqOp(..))
    import Data.SBV.Core.Model

    import qualified Data.Char as C
    import Data.List (genericLength, genericIndex, genericDrop, genericTake)
    import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf)

    import Data.Proxy

    -- For doctest use only
    --
    -- $setup
    -- >>> import Data.SBV.Provers.Prover (prove, sat)
    -- >>> :set -XOverloadedStrings

    -- | Length of a string.
    --
    -- >>> sat $ \s -> length s .== 2
    -- Satisfiable. Model:
    --   s0 = "\NUL\NUL" :: String
    -- >>> sat $ \s -> length s .< 0
    -- Unsatisfiable
    -- >>> prove $ \s1 s2 -> length s1 + length s2 .== length (s1 .++ s2)
    -- Q.E.D.
    length :: SString -> SInteger
    length :: SString -> SInteger
    length = StrOp -> Maybe ([Char] -> Integer) -> SString -> SInteger
    forall a b.
    (SymVal a, SymVal b) =>
    StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 StrOp
    StrLen (([Char] -> Integer) -> Maybe ([Char] -> Integer)
    forall a. a -> Maybe a
    Just (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Int -> Integer) -> ([Char] -> Int) -> [Char] -> Integer
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    P.length))

    -- | @`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.
    null :: SString -> SBool
    null :: SString -> SBool
    null s :: SString
    s
      | Just cs :: [Char]
    cs <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    P.null [Char]
    cs)
      | Bool
    True
      = SString
    s SString -> SString -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal ""

    -- | @`head`@ returns the head of a string. Unspecified if the string is empty.
    --
    -- >>> prove $ \c -> head (singleton c) .== c
    -- Q.E.D.
    head :: SString -> SChar
    head :: SString -> SChar
    head = (SString -> SInteger -> SChar
    `strToCharAt` 0)

    -- | @`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.
    tail :: SString -> SString
    tail :: SString -> SString
    tail s :: SString
    s
     | Just (_:cs :: [Char]
    cs) <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s
     = [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal [Char]
    cs
     | Bool
    True
     = SString -> SInteger -> SInteger -> SString
    subStr SString
    s 1 (SString -> SInteger
    length SString
    s SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 1)

    -- | @`uncons` returns the pair of the first character and tail. Unspecified if the string is empty.
    uncons :: SString -> (SChar, SString)
    uncons :: SString -> (SChar, SString)
    uncons l :: SString
    l = (SString -> SChar
    head SString
    l, SString -> SString
    tail SString
    l)

    -- | @`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.
    init :: SString -> SString
    init :: SString -> SString
    init s :: SString
    s
     | Just cs :: [Char]
    cs@(_:_) <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s
     = [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> SString) -> [Char] -> SString
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    forall a. [a] -> [a]
    P.init [Char]
    cs
     | Bool
    True
     = SString -> SInteger -> SInteger -> SString
    subStr SString
    s 0 (SString -> SInteger
    length SString
    s SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - 1)

    -- | @`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.
    singleton :: SChar -> SString
    singleton :: SChar -> SString
    singleton = StrOp -> Maybe (Char -> [Char]) -> SChar -> SString
    forall a b.
    (SymVal a, SymVal b) =>
    StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 StrOp
    StrUnit ((Char -> [Char]) -> Maybe (Char -> [Char])
    forall a. a -> Maybe a
    Just Char -> [Char]
    forall a. a -> [a]
    wrap)
      where wrap :: a -> [a]
    wrap c :: a
    c = [a
    c]

    -- | @`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 = "\NUL\NUL\EOT" :: String
    strToStrAt :: SString -> SInteger -> SString
    strToStrAt :: SString -> SInteger -> SString
    strToStrAt s :: SString
    s offset :: SInteger
    offset = SString -> SInteger -> SInteger -> SString
    subStr SString
    s SInteger
    offset 1

    -- | @`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.
    strToCharAt :: SString -> SInteger -> SChar
    strToCharAt :: SString -> SInteger -> SChar
    strToCharAt s :: SString
    s i :: SInteger
    i
      | Just cs :: [Char]
    cs <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s, Just ci :: Integer
    ci <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    i, Integer
    ci Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0, Integer
    ci Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Char] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Char]
    cs, let c :: Int
    c = Char -> Int
    C.ord ([Char]
    cs [Char] -> Integer -> Char
    forall i a. Integral i => [a] -> i -> a
    `genericIndex` Integer
    ci)
      = Char -> SChar
    forall a. SymVal a => a -> SBV a
    literal (Int -> Char
    C.chr Int
    c)
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> Integer -> Char)
    -> SString
    -> SInteger
    -> SChar
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 StrOp
    StrNth Maybe ([Char] -> Integer -> Char)
    forall a. Maybe a
    Nothing SString
    s SInteger
    i

    -- | Short cut for 'strToCharAt'
    (.!!) :: SString -> SInteger -> SChar
    .!! :: SString -> SInteger -> SChar
    (.!!) = SString -> SInteger -> SChar
    strToCharAt

    -- | @`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.
    implode :: [SChar] -> SString
    implode :: [SChar] -> SString
    implode = (SChar -> SString -> SString) -> SString -> [SChar] -> SString
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (SString -> SString -> SString
    (.++) (SString -> SString -> SString)
    -> (SChar -> SString) -> SChar -> SString -> SString
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SChar -> SString
    singleton) ""

    -- | Prepend an element, the traditional @cons@.
    infixr 5 .:
    (.:) :: SChar -> SString -> SString
    c :: SChar
    c .: :: SChar -> SString -> SString
    .: cs :: SString
    cs = SChar -> SString
    singleton SChar
    c SString -> SString -> SString
    .++ SString
    cs

    -- | Append an element
    snoc :: SString -> SChar -> SString
    s :: SString
    s snoc :: SString -> SChar -> SString
    `snoc` c :: SChar
    c = SString
    s SString -> SString -> SString
    .++ SChar -> SString
    singleton SChar
    c

    -- | 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.
    nil :: SString
    nil :: SString
    nil = ""

    -- | Concatenate two strings. See also `.++`.
    concat :: SString -> SString -> SString
    concat :: SString -> SString -> SString
    concat x :: SString
    x y :: SString
    y | SString -> Bool
    isConcretelyEmpty SString
    x = SString
    y
               | SString -> Bool
    isConcretelyEmpty SString
    y = SString
    x
               | Bool
    True                = StrOp
    -> Maybe ([Char] -> [Char] -> [Char])
    -> SString
    -> SString
    -> SString
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 StrOp
    StrConcat (([Char] -> [Char] -> [Char]) -> Maybe ([Char] -> [Char] -> [Char])
    forall a. a -> Maybe a
    Just [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    (++)) SString
    x SString
    y

    -- | 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
    infixr 5 .++
    (.++) :: SString -> SString -> SString
    .++ :: SString -> SString -> SString
    (.++) = SString -> SString -> SString
    concat

    -- | @`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.
    isInfixOf :: SString -> SString -> SBool
    sub :: SString
    sub isInfixOf :: SString -> SString -> SBool
    `isInfixOf` s :: SString
    s
      | SString -> Bool
    isConcretelyEmpty SString
    sub
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal Bool
    True
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> [Char] -> Bool) -> SString -> SString -> SBool
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 StrOp
    StrContains (([Char] -> [Char] -> Bool) -> Maybe ([Char] -> [Char] -> Bool)
    forall a. a -> Maybe a
    Just (([Char] -> [Char] -> Bool) -> [Char] -> [Char] -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    L.isInfixOf)) SString
    s SString
    sub -- NB. flip, since `StrContains` takes args in rev order!

    -- | @`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.
    isPrefixOf :: SString -> SString -> SBool
    pre :: SString
    pre isPrefixOf :: SString -> SString -> SBool
    `isPrefixOf` s :: SString
    s
      | SString -> Bool
    isConcretelyEmpty SString
    pre
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal Bool
    True
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> [Char] -> Bool) -> SString -> SString -> SBool
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 StrOp
    StrPrefixOf (([Char] -> [Char] -> Bool) -> Maybe ([Char] -> [Char] -> Bool)
    forall a. a -> Maybe a
    Just [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    L.isPrefixOf) SString
    pre SString
    s

    -- | @`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.
    isSuffixOf :: SString -> SString -> SBool
    suf :: SString
    suf isSuffixOf :: SString -> SString -> SBool
    `isSuffixOf` s :: SString
    s
      | SString -> Bool
    isConcretelyEmpty SString
    suf
      = Bool -> SBool
    forall a. SymVal a => a -> SBV a
    literal Bool
    True
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> [Char] -> Bool) -> SString -> SString -> SBool
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 StrOp
    StrSuffixOf (([Char] -> [Char] -> Bool) -> Maybe ([Char] -> [Char] -> Bool)
    forall a. a -> Maybe a
    Just [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    L.isSuffixOf) SString
    suf SString
    s

    -- | @`take` len s@. Corresponds to Haskell's `take` on symbolic-strings.
    --
    -- >>> prove $ \s i -> i .>= 0 .=> length (take i s) .<= i
    -- Q.E.D.
    take :: SInteger -> SString -> SString
    take :: SInteger -> SString -> SString
    take i :: SInteger
    i s :: SString
    s = SBool -> SString -> SString -> SString
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= 0)        ([Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal "")
             (SString -> SString) -> SString -> SString
    forall a b. (a -> b) -> a -> b
    $ SBool -> SString -> SString -> SString
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SString -> SInteger
    length SString
    s) SString
    s
             (SString -> SString) -> SString -> SString
    forall a b. (a -> b) -> a -> b
    $ SString -> SInteger -> SInteger -> SString
    subStr SString
    s 0 SInteger
    i

    -- | @`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.
    drop :: SInteger -> SString -> SString
    drop :: SInteger -> SString -> SString
    drop i :: SInteger
    i s :: SString
    s = SBool -> SString -> SString -> SString
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SInteger
    ls) ([Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal "")
             (SString -> SString) -> SString -> SString
    forall a b. (a -> b) -> a -> b
    $ SBool -> SString -> SString -> SString
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SInteger
    i SInteger -> SInteger -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= 0)  SString
    s
             (SString -> SString) -> SString -> SString
    forall a b. (a -> b) -> a -> b
    $ SString -> SInteger -> SInteger -> SString
    subStr SString
    s SInteger
    i (SInteger
    ls SInteger -> SInteger -> SInteger
    forall a. Num a => a -> a -> a
    - SInteger
    i)
      where ls :: SInteger
    ls = SString -> SInteger
    length SString
    s

    -- | @`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
    subStr :: SString -> SInteger -> SInteger -> SString
    subStr :: SString -> SInteger -> SInteger -> SString
    subStr s :: SString
    s offset :: SInteger
    offset len :: SInteger
    len
      | Just c :: [Char]
    c <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s                    -- a constant string
      , Just o :: Integer
    o <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    offset               -- a constant offset
      , Just l :: Integer
    l <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    len                  -- a constant length
      , let lc :: Integer
    lc = [Char] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Char]
    c                 -- length of the string
      , let valid :: Integer -> Bool
    valid x :: Integer
    x = Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 Bool -> Bool -> Bool
    && Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lc          -- predicate that checks valid point
      , Integer -> Bool
    valid Integer
    o                                  -- offset is valid
      , Integer
    l Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0                                   -- length is not-negative
      , Integer -> Bool
    valid (Integer -> Bool) -> Integer -> Bool
    forall a b. (a -> b) -> a -> b
    $ Integer
    o Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    l                            -- we don't overrun
      = [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> SString) -> [Char] -> SString
    forall a b. (a -> b) -> a -> b
    $ Integer -> [Char] -> [Char]
    forall i a. Integral i => i -> [a] -> [a]
    genericTake Integer
    l ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ Integer -> [Char] -> [Char]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop Integer
    o [Char]
    c
      | Bool
    True                                     -- either symbolic, or something is out-of-bounds
      = StrOp
    -> Maybe ([Char] -> Integer -> Integer -> [Char])
    -> SString
    -> SInteger
    -> SInteger
    -> SString
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    StrOp
    -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 StrOp
    StrSubstr Maybe ([Char] -> Integer -> Integer -> [Char])
    forall a. Maybe a
    Nothing SString
    s SInteger
    offset SInteger
    len

    -- | @`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.
    replace :: SString -> SString -> SString -> SString
    replace :: SString -> SString -> SString -> SString
    replace s :: SString
    s src :: SString
    src dst :: SString
    dst
      | Just b :: [Char]
    b <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    src, [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    P.null [Char]
    b   -- If src is null, simply prepend
      = SString
    dst SString -> SString -> SString
    .++ SString
    s
      | Just a :: [Char]
    a <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s
      , Just b :: [Char]
    b <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    src
      , Just c :: [Char]
    c <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    dst
      = [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> SString) -> [Char] -> SString
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char] -> [Char] -> [Char]
    forall a. Eq a => [a] -> [a] -> [a] -> [a]
    walk [Char]
    a [Char]
    b [Char]
    c
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> [Char] -> [Char] -> [Char])
    -> SString
    -> SString
    -> SString
    -> SString
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    StrOp
    -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 StrOp
    StrReplace Maybe ([Char] -> [Char] -> [Char] -> [Char])
    forall a. Maybe a
    Nothing SString
    s SString
    src SString
    dst
      where walk :: [a] -> [a] -> [a] -> [a]
    walk haystack :: [a]
    haystack needle :: [a]
    needle newNeedle :: [a]
    newNeedle = [a] -> [a]
    go [a]
    haystack   -- note that needle is guaranteed non-empty here.
               where go :: [a] -> [a]
    go []       = []
                     go i :: [a]
    i@(c :: a
    c:cs :: [a]
    cs)
                      | [a]
    needle [a] -> [a] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `L.isPrefixOf` [a]
    i = [a]
    newNeedle [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [a] -> [a]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop ([a] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [a]
    needle :: Integer) [a]
    i
                      | Bool
    True                    = a
    c a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> [a]
    go [a]
    cs

    -- | @`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 .< length 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.
    indexOf :: SString -> SString -> SInteger
    indexOf :: SString -> SString -> SInteger
    indexOf s :: SString
    s sub :: SString
    sub = SString -> SString -> SInteger -> SInteger
    offsetIndexOf SString
    s SString
    sub 0

    -- | @`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.
    offsetIndexOf :: SString -> SString -> SInteger -> SInteger
    offsetIndexOf :: SString -> SString -> SInteger -> SInteger
    offsetIndexOf s :: SString
    s sub :: SString
    sub offset :: SInteger
    offset
      | Just c :: [Char]
    c <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s               -- a constant string
      , Just n :: [Char]
    n <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    sub             -- a constant search pattern
      , Just o :: Integer
    o <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    offset          -- at a constant offset
      , Integer
    o Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0, Integer
    o Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [Char] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [Char]
    c        -- offset is good
      = case [Integer
    i | (i :: Integer
    i, t :: [Char]
    t) <- [Integer] -> [[Char]] -> [(Integer, [Char])]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Integer
    o ..] ([Char] -> [[Char]]
    forall a. [a] -> [[a]]
    L.tails (Integer -> [Char] -> [Char]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop Integer
    o [Char]
    c)), [Char]
    n [Char] -> [Char] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `L.isPrefixOf` [Char]
    t] of
          (i :: Integer
    i:_) -> Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    i
          _     -> -1
      | Bool
    True
      = StrOp
    -> Maybe ([Char] -> [Char] -> Integer -> Integer)
    -> SString
    -> SString
    -> SInteger
    -> SInteger
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    StrOp
    -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 StrOp
    StrIndexOf Maybe ([Char] -> [Char] -> Integer -> Integer)
    forall a. Maybe a
    Nothing SString
    s SString
    sub SInteger
    offset

    -- | @`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.
    strToNat :: SString -> SInteger
    strToNat :: SString -> SInteger
    strToNat s :: SString
    s
     | Just a :: [Char]
    a <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    s
     = if (Char -> Bool) -> [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    C.isDigit [Char]
    a Bool -> Bool -> Bool
    && Bool -> Bool
    not ([Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    P.null [Char]
    a)
       then Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> Integer
    forall a. Read a => [Char] -> a
    read [Char]
    a)
       else -1
     | Bool
    True
     = StrOp -> Maybe ([Char] -> Integer) -> SString -> SInteger
    forall a b.
    (SymVal a, SymVal b) =>
    StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 StrOp
    StrStrToNat Maybe ([Char] -> Integer)
    forall a. Maybe a
    Nothing SString
    s

    -- | @`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.
    natToStr :: SInteger -> SString
    natToStr :: SInteger -> SString
    natToStr i :: SInteger
    i
     | Just v :: Integer
    v <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    i
     = [Char] -> SString
    forall a. SymVal a => a -> SBV a
    literal ([Char] -> SString) -> [Char] -> SString
    forall a b. (a -> b) -> a -> b
    $ if Integer
    v Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 then Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    v else ""
     | Bool
    True
     = StrOp -> Maybe (Integer -> [Char]) -> SInteger -> SString
    forall a b.
    (SymVal a, SymVal b) =>
    StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 StrOp
    StrNatToStr Maybe (Integer -> [Char])
    forall a. Maybe a
    Nothing SInteger
    i

    -- | Lift a unary operator over strings.
    lift1 :: forall a b. (SymVal a, SymVal b) => StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 :: StrOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 w :: StrOp
    w mbOp :: Maybe (a -> b)
    mbOp a :: SBV a
    a
      | Just cv :: SBV b
    cv <- Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    forall a b.
    (SymVal a, SymVal b) =>
    Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    concEval1 Maybe (a -> b)
    mbOp SBV a
    a
      = SBV b
    cv
      | Bool
    True
      = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SVal -> SBV b) -> SVal -> SBV b
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (StrOp -> Op
    StrOp StrOp
    w) [SV
    sva])

    -- | Lift a binary operator over strings.
    lift2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 :: StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 w :: StrOp
    w mbOp :: Maybe (a -> b -> c)
    mbOp a :: SBV a
    a b :: SBV b
    b
      | Just cv :: SBV c
    cv <- Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 Maybe (a -> b -> c)
    mbOp SBV a
    a SBV b
    b
      = SBV c
    cv
      | Bool
    True
      = SVal -> SBV c
    forall a. SVal -> SBV a
    SBV (SVal -> SBV c) -> SVal -> SBV c
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    b
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (StrOp -> Op
    StrOp StrOp
    w) [SV
    sva, SV
    svb])

    -- | Lift a ternary operator over strings.
    lift3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => StrOp -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 :: StrOp
    -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 w :: StrOp
    w mbOp :: Maybe (a -> b -> c -> d)
    mbOp a :: SBV a
    a b :: SBV b
    b c :: SBV c
    c
      | Just cv :: SBV d
    cv <- Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    concEval3 Maybe (a -> b -> c -> d)
    mbOp SBV a
    a SBV b
    b SBV c
    c
      = SBV d
    cv
      | Bool
    True
      = SVal -> SBV d
    forall a. SVal -> SBV a
    SBV (SVal -> SBV d) -> SVal -> SBV d
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    b
                      SV
    svc <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    c
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (StrOp -> Op
    StrOp StrOp
    w) [SV
    sva, SV
    svb, SV
    svc])

    -- | Concrete evaluation for unary ops
    concEval1 :: (SymVal a, SymVal b) => Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    concEval1 :: Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    concEval1 mbOp :: Maybe (a -> b)
    mbOp a :: SBV a
    a = b -> SBV b
    forall a. SymVal a => a -> SBV a
    literal (b -> SBV b) -> Maybe b -> Maybe (SBV b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b)
    mbOp Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a)

    -- | Concrete evaluation for binary ops
    concEval2 :: (SymVal a, SymVal b, SymVal c) => Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 :: Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 mbOp :: Maybe (a -> b -> c)
    mbOp a :: SBV a
    a b :: SBV b
    b = c -> SBV c
    forall a. SymVal a => a -> SBV a
    literal (c -> SBV c) -> Maybe c -> Maybe (SBV c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b -> c)
    mbOp Maybe (a -> b -> c) -> Maybe a -> Maybe (b -> c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a Maybe (b -> c) -> Maybe b -> Maybe c
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    b)

    -- | Concrete evaluation for ternary ops
    concEval3 :: (SymVal a, SymVal b, SymVal c, SymVal d) => Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    concEval3 :: Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    concEval3 mbOp :: Maybe (a -> b -> c -> d)
    mbOp a :: SBV a
    a b :: SBV b
    b c :: SBV c
    c = d -> SBV d
    forall a. SymVal a => a -> SBV a
    literal (d -> SBV d) -> Maybe d -> Maybe (SBV d)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b -> c -> d)
    mbOp Maybe (a -> b -> c -> d) -> Maybe a -> Maybe (b -> c -> d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a Maybe (b -> c -> d) -> Maybe b -> Maybe (c -> d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    b Maybe (c -> d) -> Maybe c -> Maybe d
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    c)

    -- | Is the string concretely known empty?
    isConcretelyEmpty :: SString -> Bool
    isConcretelyEmpty :: SString -> Bool
    isConcretelyEmpty ss :: SString
    ss | Just s :: [Char]
    s <- SString -> Maybe [Char]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SString
    ss = [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    P.null [Char]
    s
                         | Bool
    True                   = Bool
    False