    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.BoundedList
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- A collection of bounded list utilities, useful when working with symbolic lists.
    -- These functions all take a concrete bound, and operate on the prefix of a symbolic
    -- list that is at most that long. Due to limitations on writing recursive functions
    -- over lists (the classic symbolic termination problem), we cannot write arbitrary
    -- recursive programs on symbolic lists. But most of the time all we need is a
    -- bounded prefix of this list, at which point these functions come in handy.
    -----------------------------------------------------------------------------

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

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.BoundedList (
         -- * General folds
         bfoldr, bfoldrM, bfoldl, bfoldlM
         -- * Map, filter, zipWith, elem
       , bmap, bmapM, bfilter, bzipWith, belem
         -- * Aggregates
       , bsum, bprod, band, bor, bany, ball, bmaximum, bminimum
         -- * Miscellaneous: Reverse and sort
       , breverse, bsort
       )
       where

    import Data.SBV
    import Data.SBV.List ((.:), (.++))
    import qualified Data.SBV.List as L

    -- | Case analysis on a symbolic list. (Not exported.)
    lcase :: (SymVal a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase :: SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase s :: SList a
    s e :: b
    e c :: SBV a -> SList a -> b
    c = SBool -> b -> b -> b
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SList a -> SBool
    forall a. SymVal a => SList a -> SBool
    L.null SList a
    s) b
    e (SBV a -> SList a -> b
    c (SList a -> SBV a
    forall a. SymVal a => SList a -> SBV a
    L.head SList a
    s) (SList a -> SList a
    forall a. SymVal a => SList a -> SList a
    L.tail SList a
    s))

    -- | Bounded fold from the right.
    bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr :: Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr cnt :: Int
    cnt f :: SBV a -> SBV b -> SBV b
    f b :: SBV b
    b = Int -> SList a -> SBV b
    forall t. (Eq t, Num t) => t -> SList a -> SBV b
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
      where go :: t -> SList a -> SBV b
    go 0 _ = SBV b
    b
            go i :: t
    i s :: SList a
    s = SList a -> SBV b -> (SBV a -> SList a -> SBV b) -> SBV b
    forall a b.
    (SymVal a, Mergeable b) =>
    SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase SList a
    s SBV b
    b (\h :: SBV a
    h t :: SList a
    t -> SBV a
    h SBV a -> SBV b -> SBV b
    `f` t -> SList a -> SBV b
    go (t
    it -> t -> t
    forall a. Num a => a -> a -> a
    -1) SList a
    t)

    -- | Bounded monadic fold from the right.
    bfoldrM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b)))
            => Int -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)
    bfoldrM :: Int
    -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)
    bfoldrM cnt :: Int
    cnt f :: SBV a -> SBV b -> m (SBV b)
    f b :: SBV b
    b = Int -> SList a -> m (SBV b)
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
      where go :: Int -> SList a -> m (SBV b)
            go :: Int -> SList a -> m (SBV b)
    go 0 _ = SBV b -> m (SBV b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV b
    b
            go i :: Int
    i s :: SList a
    s = SList a
    -> m (SBV b) -> (SBV a -> SList a -> m (SBV b)) -> m (SBV b)
    forall a b.
    (SymVal a, Mergeable b) =>
    SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase SList a
    s (SBV b -> m (SBV b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV b
    b) (\h :: SBV a
    h t :: SList a
    t -> SBV a -> SBV b -> m (SBV b)
    f SBV a
    h (SBV b -> m (SBV b)) -> m (SBV b) -> m (SBV b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> SList a -> m (SBV b)
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) SList a
    t)

    -- | Bounded fold from the left.
    bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl :: Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl cnt :: Int
    cnt f :: SBV b -> SBV a -> SBV b
    f = Int -> SBV b -> SList a -> SBV b
    forall t. (Eq t, Num t) => t -> SBV b -> SList a -> SBV b
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
      where go :: t -> SBV b -> SList a -> SBV b
    go 0 b :: SBV b
    b _ = SBV b
    b
            go i :: t
    i b :: SBV b
    b s :: SList a
    s = SList a -> SBV b -> (SBV a -> SList a -> SBV b) -> SBV b
    forall a b.
    (SymVal a, Mergeable b) =>
    SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase SList a
    s SBV b
    b (\h :: SBV a
    h t :: SList a
    t -> t -> SBV b -> SList a -> SBV b
    go (t
    it -> t -> t
    forall a. Num a => a -> a -> a
    -1) (SBV b
    b SBV b -> SBV a -> SBV b
    `f` SBV a
    h) SList a
    t)

    -- | Bounded monadic fold from the left.
    bfoldlM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b)))
            => Int -> (SBV b -> SBV a -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)
    bfoldlM :: Int
    -> (SBV b -> SBV a -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)
    bfoldlM cnt :: Int
    cnt f :: SBV b -> SBV a -> m (SBV b)
    f = Int -> SBV b -> SList a -> m (SBV b)
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
      where go :: Int -> SBV b -> SList a -> m (SBV b)
            go :: Int -> SBV b -> SList a -> m (SBV b)
    go 0 b :: SBV b
    b _ = SBV b -> m (SBV b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV b
    b
            go i :: Int
    i b :: SBV b
    b s :: SList a
    s = SList a
    -> m (SBV b) -> (SBV a -> SList a -> m (SBV b)) -> m (SBV b)
    forall a b.
    (SymVal a, Mergeable b) =>
    SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase SList a
    s (SBV b -> m (SBV b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return SBV b
    b) (\h :: SBV a
    h t :: SList a
    t -> do { SBV b
    fbh <- SBV b -> SBV a -> m (SBV b)
    f SBV b
    b SBV a
    h; Int -> SBV b -> SList a -> m (SBV b)
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) SBV b
    fbh SList a
    t })

    -- | Bounded sum.
    bsum :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
    bsum :: Int -> SList a -> SBV a
    bsum i :: Int
    i = Int -> (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl Int
    i SBV a -> SBV a -> SBV a
    forall a. Num a => a -> a -> a
    (+) 0

    -- | Bounded product.
    bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
    bprod :: Int -> SList a -> SBV a
    bprod i :: Int
    i = Int -> (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl Int
    i SBV a -> SBV a -> SBV a
    forall a. Num a => a -> a -> a
    (*) 1

    -- | Bounded map.
    bmap :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b) -> SList a -> SList b
    bmap :: Int -> (SBV a -> SBV b) -> SList a -> SList b
    bmap i :: Int
    i f :: SBV a -> SBV b
    f = Int
    -> (SBV a -> SList b -> SList b) -> SList b -> SList a -> SList b
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    i (\x :: SBV a
    x -> (SBV a -> SBV b
    f SBV a
    x SBV b -> SList b -> SList b
    forall a. SymVal a => SBV a -> SList a -> SList a
    .:)) []

    -- | Bounded monadic map.
    bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b])))
          => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b)
    bmapM :: Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b)
    bmapM i :: Int
    i f :: SBV a -> m (SBV b)
    f = Int
    -> (SBV a -> SList b -> m (SList b))
    -> SList b
    -> SList a
    -> m (SList b)
    forall a b (m :: * -> *).
    (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b))) =>
    Int
    -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)
    bfoldrM Int
    i (\a :: SBV a
    a bs :: SList b
    bs -> SBV b -> SList b -> SList b
    forall a. SymVal a => SBV a -> SList a -> SList a
    (.:) (SBV b -> SList b -> SList b)
    -> m (SBV b) -> m (SList b -> SList b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> SBV a -> m (SBV b)
    f SBV a
    a m (SList b -> SList b) -> m (SList b) -> m (SList b)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SList b -> m (SList b)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SList b
    bs) []

    -- | Bounded filter.
    bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a
    bfilter :: Int -> (SBV a -> SBool) -> SList a -> SList a
    bfilter i :: Int
    i f :: SBV a -> SBool
    f = Int
    -> (SBV a -> SList a -> SList a) -> SList a -> SList a -> SList a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    i (\x :: SBV a
    x y :: SList a
    y -> SBool -> SList a -> SList a -> SList a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV a -> SBool
    f SBV a
    x) (SBV a
    x SBV a -> SList a -> SList a
    forall a. SymVal a => SBV a -> SList a -> SList a
    .: SList a
    y) SList a
    y) []

    -- | Bounded logical and
    band :: Int -> SList Bool -> SBool
    band :: Int -> SList Bool -> SBool
    band i :: Int
    i = Int -> (SBool -> SBool -> SBool) -> SBool -> SList Bool -> SBool
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    i SBool -> SBool -> SBool
    (.&&) (SBool
    sTrue  :: SBool)

    -- | Bounded logical or
    bor :: Int -> SList Bool -> SBool
    bor :: Int -> SList Bool -> SBool
    bor i :: Int
    i = Int -> (SBool -> SBool -> SBool) -> SBool -> SList Bool -> SBool
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    i SBool -> SBool -> SBool
    (.||) (SBool
    sFalse :: SBool)

    -- | Bounded any
    bany :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
    bany :: Int -> (SBV a -> SBool) -> SList a -> SBool
    bany i :: Int
    i f :: SBV a -> SBool
    f = Int -> SList Bool -> SBool
    bor Int
    i (SList Bool -> SBool)
    -> (SList a -> SList Bool) -> SList a -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> (SBV a -> SBool) -> SList a -> SList Bool
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b) -> SList a -> SList b
    bmap Int
    i SBV a -> SBool
    f

    -- | Bounded all
    ball :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
    ball :: Int -> (SBV a -> SBool) -> SList a -> SBool
    ball i :: Int
    i f :: SBV a -> SBool
    f = Int -> SList Bool -> SBool
    band Int
    i (SList Bool -> SBool)
    -> (SList a -> SList Bool) -> SList a -> SBool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> (SBV a -> SBool) -> SList a -> SList Bool
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b) -> SList a -> SList b
    bmap Int
    i SBV a -> SBool
    f

    -- | Bounded maximum. Undefined if list is empty.
    bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
    bmaximum :: Int -> SList a -> SBV a
    bmaximum i :: Int
    i l :: SList a
    l = Int -> (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) SBV a -> SBV a -> SBV a
    forall a. OrdSymbolic a => a -> a -> a
    smax (SList a -> SBV a
    forall a. SymVal a => SList a -> SBV a
    L.head SList a
    l) (SList a -> SList a
    forall a. SymVal a => SList a -> SList a
    L.tail SList a
    l)

    -- | Bounded minimum. Undefined if list is empty.
    bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
    bminimum :: Int -> SList a -> SBV a
    bminimum i :: Int
    i l :: SList a
    l = Int -> (SBV a -> SBV a -> SBV a) -> SBV a -> SList a -> SBV a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldl (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) SBV a -> SBV a -> SBV a
    forall a. OrdSymbolic a => a -> a -> a
    smin (SList a -> SBV a
    forall a. SymVal a => SList a -> SBV a
    L.head SList a
    l) (SList a -> SList a
    forall a. SymVal a => SList a -> SList a
    L.tail SList a
    l)

    -- | Bounded zipWith
    bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
    bzipWith :: Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
    bzipWith cnt :: Int
    cnt f :: SBV a -> SBV b -> SBV c
    f = Int -> SList a -> SList b -> SList c
    forall t. (Eq t, Num t) => t -> SList a -> SList b -> SList c
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
       where go :: t -> SList a -> SList b -> SList c
    go 0 _  _  = []
             go i :: t
    i xs :: SList a
    xs ys :: SList b
    ys = SBool -> SList c -> SList c -> SList c
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SList a -> SBool
    forall a. SymVal a => SList a -> SBool
    L.null SList a
    xs SBool -> SBool -> SBool
    .|| SList b -> SBool
    forall a. SymVal a => SList a -> SBool
    L.null SList b
    ys)
                              []
                              (SBV a -> SBV b -> SBV c
    f (SList a -> SBV a
    forall a. SymVal a => SList a -> SBV a
    L.head SList a
    xs) (SList b -> SBV b
    forall a. SymVal a => SList a -> SBV a
    L.head SList b
    ys) SBV c -> SList c -> SList c
    forall a. SymVal a => SBV a -> SList a -> SList a
    .: t -> SList a -> SList b -> SList c
    go (t
    it -> t -> t
    forall a. Num a => a -> a -> a
    -1) (SList a -> SList a
    forall a. SymVal a => SList a -> SList a
    L.tail SList a
    xs) (SList b -> SList b
    forall a. SymVal a => SList a -> SList a
    L.tail SList b
    ys))

    -- | Bounded element check
    belem :: (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
    belem :: Int -> SBV a -> SList a -> SBool
    belem i :: Int
    i e :: SBV a
    e = Int -> (SBV a -> SBool) -> SList a -> SBool
    forall a. SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
    bany Int
    i (SBV a
    e SBV a -> SBV a -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .==)

    -- | Bounded reverse
    breverse :: SymVal a => Int -> SList a -> SList a
    breverse :: Int -> SList a -> SList a
    breverse cnt :: Int
    cnt = Int
    -> (SBV a -> SList a -> SList a) -> SList a -> SList a -> SList a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    cnt (\a :: SBV a
    a b :: SList a
    b -> SList a
    b 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
    L.singleton SBV a
    a) []

    -- | Bounded paramorphism (not exported).
    bpara :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV [a] -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bpara :: Int
    -> (SBV a -> SBV [a] -> SBV b -> SBV b)
    -> SBV b
    -> SBV [a]
    -> SBV b
    bpara cnt :: Int
    cnt f :: SBV a -> SBV [a] -> SBV b -> SBV b
    f b :: SBV b
    b = Int -> SBV [a] -> SBV b
    forall t. (Eq t, Num t) => t -> SBV [a] -> SBV b
    go (Int
    cnt Int -> Int -> Int
    forall a. Ord a => a -> a -> a
    `max` 0)
      where go :: t -> SBV [a] -> SBV b
    go 0 _ = SBV b
    b
            go i :: t
    i s :: SBV [a]
    s = SBV [a] -> SBV b -> (SBV a -> SBV [a] -> SBV b) -> SBV b
    forall a b.
    (SymVal a, Mergeable b) =>
    SList a -> b -> (SBV a -> SList a -> b) -> b
    lcase SBV [a]
    s SBV b
    b (\h :: SBV a
    h t :: SBV [a]
    t -> SBV a -> SBV [a] -> SBV b -> SBV b
    f SBV a
    h SBV [a]
    t (t -> SBV [a] -> SBV b
    go (t
    it -> t -> t
    forall a. Num a => a -> a -> a
    -1) SBV [a]
    t))

    -- | Insert an element into a sorted list (not exported).
    binsert :: (Ord a, SymVal a) => Int -> SBV a -> SList a -> SList a
    binsert :: Int -> SBV a -> SList a -> SList a
    binsert cnt :: Int
    cnt a :: SBV a
    a = Int
    -> (SBV a -> SList a -> SList a -> SList a)
    -> SList a
    -> SList a
    -> SList a
    forall a b.
    (SymVal a, SymVal b) =>
    Int
    -> (SBV a -> SBV [a] -> SBV b -> SBV b)
    -> SBV b
    -> SBV [a]
    -> SBV b
    bpara Int
    cnt SBV a -> SList a -> SList a -> SList a
    f (SBV a -> SList a
    forall a. SymVal a => SBV a -> SList a
    L.singleton SBV a
    a)
      where f :: SBV a -> SList a -> SList a -> SList a
    f sortedHd :: SBV a
    sortedHd sortedTl :: SList a
    sortedTl sortedTl' :: SList a
    sortedTl' = SBool -> SList a -> SList a -> SList a
    forall a. Mergeable a => SBool -> a -> a -> a
    ite (SBV a
    a SBV a -> SBV a -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .< SBV a
    sortedHd)
                                                (SBV a
    a SBV a -> SList a -> SList a
    forall a. SymVal a => SBV a -> SList a -> SList a
    .: SBV a
    sortedHd SBV a -> SList a -> SList a
    forall a. SymVal a => SBV a -> SList a -> SList a
    .: SList a
    sortedTl)
                                                (SBV a
    sortedHd SBV a -> SList a -> SList a
    forall a. SymVal a => SBV a -> SList a -> SList a
    .: SList a
    sortedTl')

    -- | Bounded insertion sort
    bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a
    bsort :: Int -> SList a -> SList a
    bsort cnt :: Int
    cnt = Int
    -> (SBV a -> SList a -> SList a) -> SList a -> SList a -> SList a
    forall a b.
    (SymVal a, SymVal b) =>
    Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
    bfoldr Int
    cnt (Int -> SBV a -> SList a -> SList a
    forall a. (Ord a, SymVal a) => Int -> SBV a -> SList a -> SList a
    binsert Int
    cnt) []

    -- Hlint is thinking "OverloadedLists" is wrong, but GHC wants it.
    {-# ANN module ("HLint: ignore Unused LANGUAGE pragma" :: String) #-}