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

    import Prelude hiding (head, tail, init, length, take, drop, concat, null, elem, notElem)
    import qualified Prelude as P

    import Data.SBV.Core.Data hiding (StrOp(..))
    import Data.SBV.Core.Model

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

    import Data.Proxy

    -- For doctest use only
    --
    -- $setup
    -- >>> import Data.SBV.Provers.Prover (prove, sat)
    -- >>> import Data.Int
    -- >>> import Data.Word
    -- >>> :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 :: SList a -> SInteger
    length = SeqOp -> Maybe ([a] -> Integer) -> SList 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 (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 :: SList a -> SBool
    null l :: SList a
    l
      | Just cs :: [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 (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
    .== 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 :: SList a -> SBV a
    head = (SList a -> SInteger -> SBV a
    forall a. SymVal a => SList a -> SInteger -> SBV a
    `elemAt` 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 :: SList a -> SList a
    tail l :: SList a
    l
     | Just (_:cs :: [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 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
    - 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 :: SList a -> (SBV a, SList a)
    uncons l :: 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 :: SList a -> SList a
    init l :: SList a
    l
     | Just cs :: [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] -> SList a) -> [a] -> SList a
    forall a b. (a -> b) -> a -> b
    $ [a] -> [a]
    forall a. [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 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
    - 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 :: SBV a -> SList a
    singleton = SeqOp -> Maybe (a -> [a]) -> SBV a -> SList 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,0,8] :: [Word16]
    listToListAt :: SymVal a => SList a -> SInteger -> SList a
    listToListAt :: SList a -> SInteger -> SList a
    listToListAt s :: SList a
    s offset :: SInteger
    offset = SList a -> SInteger -> SInteger -> SList a
    forall a. SymVal a => SList a -> SInteger -> SInteger -> SList a
    subList SList a
    s SInteger
    offset 1

    -- | @`elemAt` l i@ is the value stored at location @i@. 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 :: forall a. SymVal a => SList a -> SInteger -> SBV a
    elemAt :: SList a -> SInteger -> SBV a
    elemAt l :: SList a
    l i :: SInteger
    i
      | Just xs :: [a]
    xs <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    l, Just ci :: Integer
    ci <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    i, Integer
    ci Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0, Integer
    ci Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < [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
    .!! :: 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 -> map (elemAt (implode [e1, e2, e3])) (map literal [0 .. 2]) .== [e1, e2, e3]
    -- Q.E.D.
    implode :: SymVal a => [SBV a] -> SList a
    implode :: [SBV a] -> SList a
    implode = (SBV a -> SList a -> SList a) -> SList a -> [SBV a] -> SList a
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    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 [])

    -- | Concatenate two lists. See also `.++`.
    concat :: SymVal a => SList a -> SList a -> SList a
    concat :: SList a -> SList a -> SList a
    concat x :: SList a
    x y :: 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]
    (++)) SList a
    x SList a
    y

    -- | Prepend an element, the traditional @cons@.
    infixr 5 .:
    (.:) :: SymVal a => SBV a -> SList a -> SList a
    a :: SBV a
    a .: :: SBV a -> SList a -> SList a
    .: as :: 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
    as :: SList a
    as snoc :: SList a -> SBV a -> SList a
    `snoc` a :: 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 :: SList a
    nil = []

    -- | Short cut for `concat`.
    --
    -- >>> 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 -> SList a -> SList a
    (.++) = SList a -> SList a -> SList a
    forall a. SymVal a => SList a -> SList a -> SList a
    concat

    -- | @`elem` e l@. Does @l@ contain the element @e@?
    elem :: (Eq a, SymVal a) => SBV a -> SList a -> SBool
    e :: SBV a
    e elem :: SBV a -> SList a -> SBool
    `elem` l :: 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
    e :: SBV a
    e notElem :: SBV a -> SList a -> SBool
    `notElem` l :: 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
    sub :: SList a
    sub isInfixOf :: SList a -> SList a -> SBool
    `isInfixOf` l :: 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
    pre :: SList a
    pre isPrefixOf :: SList a -> SList a -> SBool
    `isPrefixOf` l :: 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
    suf :: SList a
    suf isSuffixOf :: SList a -> SList a -> SBool
    `isSuffixOf` l :: 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 :: SInteger -> SList a -> SList a
    take i :: SInteger
    i l :: 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
    .<= 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 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 :: SInteger -> SList a -> SList a
    drop i :: SInteger
    i s :: 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
    .<= 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 :: SList a -> SInteger -> SInteger -> SList a
    subList l :: SList a
    l offset :: SInteger
    offset len :: SInteger
    len
      | Just c :: [a]
    c  <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    l                   -- a constant list
      , Just o :: Integer
    o  <- SInteger -> Maybe Integer
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SInteger
    offset              -- a constant offset
      , Just sz :: 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 x :: Integer
    x = Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 Bool -> Bool -> Bool
    && Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    lc          -- 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
    >= 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 :: SList a -> SList a -> SList a -> SList a
    replace l :: SList a
    l src :: SList a
    src dst :: SList a
    dst
      | Just b :: [a]
    b <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    src, [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]
    a <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    l
      , Just b :: [a]
    b <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    src
      , Just c :: [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 haystack :: [a]
    haystack needle :: [a]
    needle newNeedle :: [a]
    newNeedle = [a] -> [a]
    go [a]
    haystack   -- note that needle is guaranteed non-empty here.
               where go :: [a] -> [a]
    go []       = []
                     go i :: [a]
    i@(c :: a
    c:cs :: [a]
    cs)
                      | [a]
    needle [a] -> [a] -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `L.isPrefixOf` [a]
    i = [a]
    newNeedle [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ Integer -> [a] -> [a]
    forall i a. Integral i => i -> [a] -> [a]
    genericDrop ([a] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [a]
    needle :: Integer) [a]
    i
                      | Bool
    True                    = a
    c a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a] -> [a]
    go [a]
    cs

    -- | @`indexOf` 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 :: SList a -> SList a -> SInteger
    indexOf s :: SList a
    s sub :: 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 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 :: SList a -> SList a -> SInteger -> SInteger
    offsetIndexOf s :: SList a
    s sub :: SList a
    sub offset :: SInteger
    offset
      | Just c :: [a]
    c <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    s        -- a constant list
      , Just n :: [a]
    n <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    sub      -- a constant search pattern
      , Just o :: 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
    >= 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 | (i :: Integer
    i, t :: [a]
    t) <- [Integer] -> [[a]] -> [(Integer, [a])]
    forall a b. [a] -> [b] -> [(a, b)]
    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
          (i :: Integer
    i:_) -> Integer -> SInteger
    forall a. SymVal a => a -> SBV a
    literal Integer
    i
          _     -> -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

    -- | Lift a unary operator over lists.
    lift1 :: forall a b. (SymVal a, SymVal b) => SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 :: SeqOp -> Maybe (a -> b) -> SBV a -> SBV b
    lift1 w :: SeqOp
    w mbOp :: Maybe (a -> b)
    mbOp a :: SBV a
    a
      | Just cv :: SBV b
    cv <- Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    forall a b.
    (SymVal a, SymVal b) =>
    Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    concEval1 Maybe (a -> b)
    mbOp SBV a
    a
      = SBV b
    cv
      | Bool
    True
      = SVal -> SBV b
    forall a. SVal -> SBV a
    SBV (SVal -> SBV b) -> SVal -> SBV b
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy b -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy b
    forall k (t :: k). Proxy t
    Proxy @b)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (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 :: SeqOp -> Maybe (a -> b -> c) -> SBV a -> SBV b -> SBV c
    lift2 w :: SeqOp
    w mbOp :: Maybe (a -> b -> c)
    mbOp a :: SBV a
    a b :: SBV b
    b
      | Just cv :: SBV c
    cv <- Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    forall a b c.
    (SymVal a, SymVal b, SymVal c) =>
    Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 Maybe (a -> b -> c)
    mbOp SBV a
    a SBV b
    b
      = SBV c
    cv
      | Bool
    True
      = SVal -> SBV c
    forall a. SVal -> SBV a
    SBV (SVal -> SBV c) -> SVal -> SBV c
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy c -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy c
    forall k (t :: k). Proxy t
    Proxy @c)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    b
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (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 :: SeqOp
    -> Maybe (a -> b -> c -> d) -> SBV a -> SBV b -> SBV c -> SBV d
    lift3 w :: SeqOp
    w mbOp :: Maybe (a -> b -> c -> d)
    mbOp a :: SBV a
    a b :: SBV b
    b c :: SBV c
    c
      | Just cv :: SBV d
    cv <- Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    forall a b c d.
    (SymVal a, SymVal b, SymVal c, SymVal d) =>
    Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    concEval3 Maybe (a -> b -> c -> d)
    mbOp SBV a
    a SBV b
    b SBV c
    c
      = SBV d
    cv
      | Bool
    True
      = SVal -> SBV d
    forall a. SVal -> SBV a
    SBV (SVal -> SBV d) -> SVal -> SBV d
    forall a b. (a -> b) -> a -> b
    $ Kind -> Either CV (Cached SV) -> SVal
    SVal Kind
    k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
    forall a b. (a -> b) -> a -> b
    $ Cached SV -> Either CV (Cached SV)
    forall a b. b -> Either a b
    Right (Cached SV -> Either CV (Cached SV))
    -> Cached SV -> Either CV (Cached SV)
    forall a b. (a -> b) -> a -> b
    $ (State -> IO SV) -> Cached SV
    forall a. (State -> IO a) -> Cached a
    cache State -> IO SV
    r
      where k :: Kind
    k = Proxy d -> Kind
    forall a. HasKind a => a -> Kind
    kindOf (Proxy d
    forall k (t :: k). Proxy t
    Proxy @d)
            r :: State -> IO SV
    r st :: State
    st = do SV
    sva <- State -> SBV a -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV a
    a
                      SV
    svb <- State -> SBV b -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV b
    b
                      SV
    svc <- State -> SBV c -> IO SV
    forall a. State -> SBV a -> IO SV
    sbvToSV State
    st SBV c
    c
                      State -> Kind -> SBVExpr -> IO SV
    newExpr State
    st Kind
    k (Op -> [SV] -> SBVExpr
    SBVApp (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 :: Maybe (a -> b) -> SBV a -> Maybe (SBV b)
    concEval1 mbOp :: Maybe (a -> b)
    mbOp a :: SBV a
    a = b -> SBV b
    forall a. SymVal a => a -> SBV a
    literal (b -> SBV b) -> Maybe b -> Maybe (SBV b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b)
    mbOp Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a)

    -- | Concrete evaluation for binary ops
    concEval2 :: (SymVal a, SymVal b, SymVal c) => Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 :: Maybe (a -> b -> c) -> SBV a -> SBV b -> Maybe (SBV c)
    concEval2 mbOp :: Maybe (a -> b -> c)
    mbOp a :: SBV a
    a b :: SBV b
    b = c -> SBV c
    forall a. SymVal a => a -> SBV a
    literal (c -> SBV c) -> Maybe c -> Maybe (SBV c)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b -> c)
    mbOp Maybe (a -> b -> c) -> Maybe a -> Maybe (b -> c)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a Maybe (b -> c) -> Maybe b -> Maybe c
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    b)

    -- | 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 :: Maybe (a -> b -> c -> d)
    -> SBV a -> SBV b -> SBV c -> Maybe (SBV d)
    concEval3 mbOp :: Maybe (a -> b -> c -> d)
    mbOp a :: SBV a
    a b :: SBV b
    b c :: SBV c
    c = d -> SBV d
    forall a. SymVal a => a -> SBV a
    literal (d -> SBV d) -> Maybe d -> Maybe (SBV d)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Maybe (a -> b -> c -> d)
    mbOp Maybe (a -> b -> c -> d) -> Maybe a -> Maybe (b -> c -> d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV a -> Maybe a
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV a
    a Maybe (b -> c -> d) -> Maybe b -> Maybe (c -> d)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV b -> Maybe b
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV b
    b Maybe (c -> d) -> Maybe c -> Maybe d
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SBV c -> Maybe c
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SBV c
    c)

    -- | Is the list concretely known empty?
    isConcretelyEmpty :: SymVal a => SList a -> Bool
    isConcretelyEmpty :: SList a -> Bool
    isConcretelyEmpty sl :: SList a
    sl | Just l :: [a]
    l <- SList a -> Maybe [a]
    forall a. SymVal a => SBV a -> Maybe a
    unliteral SList a
    sl = [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    P.null [a]
    l
                         | Bool
    True                   = Bool
    False