{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- |
-- Module      :   Grisette.Lib.Data.List
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Lib.Data.List
  ( -- * Special folds
    symAnd,
    symOr,
    symAny,
    symAll,
    mrgMaximum,
    symMaximum,
    mrgMinimum,
    symMinimum,

    -- * Sublists

    -- ** Extracting sublists
    mrgTake,
    mrgDrop,
    mrgSplitAt,
    mrgTakeWhile,
    mrgDropWhile,
    mrgDropWhileEnd,
    mrgSpan,
    mrgBreak,
    mrgStripPrefix,
    mrgGroup,

    -- ** Predicates
    symIsPrefixOf,
    symIsSuffixOf,
    symIsInfixOf,
    symIsSubsequenceOf,

    -- * Searching lists

    -- ** Searching by equality
    symElem,
    symNotElem,
    mrgLookup,

    -- ** Searching with a predicate
    mrgFind,
    mrgFilter,
    mrgPartition,

    -- * Indexing lists
    (.!?),
    mrgElemIndex,
    mrgElemIndices,
    mrgFindIndex,
    mrgFindIndices,

    -- * Special lists

    -- ** "Set" operations
    mrgNub,
    mrgDelete,
    (.\\),
    mrgUnion,
    mrgIntersect,

    -- ** Ordered lists (sorting not supported yet)
    mrgInsert,

    -- * Generalized functions

    -- ** The "By" operations

    -- *** User-supplied equality (replacing an 'SymEq' context)
    mrgNubBy,
    mrgDeleteBy,
    mrgDeleteFirstsBy,
    mrgUnionBy,
    mrgIntersectBy,
    mrgGroupBy,

    -- *** User-supplied comparison (replacing an 'SymOrd' context)
    mrgInsertBy,
    mrgMaximumBy,
    symMaximumBy,
    mrgMinimumBy,
    symMinimumBy,
  )
where

import Data.Bifunctor (Bifunctor (first, second))
import Data.List (tails)
import Data.Maybe (listToMaybe)
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Control.Monad.Union (Union, liftUnion)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&), (.||)))
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.SimpleMergeable (SymBranching, mrgIf)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((./=), (.==)))
import Grisette.Internal.Core.Data.Class.SymOrd (SymOrd ((.<=), (.>=)))
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Lib.Control.Applicative (mrgPure)
import Grisette.Lib.Control.Monad (mrgReturn)
import Grisette.Lib.Data.Foldable
  ( mrgFind,
    mrgFoldlM,
    mrgMaximum,
    mrgMaximumBy,
    mrgMinimum,
    mrgMinimumBy,
    symAll,
    symAnd,
    symAny,
    symElem,
    symMaximum,
    symMaximumBy,
    symMinimum,
    symMinimumBy,
    symNotElem,
    symOr,
  )
import Grisette.Lib.Data.Functor (mrgFmap)

symListOpOnSymInt ::
  (Applicative u, SymBranching u, Mergeable b, Num int, SymOrd int) =>
  Bool ->
  (Int -> [a] -> b) ->
  int ->
  [a] ->
  u b
symListOpOnSymInt :: forall (u :: * -> *) b int a.
(Applicative u, SymBranching u, Mergeable b, Num int,
 SymOrd int) =>
Bool -> (Int -> [a] -> b) -> int -> [a] -> u b
symListOpOnSymInt Bool
reversed Int -> [a] -> b
f int
x [a]
vs = do
  let zipped :: [(int, u b)]
