{-# 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 StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable () where
import Control.Exception
( ArithException
( Denormal,
DivideByZero,
LossOfPrecision,
Overflow,
RatioZeroDenominator,
Underflow
),
)
import Control.Monad.Cont (ContT (ContT))
import Control.Monad.Except (ExceptT)
import Control.Monad.Identity
( Identity,
IdentityT (IdentityT, runIdentityT),
)
import qualified Control.Monad.RWS.Lazy as RWSLazy
import qualified Control.Monad.RWS.Strict as RWSStrict
import Control.Monad.Reader (ReaderT (ReaderT, runReaderT))
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Maybe (MaybeT)
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Compose (Compose (Compose, getCompose))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Monoid (Alt, Ap, Endo (Endo, appEndo))
import qualified Data.Monoid as Monoid
import Data.Ord (Down)
import Data.Ratio (Ratio)
import qualified Data.Text as T
import Data.Typeable (Proxy, Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (+), type (<=))
import Generics.Deriving
( Default (Default),
Default1 (Default1),
K1 (K1),
M1 (M1),
Par1 (Par1),
Rec1 (Rec1),
U1,
V1,
(:.:) (Comp1),
type (:*:),
type (:+:),
)
import Grisette.Internal.Core.Control.Exception
( AssertionError,
VerificationConditions,
)
import Grisette.Internal.Core.Data.Class.BitCast (bitCastOrCanonical)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
Mergeable1 (liftRootStrategy),
Mergeable2 (liftRootStrategy2),
Mergeable3 (liftRootStrategy3),
MergingStrategy (NoStrategy, SimpleStrategy, SortedStrategy),
StrategyList (StrategyList),
buildStrategyList,
rootStrategy1,
wrapStrategy,
)
import Grisette.Internal.SymPrim.AlgReal (AlgReal, AlgRealPoly, RealPoint)
import Grisette.Internal.SymPrim.BV
( IntN,
WordN,
)
import Grisette.Internal.SymPrim.FP
( FP,
FPRoundingMode,
NotRepresentableFPError,
ValidFP,
withValidFPProofs,
)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
import Grisette.Internal.TH.Derivation.Derive (derive)
import Unsafe.Coerce (unsafeCoerce)
#define CONCRETE_ORD_MERGEABLE(type) \
instance Mergeable type where \
rootStrategy = \
let sub = SimpleStrategy $ \_ t _ -> t \
in SortedStrategy id $ const sub
#define CONCRETE_ORD_MERGEABLE_BV(type) \
instance (KnownNat n, 1 <= n) => Mergeable (type n) where \
rootStrategy = \
let sub = SimpleStrategy $ \_ t _ -> t \
in SortedStrategy id $ const sub
#if 1
CONCRETE_ORD_MERGEABLE(Bool)
CONCRETE_ORD_MERGEABLE(Integer)
CONCRETE_ORD_MERGEABLE(Char)
CONCRETE_ORD_MERGEABLE(Int)
CONCRETE_ORD_MERGEABLE(Int8)
CONCRETE_ORD_MERGEABLE(Int16)
CONCRETE_ORD_MERGEABLE(Int32)
CONCRETE_ORD_MERGEABLE(Int64)
CONCRETE_ORD_MERGEABLE(Word)
CONCRETE_ORD_MERGEABLE(Word8)
CONCRETE_ORD_MERGEABLE(Word16)
CONCRETE_ORD_MERGEABLE(Word32)
CONCRETE_ORD_MERGEABLE(Word64)
CONCRETE_ORD_MERGEABLE(Float)
CONCRETE_ORD_MERGEABLE(Double)
CONCRETE_ORD_MERGEABLE(B.ByteString)
CONCRETE_ORD_MERGEABLE(T.Text)
CONCRETE_ORD_MERGEABLE(FPRoundingMode)
CONCRETE_ORD_MERGEABLE(Monoid.All)
CONCRETE_ORD_MERGEABLE(Monoid.Any)
CONCRETE_ORD_MERGEABLE_BV(WordN)
CONCRETE_ORD_MERGEABLE_BV(IntN)
#endif
instance Mergeable (Proxy a) where
rootStrategy :: MergingStrategy (Proxy a)
rootStrategy = (SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a))
-> (SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a)
forall a b. (a -> b) -> a -> b
$ \SymBool
_ Proxy a
t Proxy a
_ -> Proxy a
t
instance Mergeable1 Proxy where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (Proxy a)
liftRootStrategy MergingStrategy a
_ = (SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a))
-> (SymBool -> Proxy a -> Proxy a -> Proxy a)
-> MergingStrategy (Proxy a)
forall a b. (a -> b) -> a -> b
$ \SymBool
_ Proxy a
t Proxy a
_ -> Proxy a
t
{-# INLINE liftRootStrategy #-}
instance (Integral a, Typeable a, Show a) => Mergeable (Ratio a) where
rootStrategy :: MergingStrategy (Ratio a)
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 (Ratio a -> Ratio a)
-> (Ratio a -> MergingStrategy (Ratio a))
-> MergingStrategy (Ratio a)
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy Ratio a -> Ratio a
forall a. a -> a
id ((Ratio a -> MergingStrategy (Ratio a))
-> MergingStrategy (Ratio a))
-> (Ratio a -> MergingStrategy (Ratio a))
-> MergingStrategy (Ratio a)
forall a b. (a -> b) -> a -> b
$ MergingStrategy (Ratio a) -> Ratio a -> MergingStrategy (Ratio a)
forall a b. a -> b -> a
const MergingStrategy (Ratio a)
forall {a}. MergingStrategy a
sub
instance (ValidFP eb sb) => Mergeable (FP eb sb) where
rootStrategy :: MergingStrategy (FP eb sb)
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 forall (eb :: Nat) (sb :: Nat) r.
ValidFP eb sb =>
((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
1 <= eb, 1 <= sb) =>
r)
-> r
withValidFPProofs @eb @sb
(((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
1 <= eb, 1 <= sb) =>
MergingStrategy (FP eb sb))
-> MergingStrategy (FP eb sb))
-> ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb),
1 <= eb, 1 <= sb) =>
MergingStrategy (FP eb sb))
-> MergingStrategy (FP eb sb)
forall a b. (a -> b) -> a -> b
$ (FP eb sb -> WordN (eb + sb))
-> (WordN (eb + sb) -> MergingStrategy (FP eb sb))
-> MergingStrategy (FP eb sb)
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy
(\FP eb sb
fp -> (FP eb sb -> WordN (eb + sb)
forall from to. BitCastOrCanonical from to => from -> to
bitCastOrCanonical FP eb sb
fp :: WordN (eb + sb)))
((WordN (eb + sb) -> MergingStrategy (FP eb sb))
-> MergingStrategy (FP eb sb))
-> (WordN (eb + sb) -> MergingStrategy (FP eb sb))
-> MergingStrategy (FP eb sb)
forall a b. (a -> b) -> a -> b
$ MergingStrategy (FP eb sb)
-> WordN (eb + sb) -> MergingStrategy (FP eb sb)
forall a b. a -> b -> a
const MergingStrategy (FP eb sb)
forall {a}. MergingStrategy a
sub
instance Mergeable (a =-> b) where
rootStrategy :: MergingStrategy (a =-> b)
rootStrategy = MergingStrategy (a =-> b)
forall {a}. MergingStrategy a
NoStrategy
instance Mergeable (a --> b) where
rootStrategy :: MergingStrategy (a --> b)
rootStrategy = (SymBool -> (a --> b) -> (a --> b) -> a --> b)
-> MergingStrategy (a --> b)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> (a --> b) -> (a --> b) -> a --> b
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
#define MERGEABLE_SIMPLE(symtype) \
instance Mergeable symtype where \
rootStrategy = SimpleStrategy symIte
#define MERGEABLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \
rootStrategy = SimpleStrategy symIte
#define MERGEABLE_FUN(cop, op, consop) \
instance Mergeable (op sa sb) where \
rootStrategy = SimpleStrategy symIte
#if 1
MERGEABLE_SIMPLE(SymInteger)
MERGEABLE_SIMPLE(SymFPRoundingMode)
MERGEABLE_SIMPLE(SymAlgReal)
MERGEABLE_BV(SymIntN)
MERGEABLE_BV(SymWordN)
MERGEABLE_FUN((=->), (=~>), SymTabularFun)
MERGEABLE_FUN((-->), (-~>), SymGeneralFun)
#endif
instance (ValidFP eb sb) => Mergeable (SymFP eb sb) where
rootStrategy :: MergingStrategy (SymFP eb sb)
rootStrategy = (SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb)
-> MergingStrategy (SymFP eb sb)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb
forall v. ITEOp v => SymBool -> v -> v -> v
symIte
instance (Mergeable b) => Mergeable (a -> b) where
rootStrategy :: MergingStrategy (a -> b)
rootStrategy = case forall a. Mergeable a => MergingStrategy a
rootStrategy @b of
SimpleStrategy SymBool -> b -> b -> b
m -> (SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b))
-> (SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b)
forall a b. (a -> b) -> a -> b
$ \SymBool
cond a -> b
t a -> b
f a
v -> SymBool -> b -> b -> b
m SymBool
cond (a -> b
t a
v) (a -> b
f a
v)
MergingStrategy b
_ -> MergingStrategy (a -> b)
forall {a}. MergingStrategy a
NoStrategy
{-# INLINE rootStrategy #-}
instance Mergeable1 ((->) a) where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy (a -> a)
liftRootStrategy MergingStrategy a
ms = case MergingStrategy a
ms of
SimpleStrategy SymBool -> a -> a -> a
m -> (SymBool -> (a -> a) -> (a -> a) -> a -> a)
-> MergingStrategy (a -> a)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> (a -> a) -> (a -> a) -> a -> a)
-> MergingStrategy (a -> a))
-> (SymBool -> (a -> a) -> (a -> a) -> a -> a)
-> MergingStrategy (a -> a)
forall a b. (a -> b) -> a -> b
$ \SymBool
cond a -> a
t a -> a
f a
v -> SymBool -> a -> a -> a
m SymBool
cond (a -> a
t a
v) (a -> a
f a
v)
MergingStrategy a
_ -> MergingStrategy (a -> a)
forall {a}. MergingStrategy a
NoStrategy
{-# INLINE liftRootStrategy #-}
instance Mergeable2 ((->)) where
liftRootStrategy2 :: forall a b.
MergingStrategy a -> MergingStrategy b -> MergingStrategy (a -> b)
liftRootStrategy2 MergingStrategy a
_ MergingStrategy b
ms = case MergingStrategy b
ms of
SimpleStrategy SymBool -> b -> b -> b
m -> (SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b)
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b))
-> (SymBool -> (a -> b) -> (a -> b) -> a -> b)
-> MergingStrategy (a -> b)
forall a b. (a -> b) -> a -> b
$ \SymBool
cond a -> b
t a -> b
f a
v -> SymBool -> b -> b -> b
m SymBool
cond (a -> b
t a
v) (a -> b
f a
v)
MergingStrategy b
_ -> MergingStrategy (a -> b)
forall {a}. MergingStrategy a
NoStrategy
{-# INLINE liftRootStrategy2 #-}
instance (Mergeable a) => Mergeable [a] where
rootStrategy :: MergingStrategy [a]
rootStrategy = case MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy :: MergingStrategy a of
SimpleStrategy SymBool -> a -> a -> a
m ->
([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ \Int
_ ->
(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
cond -> (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SymBool -> a -> a -> a
m SymBool
cond)
MergingStrategy a
NoStrategy ->
([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ MergingStrategy [a] -> Int -> MergingStrategy [a]
forall a b. a -> b -> a
const MergingStrategy [a]
forall {a}. MergingStrategy a
NoStrategy
MergingStrategy a
_ -> ([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ \Int
_ ->
([a] -> StrategyList [])
-> (StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy (MergingStrategy a -> [a] -> StrategyList []
forall a (container :: * -> *).
Functor container =>
MergingStrategy a -> container a -> StrategyList container
buildStrategyList MergingStrategy a
forall a. Mergeable a => MergingStrategy a
rootStrategy) ((StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a])
-> (StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$
\(StrategyList [[DynamicSortedIdx]]
_ [MergingStrategy a]
strategies) ->
let [MergingStrategy a]
s :: [MergingStrategy a] = [MergingStrategy a] -> [MergingStrategy a]
forall a b. a -> b
unsafeCoerce [MergingStrategy a]
strategies
allSimple :: Bool
allSimple = (MergingStrategy a -> Bool) -> [MergingStrategy a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case SimpleStrategy SymBool -> a -> a -> a
_ -> Bool
True; MergingStrategy a
_ -> Bool
False) [MergingStrategy a]
s
in if Bool
allSimple
then (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
cond [a]
l [a]
r ->
( \case
(SimpleStrategy SymBool -> a -> a -> a
f, a
l1, a
r1) -> SymBool -> a -> a -> a
f SymBool
cond a
l1 a
r1
(MergingStrategy a, a, a)
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
)
((MergingStrategy a, a, a) -> a)
-> [(MergingStrategy a, a, a)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MergingStrategy a] -> [a] -> [a] -> [(MergingStrategy a, a, a)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [MergingStrategy a]
s [a]
l [a]
r
else MergingStrategy [a]
forall {a}. MergingStrategy a
NoStrategy
{-# INLINE rootStrategy #-}
instance Mergeable1 [] where
liftRootStrategy :: forall a. MergingStrategy a -> MergingStrategy [a]
liftRootStrategy (MergingStrategy a
ms :: MergingStrategy a) = case MergingStrategy a
ms of
SimpleStrategy SymBool -> a -> a -> a
m ->
([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ \Int
_ ->
(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
cond -> (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SymBool -> a -> a -> a
m SymBool
cond)
MergingStrategy a
NoStrategy ->
([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ MergingStrategy [a] -> Int -> MergingStrategy [a]
forall a b. a -> b -> a
const MergingStrategy [a]
forall {a}. MergingStrategy a
NoStrategy
MergingStrategy a
_ -> ([a] -> Int) -> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Int -> MergingStrategy [a]) -> MergingStrategy [a])
-> (Int -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ \Int
_ ->
([a] -> StrategyList [])
-> (StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a]
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy (MergingStrategy a -> [a] -> StrategyList []
forall a (container :: * -> *).
Functor container =>
MergingStrategy a -> container a -> StrategyList container
buildStrategyList MergingStrategy a
ms) ((StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a])
-> (StrategyList [] -> MergingStrategy [a]) -> MergingStrategy [a]
forall a b. (a -> b) -> a -> b
$ \(StrategyList [[DynamicSortedIdx]]
_ [MergingStrategy a]
strategies) ->
let [MergingStrategy a]
s :: [MergingStrategy a] = [MergingStrategy a] -> [MergingStrategy a]
forall a b. a -> b
unsafeCoerce [MergingStrategy a]
strategies
allSimple :: Bool
allSimple = (MergingStrategy a -> Bool) -> [MergingStrategy a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case SimpleStrategy SymBool -> a -> a -> a
_ -> Bool
True; MergingStrategy a
_ -> Bool
False) [MergingStrategy a]
s
in if Bool
allSimple
then (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
cond [a]
l [a]
r ->
( \case
(SimpleStrategy SymBool -> a -> a -> a
f, a
l1, a
r1) -> SymBool -> a -> a -> a
f SymBool
cond a
l1 a
r1
(MergingStrategy a, a, a)
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
)
((MergingStrategy a, a, a) -> a)
-> [(MergingStrategy a, a, a)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MergingStrategy a] -> [a] -> [a] -> [(MergingStrategy a, a, a)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [MergingStrategy a]
s [a]
l [a]
r
else MergingStrategy [a]
forall {a}. MergingStrategy a
NoStrategy
{-# INLINE liftRootStrategy #-}
instance Mergeable () where
rootStrategy :: MergingStrategy ()
rootStrategy = (SymBool -> () -> () -> ()) -> MergingStrategy ()
forall a. (SymBool -> a -> a -> a) -> MergingStrategy a
SimpleStrategy ((SymBool -> () -> () -> ()) -> MergingStrategy ())
-> (SymBool -> () -> () -> ()) -> MergingStrategy ()
forall a b. (a -> b) -> a -> b
$ \SymBool
_ ()
t ()
_ -> ()
t
derive
[ ''Either,
''(,)
]
[''Mergeable, ''Mergeable1, ''Mergeable2]