-----------------------------------------------------------------------------
-- |
-- 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 Prelude hiding ((++))

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 SList a
s b
e 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 Int
cnt SBV a -> SBV b -> SBV b
f 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` Int
0)
  where go :: t -> SList a -> SBV b
go t
0 SList a
_ = SBV b
b
        go t
i 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 (\SBV a
h 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
-t
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 Int
cnt SBV a -> SBV b -> m (SBV b)
f SBV b
b = Int -> SList a -> m (SBV b)
go (Int
cnt Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
0)
  where go :: Int -> SList a -> m (SBV b)
        go :: Int -> SList a -> m (SBV b)
go Int
0 SList a
_ = SBV b -> m (SBV b)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV b
b
        go Int
i 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) (\SBV a
h 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
-Int
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 Int
cnt 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` Int
0)
  where go :: t -> SBV b -> SList a -> SBV b
go t
0 SBV b
b SList a
_ = SBV b
b
        go t
i SBV b
b 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 (\SBV a
h SList a
t -> t -> SBV b -> SList a -> SBV b
go (t
it -> t -> t
forall a. Num a => a -> a -> a
-t
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 Int
cnt 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` Int
0)
  where go :: Int -> SBV b -> SList a -> m (SBV b)
        go :: Int -> SBV b -> SList a -> m (SBV b)
go Int
0 SBV b
b SList a
_ = SBV b -> m (SBV b)
forall (m :: * -> *) a. Monad m => a -> m a
return SBV b
b
        go Int
i SBV b
b 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) (\SBV a
h 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
-Int
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 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
(+) SBV a
0

-- | Bounded product.
bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
bprod :: Int -> SList a -> SBV a
bprod 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
(*) SBV 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 Int
i 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 (\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 Int
i 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 (\SBV a
a 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 Int
i 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 (\SBV a
x 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 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 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 Int
i 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 Int
i 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 Int
i 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
-Int
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 Int
i 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
-Int
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 Int
cnt 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` Int
0)
   where go :: t -> SList a -> SList b -> SList c
go t
0 SList a
_  SList b
_  = []
         go t
i SList a
xs 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
-t
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 Int
i 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 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 (\SBV a
a 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 Int
cnt SBV a -> SBV [a] -> SBV b -> SBV b
f 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` Int
0)
  where go :: t -> SBV [a] -> SBV b
go t
0 SBV [a]
_ = SBV b
b
        go t
i 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 (\SBV a
h 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
-t
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 Int
cnt 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 SBV a
sortedHd SList a
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 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) []