zipped =
        (\Int
n -> (Int -> int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n, b -> u b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (b -> u b) -> b -> u b
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> b
f Int
n [a]
vs))
          (Int -> (int, u b)) -> [Int] -> [(int, u b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (if Bool
reversed then [Int] -> [Int]
forall a. [a] -> [a]
reverse else [Int] -> [Int]
forall a. a -> a
id) [Int
1 .. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
vs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
  let outerMostX :: Int
outerMostX = if Bool
reversed then [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
vs else Int
0
  let innerMostX :: Int
innerMostX = if Bool
reversed then Int
0 else [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
vs
  let guardCond :: SymBool
guardCond =
        if Bool
reversed then (int
x int -> int -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= Int -> int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
vs)) else (int
x int -> int -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= int
0)
  SymBool -> u b -> u b -> u b
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
guardCond (b -> u b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (b -> u b) -> b -> u b
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> b
f Int
outerMostX [a]
vs) (u b -> u b) -> u b -> u b
forall a b. (a -> b) -> a -> b
$
    ((int, u b) -> u b -> u b) -> u b -> [(int, u b)] -> u b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
      (\(int
n, u b
l) u b
acc -> SymBool -> u b -> u b -> u b
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (int
x int -> int -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== int
n) u b
l u b
acc)
      (b -> u b
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (b -> u b) -> b -> u b
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> b
f Int
innerMostX [a]
vs)
      [(int, u b)]
zipped

-- | Symbolic version of 'Data.List.take', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(n) cases and O(n) sized branch constraints.
mrgTake ::
  (Applicative u, SymBranching u, Mergeable a, Num int, SymOrd int) =>
  int ->
  [a] ->
  u [a]
mrgTake :: forall (u :: * -> *) a int.
(Applicative u, SymBranching u, Mergeable a, Num int,
 SymOrd int) =>
int -> [a] -> u [a]
mrgTake = Bool -> (Int -> [a] -> [a]) -> int -> [a] -> u [a]
forall (u :: * -> *) b int a.
(Applicative u, SymBranching u, Mergeable b, Num int,
 SymOrd int) =>
Bool -> (Int -> [a] -> b) -> int -> [a] -> u b
symListOpOnSymInt Bool
False Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take

-- | Symbolic version of 'Data.List.drop', 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]
mrgDrop :: forall (u :: * -> *) a int.
(Applicative u, SymBranching u, Mergeable a, Num int,
 SymOrd int) =>
int -> [a] -> u [a]
mrgDrop = Bool -> (Int -> [a] -> [a]) -> int -> [a] -> u [a]
forall (u :: * -> *) b int a.
(Applicative u, SymBranching u, Mergeable b, Num int,
 SymOrd int) =>
Bool -> (Int -> [a] -> b) -> int -> [a] -> u b
symListOpOnSymInt Bool
True Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop

-- | Symbolic version of 'Data.List.splitAt', 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])
mrgSplitAt :: forall a int (u :: * -> *).
(MonadUnion u, Mergeable a, Num int, SymOrd int) =>
int -> [a] -> u ([a], [a])
mrgSplitAt = Bool -> (Int -> [a] -> ([a], [a])) -> int -> [a] -> u ([a], [a])
forall (u :: * -> *) b int a.
(Applicative u, SymBranching u, Mergeable b, Num int,
 SymOrd int) =>
Bool -> (Int -> [a] -> b) -> int -> [a] -> u b
symListOpOnSymInt Bool
False Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt

-- | Symbolic version of 'Data.List.takeWhile', 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]
mrgTakeWhile :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgTakeWhile a -> SymBool
_ [] = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgTakeWhile a -> SymBool
p (a
x : [a]
xs) =
  SymBool -> u [a] -> u [a] -> u [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a -> SymBool
p a
x) (([a] -> [a]) -> u [a] -> u [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (u [a] -> u [a]) -> u [a] -> u [a]
forall a b. (a -> b) -> a -> b
$ (a -> SymBool) -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgTakeWhile a -> SymBool
p [a]
xs) ([a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [])

-- | Symbolic version of 'Data.List.dropWhile', 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]
mrgDropWhile :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgDropWhile a -> SymBool
_ [] = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgDropWhile a -> SymBool
p [a]
r = do
  let allConds :: [SymBool]
allConds = [SymBool] -> [SymBool]
forall a. [a] -> [a]
reverse ([SymBool] -> [SymBool]) -> [SymBool] -> [SymBool]
forall a b. (a -> b) -> a -> b
$ (SymBool -> SymBool -> SymBool) -> [SymBool] -> [SymBool]
forall a. (a -> a -> a) -> [a] -> [a]
scanl1 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
(.&&) ([SymBool] -> [SymBool]) -> [SymBool] -> [SymBool]
forall a b. (a -> b) -> a -> b
$ a -> SymBool
p (a -> SymBool) -> [a] -> [SymBool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
r
  ((SymBool, [a]) -> u [a] -> u [a])
-> u [a] -> [(SymBool, [a])] -> u [a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(SymBool
cond, [a]
l) u [a]
acc -> SymBool -> u [a] -> u [a] -> u [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf SymBool
cond ([a] -> u [a]
forall a. a -> u a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
l) u [a]
acc) ([a] -> u [a]
forall a. a -> u a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
r) ([(SymBool, [a])] -> u [a]) -> [(SymBool, [a])] -> u [a]
forall a b. (a -> b) -> a -> b
$
    [SymBool] -> [[a]] -> [(SymBool, [a])]
forall a b. [a] -> [b] -> [(a, b)]
zip [SymBool]
allConds ([[a]] -> [(SymBool, [a])]) -> [[a]] -> [(SymBool, [a])]
forall a b. (a -> b) -> a -> b
$
      [[a]] -> [[a]]
forall a. [a] -> [a]
reverse ([[a]] -> [[a]]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> a -> b
$
        [a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
r

-- | Symbolic version of 'Data.List.dropWhileEnd', 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]
mrgDropWhileEnd :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgDropWhileEnd a -> SymBool
p =
  (a -> u [a] -> u [a]) -> u [a] -> [a] -> u [a]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    ( \a
x u [a]
xs -> do
        xsv <- u [a]
xs
        mrgIf (p x .&& con (null xsv)) (mrgPure []) (mrgPure $ x : xsv)
    )
    ([a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [])

-- | Symbolic version of 'Data.List.span', 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])
mrgSpan :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgSpan a -> SymBool
_ [] = ([a], [a]) -> u ([a], [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ([], [])
mrgSpan a -> SymBool
p xs :: [a]
xs@(a
x : [a]
xs') =
  SymBool -> u ([a], [a]) -> u ([a], [a]) -> u ([a], [a])
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a -> SymBool
p a
x) ((([a], [a]) -> ([a], [a])) -> u ([a], [a]) -> u ([a], [a])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) (u ([a], [a]) -> u ([a], [a])) -> u ([a], [a]) -> u ([a], [a])
forall a b. (a -> b) -> a -> b
$ (a -> SymBool) -> [a] -> u ([a], [a])
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgSpan a -> SymBool
p [a]
xs') (([a], [a]) -> u ([a], [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ([], [a]
xs))

-- | Symbolic version of 'Data.List.break', 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])
mrgBreak :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgBreak a -> SymBool
p = (a -> SymBool) -> [a] -> u ([a], [a])
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgSpan (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (SymBool -> SymBool) -> (a -> SymBool) -> a -> SymBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SymBool
p)

-- | Symbolic version of 'Data.List.stripPrefix', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Generate O(1) cases and O(len(prefix)) sized branch constraints.
mrgStripPrefix ::
  (Applicative u, SymBranching u, Mergeable a, SymEq a) =>
  [a] ->
  [a] ->
  u (Maybe [a])
mrgStripPrefix :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a, SymEq a) =>
[a] -> [a] -> u (Maybe [a])
mrgStripPrefix [] [a]
ys = Maybe [a] -> u (Maybe [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe [a] -> u (Maybe [a])) -> Maybe [a] -> u (Maybe [a])
forall a b. (a -> b) -> a -> b
$ [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
ys
mrgStripPrefix (a
x : [a]
xs) (a
y : [a]
ys) =
  SymBool -> u (Maybe [a]) -> u (Maybe [a]) -> u (Maybe [a])
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
y) ([a] -> [a] -> u (Maybe [a])
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a, SymEq a) =>
[a] -> [a] -> u (Maybe [a])
mrgStripPrefix [a]
xs [a]
ys) (Maybe [a] -> u (Maybe [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe [a]
forall a. Maybe a
Nothing)
mrgStripPrefix [a]
_ [a]
_ = Maybe [a] -> u (Maybe [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe [a]
forall a. Maybe a
Nothing

-- | Symbolic version of 'Data.List.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.
mrgGroup ::
  (MonadUnion u, Mergeable a, SymEq a) =>
  [a] ->
  u [[a]]
mrgGroup :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a, SymEq a) =>
[a] -> u [[a]]
mrgGroup = (a -> a -> SymBool) -> [a] -> u [[a]]
forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> u [[a]]
mrgGroupBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.isPrefixOf'.
--
-- Generate O(len(prefix)) sized constraints.
symIsPrefixOf :: (SymEq a) => [a] -> [a] -> SymBool
symIsPrefixOf :: forall a. SymEq a => [a] -> [a] -> SymBool
symIsPrefixOf [] [a]
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
symIsPrefixOf [a]
_ [] = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
symIsPrefixOf (a
x : [a]
xs) (a
y : [a]
ys) =
  a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
y SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& [a] -> [a] -> SymBool
forall a. SymEq a => [a] -> [a] -> SymBool
symIsPrefixOf [a]
xs [a]
ys

-- | Symbolic version of 'Data.List.isSuffixOf'.
--
-- Generate O(len(suffix)) sized constraints.
symIsSuffixOf :: (SymEq a) => [a] -> [a] -> SymBool
symIsSuffixOf :: forall a. SymEq a => [a] -> [a] -> SymBool
symIsSuffixOf [a]
ns [a]
hs = [a] -> [a] -> SymBool
forall a. SymEq a => [a] -> [a] -> SymBool
symIsPrefixOf ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ns) ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
hs)

-- | Symbolic version of 'Data.List.isInfixOf'.
--
-- Generate O(len(haystack) * len(needle)) sized constraints.
symIsInfixOf :: (SymEq a) => [a] -> [a] -> SymBool
symIsInfixOf :: forall a. SymEq a => [a] -> [a] -> SymBool
symIsInfixOf [a]
needle [a]
haystack = ([a] -> SymBool) -> [[a]] -> SymBool
forall (t :: * -> *) a.
Foldable t =>
(a -> SymBool) -> t a -> SymBool
symAny ([a] -> [a] -> SymBool
forall a. SymEq a => [a] -> [a] -> SymBool
symIsPrefixOf [a]
needle) ([a] -> [[a]]
forall a. [a] -> [[a]]
tails [a]
haystack)

-- | Symbolic version of 'Data.List.isSubsequenceOf'.
--
-- Generate O(len(haystack) * len(needle)) sized constraints.
symIsSubsequenceOf :: (SymEq a) => [a] -> [a] -> SymBool
symIsSubsequenceOf :: forall a. SymEq a => [a] -> [a] -> SymBool
symIsSubsequenceOf [] [a]
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
symIsSubsequenceOf [a]
_ [] = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
symIsSubsequenceOf a :: [a]
a@(a
x : [a]
a') (a
y : [a]
b) =
  SymBool -> SymBool -> SymBool -> SymBool
forall v. ITEOp v => SymBool -> v -> v -> v
symIte (a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
y) ([a] -> [a] -> SymBool
forall a. SymEq a => [a] -> [a] -> SymBool
symIsSubsequenceOf [a]
a' [a]
b) ([a] -> [a] -> SymBool
forall a. SymEq a => [a] -> [a] -> SymBool
symIsSubsequenceOf [a]
a [a]
b)

-- | Symbolic version of 'Data.List.lookup', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(n) cases and O(n) sized branch constraints.
mrgLookup ::
  forall a b u.
  (Applicative u, SymBranching u, Mergeable b, SymEq a) =>
  a ->
  [(a, b)] ->
  u (Maybe b)
mrgLookup :: forall a b (u :: * -> *).
(Applicative u, SymBranching u, Mergeable b, SymEq a) =>
a -> [(a, b)] -> u (Maybe b)
mrgLookup a
_ [] = Maybe b -> u (Maybe b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe b
forall a. Maybe a
Nothing
mrgLookup a
key [(a, b)]
l =
  SymBool -> u (Maybe b) -> u (Maybe b) -> u (Maybe b)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf ((a -> SymBool) -> [a] -> SymBool
forall (t :: * -> *) a.
Foldable t =>
(a -> SymBool) -> t a -> SymBool
symAll (a
key a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
./=) ((a, b) -> a
forall a b. (a, b) -> a
fst ((a, b) -> a) -> [(a, b)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, b)]
l)) (Maybe b -> u (Maybe b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure Maybe b
forall a. Maybe a
Nothing) (u (Maybe b) -> u (Maybe b)) -> u (Maybe b) -> u (Maybe b)
forall a b. (a -> b) -> a -> b
$
    [(a, b)] -> u (Maybe b)
mrgLookup' [(a, b)]
l
  where
    mrgLookup' :: [(a, b)] -> u (Maybe b)
    mrgLookup' :: [(a, b)] -> u (Maybe b)
mrgLookup' [] = [Char] -> u (Maybe b)
forall a. HasCallStack => [Char] -> a
error [Char]
"mrgLookup: impossible"
    mrgLookup' [(a
_, b
y)] = Maybe b -> u (Maybe b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe b -> u (Maybe b)) -> Maybe b -> u (Maybe b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. a -> Maybe a
Just b
y
    mrgLookup' ((a
x, b
y) : [(a, b)]
xys) =
      SymBool -> u (Maybe b) -> u (Maybe b) -> u (Maybe b)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
