{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.List (
length, null
, head, tail, uncons, init, singleton, listToListAt, elemAt, (!!), implode, concat, (.:), snoc, nil, (++)
, elem, notElem, isInfixOf, isSuffixOf, isPrefixOf
, take, drop, subList, replace, indexOf, offsetIndexOf
, reverse
, map, mapi
, foldl, foldr, foldli, foldri
, zip, zipWith
, filter
, all, any
) where
import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem,
notElem, reverse, (++), (!!), map, foldl, foldr, zip, zipWith, filter, all, any)
import qualified Prelude as P
import Data.SBV.Core.Data hiding (StrOp(..))
import Data.SBV.Core.Model
import Data.SBV.Lambda
import Data.SBV.Tuple
import Data.Maybe (isNothing, catMaybes)
import Data.List (genericLength, genericIndex, genericDrop, genericTake)
import qualified Data.List as L (tails, isSuffixOf, isPrefixOf, isInfixOf)
import Data.Proxy
length :: SymVal a => SList a -> SInteger
length :: forall a. SymVal a => SList a -> SInteger
length = SeqOp -> Maybe ([a] -> Integer) -> SBV [a] -> SInteger
forall a b.
(SymVal a, SymVal b) =>
SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 SeqOp
SeqLen (([a] -> Integer) -> Maybe ([a] -> Integer)
forall a. a -> Maybe a
Just (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
P.length))
null :: SymVal a => SList a -> SBool
null :: forall a. SymVal a => SList a -> SBool
null SList a
l
| Just [a]
cs <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
= Bool -> SBool
forall a. SymVal a => a -> SBV a
literal ([a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
cs)
| Bool
True
= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
head :: SymVal a => SList a -> SBV a
head :: forall a. SymVal a => SList a -> SBV a
head = (SList a -> SInteger -> SBV a
forall a. SymVal a => SList a -> SInteger -> SBV a
`elemAt` SInteger
0)
tail :: SymVal a => SList a -> SList a
tail :: forall a. SymVal a => SList a -> SList a
tail SList a
l
| Just (a
_:[a]
cs) <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
= [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
cs
| Bool
True
= SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
1 (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)
uncons :: SymVal a => SList a -> (SBV a, SList a)
uncons :: forall a. SymVal a => SList a -> (SBV a, SList a)
uncons SList a
l = (SList a -> SBV a
forall a. SymVal a => SList a -> SBV a
head SList a
l, SList a -> SList a
forall a. SymVal a => SList a -> SList a
tail SList a
l)
init :: SymVal a => SList a -> SList a
init :: forall a. SymVal a => SList a -> SList a
init SList a
l
| Just cs :: [a]
cs@(a
_:[a]
_) <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
= [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. HasCallStack => [a] -> [a]
P.init [a]
cs
| Bool
True
= SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
0 (SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
1)
singleton :: SymVal a => SBV a -> SList a
singleton :: forall a. SymVal a => SBV a -> SList a
singleton = SeqOp -> Maybe (a -> [a]) -> SBV a -> SBV [a]
forall a b.
(SymVal a, SymVal b) =>
SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 SeqOp
SeqUnit ((a -> [a]) -> Maybe (a -> [a])
forall a. a -> Maybe a
Just (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []))
listToListAt :: SymVal a => SList a -> SInteger -> SList a
listToListAt :: forall a. SymVal a => SList a -> SInteger -> SList a
listToListAt SList a
s SInteger
offset = SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
s SInteger
offset SInteger
1
elemAt :: SymVal a => SList a -> SInteger -> SBV a
elemAt :: forall a. SymVal a => SList a -> SInteger -> SBV a
elemAt SList a
l SInteger
i
| Just [a]
xs <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, 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
< [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
xs, let x :: a
x = [a]
xs [a] -> Integer -> a
forall i a. Integral i => [a] -> i -> a
`genericIndex` Integer
ci
= a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
x
| Bool
True
= SeqOp
-> Maybe ([a] -> Integer -> a) -> SList a -> SInteger -> SBV a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
SeqNth Maybe ([a] -> Integer -> a)
forall a. Maybe a
Nothing SList a
l SInteger
i
(!!) :: SymVal a => SList a -> SInteger -> SBV a
!! :: forall a. SymVal a => SList a -> SInteger -> SBV a
(!!) = SList a -> SInteger -> SBV a
forall a. SymVal a => SList a -> SInteger -> SBV a
elemAt
implode :: SymVal a => [SBV a] -> SList a
implode :: forall a. SymVal a => [SBV a] -> SList a
implode = (SBV a -> SList a -> SList a) -> SList a -> [SBV a] -> SList a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
P.foldr (SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
(++) (SList a -> SList a -> SList a)
-> (SBV a -> SList a) -> SBV a -> SList a -> SList a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton) ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])
infixr 5 .:
(.:) :: SymVal a => SBV a -> SList a -> SList a
SBV a
a .: :: forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
as = SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton SBV a
a SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
as
snoc :: SymVal a => SList a -> SBV a -> SList a
SList a
as snoc :: forall a. SymVal a => SList a -> SBV a -> SList a
`snoc` SBV a
a = SList a
as SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton SBV a
a
nil :: SymVal a => SList a
nil :: forall a. SymVal a => SList a
nil = []
infixr 5 ++
(++) :: SymVal a => SList a -> SList a -> SList a
SList a
x ++ :: forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
y | SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
x = SList a
y
| SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
y = SList a
x
| Bool
True = SeqOp -> Maybe ([a] -> [a] -> [a]) -> SList a -> SList a -> SList a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
SeqConcat (([a] -> [a] -> [a]) -> Maybe ([a] -> [a] -> [a])
forall a. a -> Maybe a
Just [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(P.++)) SList a
x SList a
y
elem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
SBV a
e elem :: forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
l = SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton SBV a
e SList a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isInfixOf` SList a
l
notElem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
SBV a
e notElem :: forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`notElem` SList a
l = SBool -> SBool
sNot (SBV a
e SBV a -> SList a -> SBool
forall a. (Eq a, SymVal a) => SBV a -> SList a -> SBool
`elem` SList a
l)
isInfixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
sub isInfixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isInfixOf` SList a
l
| SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
sub
= Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
| Bool
True
= SeqOp -> Maybe ([a] -> [a] -> Bool) -> SList a -> SList a -> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
SeqContains (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just (([a] -> [a] -> Bool) -> [a] -> [a] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isInfixOf)) SList a
l SList a
sub
isPrefixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
pre isPrefixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isPrefixOf` SList a
l
| SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
pre
= Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
| Bool
True
= SeqOp -> Maybe ([a] -> [a] -> Bool) -> SList a -> SList a -> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
SeqPrefixOf (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isPrefixOf) SList a
pre SList a
l
isSuffixOf :: (Eq a, SymVal a) => SList a -> SList a -> SBool
SList a
suf isSuffixOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SBool
`isSuffixOf` SList a
l
| SList a -> Bool
forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
suf
= Bool -> SBool
forall a. SymVal a => a -> SBV a
literal Bool
True
| Bool
True
= SeqOp -> Maybe ([a] -> [a] -> Bool) -> SList a -> SList a -> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
SeqSuffixOf (([a] -> [a] -> Bool) -> Maybe ([a] -> [a] -> Bool)
forall a. a -> Maybe a
Just [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isSuffixOf) SList a
suf SList a
l
take :: SymVal a => SInteger -> SList a -> SList a
take :: forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
i SList a
l = SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])
(SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
l) SList a
l
(SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
0 SInteger
i
drop :: SymVal a => SInteger -> SList a -> SList a
drop :: forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
i SList a
s = SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>= SInteger
ls) ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal [])
(SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
0) SList a
s
(SList a -> SList a) -> SList a -> SList a
forall a b. (a -> b) -> a -> b
$ SList a -> SInteger -> SInteger -> SList a
forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
s SInteger
i (SInteger
ls SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
i)
where ls :: SInteger
ls = SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList a
s
subList :: SymVal a => SList a -> SInteger -> SInteger -> SList a
subList :: forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
subList SList a
l SInteger
offset SInteger
len
| Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
, Just Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset
, Just Integer
sz <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
len
, let lc :: Integer
lc = [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c
, 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
, Integer -> Bool
valid Integer
o
, Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
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
sz
= [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericTake Integer
sz ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o [a]
c
| Bool
True
= SeqOp
-> Maybe ([a] -> Integer -> Integer -> [a])
-> SList a
-> SInteger
-> SInteger
-> SList a
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
SeqOp
-> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
lift3 SeqOp
SeqSubseq Maybe ([a] -> Integer -> Integer -> [a])
forall a. Maybe a
Nothing SList a
l SInteger
offset SInteger
len
replace :: (Eq a, SymVal a) => SList a -> SList a -> SList a -> SList a
replace :: forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SList a -> SList a
replace SList a
l SList a
src SList a
dst
| Just [a]
b <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
src, [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
b
= SList a
dst SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
l
| Just [a]
a <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
, Just [a]
b <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
src
, Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
dst
= [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> SList a) -> [a] -> SList a
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [a] -> [a]
forall {a}. Eq a => [a] -> [a] -> [a] -> [a]
walk [a]
a [a]
b [a]
c
| Bool
True
= SeqOp
-> Maybe ([a] -> [a] -> [a] -> [a])
-> SList a
-> SList a
-> SList a
-> SList a
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
SeqOp
-> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
lift3 SeqOp
SeqReplace Maybe ([a] -> [a] -> [a] -> [a])
forall a. Maybe a
Nothing SList a
l SList a
src SList a
dst
where walk :: [a] -> [a] -> [a] -> [a]
walk [a]
haystack [a]
needle [a]
newNeedle = [a] -> [a]
go [a]
haystack
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]
P.++ 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 :: (Eq a, SymVal a) => SList a -> SList a -> SInteger
indexOf :: forall a. (Eq a, SymVal a) => SList a -> SList a -> SInteger
indexOf SList a
s SList a
sub = SList a -> SList a -> SInteger -> SInteger
forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SInteger -> SInteger
offsetIndexOf SList a
s SList a
sub SInteger
0
offsetIndexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger -> SInteger
offsetIndexOf :: forall a.
(Eq a, SymVal a) =>
SList a -> SList a -> SInteger -> SInteger
offsetIndexOf SList a
s SList a
sub SInteger
offset
| Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
s
, Just [a]
n <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sub
, Just 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
>= Integer
0, Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c
= case [Integer
i | (Integer
i, [a]
t) <- [Integer] -> [[a]] -> [(Integer, [a])]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [Integer
Item [Integer]
o ..] ([a] -> [[a]]
forall a. [a] -> [[a]]
L.tails (Integer -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericDrop Integer
o [a]
c)), [a]
n [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [a]
t] of
(Integer
i:[Integer]
_) -> Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
i
[Integer]
_ -> -SInteger
1
| Bool
True
= SeqOp
-> Maybe ([a] -> [a] -> Integer -> Integer)
-> SList a
-> SList a
-> SInteger
-> SInteger
forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
SeqOp
-> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
lift3 SeqOp
SeqIndexOf Maybe ([a] -> [a] -> Integer -> Integer)
forall a. Maybe a
Nothing SList a
s SList a
sub SInteger
offset
reverse :: SymVal a => SList a -> SList a
reverse :: forall a. SymVal a => SList a -> SList a
reverse SList a
l
| Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
= [a] -> SList a
forall a. SymVal a => a -> SBV a
literal ([a] -> [a]
forall a. [a] -> [a]
P.reverse [a]
l')
| Bool
True
= SVal -> SList a
forall a. SVal -> SBV a
SBV (SVal -> SList a) -> SVal -> SList a
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 = SList a -> Kind
forall a. HasKind a => a -> Kind
kindOf SList a
l
r :: State -> IO SV
r State
st = do SV
sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (Kind -> SeqOp
SBVReverse Kind
k)) [Item [SV]
SV
sva])
map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> SList a -> SList b
map :: forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV a -> SBV b
op SList a
l
| Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just [b]
concResult <- [a] -> Maybe [b]
concreteMap [a]
l'
= [b] -> SBV [b]
forall a. SymVal a => a -> SBV a
literal [b]
concResult
| 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 concreteMap :: [a] -> Maybe [b]
concreteMap [a]
l' = case (a -> Maybe b) -> [a] -> [Maybe b]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV b -> Maybe b) -> (a -> SBV b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBV b
op (SBV a -> SBV b) -> (a -> SBV a) -> a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal) [a]
l' of
[Maybe b]
xs | (Maybe b -> Bool) -> [Maybe b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe b -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe b]
xs -> Maybe [b]
forall a. Maybe a
Nothing
| Bool
True -> [b] -> Maybe [b]
forall a. a -> Maybe a
Just ([Maybe b] -> [b]
forall a. [Maybe a] -> [a]
catMaybes [Maybe b]
xs)
k :: Kind
k = Proxy (SBV [b]) -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(SList b))
r :: State -> IO SV
r State
st = do SV
sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
String
lam <- State -> Kind -> (SBV a -> SBV b) -> IO String
forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr State
st (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)) SBV a -> SBV b
op
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (String -> SeqOp
SeqMap String
lam)) [Item [SV]
SV
sva])
mapi :: forall a b. (SymVal a, SymVal b) => (SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b
mapi :: forall a b.
(SymVal a, SymVal b) =>
(SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b
mapi SInteger -> SBV a -> SBV b
op SInteger
i SList a
l
| Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just Integer
i' <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
i, Just [b]
concResult <- Integer -> [a] -> Maybe [b]
concMapi Integer
i' [a]
l'
= [b] -> SBV [b]
forall a. SymVal a => a -> SBV a
literal [b]
concResult
| 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 concMapi :: Integer -> [a] -> Maybe [b]
concMapi Integer
b [a]
xs = case (Integer -> a -> Maybe b) -> [Integer] -> [a] -> [Maybe b]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
P.zipWith (\Integer
o a
e -> SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (SInteger -> SBV a -> SBV b
op (Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
o) (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e))) [Integer
Item [Integer]
b ..] [a]
xs of
[Maybe b]
vs | (Maybe b -> Bool) -> [Maybe b] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe b -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe b]
vs -> Maybe [b]
forall a. Maybe a
Nothing
| Bool
True -> [b] -> Maybe [b]
forall a. a -> Maybe a
Just ([Maybe b] -> [b]
forall a. [Maybe a] -> [a]
catMaybes [Maybe b]
vs)
k :: Kind
k = Proxy (SBV [b]) -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(SList b))
r :: State -> IO SV
r State
st = do SV
svi <- State -> SInteger -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SInteger
i
SV
svl <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
String
lam <- State -> Kind -> (SInteger -> SBV a -> SBV b) -> IO String
forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr State
st (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)) SInteger -> SBV a -> SBV b
op
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (String -> SeqOp
SeqMapI String
lam)) [Item [SV]
SV
svi, Item [SV]
SV
svl])
foldl :: (SymVal a, SymVal b) => (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl :: forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SBV b -> SBV a -> SBV b
op SBV b
base SList a
l
| Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just b
base' <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
base, Just b
concResult <- b -> [a] -> Maybe b
concreteFoldl b
base' [a]
l'
= b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
| 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 concreteFoldl :: b -> [a] -> Maybe b
concreteFoldl b
b [] = b -> Maybe b
forall a. a -> Maybe a
Just b
b
concreteFoldl b
b (a
e:[a]
es) = case SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV b -> SBV a -> SBV b
op (b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b) (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e)) of
Maybe b
Nothing -> Maybe b
forall a. Maybe a
Nothing
Just b
b' -> b -> [a] -> Maybe b
concreteFoldl b
b' [a]
es
k :: Kind
k = SBV b -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV b
base
r :: State -> IO SV
r State
st = do SV
svb <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
base
SV
svl <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
String
lam <- State -> Kind -> (SBV b -> SBV a -> SBV b) -> IO String
forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr State
st Kind
k SBV b -> SBV a -> SBV b
op
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (String -> SeqOp
SeqFoldLeft String
lam)) [Item [SV]
SV
svb, Item [SV]
SV
svl])
foldli :: (SymVal a, SymVal b) => (SInteger -> SBV b -> SBV a -> SBV b) -> SInteger -> SBV b -> SList a -> SBV b
foldli :: forall a b.
(SymVal a, SymVal b) =>
(SInteger -> SBV b -> SBV a -> SBV b)
-> SInteger -> SBV b -> SList a -> SBV b
foldli SInteger -> SBV b -> SBV a -> SBV b
op SInteger
baseI SBV b
baseE SList a
l
| Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just Integer
baseI' <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
baseI, Just b
baseE' <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
baseE, Just b
concResult <- Integer -> b -> [a] -> Maybe b
concreteFoldli Integer
baseI' b
baseE' [a]
l'
= b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
concResult
| 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 concreteFoldli :: Integer -> b -> [a] -> Maybe b
concreteFoldli Integer
_ b
b [] = b -> Maybe b
forall a. a -> Maybe a
Just b
b
concreteFoldli Integer
c b
b (a
e:[a]
es) = case SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (SInteger -> SBV b -> SBV a -> SBV b
op (Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
c) (b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b) (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e)) of
Maybe b
Nothing -> Maybe b
forall a. Maybe a
Nothing
Just b
b' -> Integer -> b -> [a] -> Maybe b
concreteFoldli (Integer
cInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) b
b' [a]
es
k :: Kind
k = SBV b -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV b
baseE
r :: State -> IO SV
r State
st = do SV
svi <- State -> SInteger -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SInteger
baseI
SV
sve <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
baseE
SV
sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
String
lam <- State -> Kind -> (SInteger -> SBV b -> SBV a -> SBV b) -> IO String
forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr State
st Kind
k SInteger -> SBV b -> SBV a -> SBV b
op
State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (SeqOp -> Op
SeqOp (String -> SeqOp
SeqFoldLeftI String
lam)) [Item [SV]
SV
svi, Item [SV]
SV
sve, Item [SV]
SV
sva])
foldr :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr :: forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
foldr SBV a -> SBV b -> SBV b
op SBV b
b = (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl ((SBV a -> SBV b -> SBV b) -> SBV b -> SBV a -> SBV b
forall a b c. (a -> b -> c) -> b -> a -> c
flip SBV a -> SBV b -> SBV b
op) SBV b
b (SList a -> SBV b) -> (SList a -> SList a) -> SList a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse
foldri :: (SymVal a, SymVal b) => (SBV a -> SBV b -> SInteger -> SBV b) -> SBV b -> SInteger -> SList a -> SBV b
foldri :: forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b -> SInteger -> SBV b)
-> SBV b -> SInteger -> SList a -> SBV b
foldri SBV a -> SBV b -> SInteger -> SBV b
op SBV b
baseE SInteger
baseI = (SInteger -> SBV b -> SBV a -> SBV b)
-> SInteger -> SBV b -> SList a -> SBV b
forall a b.
(SymVal a, SymVal b) =>
(SInteger -> SBV b -> SBV a -> SBV b)
-> SInteger -> SBV b -> SList a -> SBV b
foldli (\SInteger
a SBV b
b SBV a
i -> SBV a -> SBV b -> SInteger -> SBV b
op SBV a
i SBV b
b SInteger
a) SInteger
baseI SBV b
baseE (SList a -> SBV b) -> (SList a -> SList a) -> SList a -> SBV b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SList a -> SList a
forall a. SymVal a => SList a -> SList a
reverse
zip :: (SymVal a, SymVal b) => SList a -> SList b -> SList (a, b)
zip :: forall a b.
(SymVal a, SymVal b) =>
SList a -> SList b -> SList (a, b)
zip SList a
xs SList b
ys = (SBV (Integer, a) -> SBV (a, b))
-> SList (Integer, a) -> SList (a, b)
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map (\SBV (Integer, a)
t -> (SBV a, SBV b) -> SBV (a, b)
forall tup a. Tuple tup a => a -> SBV tup
tuple (SBV (Integer, a)
tSBV (Integer, a) -> (SBV (Integer, a) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (Integer, a) -> SBV a
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SList b
ys SList b -> SInteger -> SBV b
forall a. SymVal a => SList a -> SInteger -> SBV a
`elemAt` (SBV (Integer, a)
tSBV (Integer, a) -> (SBV (Integer, a) -> SInteger) -> SInteger
forall a b. a -> (a -> b) -> b
^.SBV (Integer, a) -> SInteger
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)))
((SInteger -> SBV a -> SBV (Integer, a))
-> SInteger -> SList a -> SList (Integer, a)
forall a b.
(SymVal a, SymVal b) =>
(SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b
mapi (((SInteger, SBV a) -> SBV (Integer, a))
-> SInteger -> SBV a -> SBV (Integer, a)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (SInteger, SBV a) -> SBV (Integer, a)
forall tup a. Tuple tup a => a -> SBV tup
tuple) SInteger
0 (SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList b -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList b
ys) SList a
xs))
zipWith :: (SymVal a, SymVal b, SymVal c) => (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
zipWith :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
(SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
zipWith SBV a -> SBV b -> SBV c
f SList a
xs SList b
ys = (SBV (Integer, a) -> SBV c) -> SList (Integer, a) -> SList c
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map (\SBV (Integer, a)
t -> SBV a -> SBV b -> SBV c
f (SBV (Integer, a)
tSBV (Integer, a) -> (SBV (Integer, a) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (Integer, a) -> SBV a
forall b a. HasField "_2" b a => SBV a -> SBV b
_2) (SList b
ys SList b -> SInteger -> SBV b
forall a. SymVal a => SList a -> SInteger -> SBV a
`elemAt` (SBV (Integer, a)
tSBV (Integer, a) -> (SBV (Integer, a) -> SInteger) -> SInteger
forall a b. a -> (a -> b) -> b
^.SBV (Integer, a) -> SInteger
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)))
((SInteger -> SBV a -> SBV (Integer, a))
-> SInteger -> SList a -> SList (Integer, a)
forall a b.
(SymVal a, SymVal b) =>
(SInteger -> SBV a -> SBV b) -> SInteger -> SList a -> SList b
mapi (((SInteger, SBV a) -> SBV (Integer, a))
-> SInteger -> SBV a -> SBV (Integer, a)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (SInteger, SBV a) -> SBV (Integer, a)
forall tup a. Tuple tup a => a -> SBV tup
tuple) SInteger
0 (SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
take (SList b -> SInteger
forall a. SymVal a => SList a -> SInteger
length SList b
ys) SList a
xs))
concat :: SymVal a => SList [a] -> SList a
concat :: forall a. SymVal a => SList [a] -> SList a
concat = (SBV [a] -> SBV [a] -> SBV [a]) -> SBV [a] -> SList [a] -> SBV [a]
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl SBV [a] -> SBV [a] -> SBV [a]
forall a. SymVal a => SList a -> SList a -> SList a
(++) []
all :: SymVal a => (SBV a -> SBool) -> SList a -> SBool
all :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBV a -> SBool
f = (SBool -> SBV a -> SBool) -> SBool -> SList a -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl (\SBool
sofar SBV a
e -> SBool
sofar SBool -> SBool -> SBool
.&& SBV a -> SBool
f SBV a
e) SBool
sTrue
any :: SymVal a => (SBV a -> SBool) -> SList a -> SBool
any :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBV a -> SBool
f = (SBool -> SBV a -> SBool) -> SBool -> SList a -> SBool
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl (\SBool
sofar SBV a
e -> SBool
sofar SBool -> SBool -> SBool
.|| SBV a -> SBool
f SBV a
e) SBool
sFalse
filter :: SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SList a
filter SBV a -> SBool
f = (SList a -> SBV a -> SList a) -> SList a -> SList a -> SList a
forall a b.
(SymVal a, SymVal b) =>
(SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
foldl (\SList a
sofar SBV a
e -> SList a
sofar SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SBool -> SList a -> SList a -> SList a
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
e) (SBV a -> SList a
forall a. SymVal a => SBV a -> SList a
singleton SBV a
e) []) []
lift1 :: forall a b. (SymVal a, SymVal b) => SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 :: forall a b.
(SymVal a, SymVal b) =>
SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 SeqOp
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 (forall t. Proxy t
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 (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva])
lift2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 SeqOp
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 (forall t. Proxy t
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 (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva, Item [SV]
SV
svb])
lift3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => SeqOp -> 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) =>
SeqOp
-> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
lift3 SeqOp
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 (forall t. Proxy t
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 (SeqOp -> Op
SeqOp SeqOp
w) [Item [SV]
SV
sva, Item [SV]
SV
svb, Item [SV]
SV
svc])
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 = 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 a b. 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 :: 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 = 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 a b. 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 Maybe (b -> c) -> Maybe b -> Maybe c
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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 :: 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 = 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 a b. 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 Maybe (b -> c -> d) -> Maybe b -> Maybe (c -> d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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 a b. Maybe (a -> b) -> Maybe a -> Maybe b
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 :: SymVal a => SList a -> Bool
isConcretelyEmpty :: forall a. SymVal a => SList a -> Bool
isConcretelyEmpty SList a
sl | Just [a]
l <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sl = [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [a]
l
| Bool
True = Bool
False