-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.List
-- Copyright : (c) Joel Burget
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- A collection of list utilities, useful when working with symbolic lists.
-- 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 @OverloadedLists@ extension to allow literal lists to
-- be used as symbolic-lists.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.List (
        -- * Length, emptiness
          length, null
        -- * Deconstructing/Reconstructing
        , head, tail, uncons, init, singleton, listToListAt, elemAt, (!!), implode, concat, (.:), snoc, nil, (++)
        -- * Containment
        , elem, notElem, isInfixOf, isSuffixOf, isPrefixOf
        -- * Sublists
        , take, drop, splitAt, subList, replace, indexOf, offsetIndexOf
        -- * Reverse
        , reverse
        -- * Mapping
        , map, concatMap
        -- * Folding
        , foldl, foldr
        -- * Zipping
        , zip, zipWith
        -- * Filtering
        , filter, partition
        -- * Other list functions
        , all, any, and, or
        ) where

import Prelude hiding (head, tail, init, length, take, drop, splitAt, concat, null, elem,
                       notElem, reverse, (++), (!!), map, concatMap, foldl, foldr, zip, zipWith, filter,
                       all, any, and, or)
import qualified Prelude as P

import Data.SBV.Core.Kind
import Data.SBV.Core.Data hiding (StrOp(..))
import Data.SBV.Core.Model
import Data.SBV.Core.Symbolic (registerSpecialFunction)

import Data.SBV.Lambda

import Data.SBV.Tuple hiding (fst, snd)

import Data.Maybe (isNothing, catMaybes)

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

import Data.Proxy

-- $setup
-- >>> -- For doctest purposes only:
-- >>> 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(map)
-- >>> import Data.SBV
-- >>> :set -XDataKinds
-- >>> :set -XOverloadedLists
-- >>> :set -XScopedTypeVariables

-- | Length of a list.
--
-- >>> sat $ \(l :: SList Word16) -> length l .== 2
-- Satisfiable. Model:
--   s0 = [0,0] :: [Word16]
-- >>> sat $ \(l :: SList Word16) -> length l .< 0
-- Unsatisfiable
-- >>> prove $ \(l1 :: SList Word16) (l2 :: SList Word16) -> length l1 + length l2 .== length (l1 ++ l2)
-- Q.E.D.
length :: SymVal a => SList a -> SInteger
length :: forall a. SymVal a => SList a -> SInteger
length = Bool -> SeqOp -> Maybe ([a] -> Integer) -> SBV [a] -> SInteger
forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
False 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` s@ is True iff the list is empty
--
-- >>> prove $ \(l :: SList Word16) -> null l .<=> length l .== 0
-- Q.E.D.
-- >>> prove $ \(l :: SList Word16) -> null l .<=> l .== []
-- Q.E.D.
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`@ returns the first element of a list. Unspecified if the list is empty.
--
-- >>> prove $ \c -> head (singleton c) .== (c :: SInteger)
-- Q.E.D.
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`@ returns the tail of a list. Unspecified if the list is empty.
--
-- >>> prove $ \(h :: SInteger) t -> tail (singleton h ++ t) .== t
-- Q.E.D.
-- >>> prove $ \(l :: SList Integer) -> length l .> 0 .=> length (tail l) .== length l - 1
-- Q.E.D.
-- >>> prove $ \(l :: SList Integer) -> sNot (null l) .=> singleton (head l) ++ tail l .== l
-- Q.E.D.
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`@ returns the pair of the head and tail. Unspecified if the list is empty.
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`@ returns all but the last element of the list. Unspecified if the list is empty.
--
-- >>> prove $ \(h :: SInteger) t -> init (t ++ singleton h) .== t
-- Q.E.D.
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` x@ is the list of length 1 that contains the only value @x@.
--
-- >>> prove $ \(x :: SInteger) -> head (singleton x) .== x
-- Q.E.D.
-- >>> prove $ \(x :: SInteger) -> length (singleton x) .== 1
-- Q.E.D.
singleton :: SymVal a => SBV a -> SList a
singleton :: forall a. SymVal a => SBV a -> SList a
singleton = Bool -> SeqOp -> Maybe (a -> [a]) -> SBV a -> SBV [a]
forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
False SeqOp
SeqUnit ((a -> [a]) -> Maybe (a -> [a])
forall a. a -> Maybe a
Just (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []))

