-----------------------------------------------------------------------------
-- |
-- 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, subList, replace, indexOf, offsetIndexOf
        -- * Reverse
        , reverse
        -- * Mapping
        , map, mapi
        -- * Folding
        , foldl, foldr, foldli, foldri
        -- * Zipping
        , zip, zipWith
        -- * Filtering
        , filter
        -- * Other list functions
        , 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

-- $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 = 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` 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 = 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` 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,32] :: [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.
--
-- ->>> prove $ \(l :: SList Integer) i e -> i `inRange` (0, length l - 1) .&& l `elemAt` i .== e .=> indexOf l (singleton e) .<= i
-- 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
  = 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

-- | 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                = 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` 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
  = 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 -- 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
  = 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` 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
  = 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` 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

-- | @`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
  = 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` 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 :: (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
  | 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   -- 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

-- | @`indexOf` l sub@. Retrieves first position of @sub@ in @l@, @-1@ if there are no occurrences.
-- Equivalent to @`offsetIndexOf` l sub 0@.
--
-- ->>> prove $ \(l :: SList Int8) i -> i .> 0 .&& i .< length l .=> indexOf l (subList l i 1) .<= i
-- Q.E.D.
--
-- >>> 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 :: (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        -- 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
  = 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` 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 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` op 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
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` op s@ maps the operation on to sequence, with the counter given at each element, starting
-- at the given value. In Haskell terms, it is:
--
-- @
--    mapi :: (Integer -> a -> b) -> Integer -> [a] -> [b]
--    mapi f i xs = zipWith f [i..] xs
-- @
--
-- Note that `mapi` is definable in terms of `Data.SBV.List.zipWith`, with extra coding. The reason why SBV provides
-- this function natively is because it maps to a native function in the underlying solver. So, hopefully it'll perform
-- better in terms being decidable.
--
-- >>> mapi (+) 10 [1 .. 5 :: Integer]
-- [11,13,15,17,19] :: [SInteger]
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` op 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 :: (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` op i base s@ folds the sequence, with the counter given at each element, starting
-- at the given value. In Haskell terms, it is:
--
-- @
--   foldli :: (Integer -> b -> a -> b) -> Integer -> b -> [a] -> b
--   foldli f c e xs = foldl (\b (i, a) -> f i b a) e (zip [c..] xs)
-- @
--
-- While this function is rather odd looking, it maps directly to the implementation in the underlying solver,
-- and proofs involving it might have better decidability.
--
-- >>> foldli (\i b a -> i+b+a) 10 0 [1 .. 5 :: Integer]
-- 75 :: SInteger
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` op 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 :: (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` op base i s@ folds the sequence from the right, with the counter given at each element, starting
-- at the given value. This function is provided as a parallel to `foldli`.
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` 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 :: (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` 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 :: (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))

-- | Concatenate list of lists.
--
-- NB. Concat is typically defined in terms of foldr. Here we prefer foldl, since the underlying solver
-- primitive is foldl: Otherwise, we'd induce an extra call to reverse.
--
-- >>> concat [[1..3::Integer], [4..7], [8..10]]
-- [1,2,3,4,5,6,7,8,9,10] :: [SInteger]
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
(++) []

-- | 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 :: 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

-- | 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 :: 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 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 :: 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) []) []

-- | Lift a unary operator over lists.
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])

-- | Lift a binary operator over lists.
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])

-- | Lift a ternary operator over lists.
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])

-- | Concrete evaluation for unary ops
concEval1 :: (SymVal a, SymVal b) => Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 :: forall a b.
(SymVal a, SymVal b) =>
Maybe (a -> b) -> SBV a -> Maybe (SBV b)
concEval1 Maybe (a -> b)
mbOp SBV a
a = 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)

-- | Concrete evaluation for binary ops
concEval2 :: (SymVal a, SymVal b, SymVal c) => Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
concEval2 Maybe (a -> b -> c)
mbOp SBV a
a SBV b
b = 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)

-- | Concrete evaluation for ternary ops
concEval3 :: (SymVal a, SymVal b, SymVal c, SymVal d) => Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
concEval3 :: forall a b c d.
(SymVal a, SymVal b, SymVal c, SymVal d) =>
Maybe (a -> b -> c -> d)
-> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
concEval3 Maybe (a -> b -> c -> d)
mbOp SBV a
a SBV b
b SBV c
c = 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)

-- | 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