| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.BoundedList
Description
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.
Synopsis
- bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> 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)
- bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> 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)
- bmap :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b) -> SList a -> SList b
- bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b)
- bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a
- bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
- belem :: (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
- bsum :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
- bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
- band :: Int -> SList Bool -> SBool
- bor :: Int -> SList Bool -> SBool
- bany :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
- ball :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
- bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
- bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
- breverse :: SymVal a => Int -> SList a -> SList a
- bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a
General folds
bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b Source #
Bounded 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) Source #
Bounded monadic fold from the right.
bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b Source #
Bounded 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) Source #
Bounded monadic fold from the left.
Map, filter, zipWith, elem
bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b) Source #
Bounded monadic map.
bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c Source #
Bounded zipWith
Aggregates
bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a Source #
Bounded maximum. Undefined if list is empty.
bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a Source #
Bounded minimum. Undefined if list is empty.