-- | @`listToListAt` l offset@. List of length 1 at @offset@ in @l@. Unspecified if
-- index is out of bounds.
--
-- >>> prove $ \(l1 :: SList Integer) l2 -> listToListAt (l1 ++ l2) (length l1) .== listToListAt l2 0
-- Q.E.D.
-- >>> sat $ \(l :: SList Word16) -> length l .>= 2 .&& listToListAt l 0 ./= listToListAt l (length l - 1)
-- Satisfiable. Model:
--   s0 = [0,64] :: [Word16]
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` l i@ is the value stored at location @i@, starting at 0. Unspecified if
-- index is out of bounds.
--
-- >>> prove $ \i -> i `inRange` (0, 4) .=> [1,1,1,1,1] `elemAt` i .== (1::SInteger)
-- Q.E.D.
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
  = Bool
-> SeqOp
-> Maybe ([a] -> Integer -> a)
-> SList a
-> SInteger
-> SBV a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
False SeqOp
SeqNth Maybe ([a] -> Integer -> a)
forall a. Maybe a
Nothing SList a
l SInteger
i

-- | Short cut for 'elemAt'
(!!) :: 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` es@ is the list of length @|es|@ containing precisely those
-- elements. Note that there is no corresponding function @explode@, since
-- we wouldn't know the length of a symbolic list.
--
-- >>> prove $ \(e1 :: SInteger) e2 e3 -> length (implode [e1, e2, e3]) .== 3
-- Q.E.D.
-- >>> prove $ \(e1 :: SInteger) e2 e3 -> P.map (elemAt (implode [e1, e2, e3])) (P.map literal [0 .. 2]) .== [e1, e2, e3]
-- Q.E.D.
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 [])

-- | Prepend an element, the traditional @cons@.
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

-- | Append an element
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

-- | Empty list. This value has the property that it's the only list with length 0:
--
-- >>> prove $ \(l :: SList Integer) -> length l .== 0 .<=> l .== nil
-- Q.E.D.
nil :: SymVal a => SList a
nil :: forall a. SymVal a => SList a
nil = []

-- | Append two lists.
--
-- >>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x ++ y ++ z .== [1 .. 12]
-- Satisfiable. Model:
--   s0 =      [1,2,3,4,5] :: [Integer]
--   s1 =              [6] :: [Integer]
--   s2 = [7,8,9,10,11,12] :: [Integer]
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                = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> [a])
-> SList a
-> SList a
-> SList a
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
False 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` e l@. Does @l@ contain the element @e@?
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` e l@. Does @l@ not contain the element @e@?
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` sub l@. Does @l@ contain the subsequence @sub@?
--
-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> l2 `isInfixOf` (l1 ++ l2 ++ l3)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isInfixOf` l2 .&& l2 `isInfixOf` l1 .<=> l1 .== l2
-- Q.E.D.
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
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True 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 -- NB. flip, since `SeqContains` takes args in rev order!

-- | @`isPrefixOf` pre l@. Is @pre@ a prefix of @l@?
--
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` (l1 ++ l2)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 -> l1 `isPrefixOf` l2 .=> subList l2 0 (length l1) .== l1
-- Q.E.D.
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
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True 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` suf l@. Is @suf@ a suffix of @l@?
--
-- >>> prove $ \(l1 :: SList Word16) l2 -> l2 `isSuffixOf` (l1 ++ l2)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Word16) l2 -> l1 `isSuffixOf` l2 .=> subList l2 (length l2 - length l1) (length l1) .== l1
-- Q.E.D.
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
  = Bool
-> SeqOp
-> Maybe ([a] -> [a] -> Bool)
-> SList a
-> SList a
-> SBool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
True 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` len l@. Corresponds to Haskell's `take` on symbolic lists.
--
-- >>> prove $ \(l :: SList Integer) i -> i .>= 0 .=> length (take i l) .<= i
-- Q.E.D.
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` len s@. Corresponds to Haskell's `drop` on symbolic-lists.
--
-- >>> prove $ \(l :: SList Word16) i -> length (drop i l) .<= length l
-- Q.E.D.
-- >>> prove $ \(l :: SList Word16) i -> take i l ++ drop i l .== l
-- Q.E.D.
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