key a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
x) (Maybe b -> u (Maybe b)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure (Maybe b -> u (Maybe b)) -> Maybe b -> u (Maybe b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. a -> Maybe a
Just b
y) ([(a, b)] -> u (Maybe b)
mrgLookup' [(a, b)]
xys)

-- | Symbolic version of 'Data.List.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.
mrgFilter ::
  (Applicative u, SymBranching u, Mergeable a) =>
  (a -> SymBool) ->
  [a] ->
  u [a]
mrgFilter :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgFilter a -> SymBool
_ [] = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgFilter a -> SymBool
p (a
x : [a]
xs) =
  SymBool -> u [a] -> u [a] -> u [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a -> SymBool
p a
x) (([a] -> [a]) -> u [a] -> u [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (u [a] -> u [a]) -> u [a] -> u [a]
forall a b. (a -> b) -> a -> b
$ (a -> SymBool) -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgFilter a -> SymBool
p [a]
xs) ((a -> SymBool) -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u [a]
mrgFilter a -> SymBool
p [a]
xs)

-- | Symbolic version of 'Data.List.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.
mrgPartition ::
  forall u a.
  (Applicative u, SymBranching u, Mergeable a) =>
  (a -> SymBool) ->
  [a] ->
  u ([a], [a])
mrgPartition :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgPartition a -> SymBool
_ [] = ([a], [a]) -> u ([a], [a])
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure ([], [])
mrgPartition a -> SymBool
p (a
x : [a]
xs) =
  SymBool -> u ([a], [a]) -> u ([a], [a]) -> u ([a], [a])
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
    (a -> SymBool
p a
x)
    ((([a], [a]) -> ([a], [a])) -> u ([a], [a]) -> u ([a], [a])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) u ([a], [a])
partitioned)
    ((([a], [a]) -> ([a], [a])) -> u ([a], [a]) -> u ([a], [a])
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) u ([a], [a])
partitioned)
  where
    partitioned :: u ([a], [a])
    partitioned :: u ([a], [a])
