-----------------------------------------------------------------------------
-- |
-- 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 SString
s
  | Just [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 [Char]
""

-- | @`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` SInteger
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 SString
s
 | Just (Char
_:[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 SInteger
1 (SString -> SInteger
length SString
s SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
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 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 SString
s
 | Just cs :: [Char]
cs@(Char
_:[Char]
_) <- 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 SInteger
0 (SString -> SInteger
length SString
s SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
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 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 SString
s SInteger
offset = SString -> SInteger -> SInteger -> SString
subStr SString
s SInteger
offset SInteger
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 SString
s SInteger
i
  | Just [Char]
cs <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s, Just 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
>= Integer
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) SString
""

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

-- | Append an element
snoc :: SString -> SChar -> SString
SString
s snoc :: SString -> SChar -> SString
`snoc` 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 = SString
""

-- | Concatenate two strings. See also `.++`.
concat :: SString -> SString -> SString
concat :: SString -> SString -> SString
concat SString
x 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
SString
sub isInfixOf :: SString -> SString -> SBool
`isInfixOf` 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
SString
pre isPrefixOf :: SString -> SString -> SBool
`isPrefixOf` 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
SString
suf isSuffixOf :: SString -> SString -> SBool
`isSuffixOf` 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 SInteger
i 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
0)        ([Char] -> SString
forall a. SymVal a => a -> SBV a
literal [Char]
"")
         (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 SInteger
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 SInteger
i 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 [Char]
"")
         (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
.<= SInteger
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 SString
s SInteger
offset SInteger
len
  | Just [Char]
c <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s                    -- a constant string
  , Just Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset               -- a constant offset
  , Just 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 Integer
x = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
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
>= Integer
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 SString
s SString
src SString
dst
  | Just [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 [Char]
a <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
  , Just [Char]
b <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
src
  , Just [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 [a]
haystack [a]
needle [a]
newNeedle = [a] -> [a]
go [a]
haystack   -- note that needle is guaranteed non-empty here.
           where go :: [a] -> [a]
go []       = []
                 go i :: [a]
i@(a
c:[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 SString
s SString
sub = SString -> SString -> SInteger -> SInteger
offsetIndexOf SString
s SString
sub SInteger
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 SString
s SString
sub SInteger
offset
  | Just [Char]
c <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s               -- a constant string
  , Just [Char]
n <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
sub             -- a constant search pattern
  , Just 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
>= Integer
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 | (Integer
i, [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
      (Integer
i:[Integer]
_) -> Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i
      [Integer]
_     -> -SInteger
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 SString
s
 | Just [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 -SInteger
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 SInteger
i
 | Just 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
>= Integer
0 then Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
v else [Char]
""
 | 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 StrOp
w Maybe (a -> b)
mbOp SBV a
a
  | Just 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 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 StrOp
w Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  | Just 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 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 StrOp
w Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Just 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 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 Maybe (a -> b)
mbOp 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 Maybe (a -> b -> c)
mbOp SBV a
a 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 Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b 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 SString
ss | Just [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