-- | @splitAt n xs = (take n xs, drop n xs)@
splitAt :: SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt :: forall a. SymVal a => SInteger -> SList a -> (SList a, SList a)
splitAt SInteger
n SList a
xs = (SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
take SInteger
n SList a
xs, SInteger -> SList a -> SList a
forall a. SymVal a => SInteger -> SList a -> SList a
drop SInteger
n SList a
xs)

-- | @`subList` s offset len@ is the sublist 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 $ \(l :: SList Integer) i -> i .>= 0 .&& i .< length l .=> subList l 0 i ++ subList l i (length l - i) .== l
-- Q.E.D.
-- >>> sat  $ \i j -> subList [1..5] i j .== ([2..4] :: SList Integer)
-- Satisfiable. Model:
--   s0 = 1 :: Integer
--   s1 = 3 :: Integer
-- >>> sat  $ \i j -> subList [1..5] i j .== ([6..7] :: SList Integer)
-- Unsatisfiable
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                   -- a constant list
  , Just Integer
o  <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset              -- a constant offset
  , Just Integer
sz <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
len                 -- a constant length
  , let lc :: Integer
lc = [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c                 -- length of the list
  , let valid :: Integer -> Bool
valid Integer
x = Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
lc          -- predicate that checks valid point
  , Integer -> Bool
valid Integer
o                                  -- offset is valid
  , Integer
sz Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0                                  -- length is not-negative
  , Integer -> Bool
valid (Integer -> Bool) -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Integer
o Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
sz                           -- we don't overrun
  = [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                                     -- either symbolic, or something is out-of-bounds
  = Bool
-> 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) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
False SeqOp
SeqSubseq Maybe ([a] -> Integer -> Integer -> [a])
forall a. Maybe a
Nothing SList a
l SInteger
offset SInteger
len

-- | @`replace` l src dst@. Replace the first occurrence of @src@ by @dst@ in @s@
--
-- >>> prove $ \l -> replace [1..5] l [6..10] .== [6..10] .=> l .== ([1..5] :: SList Word8)
-- Q.E.D.
-- >>> prove $ \(l1 :: SList Integer) l2 l3 -> length l2 .> length l1 .=> replace l1 l2 l3 .== l1
-- Q.E.D.
replace :: forall a. (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   -- If src is null, simply prepend
  = SList a
dst SList a -> SList a -> SList a
forall a. SymVal a => SList a -> SList a -> SList a
++ SList a
l
  | Kind -> Bool
eqCheckIsObjectEq Kind
ka
  , 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
  = Bool
-> 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) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
True 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   -- note that needle is guaranteed non-empty here.
           where go :: [a] -> [a]
go []       = []
                 go i :: [a]
i@(a
c:[a]
cs)
                  | [a]
needle [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`L.isPrefixOf` [a]
i = [a]
newNeedle [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
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

        ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

-- | @`indexOf` l sub@. Retrieves first position of @sub@ in @l@, @-1@ if there are no occurrences.
-- Equivalent to @`offsetIndexOf` l sub 0@.
--
-- >>> prove $ \(l1 :: SList Word16) l2 -> length l2 .> length l1 .=> indexOf l1 l2 .== -1
-- Q.E.D.
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` l sub offset@. Retrieves first position of @sub@ at or
-- after @offset@ in @l@, @-1@ if there are no occurrences.
--
-- >>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub
-- Q.E.D.
-- >>> prove $ \(l :: SList Int8) sub i -> i .>= length l .&& length sub .> 0 .=> offsetIndexOf l sub i .== -1
-- Q.E.D.
-- >>> prove $ \(l :: SList Int8) sub i -> i .> length l .=> offsetIndexOf l sub i .== -1
-- Q.E.D.
offsetIndexOf :: forall a. (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
  | Kind -> Bool
eqCheckIsObjectEq Kind
ka
  , Just [a]
c <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
s        -- a constant list
  , Just [a]
n <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
sub      -- a constant search pattern
  , Just Integer
o <- SInteger -> Maybe Integer
forall a. SymVal a => SBV a -> Maybe a
unliteral SInteger
offset   -- at a constant offset
  , Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0, Integer
o Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= [a] -> Integer
forall i a. Num i => [a] -> i
genericLength [a]
c        -- offset is good
  = 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
  = Bool
-> 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) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
True SeqOp
SeqIndexOf Maybe ([a] -> [a] -> Integer -> Integer)
forall a. Maybe a
Nothing SList a
s SList a
sub SInteger
offset
  where ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)

-- | @`reverse` s@ reverses the sequence.
--
-- NB. We can define @reverse@ in terms of @foldl@ as: @foldl (\soFar elt -> singleton elt ++ soFar) []@
-- But in my experiments, I found that this definition performs worse instead of the recursive definition
-- SBV generates for reverse calls. So we're keeping it intact.
--
-- >>> sat $ \(l :: SList Integer) -> reverse l .== literal [3, 2, 1]
-- Satisfiable. Model:
--   s0 = [1,2,3] :: [Integer]
-- >>> prove $ \(l :: SList Word32) -> reverse l .== [] .<=> null l
-- Q.E.D.
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 sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                  let op = SeqOp -> Op
SeqOp (Kind -> SeqOp
SBVReverse Kind
k)
                  registerSpecialFunction st op
                  newExpr st k (SBVApp op [sva])

-- | @`map` f s@ maps the operation on to sequence.
--
-- >>> map (+1) [1 .. 5 :: Integer]
-- [2,3,4,5,6] :: [SInteger]
-- >>> map (+1) [1 .. 5 :: WordN 8]
-- [2,3,4,5,6] :: [SWord8]
-- >>> map singleton [1 .. 3 :: Integer]
-- [[1],[2],[3]] :: [[SInteger]]
-- >>> import Data.SBV.Tuple
-- >>> import GHC.Exts (fromList)
-- >>> map (\t -> t^._1 + t^._2) (fromList [(x, y) | x <- [1..3], y <- [4..6]] :: SList (Integer, Integer))
-- [5,6,7,6,7,8,7,8,9] :: [SInteger]
--
-- Of course, SBV's 'map' can also be reused in reverse:
--
-- >>> sat $ \l -> map (+1) l .== [1,2,3 :: Integer]
-- Satisfiable. Model:
--   s0 = [0,1,2] :: [Integer]
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
f 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
klb (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
f (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)

        ka :: Kind
ka  = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
        kb :: Kind
kb  = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
        klb :: Kind
klb = 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 sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                  lam <- lambdaStr st HigherOrderArg kb f
                  let op = SeqOp -> Op
SeqOp (Kind -> Kind -> SMTLambda -> SeqOp
SBVMap Kind
ka Kind
kb SMTLambda
lam)
                  registerSpecialFunction st op
                  newExpr st klb (SBVApp op [sva])

-- | @concatMap f xs@ maps f over elements and concats the result.
concatMap :: (SymVal a, SymVal b) => (SBV a -> SList b) -> SList a -> SList b
concatMap :: forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SList b) -> SList a -> SList b
concatMap SBV a -> SList b
f SList a
xs = SList [b] -> SList b
forall a. SymVal a => SList [a] -> SList a
concat ((SBV a -> SList b) -> SList a -> SList [b]
forall a b.
(SymVal a, SymVal b) =>
(SBV a -> SBV b) -> SList a -> SList b
map SBV a -> SList b
f SList a
xs)

-- | @`foldl` f base s@ folds the from the left.
--
-- >>> foldl (+) 0 [1 .. 5 :: Integer]
-- 15 :: SInteger
-- >>> foldl (*) 1 [1 .. 5 :: Integer]
-- 120 :: SInteger
-- >>> foldl (\soFar elt -> singleton elt ++ soFar) ([] :: SList Integer) [1 .. 5 :: Integer]
-- [5,4,3,2,1] :: [SInteger]
--
-- Again, we can use 'Data.SBV.List.foldl' in the reverse too:
--
-- >>> sat $ \l -> foldl (\soFar elt -> singleton elt ++ soFar) ([] :: SList Integer) l .== [5, 4, 3, 2, 1 :: Integer]
-- Satisfiable. Model:
--   s0 = [1,2,3,4,5] :: [Integer]
foldl :: forall a b. (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
f 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
kb (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 (b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b SBV b -> SBV a -> SBV b
`f` 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

        ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
        kb :: Kind
kb = 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 svb <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
base
                  svl <- sbvToSV st l
                  lam <- lambdaStr st HigherOrderArg kb f
                  let op = SeqOp -> Op
SeqOp (Kind -> Kind -> SMTLambda -> SeqOp
SBVFoldl Kind
ka Kind
kb SMTLambda
lam)
                  registerSpecialFunction st op
                  newExpr st kb (SBVApp op [svb, svl])

-- | @`foldr` f base s@ folds the sequence from the right.
--
-- >>> foldr (+) 0 [1 .. 5 :: Integer]
-- 15 :: SInteger
-- >>> foldr (*) 1 [1 .. 5 :: Integer]
-- 120 :: SInteger
-- >>> foldr (\elt soFar -> soFar ++ singleton elt) ([] :: SList Integer) [1 .. 5 :: Integer]
-- [5,4,3,2,1] :: [SInteger]
foldr :: forall a b. (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
f 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
concreteFoldr 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
kb (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 concreteFoldr :: b -> [a] -> Maybe b
concreteFoldr b
b []     = b -> Maybe b
forall a. a -> Maybe a
Just b
b
        concreteFoldr b
b (a
e:[a]
es) = case b -> [a] -> Maybe b
concreteFoldr b
b [a]
es of
                                   Maybe b
Nothing  -> Maybe b
forall a. Maybe a
Nothing
                                   Just b
res -> SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
e SBV a -> SBV b -> SBV b
`f` b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
res)

        ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
        kb :: Kind
kb = 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 svb <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
base
                  svl <- sbvToSV st l
                  lam <- lambdaStr st HigherOrderArg kb f
                  let op = SeqOp -> Op
SeqOp (Kind -> Kind -> SMTLambda -> SeqOp
SBVFoldr Kind
ka Kind
kb SMTLambda
lam)
                  registerSpecialFunction st op
                  newExpr st kb (SBVApp op [svb, svl])

-- | @`zip` xs ys@ zips the lists to give a list of pairs. The length of the final list is
-- the minumum of the lengths of the given lists.
--
-- >>> zip [1..10::Integer] [11..20::Integer]
-- [(1,11),(2,12),(3,13),(4,14),(5,15),(6,16),(7,17),(8,18),(9,19),(10,20)] :: [(SInteger, SInteger)]
-- >>> import Data.SBV.Tuple
-- >>> foldr (+) 0 (map (\t -> t^._1+t^._2::SInteger) (zip [1..10::Integer] [10, 9..1::Integer]))
-- 110 :: SInteger
zip :: forall a b. (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
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs, Just [b]
ys' <- SList b -> Maybe [b]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList b
ys
 = [(a, b)] -> SBV [(a, b)]
forall a. SymVal a => a -> SBV a
literal ([(a, b)] -> SBV [(a, b)]) -> [(a, b)] -> SBV [(a, b)]
forall a b. (a -> b) -> a -> b
$ [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip [a]
xs' [b]
ys'
 | Bool
True
 = SVal -> SBV [(a, b)]
forall a. SVal -> SBV a
SBV (SVal -> SBV [(a, b)]) -> SVal -> SBV [(a, b)]
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kr (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 ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
       kb :: Kind
kb = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
       kr :: Kind
kr = Kind -> Kind
KList (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ [Kind] -> Kind
KTuple [Item [Kind]
Kind
ka, Item [Kind]
Kind
kb]

       r :: State -> IO SV
r State
st = do svxs <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
xs
                 svys <- sbvToSV st ys
                 let op = SeqOp -> Op
SeqOp (Kind -> Kind -> SeqOp
SBVZip Kind
ka Kind
kb)
                 registerSpecialFunction st op
                 newExpr st kr (SBVApp op [svxs, svys])

-- | @`zipWith` f xs ys@ zips the lists to give a list of pairs, applying the function to each pair of elements.
-- The length of the final list is the minumum of the lengths of the given lists.
--
-- >>> zipWith (+) [1..10::Integer] [11..20::Integer]
-- [12,14,16,18,20,22,24,26,28,30] :: [SInteger]
-- >>> foldr (+) 0 (zipWith (+) [1..10::Integer] [10, 9..1::Integer])
-- 110 :: SInteger
zipWith :: forall a b c. (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
 | Just [a]
xs' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
xs, Just [b]
ys' <- SList b -> Maybe [b]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList b
ys, Just [c]
concResult <- [a] -> [b] -> Maybe [c]
concreteZipWith [a]
xs' [b]
ys'
 = [c] -> SBV [c]
forall a. SymVal a => a -> SBV a
literal [c]
concResult
 | 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
kr (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 concreteZipWith :: [a] -> [b] -> Maybe [c]
concreteZipWith []     [b]
_      = [c] -> Maybe [c]
forall a. a -> Maybe a
Just []
       concreteZipWith [a]
_      []     = [c] -> Maybe [c]
forall a. a -> Maybe a
Just []
       concreteZipWith (a
a:[a]
as) (b
b:[b]
bs) = (:) (c -> [c] -> [c]) -> Maybe c -> Maybe ([c] -> [c])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
a SBV a -> SBV b -> SBV c
`f` b -> SBV b
forall a. SymVal a => a -> SBV a
literal b
b) Maybe ([c] -> [c]) -> Maybe [c] -> 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
<*> [a] -> [b] -> Maybe [c]
concreteZipWith [a]
as [b]
bs

       ka :: Kind
ka = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
       kb :: Kind
kb = Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @b)
       kc :: Kind
kc = Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)
       kr :: Kind
kr = Kind -> Kind
KList Kind
kc

       r :: State -> IO SV
r State
st = do svxs <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
xs
                 svys <- sbvToSV st ys
                 lam <- lambdaStr st HigherOrderArg kc f
                 let op = SeqOp -> Op
SeqOp (Kind -> Kind -> Kind -> SMTLambda -> SeqOp
SBVZipWith Kind
ka Kind
kb Kind
kc SMTLambda
lam)
                 registerSpecialFunction st op
                 newExpr st kr (SBVApp op [svxs, svys])

-- | Concatenate list of lists.
--
-- >>> concat [[1..3::Integer], [4..7], [8..10]]
-- [1,2,3,4,5,6,7,8,9,10] :: [SInteger]
concat :: forall a. SymVal a => SList [a] -> SList a
concat :: forall a. SymVal a => SList [a] -> SList a
concat SList [a]
l
  | Just [[a]]
l' <- SList [a] -> Maybe [[a]]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList [a]
l
  = [a] -> SBV [a]
forall a. SymVal a => a -> SBV a
literal ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
P.concat [[a]]
l')
  | Bool
True
  = SVal -> SBV [a]
forall a. SVal -> SBV a
SBV (SVal -> SBV [a]) -> SVal -> SBV [a]
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kla (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 ka :: Kind
ka   = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
        kla :: Kind
kla  = Proxy [a] -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @[a])

        r :: State -> IO SV
r State
st = do sva <- State -> SList [a] -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList [a]
l
                  let op = SeqOp -> Op
SeqOp (Kind -> SeqOp
SBVConcat Kind
ka)
                  registerSpecialFunction st op
                  newExpr st kla (SBVApp op [sva])

-- | Check all elements satisfy the predicate.
--
-- >>> let isEven x = x `sMod` 2 .== 0
-- >>> all isEven [2, 4, 6, 8, 10 :: Integer]
-- True
-- >>> all isEven [2, 4, 6, 1, 8, 10 :: Integer]
-- False
all :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBV a -> SBool
f SList a
l
 | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
 = (SBV a -> SBool) -> [SBV a] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAll SBV a -> SBool
f ((a -> SBV a) -> [a] -> [SBV a]
forall a b. (a -> b) -> [a] -> [b]
P.map a -> SBV a
forall a. SymVal a => a -> SBV a
literal [a]
l')
 | Bool
True
 = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (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 r :: State -> IO SV
r State
st = do sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                 lam <- lambdaStr st HigherOrderArg KBool f
                 let op = SeqOp -> Op
SeqOp (Kind -> SMTLambda -> SeqOp
SBVAll (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) SMTLambda
lam)
                 registerSpecialFunction st op
                 newExpr st KBool (SBVApp op [sva])

-- | Check some element satisfies the predicate.
-- --
-- >>> let isEven x = x `sMod` 2 .== 0
-- >>> any (sNot . isEven) [2, 4, 6, 8, 10 :: Integer]
-- False
-- >>> any isEven [2, 4, 6, 1, 8, 10 :: Integer]
-- True
any :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBV a -> SBool
f SList a
l
 | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l
 = (SBV a -> SBool) -> [SBV a] -> SBool
forall a. (a -> SBool) -> [a] -> SBool
sAny SBV a -> SBool
f ((a -> SBV a) -> [a] -> [SBV a]
forall a b. (a -> b) -> [a] -> [b]
P.map a -> SBV a
forall a. SymVal a => a -> SBV a
literal [a]
l')
 | Bool
True
 = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (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 r :: State -> IO SV
r State
st = do sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                 lam <- lambdaStr st HigherOrderArg KBool f
                 let op = SeqOp -> Op
SeqOp (Kind -> SMTLambda -> SeqOp
SBVAny (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) SMTLambda
lam)
                 registerSpecialFunction st op
                 newExpr st KBool (SBVApp op [sva])

-- | Conjunction of all the elements.
and :: SList Bool -> SBool
and :: SList Bool -> SBool
and = (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
all SBool -> SBool
forall a. a -> a
id

-- | Disjunction of all the elements.
or :: SList Bool -> SBool
or :: SList Bool -> SBool
or = (SBool -> SBool) -> SList Bool -> SBool
forall a. SymVal a => (SBV a -> SBool) -> SList a -> SBool
any SBool -> SBool
forall a. a -> a
id

-- | @filter f xs@ filters the list with the given predicate.
--
-- >>> filter (\x -> x `sMod` 2 .== 0) [1 .. 10 :: Integer]
-- [2,4,6,8,10] :: [SInteger]
-- >>> filter (\x -> x `sMod` 2 ./= 0) [1 .. 10 :: Integer]
-- [1,3,5,7,9] :: [SInteger]
filter :: forall a. 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
l
  | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just [a]
concResult <- [a] -> Maybe [a]
concreteFilter [a]
l'
  = [a] -> SList a
forall a. SymVal a => a -> SBV a
literal [a]
concResult
  | 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 concreteFilter :: [a] -> Maybe [a]
concreteFilter [a]
l' = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
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 Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe [a]
forall a. Maybe a
Nothing
                                 | Bool
True               -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
e | (Bool
True, a
e) <- [Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
l']

        k :: Kind
k = Proxy (SList a) -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(SList a))
        r :: State -> IO SV
r State
st = do sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                  lam <- lambdaStr st HigherOrderArg KBool f
                  let op = SeqOp -> Op
SeqOp (Kind -> SMTLambda -> SeqOp
SBVFilter (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) SMTLambda
lam)
                  registerSpecialFunction st op
                  newExpr st k (SBVApp op [sva])

-- | @partition f xs@ splits the list into two and returns those that satisfy the predicate in the
-- first element, and those that don't in the second.
partition :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition :: forall a. SymVal a => (SBV a -> SBool) -> SList a -> STuple [a] [a]
partition SBV a -> SBool
f SList a
l
  | Just [a]
l' <- SList a -> Maybe [a]
forall a. SymVal a => SBV a -> Maybe a
unliteral SList a
l, Just SBV ([a], [a])
concResult <- [a] -> Maybe (SBV ([a], [a]))
concretePartition [a]
l'
  = SBV ([a], [a])
concResult
  | Bool
True
  = SVal -> SBV ([a], [a])
forall a. SVal -> SBV a
SBV (SVal -> SBV ([a], [a])) -> SVal -> SBV ([a], [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 concretePartition :: [a] -> Maybe (SBV ([a], [a]))
concretePartition [a]
l' = case (a -> Maybe Bool) -> [a] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
P.map (SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBool -> Maybe Bool) -> (a -> SBool) -> a -> Maybe Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> SBool
f (SBV a -> SBool) -> (a -> SBV a) -> a -> SBool
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 Bool]
xs | (Maybe Bool -> Bool) -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
P.any Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe Bool]
xs -> Maybe (SBV ([a], [a]))
forall a. Maybe a
Nothing
                                    | Bool
True               -> let ([(Bool, a)]
ts, [(Bool, a)]
fs) = ((Bool, a) -> Bool) -> [(Bool, a)] -> ([(Bool, a)], [(Bool, a)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (Bool, a) -> Bool
forall a b. (a, b) -> a
fst ([Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
P.zip ([Maybe Bool] -> [Bool]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Bool]
xs) [a]
l')
                                                            in SBV ([a], [a]) -> Maybe (SBV ([a], [a]))
forall a. a -> Maybe a
Just (SBV ([a], [a]) -> Maybe (SBV ([a], [a])))
-> SBV ([a], [a]) -> Maybe (SBV ([a], [a]))
forall a b. (a -> b) -> a -> b
$ (SList a, SList a) -> SBV ([a], [a])
forall tup a. Tuple tup a => a -> SBV tup
tuple ([a] -> SList a
forall a. SymVal a => a -> SBV a
literal (((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
snd [(Bool, a)]
ts), [a] -> SList a
forall a. SymVal a => a -> SBV a
literal (((Bool, a) -> a) -> [(Bool, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
P.map (Bool, a) -> a
forall a b. (a, b) -> b
snd [(Bool, a)]
fs))


        k :: Kind
k = Proxy (SBV ([a], [a])) -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(STuple [a] [a]))

        r :: State -> IO SV
r State
st = do sva <- State -> SList a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SList a
l
                  lam <- lambdaStr st HigherOrderArg KBool f
                  let op = SeqOp -> Op
SeqOp (Kind -> SMTLambda -> SeqOp
SBVPartition (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) SMTLambda
lam)
                  registerSpecialFunction st op
                  newExpr st k (SBVApp op [sva])

-- | Lift a unary operator over lists.
lift1 :: forall a b. (SymVal a, SymVal b) => Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 :: forall a b.
(SymVal a, SymVal b) =>
Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
lift1 Bool
simpleEq SeqOp
w Maybe (a -> b)
mbOp SBV a
a
  | Just SBV b
cv <- Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
forall a b.
(SymVal a, SymVal b) =>
Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Bool
simpleEq 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 sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  newExpr st k (SBVApp (SeqOp w) [sva])

-- | Lift a binary operator over lists.
lift2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
lift2 Bool
simpleEq SeqOp
w Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  | Just SBV c
cv <- Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 Bool
simpleEq 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 sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  svb <- sbvToSV st b
                  newExpr st k (SBVApp (SeqOp w) [sva, svb])

-- | Lift a ternary operator over lists.
lift3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => Bool -> 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) =>
Bool
-> SeqOp
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> SBV d
lift3 Bool
simpleEq SeqOp
w Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Just SBV d
cv <- Bool
-> 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) =>
Bool
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> Maybe (SBV d)
concEval3 Bool
simpleEq 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 sva <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
a
                  svb <- sbvToSV st b
                  svc <- sbvToSV st c
                  newExpr st k (SBVApp (SeqOp w) [sva, svb, svc])

-- | Concrete evaluation for unary ops
concEval1 :: forall a b. (SymVal a, SymVal b) => Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 :: forall a b.
(SymVal a, SymVal b) =>
Bool -> Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Bool
simpleEq Maybe (a -> b)
mbOp SBV a
a
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @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)
  | Bool
True                                                  = Maybe (SBV b)
forall a. Maybe a
Nothing

-- | Concrete evaluation for binary ops
concEval2 :: forall a b c. (SymVal a, SymVal b, SymVal c) => Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Bool -> Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 Bool
simpleEq Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) = 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)
  | Bool
True                                                  = Maybe (SBV c)
forall a. Maybe a
Nothing

-- | Concrete evaluation for ternary ops
concEval3 :: forall a b c d. (SymVal a, SymVal b, SymVal c, SymVal d) => Bool -> 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) =>
Bool
-> Maybe (a -> b -> c -> d)
-> SBV a
-> SBV b
-> SBV c
-> Maybe (SBV d)
concEval3 Bool
simpleEq Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c
  | Bool -> Bool
not Bool
simpleEq Bool -> Bool -> Bool
|| Kind -> Bool
eqCheckIsObjectEq (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) = 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)
  | Bool
True                                                  = Maybe (SBV d)
forall a. Maybe a
Nothing

-- | Is the list concretely known empty?
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