| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Lib.Data.List
Description
Synopsis
- symAnd :: Foldable t => t SymBool -> SymBool
- symOr :: Foldable t => t SymBool -> SymBool
- symAny :: Foldable t => (a -> SymBool) -> t a -> SymBool
- symAll :: Foldable t => (a -> SymBool) -> t a -> SymBool
- mrgMaximum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SOrd a) => t a -> m a
- symMaximum :: forall a t. (Foldable t, Mergeable a, SOrd a, ITEOp a) => t a -> a
- mrgMinimum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SOrd a) => t a -> m a
- symMinimum :: forall a t. (Foldable t, Mergeable a, SOrd a, ITEOp a) => t a -> a
- mrgTake :: (Applicative u, UnionMergeable1 u, Mergeable a, Num int, SOrd int) => int -> [a] -> u [a]
- mrgDrop :: (Applicative u, UnionMergeable1 u, Mergeable a, Num int, SOrd int) => int -> [a] -> u [a]
- mrgSplitAt :: forall a int u. (MonadUnion u, Mergeable a, Num int, SOrd int) => int -> [a] -> u ([a], [a])
- mrgTakeWhile :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
- mrgDropWhile :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
- mrgDropWhileEnd :: (MonadUnion u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
- mrgSpan :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])
- mrgBreak :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])
- mrgStripPrefix :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => [a] -> [a] -> u (Maybe [a])
- mrgGroup :: (MonadUnion u, Mergeable a, SEq a) => [a] -> u [[a]]
- symIsPrefixOf :: SEq a => [a] -> [a] -> SymBool
- symIsSuffixOf :: SEq a => [a] -> [a] -> SymBool
- symIsInfixOf :: SEq a => [a] -> [a] -> SymBool
- symIsSubsequenceOf :: SEq a => [a] -> [a] -> SymBool
- symElem :: (Foldable t, SEq a) => a -> t a -> SymBool
- symNotElem :: (Foldable t, SEq a) => a -> t a -> SymBool
- mrgLookup :: (Applicative u, UnionMergeable1 u, Mergeable b, SEq a) => a -> [(a, b)] -> u (Maybe b)
- mrgFind :: (Foldable t, MonadUnion m, Mergeable a) => (a -> SymBool) -> t a -> m (Maybe a)
- mrgFilter :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]
- mrgPartition :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])
- (.!?) :: (MonadUnion uf, Mergeable a, Num int, SEq int) => [a] -> int -> uf (Maybe a)
- mrgElemIndex :: (MonadUnion u, Mergeable int, SEq a, Num int) => a -> [a] -> u (Maybe int)
- mrgElemIndices :: (MonadUnion u, Mergeable int, SEq a, Num int) => a -> [a] -> u [int]
- mrgFindIndex :: (Applicative u, UnionMergeable1 u, Mergeable int, SEq a, Num int) => (a -> SymBool) -> [a] -> u (Maybe int)
- mrgFindIndices :: (Applicative u, UnionMergeable1 u, Mergeable int, SEq a, Num int) => (a -> SymBool) -> [a] -> u [int]
- mrgNub :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => [a] -> u [a]
- mrgDelete :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => a -> [a] -> u [a]
- (.\\) :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a]
- mrgUnion :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a]
- mrgIntersect :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a]
- mrgInsert :: (MonadUnion m, Mergeable a, SOrd a) => a -> [a] -> m [a]
- mrgNubBy :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> a -> SymBool) -> [a] -> u [a]
- mrgDeleteBy :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> a -> SymBool) -> a -> [a] -> u [a]
- mrgDeleteFirstsBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a]
- mrgUnionBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a]
- mrgIntersectBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a]
- mrgGroupBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> u [[a]]
- mrgInsertBy :: (MonadUnion m, Mergeable a) => (a -> a -> UnionM Ordering) -> a -> [a] -> m [a]
- mrgMaximumBy :: forall t a m. (Foldable t, Mergeable a, MonadUnion m) => (a -> a -> UnionM Ordering) -> t a -> m a
- symMaximumBy :: forall t a. (Foldable t, Mergeable a, ITEOp a) => (a -> a -> UnionM Ordering) -> t a -> a
- mrgMinimumBy :: forall t a m. (Foldable t, Mergeable a, MonadUnion m) => (a -> a -> UnionM Ordering) -> t a -> m a
- symMinimumBy :: forall t a. (Foldable t, Mergeable a, ITEOp a) => (a -> a -> UnionM Ordering) -> t a -> a
Special folds
mrgMaximum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SOrd a) => t a -> m a Source #
maximum with MergingStrategy knowledge propagation.
mrgMinimum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SOrd a) => t a -> m a Source #
minimum with MergingStrategy knowledge propagation.
Sublists
Extracting sublists
mrgTake :: (Applicative u, UnionMergeable1 u, Mergeable a, Num int, SOrd int) => int -> [a] -> u [a] Source #
Symbolic version of take, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgDrop :: (Applicative u, UnionMergeable1 u, Mergeable a, Num int, SOrd int) => int -> [a] -> u [a] Source #
Symbolic version of drop, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgSplitAt :: forall a int u. (MonadUnion u, Mergeable a, Num int, SOrd int) => int -> [a] -> u ([a], [a]) Source #
Symbolic version of splitAt, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgTakeWhile :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of takeWhile, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgDropWhile :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of dropWhile, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgDropWhileEnd :: (MonadUnion u, Mergeable a) => (a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of dropWhileEnd, the result would be merged
and propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgSpan :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a]) Source #
Symbolic version of span, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgBreak :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a]) Source #
Symbolic version of break, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
mrgStripPrefix :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => [a] -> [a] -> u (Maybe [a]) Source #
Symbolic version of stripPrefix, the result would be merged and
propagate the mergeable knowledge.
Generate O(1) cases and O(len(prefix)) sized branch constraints.
mrgGroup :: (MonadUnion u, Mergeable a, SEq a) => [a] -> u [[a]] Source #
Symbolic version of group, the result would be merged and
propagate the mergeable knowledge.
This function can be very inefficient on large symbolic lists and generate O(2^n) cases. Use with caution.
Predicates
symIsPrefixOf :: SEq a => [a] -> [a] -> SymBool Source #
Symbolic version of isPrefixOf.
Generate O(len(prefix)) sized constraints.
symIsSuffixOf :: SEq a => [a] -> [a] -> SymBool Source #
Symbolic version of isSuffixOf.
Generate O(len(suffix)) sized constraints.
symIsInfixOf :: SEq a => [a] -> [a] -> SymBool Source #
Symbolic version of isInfixOf.
Generate O(len(haystack) * len(needle)) sized constraints.
symIsSubsequenceOf :: SEq a => [a] -> [a] -> SymBool Source #
Symbolic version of isSubsequenceOf.
Generate O(len(haystack) * len(needle)) sized constraints.
Searching lists
Searching by equality
mrgLookup :: (Applicative u, UnionMergeable1 u, Mergeable b, SEq a) => a -> [(a, b)] -> u (Maybe b) Source #
Symbolic version of lookup, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases and O(n) sized branch constraints.
Searching with a predicate
mrgFind :: (Foldable t, MonadUnion m, Mergeable a) => (a -> SymBool) -> t a -> m (Maybe a) Source #
elem with symbolic equality and MergingStrategy knowledge
propagation.
mrgFilter :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of filter, the result would be merged and
propagate the mergeable knowledge.
This function can be very inefficient on large symbolic lists and generate O(2^n) cases. Use with caution.
mrgPartition :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a]) Source #
Symbolic version of partition, the result would be merged and
propagate the mergeable knowledge.
This function can be very inefficient on large symbolic lists and generate O(2^n) cases. Use with caution.
Indexing lists
(.!?) :: (MonadUnion uf, Mergeable a, Num int, SEq int) => [a] -> int -> uf (Maybe a) Source #
Symbolic version of !?, the result would be merged and
propagate the mergeable knowledge.
Can generate O(1) cases and O(n) sized branch constraints.
mrgElemIndex :: (MonadUnion u, Mergeable int, SEq a, Num int) => a -> [a] -> u (Maybe int) Source #
Symbolic version of elemIndex, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases (or O(1) if int is merged), and O(n^2) sized constraints.
mrgElemIndices :: (MonadUnion u, Mergeable int, SEq a, Num int) => a -> [a] -> u [int] Source #
Symbolic version of elemIndices, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^3) sized constraints.
mrgFindIndex :: (Applicative u, UnionMergeable1 u, Mergeable int, SEq a, Num int) => (a -> SymBool) -> [a] -> u (Maybe int) Source #
Symbolic version of findIndex, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases (or O(1) if int is merged), and O(n^2) sized constraints, assuming the predicate only generates O(1) constraints.
mrgFindIndices :: (Applicative u, UnionMergeable1 u, Mergeable int, SEq a, Num int) => (a -> SymBool) -> [a] -> u [int] Source #
Symbolic version of findIndices, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^3) sized constraints, assuming the predicate only generates O(1) constraints.
Special lists
Set operations
mrgNub :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => [a] -> u [a] Source #
Symbolic version of nub, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^3) sized constraints.
mrgDelete :: (Applicative u, UnionMergeable1 u, Mergeable a, SEq a) => a -> [a] -> u [a] Source #
Symbolic version of delete, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^2) sized constraints.
(.\\) :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a] Source #
Symbolic version of \\, the result would be merged and
propagate the mergeable knowledge.
Can generate O(len(lhs)) cases, and O(len(lhs)^2 * len(rhs)) sized constraints.
mrgUnion :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a] Source #
Symbolic version of union, the result would be merged and
propagate the mergeable knowledge.
Can generate O(len(rhs)) cases, and O(len(rhs)^5 * len(lhs)) sized constraints.
Should be improvable.
mrgIntersect :: (MonadUnion u, Mergeable a, SEq a) => [a] -> [a] -> u [a] Source #
Ordered lists (sorting not supported yet)
mrgInsert :: (MonadUnion m, Mergeable a, SOrd a) => a -> [a] -> m [a] Source #
Symbolic version of insert, the result would be merged and
propagate the mergeable knowledge.
Can generate 1 case, and O(n^2) sized constraints.
Generalized functions
The By operations
User-supplied equality (replacing an SEq context)
mrgNubBy :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> a -> SymBool) -> [a] -> u [a] Source #
Symbolic version of nubBy, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^3) sized constraints, assuming the predicate only generates O(1) constraints.
mrgDeleteBy :: (Applicative u, UnionMergeable1 u, Mergeable a) => (a -> a -> SymBool) -> a -> [a] -> u [a] Source #
Symbolic version of deleteBy, the result would be merged and
propagate the mergeable knowledge.
Can generate O(n) cases, and O(n^2) sized constraints, assuming the predicate only generates O(1) constraints.
mrgDeleteFirstsBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a] Source #
Symbolic version of deleteFirstsBy, the result would be merged
and propagate the mergeable knowledge.
Can generate O(len(lhs)) cases, and O(len(lhs)^2 * len(rhs)) sized constraints, assuming the predicate only generates O(1) constraints.
mrgUnionBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a] Source #
Symbolic version of unionBy, the result would be merged and
propagate the mergeable knowledge.
Can generate O(len(rhs)) cases, and O(len(rhs)^5 * len(lhs)) sized constraints, assuming the predicate only generates O(1) constraints.
Should be improvable.
mrgIntersectBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> [a] -> u [a] Source #
Symbolic version of intersectBy, the result would be merged and
propagate the mergeable knowledge.
Can generate O(len(rhs)) cases, and O(len(lhs) * len(rhs)) constraints, assuming the predicate only generates O(1) constraints.
mrgGroupBy :: (MonadUnion u, Mergeable a) => (a -> a -> SymBool) -> [a] -> u [[a]] Source #
This function can be very inefficient on large symbolic lists and generate O(2^n) cases. Use with caution.
User-supplied comparison (replacing an SOrd context)
mrgInsertBy :: (MonadUnion m, Mergeable a) => (a -> a -> UnionM Ordering) -> a -> [a] -> m [a] Source #
Symbolic version of insertBy, the result would be merged and
propagate the mergeable knowledge.
Can generate 1 case, and O(n^2) sized constraints, assuming the ordering function only generates O(1) constraints.
mrgMaximumBy :: forall t a m. (Foldable t, Mergeable a, MonadUnion m) => (a -> a -> UnionM Ordering) -> t a -> m a Source #
maximumBy with MergingStrategy knowledge propagation.
symMaximumBy :: forall t a. (Foldable t, Mergeable a, ITEOp a) => (a -> a -> UnionM Ordering) -> t a -> a Source #
mrgMinimumBy :: forall t a m. (Foldable t, Mergeable a, MonadUnion m) => (a -> a -> UnionM Ordering) -> t a -> m a Source #
minimumBy with MergingStrategy knowledge propagation.