{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.String (
length, null
, head, tail, uncons, init, singleton, strToStrAt, strToCharAt, (.!!), implode, concat, (.:), snoc, nil, (.++)
, isInfixOf, isSuffixOf, isPrefixOf
, take, drop, subStr, replace, indexOf, offsetIndexOf
, 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
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 :: 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 :: SString -> SChar
head :: SString -> SChar
head = (SString -> SInteger -> SChar
`strToCharAt` 0)
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 :: SString -> (SChar, SString)
uncons :: SString -> (SChar, SString)
uncons l :: SString
l = (SString -> SChar
head SString
l, SString -> SString
tail SString
l)
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 :: 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 :: 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 :: 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
(.!!) :: SString -> SInteger -> SChar
.!! :: SString -> SInteger -> SChar
(.!!) = SString -> SInteger -> SChar
strToCharAt
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) ""
infixr 5 .:
(.:) :: SChar -> SString -> SString
c :: SChar
c .: :: SChar -> SString -> SString
.: cs :: SString
cs = SChar -> SString
singleton SChar
c SString -> SString -> SString
.++ SString
cs
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
nil :: SString
nil :: SString
nil = ""
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
infixr 5 .++
(.++) :: SString -> SString -> SString
.++ :: SString -> SString -> SString
(.++) = SString -> SString -> SString
concat
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
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 :: 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 :: 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 :: 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 :: 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
, Just o :: Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset
, Just l :: Integer
l <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
len
, let lc :: Integer
lc = [Char] -> Integer
forall i a. Num i => [a] -> i
genericLength [Char]
c
, 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
, Integer -> Bool
valid Integer
o
, Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 0
, 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
= [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
= 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 :: 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
= 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
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 :: 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 :: 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
, Just n :: [Char]
n <- SString -> Maybe [Char]
forall a. SymVal a => SBV a -> Maybe a
unliteral SString
sub
, Just o :: Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
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
= 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 :: 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 :: 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
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])
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])
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])
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)
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)
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)
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