    -----------------------------------------------------------------------------
    -- |
    -- 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,16] :: [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