{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
-- 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.Internal.Internal.Decl.Core.Data.Class.Mergeable
  ( -- * Merging strategy
    MergingStrategy (..),

    -- * Mergeable
    Mergeable (..),
    Mergeable1 (..),
    rootStrategy1,
    Mergeable2 (..),
    rootStrategy2,
    Mergeable3 (..),
    rootStrategy3,

    -- * Generic 'Mergeable'
    MergeableArgs (..),
    GMergeable (..),
    genericRootStrategy,
    genericLiftRootStrategy,

    -- * Combinators for manually building merging strategies
    wrapStrategy,
    product2Strategy,
    DynamicSortedIdx (..),
    StrategyList (..),
    buildStrategyList,
    resolveStrategy,
    resolveStrategy',
    resolveMergeable1,
  )
where

import Data.Functor.Classes
  ( Eq1,
    Ord1,
    Show1,
    compare1,
    eq1,
    showsPrec1,
  )
import Data.Kind (Type)
import Data.Typeable
  ( Typeable,
    eqT,
    type (:~:) (Refl),
  )
import Generics.Deriving
  ( Default,
    Default1,
    Generic (Rep, from, to),
    Generic1 (Rep1, from1, to1),
    K1 (K1, unK1),
    M1 (M1, unM1),
    Par1 (Par1, unPar1),
    Rec1 (Rec1, unRec1),
    U1,
    V1,
    (:.:) (Comp1, unComp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.Utils.Derive (Arity0, Arity1)
import Unsafe.Coerce (unsafeCoerce)

-- | Merging strategies.
--
-- __You probably do not need to know the details of this type if you are only__
-- __going to use algebraic data types. You can get merging strategies for__
-- __them with type derivation.__
--
-- In Grisette, a merged union (if-then-else tree) follows the
-- __/hierarchical sorted representation invariant/__ with regards to some
-- merging strategy.
--
-- A merging strategy encodes how to merge a __/subset/__ of the values of a
-- given type. We have three types of merging strategies:
--
-- * Simple strategy
-- * Sorted strategy
-- * No strategy
--
-- The 'SimpleStrategy' merges values with a simple merge function.
-- For example,
--
--    * the symbolic boolean values can be directly merged with 'symIte'.
--
--    * the set @{1}@, which is a subset of the values of the type @Integer@,
--        can be simply merged as the set contains only a single value.
--
--    * all the 'Just' values of the type @Maybe SymBool@ can be simply merged
--        by merging the wrapped symbolic boolean with 'symIte'.
--
-- The 'SortedStrategy' merges values by first grouping the values with an
-- indexing function, and the values with the same index will be organized as
-- a sub-tree in the if-then-else structure of
-- 'Grisette.Core.Data.UnionBase.UnionBase'. Each group (sub-tree) will be
-- further merged with a sub-strategy for the index.
-- The index type should be a totally ordered type (with the 'Ord'
-- type class). Grisette will use the indexing function to partition the values
-- into sub-trees, and organize them in a sorted way. The sub-trees will further
-- be merged with the sub-strategies. For example,
--
--    * all the integers can be merged with 'SortedStrategy' by indexing with
--      the identity function and use the 'SimpleStrategy' shown before as the
--      sub-strategies.
--
--    * all the @Maybe SymBool@ values can be merged with 'SortedStrategy' by
--      indexing with 'Data.Maybe.isJust', the 'Nothing' and 'Just' values can
--      then be merged with different simple strategies as sub-strategies.
--
-- The 'NoStrategy' does not perform any merging.
-- For example, we cannot merge values with function types that returns concrete
-- lists.
--
-- For ADTs, we can automatically derive the 'Mergeable' type class, which
-- provides a merging strategy.
--
-- If the derived version does not work for you, you should determine
-- if your type can be directly merged with a merging function. If so, you can
-- implement the merging strategy as a 'SimpleStrategy'.
-- If the type cannot be directly merged with a merging function, but could be
-- partitioned into subsets of values that can be simply merged with a function,
-- you should implement the merging strategy as a 'SortedStrategy'.
-- For easier building of the merging strategies, check out the combinators
-- like `wrapStrategy`.
--
-- For more details, please see the documents of the constructors, or refer to
-- [Grisette's paper](https://lsrcz.github.io/files/POPL23.pdf).
data MergingStrategy a where
  -- | Simple mergeable strategy.
  --
  -- For symbolic booleans, we can implement its merge strategy as follows:
  --
  -- > SimpleStrategy symIte :: MergingStrategy SymBool
  SimpleStrategy ::
    -- | Merge function.
    (SymBool -> a -> a -> a) ->
    MergingStrategy a
  -- | Sorted mergeable strategy.
  --
  -- For Integers, we can implement its merge strategy as follows:
  --
  -- > SortedStrategy id (\_ -> SimpleStrategy $ \_ t _ -> t)
  --
  -- For @Maybe SymBool@, we can implement its merge strategy as follows:
  --
  -- > SortedStrategy
  -- >   (\case; Nothing -> False; Just _ -> True)
  -- >   (\idx ->
  -- >      if idx
  -- >        then SimpleStrategy $ \_ t _ -> t
  -- >        else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ symIte cond l r)
  SortedStrategy ::
    (Ord idx, Typeable idx, Show idx) =>
    -- | Indexing function
    (a -> idx) ->
    -- | Sub-strategy function
    (idx -> MergingStrategy a) ->
    MergingStrategy a
  -- | For preventing the merging intentionally. This could be
  -- useful for keeping some value concrete and may help generate more efficient
  -- formulas.
  --
  -- See [Grisette's paper](https://lsrcz.github.io/files/POPL23.pdf) for
  -- details.
  NoStrategy :: MergingStrategy a

-- | Each type is associated with a root merge strategy given by 'rootStrategy'.
-- The root merge strategy should be able to merge every value of the type.
-- Grisette will use the root merge strategy to merge the values of the type in
-- a union.
--
-- __Note 1:__ This type class can be derived for algebraic data types.
-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.
--
-- > data X = ... deriving Generic deriving Mergeable via (Default X)
class Mergeable a where
  -- | The root merging strategy for the type.
  rootStrategy :: MergingStrategy a

  sortIndices :: a -> [DynamicSortedIdx]
  sortIndices = ([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx]
forall a b. (a, b) -> a
fst (([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx])
-> (a -> ([DynamicSortedIdx], MergingStrategy a))
-> a
-> [DynamicSortedIdx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MergingStrategy a -> a -> ([DynamicSortedIdx], MergingStrategy a)
forall x.
MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy

-- | Lifting of the 'Mergeable' class to unary type constructors.
class
  (forall a. (Mergeable a) => Mergeable (u a)) =>
  Mergeable1 (u :: Type -> Type)
  where
  -- | Lift merge strategy through the type constructor.
  liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)

-- | Lift the root merge strategy through the unary type constructor.
rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)
rootStrategy1 :: forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1 = MergingStrategy a -> MergingStrategy (u a)
forall a. MergingStrategy a -> MergingStrategy (u a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE rootStrategy1 #-}

-- | Workaround as GHC prior to 9.6 doesn't support quantified constraints
-- reliably.
--
-- Similar to https://github.com/haskell/core-libraries-committee/issues/10,
-- which is only available with 9.6 or higher.
resolveMergeable1 ::
  forall f a r. (Mergeable1 f, Mergeable a) => ((Mergeable (f a)) => r) -> r
resolveMergeable1 :: forall (f :: * -> *) a r.
(Mergeable1 f, Mergeable a) =>
(Mergeable (f a) => r) -> r
resolveMergeable1 Mergeable (f a) => r
v = r
Mergeable (f a) => r
v

-- | Lifting of the 'Mergeable' class to binary type constructors.
class
  (forall a. (Mergeable a) => Mergeable1 (u a)) =>
  Mergeable2 (u :: Type -> Type -> Type)
  where
  -- | Lift merge strategy through the type constructor.
  liftRootStrategy2 ::
    MergingStrategy a ->
    MergingStrategy b ->
    MergingStrategy (u a b)

-- | Lift the root merge strategy through the binary type constructor.
rootStrategy2 ::
  (Mergeable a, Mergeable b, Mergeable2 u) =>
  MergingStrategy (u a b)
rootStrategy2 :: forall a b (u :: * -> * -> *).
(Mergeable a, Mergeable b, Mergeable2 u) =>
MergingStrategy (u a b)
rootStrategy2 = MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
forall (u :: * -> * -> *) a b.
Mergeable2 u =>
MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
liftRootStrategy2 MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy MergingStrategy b
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE rootStrategy2 #-}

-- | Lifting of the 'Mergeable' class to ternary type constructors.
class
  (forall a. (Mergeable a) => Mergeable2 (u a)) =>
  Mergeable3 (u :: Type -> Type -> Type -> Type)
  where
  -- | Lift merge strategy through the type constructor.
  liftRootStrategy3 ::
    MergingStrategy a ->
    MergingStrategy b ->
    MergingStrategy c ->
    MergingStrategy (u a b c)

-- | Lift the root merge strategy through the binary type constructor.
rootStrategy3 ::
  (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) =>
  MergingStrategy (u a b c)
rootStrategy3 :: forall a b c (u :: * -> * -> * -> *).
(Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) =>
MergingStrategy (u a b c)
rootStrategy3 = MergingStrategy a
-> MergingStrategy b
-> MergingStrategy c
-> MergingStrategy (u a b c)
forall a b c.
MergingStrategy a
-> MergingStrategy b
-> MergingStrategy c
-> MergingStrategy (u a b c)
forall (u :: * -> * -> * -> *) a b c.
Mergeable3 u =>
MergingStrategy a
-> MergingStrategy b
-> MergingStrategy c
-> MergingStrategy (u a b c)
liftRootStrategy3 MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy MergingStrategy b
forall a. Mergeable a => MergingStrategy a
rootStrategy MergingStrategy c
forall a. Mergeable a => MergingStrategy a
rootStrategy
{-# INLINE rootStrategy3 #-}

-- | Useful utility function for building merge strategies manually.
--
-- For example, to build the merge strategy for the just branch of @Maybe a@,
-- one could write
--
-- > wrapStrategy Just fromMaybe rootStrategy :: MergingStrategy (Maybe a)
wrapStrategy ::
  -- | The merge strategy to be wrapped
  MergingStrategy a ->
  -- | The wrap function
  (a -> b) ->
  -- | The unwrap function, which does not have to be defined for every value
  (b -> a) ->
  MergingStrategy b
wrapStrategy :: forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (SimpleStrategy SymBool -> a -> a -> a
m) a -> b
wrap b -> a
unwrap =
  (SymBool -> b -> b -> b) -> MergingStrategy b
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy
    ( \SymBool
cond b
ifTrue b
ifFalse ->
        a -> b
wrap (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ SymBool -> a -> a -> a
m SymBool
cond (b -> a
unwrap b
ifTrue) (b -> a
unwrap b
ifFalse)
    )
wrapStrategy (SortedStrategy a -> idx
idxFun idx -> MergingStrategy a
substrategy) a -> b
wrap b -> a
unwrap =
  (b -> idx) -> (idx -> MergingStrategy b) -> MergingStrategy b
forall a a.
(Ord a, Typeable a, Show a) =>
(a -> a) -> (a -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
    (a -> idx
idxFun (a -> idx) -> (b -> a) -> b -> idx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
unwrap)
    (\idx
idx -> MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (idx -> MergingStrategy a
substrategy idx
idx) a -> b
wrap b -> a
unwrap)
wrapStrategy MergingStrategy a
NoStrategy a -> b
_ b -> a
_ = MergingStrategy b
forall a. MergingStrategy a
NoStrategy
{-# INLINE wrapStrategy #-}

-- | Useful utility function for building merge strategies for product types
-- manually.
--
-- For example, to build the merge strategy for the following product type,
-- one could write
--
-- > data X = X { x1 :: Int, x2 :: Bool }
-- > product2Strategy X (\(X a b) -> (a, b)) rootStrategy rootStrategy
-- >   :: MergingStrategy X
product2Strategy ::
  -- | The wrap function
  (a -> b -> r) ->
  -- | The unwrap function, which does not have to be defined for every value
  (r -> (a, b)) ->
  -- | The first merge strategy to be wrapped
  MergingStrategy a ->
  -- | The second merge strategy to be wrapped
  MergingStrategy b ->
  MergingStrategy r
product2Strategy :: forall a b r.
(a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
product2Strategy a -> b -> r
wrap r -> (a, b)
unwrap MergingStrategy a
strategy1 MergingStrategy b
strategy2 =
  case (MergingStrategy a
strategy1, MergingStrategy b
strategy2) of
    (MergingStrategy a
NoStrategy, MergingStrategy b
_) -> MergingStrategy r
forall a. MergingStrategy a
NoStrategy
    (MergingStrategy a
_, MergingStrategy b
NoStrategy) -> MergingStrategy r
forall a. MergingStrategy a
NoStrategy
    (SimpleStrategy SymBool -> a -> a -> a
m1, SimpleStrategy SymBool -> b -> b -> b
m2) ->
      (SymBool -> r -> r -> r) -> MergingStrategy r
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> r -> r -> r) -> MergingStrategy r)
-> (SymBool -> r -> r -> r) -> MergingStrategy r
forall a b. (a -> b) -> a -> b
$ \SymBool
cond r
t r
f -> case (r -> (a, b)
unwrap r
t, r -> (a, b)
unwrap r
f) of
        ((a
hdt, b
tlt), (a
hdf, b
tlf)) ->
          a -> b -> r
wrap (SymBool -> a -> a -> a
m1 SymBool
cond a
hdt a
hdf) (SymBool -> b -> b -> b
m2 SymBool
cond b
tlt b
tlf)
    (s1 :: MergingStrategy a
s1@(SimpleStrategy SymBool -> a -> a -> a
_), SortedStrategy b -> idx
idxf idx -> MergingStrategy b
subf) ->
      (r -> idx) -> (idx -> MergingStrategy r) -> MergingStrategy r
forall a a.
(Ord a, Typeable a, Show a) =>
(a -> a) -> (a -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
        (b -> idx
idxf (b -> idx) -> (r -> b) -> r -> idx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> b
forall a b. (a, b) -> b
snd ((a, b) -> b) -> (r -> (a, b)) -> r -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> (a, b)
unwrap)
        ((a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
forall a b r.
(a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
product2Strategy a -> b -> r
wrap r -> (a, b)
unwrap MergingStrategy a
s1 (MergingStrategy b -> MergingStrategy r)
-> (idx -> MergingStrategy b) -> idx -> MergingStrategy r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. idx -> MergingStrategy b
subf)
    (SortedStrategy a -> idx
idxf idx -> MergingStrategy a
subf, MergingStrategy b
s2) ->
      (r -> idx) -> (idx -> MergingStrategy r) -> MergingStrategy r
forall a a.
(Ord a, Typeable a, Show a) =>
(a -> a) -> (a -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
        (a -> idx
idxf (a -> idx) -> (r -> a) -> r -> idx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst ((a, b) -> a) -> (r -> (a, b)) -> r -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> (a, b)
unwrap)
        (\idx
idx -> (a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
forall a b r.
(a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
product2Strategy a -> b -> r
wrap r -> (a, b)
unwrap (idx -> MergingStrategy a
subf idx
idx) MergingStrategy b
s2)
{-# INLINE product2Strategy #-}

-- Derivations

-- | The arguments to the generic merging strategy function.
data family MergeableArgs arity a :: Type

data instance MergeableArgs Arity0 _ = MergeableArgs0

newtype instance MergeableArgs Arity1 a = MergeableArgs1 (MergingStrategy a)

-- | The class of types that can be generically merged.
class GMergeable arity f where
  grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a)

instance GMergeable arity V1 where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy (V1 a)
grootStrategy MergeableArgs arity a
_ = (SymBool -> V1 a -> V1 a -> V1 a) -> MergingStrategy (V1 a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy (\SymBool
_ V1 a
t V1 a
_ -> V1 a
t)
  {-# INLINE grootStrategy #-}

instance GMergeable arity U1 where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy (U1 a)
grootStrategy MergeableArgs arity a
_ = (SymBool -> U1 a -> U1 a -> U1 a) -> MergingStrategy (U1 a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy (\SymBool
_ U1 a
t U1 a
_ -> U1 a
t)
  {-# INLINE grootStrategy #-}

instance
  (GMergeable arity a, GMergeable arity b) =>
  GMergeable arity (a :*: b)
  where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy ((:*:) a b a)
grootStrategy MergeableArgs arity a
args =
    (a a -> b a -> (:*:) a b a)
-> ((:*:) a b a -> (a a, b a))
-> MergingStrategy (a a)
-> MergingStrategy (b a)
-> MergingStrategy ((:*:) a b a)
forall a b r.
(a -> b -> r)
-> (r -> (a, b))
-> MergingStrategy a
-> MergingStrategy b
-> MergingStrategy r
product2Strategy
      a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
      (\(a a
a :*: b a
b) -> (a a
a, b a
b))
      (MergeableArgs arity a -> MergingStrategy (a a)
forall a. MergeableArgs arity a -> MergingStrategy (a a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs arity a
args)
      (MergeableArgs arity a -> MergingStrategy (b a)
forall a. MergeableArgs arity a -> MergingStrategy (b a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs arity a
args)
  {-# INLINE grootStrategy #-}

instance
  (GMergeable arity a, GMergeable arity b) =>
  GMergeable arity (a :+: b)
  where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy ((:+:) a b a)
grootStrategy MergeableArgs arity a
args =
    ((:+:) a b a -> Bool)
-> (Bool -> MergingStrategy ((:+:) a b a))
-> MergingStrategy ((:+:) a b a)
forall a a.
(Ord a, Typeable a, Show a) =>
(a -> a) -> (a -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
      ( \case
          L1 a a
_ -> Bool
False
          R1 b a
_ -> Bool
True
      )
      ( \Bool
idx ->
          if Bool -> Bool
not Bool
idx
            then
              MergingStrategy (a a)
-> (a a -> (:+:) a b a)
-> ((:+:) a b a -> a a)
-> MergingStrategy ((:+:) a b a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
                (MergeableArgs arity a -> MergingStrategy (a a)
forall a. MergeableArgs arity a -> MergingStrategy (a a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs arity a
args)
                a a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
                (\case (L1 a a
v) -> a a
v; (:+:) a b a
_ -> [Char] -> a a
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen")
            else
              MergingStrategy (b a)
-> (b a -> (:+:) a b a)
-> ((:+:) a b a -> b a)
-> MergingStrategy ((:+:) a b a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
                (MergeableArgs arity a -> MergingStrategy (b a)
forall a. MergeableArgs arity a -> MergingStrategy (b a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs arity a
args)
                b a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
                (\case (R1 b a
v) -> b a
v; (:+:) a b a
_ -> [Char] -> b a
forall a. HasCallStack => [Char] -> a
error [Char]
"Should not happen")
      )
  {-# INLINE grootStrategy #-}

instance (GMergeable arity a) => GMergeable arity (M1 i c a) where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy (M1 i c a a)
grootStrategy MergeableArgs arity a
arg = MergingStrategy (a a)
-> (a a -> M1 i c a a)
-> (M1 i c a a -> a a)
-> MergingStrategy (M1 i c a a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergeableArgs arity a -> MergingStrategy (a a)
forall a. MergeableArgs arity a -> MergingStrategy (a a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs arity a
arg) a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 M1 i c a a -> a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE grootStrategy #-}

instance (Mergeable c) => GMergeable arity (K1 i c) where
  grootStrategy :: forall a. MergeableArgs arity a -> MergingStrategy (K1 i c a)
grootStrategy MergeableArgs arity a
_ = MergingStrategy c
-> (c -> K1 i c a) -> (K1 i c a -> c) -> MergingStrategy (K1 i c a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy c
forall a. Mergeable a => MergingStrategy a
rootStrategy c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE grootStrategy #-}

instance GMergeable Arity1 Par1 where
  grootStrategy :: forall a. MergeableArgs Arity1 a -> MergingStrategy (Par1 a)
grootStrategy (MergeableArgs1 MergingStrategy a
strategy) = MergingStrategy a
-> (a -> Par1 a) -> (Par1 a -> a) -> MergingStrategy (Par1 a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy MergingStrategy a
strategy a -> Par1 a
forall p. p -> Par1 p
Par1 Par1 a -> a
forall p. Par1 p -> p
unPar1
  {-# INLINE grootStrategy #-}

instance (Mergeable1 f) => GMergeable Arity1 (Rec1 f) where
  grootStrategy :: forall a. MergeableArgs Arity1 a -> MergingStrategy (Rec1 f a)
grootStrategy (MergeableArgs1 MergingStrategy a
m) =
    MergingStrategy (f a)
-> (f a -> Rec1 f a)
-> (Rec1 f a -> f a)
-> MergingStrategy (Rec1 f a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergingStrategy a -> MergingStrategy (f a)
forall a. MergingStrategy a -> MergingStrategy (f a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy MergingStrategy a
m) f a -> Rec1 f a
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 Rec1 f a -> f a
forall k (f :: k -> *) (p :: k). Rec1 f p -> f p
unRec1
  {-# INLINE grootStrategy #-}

instance
  (Mergeable1 f, GMergeable Arity1 g) =>
  GMergeable Arity1 (f :.: g)
  where
  grootStrategy :: forall a. MergeableArgs Arity1 a -> MergingStrategy ((:.:) f g a)
grootStrategy MergeableArgs Arity1 a
targs =
    MergingStrategy (f (g a))
-> (f (g a) -> (:.:) f g a)
-> ((:.:) f g a -> f (g a))
-> MergingStrategy ((:.:) f g a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergingStrategy (g a) -> MergingStrategy (f (g a))
forall a. MergingStrategy a -> MergingStrategy (f a)
forall (u :: * -> *) a.
Mergeable1 u =>
MergingStrategy a -> MergingStrategy (u a)
liftRootStrategy (MergeableArgs Arity1 a -> MergingStrategy (g a)
forall a. MergeableArgs Arity1 a -> MergingStrategy (g a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs Arity1 a
targs)) f (g a) -> (:.:) f g a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (:.:) f g a -> f (g a)
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
(:.:) f g p -> f (g p)
unComp1
  {-# INLINE grootStrategy #-}

instance (Generic a, GMergeable Arity0 (Rep a)) => Mergeable (Default a) where
  rootStrategy :: MergingStrategy (Default a)
rootStrategy = MergingStrategy a -> MergingStrategy (Default a)
forall a b. a -> b
unsafeCoerce (MergingStrategy a
forall a.
(Generic a, GMergeable Arity0 (Rep a)) =>
MergingStrategy a
genericRootStrategy :: MergingStrategy a)
  {-# INLINE rootStrategy #-}

-- | Generic 'rootStrategy'.
genericRootStrategy ::
  (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a
genericRootStrategy :: forall a.
(Generic a, GMergeable Arity0 (Rep a)) =>
MergingStrategy a
genericRootStrategy = MergingStrategy (Rep a Any)
-> (Rep a Any -> a) -> (a -> Rep a Any) -> MergingStrategy a
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergeableArgs Arity0 Any -> MergingStrategy (Rep a Any)
forall a. MergeableArgs Arity0 a -> MergingStrategy (Rep a a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy MergeableArgs Arity0 Any
forall _. MergeableArgs Arity0 _
MergeableArgs0) Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
{-# INLINE genericRootStrategy #-}

instance
  (Generic1 f, GMergeable Arity1 (Rep1 f), Mergeable a) =>
  Mergeable (Default1 f a)
  where
  rootStrategy :: MergingStrategy (Default1 f a)
rootStrategy = MergingStrategy (Default1 f a)
forall a (u :: * -> *).
(Mergeable a, Mergeable1 u) =>
MergingStrategy (u a)
rootStrategy1
  {-# INLINE rootStrategy #-}

instance (Generic1 f, GMergeable Arity1 (Rep1 f)) => Mergeable1 (Default1 f) where
  liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (Default1 f a)
liftRootStrategy (MergingStrategy a
m :: MergingStrategy a) =
    MergingStrategy (f a) -> MergingStrategy (Default1 f a)
forall a b. a -> b
unsafeCoerce (MergingStrategy a -> MergingStrategy (f a)
forall (f :: * -> *) a.
(Generic1 f, GMergeable Arity1 (Rep1 f)) =>
MergingStrategy a -> MergingStrategy (f a)
genericLiftRootStrategy MergingStrategy a
m :: MergingStrategy (f a))
  {-# INLINE liftRootStrategy #-}

-- | Generic 'liftRootStrategy'.
genericLiftRootStrategy ::
  (Generic1 f, GMergeable Arity1 (Rep1 f)) =>
  MergingStrategy a ->
  MergingStrategy (f a)
genericLiftRootStrategy :: forall (f :: * -> *) a.
(Generic1 f, GMergeable Arity1 (Rep1 f)) =>
MergingStrategy a -> MergingStrategy (f a)
genericLiftRootStrategy MergingStrategy a
m =
  MergingStrategy (Rep1 f a)
-> (Rep1 f a -> f a) -> (f a -> Rep1 f a) -> MergingStrategy (f a)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy (MergeableArgs Arity1 a -> MergingStrategy (Rep1 f a)
forall a. MergeableArgs Arity1 a -> MergingStrategy (Rep1 f a)
forall arity (f :: * -> *) a.
GMergeable arity f =>
MergeableArgs arity a -> MergingStrategy (f a)
grootStrategy (MergeableArgs Arity1 a -> MergingStrategy (Rep1 f a))
-> MergeableArgs Arity1 a -> MergingStrategy (Rep1 f a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy a -> MergeableArgs Arity1 a
forall a. MergingStrategy a -> MergeableArgs Arity1 a
MergeableArgs1 MergingStrategy a
m) Rep1 f a -> f a
forall a. Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1
{-# INLINE genericLiftRootStrategy #-}

-- | Helper type for combining arbitrary number of indices into one.
-- Useful when trying to write efficient merge strategy for lists/vectors.
data DynamicSortedIdx where
  DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx

instance Eq DynamicSortedIdx where
  (DynamicSortedIdx (idx
a :: a)) == :: DynamicSortedIdx -> DynamicSortedIdx -> Bool
== (DynamicSortedIdx (idx
b :: b)) = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @b of
    Just idx :~: idx
Refl -> idx
a idx -> idx -> Bool
forall a. Eq a => a -> a -> Bool
== idx
idx
b
    Maybe (idx :~: idx)
_ -> Bool
False
  {-# INLINE (==) #-}

instance Ord DynamicSortedIdx where
  compare :: DynamicSortedIdx -> DynamicSortedIdx -> Ordering
compare (DynamicSortedIdx (idx
a :: a)) (DynamicSortedIdx (idx
b :: b)) = case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @b of
    Just idx :~: idx
Refl -> idx -> idx -> Ordering
forall a. Ord a => a -> a -> Ordering
compare idx
a idx
idx
b
    Maybe (idx :~: idx)
_ -> [Char] -> Ordering
forall a. HasCallStack => [Char] -> a
error [Char]
"This Ord is incomplete"
  {-# INLINE compare #-}

instance Show DynamicSortedIdx where
  show :: DynamicSortedIdx -> [Char]
show (DynamicSortedIdx idx
a) = idx -> [Char]
forall a. Show a => a -> [Char]
show idx
a

-- | Resolves the indices and the terminal merge strategy for a value of some
-- 'Mergeable' type.
resolveStrategy ::
  forall x.
  MergingStrategy x ->
  x ->
  ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy :: forall x.
MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy MergingStrategy x
s x
x = x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
forall x.
x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy' x
x MergingStrategy x
s
{-# INLINE resolveStrategy #-}

-- | Resolves the indices and the terminal merge strategy for a value given a
-- merge strategy for its type.
resolveStrategy' ::
  forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy' :: forall x.
x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy' x
x = MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
go
  where
    go :: MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
    go :: MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
go (SortedStrategy x -> idx
idxFun idx -> MergingStrategy x
subStrategy) = case MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
go MergingStrategy x
ss of
      ([DynamicSortedIdx]
idxs, MergingStrategy x
r) -> (idx -> DynamicSortedIdx
forall a. (Show a, Ord a, Typeable a) => a -> DynamicSortedIdx
DynamicSortedIdx idx
idx DynamicSortedIdx -> [DynamicSortedIdx] -> [DynamicSortedIdx]
forall a. a -> [a] -> [a]
: [DynamicSortedIdx]
idxs, MergingStrategy x
r)
      where
        idx :: idx
idx = x -> idx
idxFun x
x
        ss :: MergingStrategy x
ss = idx -> MergingStrategy x
subStrategy idx
idx
    go MergingStrategy x
s = ([], MergingStrategy x
s)
{-# INLINE resolveStrategy' #-}

-- | Helper type for building efficient merge strategy for list-like containers.
data StrategyList container where
  StrategyList ::
    forall a container.
    container [DynamicSortedIdx] ->
    container (MergingStrategy a) ->
    StrategyList container

-- | Helper function for building efficient merge strategy for list-like
-- containers.
buildStrategyList ::
  forall a container.
  (Functor container) =>
  MergingStrategy a ->
  container a ->
  StrategyList container
buildStrategyList :: forall a (container :: * -> *).
Functor container =>
MergingStrategy a -> container a -> StrategyList container
buildStrategyList MergingStrategy a
s container a
l = container [DynamicSortedIdx]
-> container (MergingStrategy a) -> StrategyList container
forall a (container :: * -> *).
container [DynamicSortedIdx]
-> container (MergingStrategy a) -> StrategyList container
StrategyList container [DynamicSortedIdx]
idxs container (MergingStrategy a)
strategies
  where
    r :: container ([DynamicSortedIdx], MergingStrategy a)
r = MergingStrategy a -> a -> ([DynamicSortedIdx], MergingStrategy a)
forall x.
MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
resolveStrategy MergingStrategy a
s (a -> ([DynamicSortedIdx], MergingStrategy a))
-> container a -> container ([DynamicSortedIdx], MergingStrategy a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> container a
l
    idxs :: container [DynamicSortedIdx]
idxs = ([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx]
forall a b. (a, b) -> a
fst (([DynamicSortedIdx], MergingStrategy a) -> [DynamicSortedIdx])
-> container ([DynamicSortedIdx], MergingStrategy a)
-> container [DynamicSortedIdx]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> container ([DynamicSortedIdx], MergingStrategy a)
r
    strategies :: container (MergingStrategy a)
strategies = ([DynamicSortedIdx], MergingStrategy a) -> MergingStrategy a
forall a b. (a, b) -> b
snd (([DynamicSortedIdx], MergingStrategy a) -> MergingStrategy a)
-> container ([DynamicSortedIdx], MergingStrategy a)
-> container (MergingStrategy a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> container ([DynamicSortedIdx], MergingStrategy a)
r
{-# INLINE buildStrategyList #-}

instance (Eq1 container) => Eq (StrategyList container) where
  (StrategyList container [DynamicSortedIdx]
idxs1 container (MergingStrategy a)
_) == :: StrategyList container -> StrategyList container -> Bool
== (StrategyList container [DynamicSortedIdx]
idxs2 container (MergingStrategy a)
_) = container [DynamicSortedIdx]
-> container [DynamicSortedIdx] -> Bool
forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 container [DynamicSortedIdx]
idxs1 container [DynamicSortedIdx]
idxs2
  {-# INLINE (==) #-}

instance (Ord1 container) => Ord (StrategyList container) where
  compare :: StrategyList container -> StrategyList container -> Ordering
compare (StrategyList container [DynamicSortedIdx]
idxs1 container (MergingStrategy a)
_) (StrategyList container [DynamicSortedIdx]
idxs2 container (MergingStrategy a)
_) = container [DynamicSortedIdx]
-> container [DynamicSortedIdx] -> Ordering
forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1 container [DynamicSortedIdx]
idxs1 container [DynamicSortedIdx]
idxs2
  {-# INLINE compare #-}

instance (Show1 container) => Show (StrategyList container) where
  showsPrec :: Int -> StrategyList container -> ShowS
showsPrec Int
i (StrategyList container [DynamicSortedIdx]
idxs1 container (MergingStrategy a)
_) = Int -> container [DynamicSortedIdx] -> ShowS
forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
i container [DynamicSortedIdx]
idxs1
  {-# INLINE showsPrec #-}

instance Mergeable SymBool where
  rootStrategy :: MergingStrategy SymBool
rootStrategy = (SymBool -> SymBool -> SymBool -> SymBool)
-> MergingStrategy SymBool
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> SymBool -> SymBool -> SymBool
forall v. ITEOp v => SymBool -> v -> v -> v
symIte

instance Mergeable Ordering where
  rootStrategy :: MergingStrategy Ordering
rootStrategy =
    let sub :: MergingStrategy a
sub = (SymBool -> a -> a -> a) -> MergingStrategy a
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> a -> a -> a) -> MergingStrategy a)
-> (SymBool -> a -> a -> a) -> MergingStrategy a
forall a b. (a -> b) -> a -> b
$ \SymBool
_ a
t a
_ -> a
t
     in (Ordering -> Ordering)
-> (Ordering -> MergingStrategy Ordering)
-> MergingStrategy Ordering
forall a a.
(Ord a, Typeable a, Show a) =>
(a -> a) -> (a -> MergingStrategy a) -> MergingStrategy a
SortedStrategy Ordering -> Ordering
forall a. a -> a
id ((Ordering -> MergingStrategy Ordering)
 -> MergingStrategy Ordering)
-> (Ordering -> MergingStrategy Ordering)
-> MergingStrategy Ordering
forall a b. (a -> b) -> a -> b
$ MergingStrategy Ordering -> Ordering -> MergingStrategy Ordering
forall a b. a -> b -> a
const MergingStrategy Ordering
forall a. MergingStrategy a
sub