-----------------------------------------------------------------------------
-- |
-- 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
        -- * Reverse
        , reverse
        -- * Conversion to\/from naturals
        , strToNat, natToStr
        ) where

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

import Data.SBV.Core.Data hiding (SeqOp(..))
import Data.SBV.Core.Data (SeqOp(SBVReverse))
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

-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
-- >>> import Prelude hiding (head, tail, init, length, take, drop, concat, null, reverse, (++), (!!))
-- >>> :set -XOverloadedStrings

-- | Length of a string.
--
-- >>> sat $ \s -> length s .== 2
-- Satisfiable. Model:
--   s0 = "BA" :: 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 = forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 StrOp
StrLen (forall a. a -> Maybe a
Just (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 String
cs <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
  = forall a. SymVal a => a -> SBV a
literal (forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null String
cs)
  | Bool
True
  = SString
s forall a. EqSymbolic a => a -> a -> SBool
.== forall a. SymVal a => a -> SBV a
literal String
""

-- | @`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
_:String
cs) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
 = forall a. SymVal a => a -> SBV a
literal String
cs
 | Bool
True
 = SString -> SInteger -> SInteger -> SString
subStr SString
s SInteger
1 (SString -> SInteger
length SString
s 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 :: String
cs@(Char
_:String
_) <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
 = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
P.init String
cs
 | Bool
True
 = SString -> SInteger -> SInteger -> SString
subStr SString
s SInteger
0 (SString -> SInteger
length SString
s 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 = forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 StrOp
StrUnit (forall a. a -> Maybe a
Just 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 = "AB" :: 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 String
cs <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s, Just Integer
ci <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
i, Integer
ci forall a. Ord a => a -> a -> Bool
>= Integer
0, Integer
ci forall a. Ord a => a -> a -> Bool
< forall i a. Num i => [a] -> i
genericLength String
cs, let c :: Int
c = Char -> Int
C.ord (String
cs forall i a. Integral i => [a] -> i -> a
`genericIndex` Integer
ci)
  = forall a. SymVal a => a -> SBV a
literal (Int -> Char
C.chr Int
c)
  | Bool
True
  = forall a b c.
(SymVal a, SymVal b, SymVal c) =>
StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 StrOp
StrNth 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SString -> 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                = forall a b c.
(SymVal a, SymVal b, SymVal c) =>
StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 StrOp
StrConcat (forall a. a -> Maybe a
Just forall a. [a] -> [a] -> [a]
(P.++)) 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
  = forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = forall a b c.
(SymVal a, SymVal b, SymVal c) =>
StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 StrOp
StrContains (forall a. a -> Maybe a
Just (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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
  = forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = forall a b c.
(SymVal a, SymVal b, SymVal c) =>
StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 StrOp
StrPrefixOf (forall a. a -> Maybe a
Just 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
  = forall a. SymVal a => a -> SBV a
literal Bool
True
  | Bool
True
  = forall a b c.
(SymVal a, SymVal b, SymVal c) =>
StrOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 StrOp
StrSuffixOf (forall a. a -> Maybe a
Just 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 = forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0)        (forall a. SymVal a => a -> SBV a
literal String
"")
         forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i forall a. OrdSymbolic a => a -> a -> SBool
.>= SString -> SInteger
length SString
s) SString
s
         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 = forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
ls) (forall a. SymVal a => a -> SBV a
literal String
"")
         forall a b. (a -> b) -> a -> b
$ forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0)  SString
s
         forall a b. (a -> b) -> a -> b
$ SString -> SInteger -> SInteger -> SString
subStr SString
s SInteger
i (SInteger
ls 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 String
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s                    -- a constant string
  , Just Integer
o <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset               -- a constant offset
  , Just Integer
l <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
len                  -- a constant length
  , let lc :: Integer
lc = forall i a. Num i => [a] -> i
genericLength String
c                 -- length of the string
  , let valid :: Integer -> Bool
valid Integer
x = Integer
x forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
x forall a. Ord a => a -> a -> Bool
<= Integer
lc          -- predicate that checks valid point
  , Integer -> Bool
valid Integer
o                                  -- offset is valid
  , Integer
l forall a. Ord a => a -> a -> Bool
>= Integer
0                                   -- length is not-negative
  , Integer -> Bool
valid forall a b. (a -> b) -> a -> b
$ Integer
o forall a. Num a => a -> a -> a
+ Integer
l                            -- we don't overrun
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
l forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o String
c
  | Bool
True                                     -- either symbolic, or something is out-of-bounds
  = 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 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 String
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
src, forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null String
b   -- If src is null, simply prepend
  = SString
dst SString -> SString -> SString
++ SString
s
  | Just String
a <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
  , Just String
b <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
src
  , Just String
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
dst
  = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ forall {a}. Eq a => [a] -> [a] -> [a] -> [a]
walk String
a String
b String
c
  | Bool
True
  = 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 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 forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [a]
i = [a]
newNeedle forall a. [a] -> [a] -> [a]
P.++ forall i a. Integral i => i -> [a] -> [a]
genericDrop (forall i a. Num i => [a] -> i
genericLength [a]
needle :: Integer) [a]
i
                  | Bool
True                    = a
c 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 String
c <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s               -- a constant string
  , Just String
n <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
sub             -- a constant search pattern
  , Just Integer
o <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset          -- at a constant offset
  , Integer
o forall a. Ord a => a -> a -> Bool
>= Integer
0, Integer
o forall a. Ord a => a -> a -> Bool
<= forall i a. Num i => [a] -> i
genericLength String
c        -- offset is good
  = case [Integer
i | (Integer
i, String
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
o ..] (forall a. [a] -> [[a]]
L.tails (forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o String
c)), String
n forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` String
t] of
      (Integer
i:[Integer]
_) -> forall a. SymVal a => a -> SBV a
literal Integer
i
      [Integer]
_     -> -SInteger
1
  | Bool
True
  = 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 forall a. Maybe a
Nothing SString
s SString
sub SInteger
offset

-- | @`reverse` s@ reverses the string.
-- >>> sat $ \s -> reverse s .== "abc"
-- Satisfiable. Model:
--   s0 = "cba" :: String
-- >>> prove $ \s -> reverse s .== "" .<=> null s
-- Q.E.D.
reverse :: SString -> SString
reverse :: SString -> SString
reverse SString
s
  | Just String
s' <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
  = forall a. SymVal a => a -> SBV a
literal (forall a. [a] -> [a]
P.reverse String
s')
  | Bool
True
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KString forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SString
s
                  State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KString (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (Kind -> SeqOp
SBVReverse Kind
KString)) [SV
sva])

-- | @`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 String
a <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
s
 = if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
C.isDigit String
a Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null String
a)
   then forall a. SymVal a => a -> SBV a
literal (forall a. Read a => String -> a
read String
a)
   else -SInteger
1
 | Bool
True
 = forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 StrOp
StrStrToNat 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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
i
 = forall a. SymVal a => a -> SBV a
literal forall a b. (a -> b) -> a -> b
$ if Integer
v forall a. Ord a => a -> a -> Bool
>= Integer
0 then forall a. Show a => a -> String
show Integer
v else String
""
 | Bool
True
 = forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 StrOp
StrNatToStr 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 :: forall a b.
(SymVal a, SymVal b) =>
StrOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 StrOp
w Maybe (a -> b)
mbOp SBV a
a
  | Just SBV b
cv <- 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
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)
        r :: State -> IO SV
r State
st = do SV
sva <- 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 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
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 <- 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
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c)
        r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb <- 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 :: 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
w Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Just SBV d
cv <- 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
  = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d)
        r :: State -> IO SV
r State
st = do SV
sva <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  SV
svb <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
b
                  SV
svc <- 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 :: forall a b.
(SymVal a, SymVal b) =>
Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Maybe (a -> b)
mbOp SBV a
a = forall a. SymVal a => a -> SBV a
literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b)
mbOp forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 :: 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 = forall a. SymVal a => a -> SBV a
literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b -> c)
mbOp forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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 :: 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 = forall a. SymVal a => a -> SBV a
literal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe (a -> b -> c -> d)
mbOp forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 String
s <- forall a. SymVal a => SBV a -> Maybe a
unliteral SString
ss = forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null String
s
                     | Bool
True                   = Bool
False

{-# ANN implode ("HLint: ignore Use concatMap" :: String) #-}