Grisette.Lib.Data.List

Special folds

symAnd :: Foldable t => t SymBool -> SymBool

and on symbolic boolean.

symOr :: Foldable t => t SymBool -> SymBool

or on symbolic boolean.

symAny :: Foldable t => (a -> SymBool) -> t a -> SymBool

any on symbolic boolean.

symAll :: Foldable t => (a -> SymBool) -> t a -> SymBool

all on symbolic boolean.

mrgMaximum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SymOrd a) => t a -> m a

maximum with MergingStrategy knowledge propagation.

symMaximum :: forall a t. (Foldable t, Mergeable a, SymOrd a, ITEOp a) => t a -> a

maximum with result merged with ITEOp.

mrgMinimum :: forall a t m. (Foldable t, MonadUnion m, Mergeable a, SymOrd a) => t a -> m a

minimum with MergingStrategy knowledge propagation.

symMinimum :: forall a t. (Foldable t, Mergeable a, SymOrd a, ITEOp a) => t a -> a

minimum with result merged with ITEOp.

Sublists

Extracting sublists

mrgTake :: (Applicative u, SymBranching u, Mergeable a, Num int, SymOrd int) => int -> [a] -> u [a]

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, SymBranching u, Mergeable a, Num int, SymOrd int) => int -> [a] -> u [a]

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, SymOrd int) => int -> [a] -> u ([a], [a])

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, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]

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, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]

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]

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, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])

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, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])

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, SymBranching u, Mergeable a, SymEq a) => [a] -> [a] -> u (Maybe [a])

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, SymEq a) => [a] -> u [[a]]

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 :: SymEq a => [a] -> [a] -> SymBool

Symbolic version of isPrefixOf.

Generate O(len(prefix)) sized constraints.

symIsSuffixOf :: SymEq a => [a] -> [a] -> SymBool

Symbolic version of isSuffixOf.

Generate O(len(suffix)) sized constraints.

symIsInfixOf :: SymEq a => [a] -> [a] -> SymBool

Symbolic version of isInfixOf.

Generate O(len(haystack) * len(needle)) sized constraints.

symIsSubsequenceOf :: SymEq a => [a] -> [a] -> SymBool

Symbolic version of isSubsequenceOf.

Generate O(len(haystack) * len(needle)) sized constraints.

Searching lists

Searching by equality

symElem :: (Foldable t, SymEq a) => a -> t a -> SymBool

elem with symbolic equality.

symNotElem :: (Foldable t, SymEq a) => a -> t a -> SymBool

elem with symbolic equality.

mrgLookup :: forall a b u. (Applicative u, SymBranching u, Mergeable b, SymEq a) => a -> [(a, b)] -> u (Maybe b)

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)

elem with symbolic equality and MergingStrategy knowledge propagation.

mrgFilter :: (Applicative u, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u [a]

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 :: forall u a. (Applicative u, SymBranching u, Mergeable a) => (a -> SymBool) -> [a] -> u ([a], [a])

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

(.!?) :: forall a uf int. (MonadUnion uf, Mergeable a, Num int, SymEq int) => [a] -> int -> uf (Maybe a)

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, SymEq a, Num int) => a -> [a] -> u (Maybe int)

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, SymEq a, Num int) => a -> [a] -> u [int]

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, SymBranching u, Mergeable int, SymEq a, Num int) => (a -> SymBool) -> [a] -> u (Maybe int)

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 :: forall u a int. (Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) => (a -> SymBool) -> [a] -> u [int]

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, SymBranching u, Mergeable a, SymEq a) => [a] -> u [a]

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, SymBranching u, Mergeable a, SymEq a) => a -> [a] -> u [a]

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, SymEq a) => [a] -> [a] -> u [a]

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, SymEq a) => [a] -> [a] -> u [a]

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, SymEq a) => [a] -> [a] -> u [a]

Symbolic version of intersect, the result would be merged and propagate the mergeable knowledge.

Can generate O(len(rhs)) cases, and O(len(lhs) * len(rhs)) constraints.

Ordered lists (sorting not supported yet)

mrgInsert :: (MonadUnion m, Mergeable a, SymOrd a) => a -> [a] -> m [a]

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 SymEq context)

mrgNubBy :: forall a u. (Applicative u, SymBranching u, Mergeable a) => (a -> a -> SymBool) -> [a] -> u [a]

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, SymBranching u, Mergeable a) => (a -> a -> SymBool) -> a -> [a] -> u [a]

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]

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]

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]

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]]

This function can be very inefficient on large symbolic lists and generate O(2^n) cases. Use with caution.

User-supplied comparison (replacing an SymOrd context)

mrgInsertBy :: (MonadUnion m, Mergeable a) => (a -> a -> Union Ordering) -> a -> [a] -> m [a]

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 -> Union Ordering) -> t a -> m a

maximumBy with MergingStrategy knowledge propagation.

symMaximumBy :: forall t a. (Foldable t, Mergeable a, ITEOp a) => (a -> a -> Union Ordering) -> t a -> a

maximumBy with result merged with ITEOp.

mrgMinimumBy :: forall t a m. (Foldable t, Mergeable a, MonadUnion m) => (a -> a -> Union Ordering) -> t a -> m a

minimumBy with MergingStrategy knowledge propagation.

symMinimumBy :: forall t a. (Foldable t, Mergeable a, ITEOp a) => (a -> a -> Union Ordering) -> t a -> a

minimumBy with result merged with ITEOp.