{-# LANGUAGE OverloadedLists #-}
module Data.SBV.List.Bounded (
bfoldr, bfoldl
, bmap, bfilter, bzipWith, belem
, bsum, bprod, band, bor, bany, ball, bmaximum, bminimum
)
where
import Data.SBV
import Data.SBV.List ((.:))
import qualified Data.SBV.List as L
lcase :: (SymWord a, Mergeable b) => SList a -> b -> (SBV a -> SList a -> b) -> b
lcase s e c = ite (L.null s) e (c (L.head s) (L.tail s))
bfoldr :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
bfoldr cnt f b = go (cnt `max` 0)
where go 0 _ = b
go i s = lcase s b (\h t -> h `f` go (i-1) t)
bfoldl :: (SymWord a, SymWord b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
bfoldl cnt f = go (cnt `max` 0)
where go 0 b _ = b
go i b s = lcase s b (\h t -> go (i-1) (b `f` h) t)
bsum :: (SymWord a, Num a) => Int -> SList a -> SBV a
bsum i = bfoldl i (+) 0
bprod :: (SymWord a, Num a) => Int -> SList a -> SBV a
bprod i = bfoldl i (*) 1
bmap :: (SymWord a, SymWord b) => Int -> (SBV a -> SBV b) -> SList a -> SList b
bmap i f = bfoldr i (\x -> (f x .:)) []
bfilter :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SList a
bfilter i f = bfoldr i (\x y -> ite (f x) (x .: y) y) []
band :: Int -> SList Bool -> SBool
band i = bfoldr i (&&&) (true :: SBool)
bor :: Int -> SList Bool -> SBool
bor i = bfoldr i (|||) (false :: SBool)
bany :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SBool
bany i f = bor i . bmap i f
ball :: SymWord a => Int -> (SBV a -> SBool) -> SList a -> SBool
ball i f = band i . bmap i f
bmaximum :: (SymWord a, Num a) => Int -> SList a -> SBV a
bmaximum i l = bfoldl (i-1) smax (L.head l) (L.tail l)
bminimum :: (SymWord a, Num a) => Int -> SList a -> SBV a
bminimum i l = bfoldl (i-1) smin (L.head l) (L.tail l)
bzipWith :: (SymWord a, SymWord b, SymWord c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
bzipWith cnt f = go (cnt `max` 0)
where go 0 _ _ = []
go i xs ys = ite (L.null xs ||| L.null ys)
[]
(f (L.head xs) (L.head ys) .: go (i-1) (L.tail xs) (L.tail ys))
belem :: SymWord a => Int -> SBV a -> SList a -> SBool
belem i e = bany i (e .==)