partitioned = (a -> SymBool) -> [a] -> u ([a], [a])
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgPartition a -> SymBool
p [a]
xs

-- | Symbolic version of 'Data.List.!?', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(1) cases and O(n) sized branch constraints.
(.!?) ::
  forall a uf int.
  ( MonadUnion uf,
    Mergeable a,
    Num int,
    SymEq int
  ) =>
  [a] ->
  int ->
  uf (Maybe a)
[a]
l .!? :: forall a (uf :: * -> *) int.
(MonadUnion uf, Mergeable a, Num int, SymEq int) =>
[a] -> int -> uf (Maybe a)
.!? int
p = [a] -> int -> int -> uf (Maybe a)
go [a]
l int
p int
0
  where
    go :: [a] -> int -> int -> uf (Maybe a)
    go :: [a] -> int -> int -> uf (Maybe a)
go [] int
_ int
_ = Maybe a -> uf (Maybe a)
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn Maybe a
forall a. Maybe a
Nothing
    go (a
x : [a]
xs) int
p1 int
i = SymBool -> uf (Maybe a) -> uf (Maybe a) -> uf (Maybe a)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (int
p1 int -> int -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== int
i) (Maybe a -> uf (Maybe a)
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn (Maybe a -> uf (Maybe a)) -> Maybe a -> uf (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
x) ([a] -> int -> int -> uf (Maybe a)
go [a]
xs int
p1 (int -> uf (Maybe a)) -> int -> uf (Maybe a)
forall a b. (a -> b) -> a -> b
$ int
i int -> int -> int
forall a. Num a => a -> a -> a
+ int
1)

-- | Symbolic version of 'Data.List.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.
mrgElemIndex ::
  (MonadUnion u, Mergeable int, SymEq a, Num int) =>
  a ->
  [a] ->
  u (Maybe int)
mrgElemIndex :: forall (u :: * -> *) int a.
(MonadUnion u, Mergeable int, SymEq a, Num int) =>
a -> [a] -> u (Maybe int)
mrgElemIndex a
x = (a -> SymBool) -> [a] -> u (Maybe int)
forall (u :: * -> *) int a.
(Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
(a -> SymBool) -> [a] -> u (Maybe int)
mrgFindIndex (a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.==)

-- | Symbolic version of 'Data.List.elemIndices', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(n) cases, and O(n^3) sized constraints.
mrgElemIndices ::
  (MonadUnion u, Mergeable int, SymEq a, Num int) =>
  a ->
  [a] ->
  u [int]
mrgElemIndices :: forall (u :: * -> *) int a.
(MonadUnion u, Mergeable int, SymEq a, Num int) =>
a -> [a] -> u [int]
mrgElemIndices a
x = (a -> SymBool) -> [a] -> u [int]
forall (u :: * -> *) a int.
(Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
(a -> SymBool) -> [a] -> u [int]
mrgFindIndices (a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.==)

-- | Symbolic version of 'Data.List.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.
mrgFindIndex ::
  (Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
  (a -> SymBool) ->
  [a] ->
  u (Maybe int)
mrgFindIndex :: forall (u :: * -> *) int a.
(Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
(a -> SymBool) -> [a] -> u (Maybe int)
mrgFindIndex a -> SymBool
p [a]
l = ([int] -> Maybe int) -> u [int] -> u (Maybe int)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap [int] -> Maybe int
forall a. [a] -> Maybe a
listToMaybe (u [int] -> u (Maybe int)) -> u [int] -> u (Maybe int)
forall a b. (a -> b) -> a -> b
$ (a -> SymBool) -> [a] -> u [int]
forall (u :: * -> *) a int.
(Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
(a -> SymBool) -> [a] -> u [int]
mrgFindIndices a -> SymBool
p [a]
l

-- | Symbolic version of 'Data.List.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.
mrgFindIndices ::
  forall u a int.
  (Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
  (a -> SymBool) ->
  [a] ->
  u [int]
mrgFindIndices :: forall (u :: * -> *) a int.
(Applicative u, SymBranching u, Mergeable int, SymEq a, Num int) =>
(a -> SymBool) -> [a] -> u [int]
mrgFindIndices a -> SymBool
p [a]
xs = [(a, int)] -> u [int]
go ([(a, int)] -> u [int]) -> [(a, int)] -> u [int]
forall a b. (a -> b) -> a -> b
$ [a] -> [int] -> [(a, int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs ([int] -> [(a, int)]) -> [int] -> [(a, int)]
forall a b. (a -> b) -> a -> b
$ Integer -> int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> int) -> [Integer] -> [int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 ..]
  where
    go :: [(a, int)] -> u [int]
    go :: [(a, int)] -> u [int]
go [] = [int] -> u [int]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
    go ((a
x, int
y) : [(a, int)]
xys) = SymBool -> u [int] -> u [int] -> u [int]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a -> SymBool
p a
x) (([int] -> [int]) -> u [int] -> u [int]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (int
y int -> [int] -> [int]
forall a. a -> [a] -> [a]
:) (u [int] -> u [int]) -> u [int] -> u [int]
forall a b. (a -> b) -> a -> b
$ [(a, int)] -> u [int]
go [(a, int)]
xys) ([(a, int)] -> u [int]
go [(a, int)]
xys)

-- | Symbolic version of 'Data.List.nub', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(n) cases, and O(n^3) sized constraints.
mrgNub ::
  (Applicative u, SymBranching u, Mergeable a, SymEq a) =>
  [a] ->
  u [a]
mrgNub :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a, SymEq a) =>
[a] -> u [a]
mrgNub = (a -> a -> SymBool) -> [a] -> u [a]
forall a (u :: * -> *).
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> u [a]
mrgNubBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.delete', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(n) cases, and O(n^2) sized constraints.
mrgDelete ::
  (Applicative u, SymBranching u, Mergeable a, SymEq a) =>
  a ->
  [a] ->
  u [a]
mrgDelete :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a, SymEq a) =>
a -> [a] -> u [a]
mrgDelete = (a -> a -> SymBool) -> a -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> a -> [a] -> u [a]
mrgDeleteBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.\\', 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.
(.\\) ::
  (MonadUnion u, Mergeable a, SymEq a) =>
  [a] ->
  [a] ->
  u [a]
.\\ :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a, SymEq a) =>
[a] -> [a] -> u [a]
(.\\) = (a -> a -> SymBool) -> [a] -> [a] -> u [a]
forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgDeleteFirstsBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.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.
mrgUnion ::
  (MonadUnion u, Mergeable a, SymEq a) =>
  [a] ->
  [a] ->
  u [a]
mrgUnion :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a, SymEq a) =>
[a] -> [a] -> u [a]
mrgUnion = (a -> a -> SymBool) -> [a] -> [a] -> u [a]
forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgUnionBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.intersect', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate O(len(rhs)) cases, and O(len(lhs) * len(rhs)) constraints.
mrgIntersect ::
  (MonadUnion u, Mergeable a, SymEq a) =>
  [a] ->
  [a] ->
  u [a]
mrgIntersect :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a, SymEq a) =>
[a] -> [a] -> u [a]
mrgIntersect = (a -> a -> SymBool) -> [a] -> [a] -> u [a]
forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgIntersectBy a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
(.==)

-- | Symbolic version of 'Data.List.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.
mrgNubBy ::
  forall a u.
  (Applicative u, SymBranching u, Mergeable a) =>
  (a -> a -> SymBool) ->
  [a] ->
  u [a]
mrgNubBy :: forall a (u :: * -> *).
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> u [a]
mrgNubBy a -> a -> SymBool
eq [a]
l = [a] -> [a] -> u [a]
mrgNubBy' [a]
l []
  where
    mrgNubBy' :: [a] -> [a] -> u [a]
    mrgNubBy' :: [a] -> [a] -> u [a]
mrgNubBy' [] [a]
_ = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
    mrgNubBy' (a
y : [a]
ys) [a]
xs =
      SymBool -> u [a] -> u [a] -> u [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
        (a -> [a] -> SymBool
mrgElemBy a
y [a]
xs)
        ([a] -> [a] -> u [a]
mrgNubBy' [a]
ys [a]
xs)
        (([a] -> [a]) -> u [a] -> u [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (u [a] -> u [a]) -> u [a] -> u [a]
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> u [a]
mrgNubBy' [a]
ys (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs))
    mrgElemBy :: a -> [a] -> SymBool
mrgElemBy a
_ [] = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
    mrgElemBy a
x (a
y : [a]
ys) = a -> a -> SymBool
eq a
x a
y SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a -> [a] -> SymBool
mrgElemBy a
x [a]
ys

-- | Symbolic version of 'Data.List.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.
mrgDeleteBy ::
  (Applicative u, SymBranching u, Mergeable a) =>
  (a -> a -> SymBool) ->
  a ->
  [a] ->
  u [a]
mrgDeleteBy :: forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> a -> [a] -> u [a]
mrgDeleteBy a -> a -> SymBool
_ a
_ [] = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgDeleteBy a -> a -> SymBool
eq a
x (a
y : [a]
ys) =
  SymBool -> u [a] -> u [a] -> u [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a -> a -> SymBool
eq a
x a
y) ([a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [a]
ys) (([a] -> [a]) -> u [a] -> u [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (u [a] -> u [a]) -> u [a] -> u [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> SymBool) -> a -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> a -> [a] -> u [a]
mrgDeleteBy a -> a -> SymBool
eq a
x [a]
ys)

-- | Symbolic version of 'Data.List.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.
mrgDeleteFirstsBy ::
  (MonadUnion u, Mergeable a) =>
  (a -> a -> SymBool) ->
  [a] ->
  [a] ->
  u [a]
mrgDeleteFirstsBy :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgDeleteFirstsBy a -> a -> SymBool
eq = ([a] -> a -> u [a]) -> [a] -> [a] -> u [a]
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM ((a -> [a] -> u [a]) -> [a] -> a -> u [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> [a] -> u [a]) -> [a] -> a -> u [a])
-> (a -> [a] -> u [a]) -> [a] -> a -> u [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> SymBool) -> a -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> a -> [a] -> u [a]
mrgDeleteBy a -> a -> SymBool
eq)

-- | Symbolic version of 'Data.List.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.
mrgUnionBy ::
  (MonadUnion u, Mergeable a) =>
  (a -> a -> SymBool) ->
  [a] ->
  [a] ->
  u [a]
mrgUnionBy :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgUnionBy a -> a -> SymBool
eq [a]
xs [a]
ys =
  ([a] -> [a]) -> u [a] -> u [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++) (u [a] -> u [a]) -> u [a] -> u [a]
forall a b. (a -> b) -> a -> b
$
    ((a -> a -> SymBool) -> [a] -> u [a]
forall a (u :: * -> *).
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> u [a]
mrgNubBy a -> a -> SymBool
eq [a]
ys)
      u [a] -> ([a] -> u [a]) -> u [a]
forall a b. u a -> (a -> u b) -> u b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[a]
nubbed -> ([a] -> a -> u [a]) -> [a] -> [a] -> u [a]
forall (m :: * -> *) b (t :: * -> *) a.
(MonadTryMerge m, Mergeable b, Foldable t) =>
(b -> a -> m b) -> b -> t a -> m b
mrgFoldlM ((a -> [a] -> u [a]) -> [a] -> a -> u [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> [a] -> u [a]) -> [a] -> a -> u [a])
-> (a -> [a] -> u [a]) -> [a] -> a -> u [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> SymBool) -> a -> [a] -> u [a]
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> a -> SymBool) -> a -> [a] -> u [a]
mrgDeleteBy a -> a -> SymBool
eq) [a]
nubbed [a]
xs

-- | Symbolic version of 'Data.List.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.
mrgIntersectBy ::
  (MonadUnion u, Mergeable a) =>
  (a -> a -> SymBool) ->
  [a] ->
  [a] ->
  u [a]
mrgIntersectBy :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgIntersectBy a -> a -> SymBool
_ [] [a]
_ = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgIntersectBy a -> a -> SymBool
_ [a]
_ [] = [a] -> u [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgIntersectBy a -> a -> SymBool
eq [a]
xs [a]
ys = do
  tl <- (a -> a -> SymBool) -> [a] -> [a] -> u [a]
forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> [a] -> u [a]
mrgIntersectBy a -> a -> SymBool
eq ([a] -> [a]
forall a. HasCallStack => [a] -> [a]
tail [a]
xs) [a]
ys
  mrgIf (symAny (eq (head xs)) ys) (mrgReturn $ head xs : tl) (mrgPure tl)

-- | This function can be very inefficient on large symbolic lists and generate
-- O(2^n) cases. Use with caution.
mrgGroupBy ::
  (MonadUnion u, Mergeable a) =>
  (a -> a -> SymBool) ->
  [a] ->
  u [[a]]
mrgGroupBy :: forall (u :: * -> *) a.
(MonadUnion u, Mergeable a) =>
(a -> a -> SymBool) -> [a] -> u [[a]]
mrgGroupBy a -> a -> SymBool
_ [] = [[a]] -> u [[a]]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure []
mrgGroupBy a -> a -> SymBool
eq (a
x : [a]
xs) = do
  (ys, zs) <- (a -> SymBool) -> [a] -> u ([a], [a])
forall (u :: * -> *) a.
(Applicative u, SymBranching u, Mergeable a) =>
(a -> SymBool) -> [a] -> u ([a], [a])
mrgSpan (a -> a -> SymBool
eq a
x) [a]
xs
  tl <- mrgGroupBy eq zs
  mrgReturn $ (x : ys) : tl

-- | Symbolic version of 'Data.List.insert', the result would be merged and
-- propagate the mergeable knowledge.
--
-- Can generate 1 case, and O(n^2) sized constraints.
mrgInsert ::
  (MonadUnion m, Mergeable a, SymOrd a) =>
  a ->
  [a] ->
  m [a]
mrgInsert :: forall (m :: * -> *) a.
(MonadUnion m, Mergeable a, SymOrd a) =>
a -> [a] -> m [a]
mrgInsert a
x [] = [a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [a
x]
mrgInsert a
x ys :: [a]
ys@(a
y : [a]
ys') =
  SymBool -> m [a] -> m [a] -> m [a]
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= a
y) ([a] -> m [a]
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys) (([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (m [a] -> m [a]) -> m [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ a -> [a] -> m [a]
forall (m :: * -> *) a.
(MonadUnion m, Mergeable a, SymOrd a) =>
a -> [a] -> m [a]
mrgInsert a
x [a]
ys')

-- | Symbolic version of 'Data.List.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.
mrgInsertBy ::
  (MonadUnion m, Mergeable a) =>
  (a -> a -> Union Ordering) ->
  a ->
  [a] ->
  m [a]
mrgInsertBy :: forall (m :: * -> *) a.
(MonadUnion m, Mergeable a) =>
(a -> a -> Union Ordering) -> a -> [a] -> m [a]
mrgInsertBy a -> a -> Union Ordering
_ a
x [] = [a] -> m [a]
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgPure [a
x]
mrgInsertBy a -> a -> Union Ordering
cmp a
x ys :: [a]
ys@(a
y : [a]
ys') = do
  r <- Union Ordering -> m Ordering
forall (u :: * -> *) a.
(Mergeable a, SymBranching u, Applicative u) =>
Union a -> u a
liftUnion (Union Ordering -> m Ordering) -> Union Ordering -> m Ordering
forall a b. (a -> b) -> a -> b
$ a -> a -> Union Ordering
cmp a
x a
y
  case r of
    Ordering
GT -> ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (m [a] -> m [a]) -> m [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ (a -> a -> Union Ordering) -> a -> [a] -> m [a]
forall (m :: * -> *) a.
(MonadUnion m, Mergeable a) =>
(a -> a -> Union Ordering) -> a -> [a] -> m [a]
mrgInsertBy a -> a -> Union Ordering
cmp a
x [a]
ys'
    Ordering
_ -> [a] -> m [a]
forall (u :: * -> *) a. (MonadTryMerge u, Mergeable a) => a -> u a
mrgReturn ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys