-----------------------------------------------------------------------------
-- |
-- 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 :: forall a b.
(SymVal a, Mergeable b) =>
SList a -> b -> (SBV a -> SList a -> b) -> b
lcase SList a
s b
e SBV a -> SList a -> b
c = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. SymVal a => SList a -> SBool
L.null SList a
s) b
e (SBV a -> SList a -> b
c (forall a. SymVal a => SList a -> SBV a
L.head SList a
s) (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 :: 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 -> SBV b -> SBV b
f SBV b
b = forall {t}. (Eq t, Num t) => t -> SList a -> SBV b
go (Int
cnt 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 = 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
iforall 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 :: 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
cnt SBV a -> SBV b -> m (SBV b)
f SBV b
b = Int -> SList a -> m (SBV b)
go (Int
cnt 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return SBV b
b
        go Int
i SList a
s = forall a b.
(SymVal a, Mergeable b) =>
SList a -> b -> (SBV a -> SList a -> b) -> b
lcase SList a
s (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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> SList a -> m (SBV b)
go (Int
iforall 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 :: forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl Int
cnt SBV b -> SBV a -> SBV b
f = forall {t}. (Eq t, Num t) => t -> SBV b -> SList a -> SBV b
go (Int
cnt 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 = 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
iforall 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 :: 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
cnt SBV b -> SBV a -> m (SBV b)
f = Int -> SBV b -> SList a -> m (SBV b)
go (Int
cnt 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return SBV b
b
        go Int
i SBV b
b SList a
s = forall a b.
(SymVal a, Mergeable b) =>
SList a -> b -> (SBV a -> SList a -> b) -> b
lcase SList a
s (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
iforall 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 :: forall a. (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
bsum Int
i = forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl Int
i 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 :: forall a. (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
bprod Int
i = forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl Int
i 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 :: forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV a -> SBV b) -> SList a -> SList b
bmap Int
i SBV a -> SBV b
f = 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 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 :: forall a b (m :: * -> *).
(SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) =>
Int -> (SBV a -> m (SBV b)) -> SList a -> m (SBV [b])
bmapM Int
i SBV a -> m (SBV b)
f = 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 SBV [b]
bs -> forall a. SymVal a => SBV a -> SList a -> SList a
(.:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBV a -> m (SBV b)
f SBV a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SBV [b]
bs) []

-- | Bounded filter.
bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a
bfilter :: forall a. SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a
bfilter Int
i SBV a -> SBool
f = 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]
y -> forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a -> SBool
f SBV a
x) (SBV a
x forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV [a]
y) SBV [a]
y) []

-- | Bounded logical and
band :: Int -> SList Bool -> SBool
band :: Int -> SList Bool -> SBool
band Int
i = 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 = 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 :: forall a. SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
bany Int
i SBV a -> SBool
f = Int -> SList Bool -> SBool
bor Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
ball Int
i SBV a -> SBool
f = Int -> SList Bool -> SBool
band Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall a. (Ord a, SymVal a) => Int -> SList a -> SBV a
bmaximum Int
i SList a
l = forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl (Int
iforall a. Num a => a -> a -> a
-Int
1) forall a. OrdSymbolic a => a -> a -> a
smax (forall a. SymVal a => SList a -> SBV a
L.head SList a
l) (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 :: forall a. (Ord a, SymVal a) => Int -> SList a -> SBV a
bminimum Int
i SList a
l = forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl (Int
iforall a. Num a => a -> a -> a
-Int
1) forall a. OrdSymbolic a => a -> a -> a
smin (forall a. SymVal a => SList a -> SBV a
L.head SList a
l) (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 :: forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
bzipWith Int
cnt SBV a -> SBV b -> SBV c
f = forall {t}. (Eq t, Num t) => t -> SList a -> SList b -> SList c
go (Int
cnt 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 = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. SymVal a => SList a -> SBool
L.null SList a
xs SBool -> SBool -> SBool
.|| forall a. SymVal a => SList a -> SBool
L.null SList b
ys)
                          []
                          (SBV a -> SBV b -> SBV c
f (forall a. SymVal a => SList a -> SBV a
L.head SList a
xs) (forall a. SymVal a => SList a -> SBV a
L.head SList b
ys) forall a. SymVal a => SBV a -> SList a -> SList a
.: t -> SList a -> SList b -> SList c
go (t
iforall a. Num a => a -> a -> a
-t
1) (forall a. SymVal a => SList a -> SList a
L.tail SList a
xs) (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 :: forall a. (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
belem Int
i SBV a
e = forall a. SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
bany Int
i (SBV a
e forall a. EqSymbolic a => a -> a -> SBool
.==)

-- | Bounded reverse
breverse :: SymVal a => Int -> SList a -> SList a
breverse :: forall a. SymVal a => Int -> SList a -> SList a
breverse Int
cnt = 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 SBV [a]
b -> SBV [a]
b forall a. SymVal a => SList a -> SList 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 :: 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 -> SBV [a] -> SBV b -> SBV b
f SBV b
b = forall {t}. (Eq t, Num t) => t -> SBV [a] -> SBV b
go (Int
cnt 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 = 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
iforall 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 :: forall a. (Ord a, SymVal a) => Int -> SBV a -> SList a -> SList a
binsert Int
cnt SBV a
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 (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' = forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
a forall a. OrdSymbolic a => a -> a -> SBool
.< SBV a
sortedHd)
                                            (SBV a
a forall a. SymVal a => SBV a -> SList a -> SList a
.: SBV a
sortedHd forall a. SymVal a => SBV a -> SList a -> SList a
.: SList a
sortedTl)
                                            (SBV a
sortedHd 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 :: forall a. (Ord a, SymVal a) => Int -> SList a -> SList a
bsort Int
cnt = forall a b.
(SymVal a, SymVal b) =>
Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
bfoldr Int
cnt (forall a. (Ord a, SymVal a) => Int -> SBV a -> SList a -> SList a
binsert Int
cnt) []