{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# 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.Core.Data.Class.ToSym
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.ToSym
  ( -- * Converting to symbolic values
    ToSym (..),
    ToSym1 (..),
    toSym1,
    ToSym2 (..),
    toSym2,

    -- * Generic 'ToSym'
    ToSymArgs (..),
    GToSym (..),
    genericToSym,
    genericLiftToSym,
  )
where

import Control.Monad.Identity
  ( Identity (Identity, runIdentity),
    IdentityT (IdentityT),
  )
import Control.Monad.Reader (ReaderT (ReaderT))
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Except (ExceptT (ExceptT))
import Control.Monad.Trans.Maybe (MaybeT (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))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Kind (Type)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down)
import Data.Ratio (Ratio, denominator, numerator, (%))
import qualified Data.Text as T
import Data.Typeable (Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default),
    Default1 (Default1),
    Generic (Rep, from, to),
    Generic1 (Rep1, from1, to1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1 (U1),
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.Mergeable
  ( GMergeable,
    Mergeable,
    Mergeable1,
    Mergeable2,
    resolveMergeable1,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV
  ( IntN,
    WordN,
  )
import Grisette.Internal.SymPrim.FP
  ( FP,
    FPRoundingMode,
    NotRepresentableFPError,
    ValidFP,
  )
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.IntBitwidth (intBitwidthQ)
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep,
    SupportedNonFuncPrim,
    SupportedPrim,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN,
    SymWordN,
  )
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymFP
  ( SymFP,
    SymFP32,
    SymFP64,
    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.DeriveBuiltin (deriveBuiltins)
import Grisette.Internal.TH.DeriveInstanceProvider
  ( Strategy (ViaDefault, ViaDefault1),
  )
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.SymPrim

-- | Convert a concrete value to symbolic value.
class (Mergeable b) => ToSym a b where
  -- | Convert a concrete value to symbolic value.
  --
  -- >>> toSym False :: SymBool
  -- false
  --
  -- >>> toSym [False, True] :: [SymBool]
  -- [false,true]
  toSym :: a -> b

instance {-# INCOHERENT #-} (Mergeable a) => ToSym a a where
  toSym :: a -> a
toSym = a -> a
forall a. a -> a
id
  {-# INLINE toSym #-}

-- | Lifting of 'ToSym' to unary type constructors.
class
  (forall a b. (ToSym a b) => ToSym (f1 a) (f2 b), Mergeable1 f2) =>
  ToSym1 f1 f2
  where
  -- | Lift a conversion to symbolic function to unary type constructors.
  liftToSym :: (Mergeable b) => (a -> b) -> f1 a -> f2 b

-- | Lift the standard 'toSym' to unary type constructors.
toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b
toSym1 :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1 = (a -> b) -> f1 a -> f2 b
forall b a. Mergeable b => (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
forall a b. ToSym a b => a -> b
toSym
{-# INLINE toSym1 #-}

-- | Lifting of 'ToSym' to binary type constructors.
class
  (forall a b. (ToSym a b) => ToSym1 (f1 a) (f2 b), Mergeable2 f2) =>
  ToSym2 f1 f2
  where
  -- | Lift conversion to symbolic functions to binary type constructors.
  liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d

-- | Lift the standard 'toSym' to binary type constructors.
toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d
toSym2 :: forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
(ToSym2 f1 f2, ToSym a b, ToSym c d) =>
f1 a c -> f2 b d
toSym2 = (a -> b) -> (c -> d) -> f1 a c -> f2 b d
forall a b c d. (a -> b) -> (c -> d) -> f1 a c -> f2 b d
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
forall a b. ToSym a b => a -> b
toSym c -> d
forall a b. ToSym a b => a -> b
toSym
{-# INLINE toSym2 #-}

-- Derivations

-- | The arguments to the generic 'toSym' function.
data family ToSymArgs arity a b :: Type

data instance ToSymArgs Arity0 _ _ = ToSymArgs0

data instance ToSymArgs Arity1 _ _ where
  ToSymArgs1 :: (Mergeable b) => (a -> b) -> ToSymArgs Arity1 a b

-- | The class of types that can be generically converted to symbolic values.
class GToSym arity f1 f2 where
  gtoSym :: ToSymArgs arity a b -> f1 a -> f2 b

instance GToSym arity V1 V1 where
  gtoSym :: forall a b. ToSymArgs arity a b -> V1 a -> V1 b
gtoSym ToSymArgs arity a b
_ V1 a
_ = [Char] -> V1 b
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
  {-# INLINE gtoSym #-}

instance GToSym arity U1 U1 where
  gtoSym :: forall a b. ToSymArgs arity a b -> U1 a -> U1 b
gtoSym ToSymArgs arity a b
_ U1 a
_ = U1 b
forall k (p :: k). U1 p
U1
  {-# INLINE gtoSym #-}

instance
  (GToSym arity a b, GToSym arity c d) =>
  GToSym arity (a :+: c) (b :+: d)
  where
  gtoSym :: forall a b. ToSymArgs arity a b -> (:+:) a c a -> (:+:) b d b
gtoSym ToSymArgs arity a b
args (L1 a a
a) = b b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (b b -> (:+:) b d b) -> b b -> (:+:) b d b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> a a -> b b
forall a b. ToSymArgs arity a b -> a a -> b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args a a
a
  gtoSym ToSymArgs arity a b
args (R1 c a
b) = d b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (d b -> (:+:) b d b) -> d b -> (:+:) b d b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> c a -> d b
forall a b. ToSymArgs arity a b -> c a -> d b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args c a
b
  {-# INLINE gtoSym #-}

instance
  (GToSym arity a b, GToSym arity c d) =>
  GToSym arity (a :*: c) (b :*: d)
  where
  gtoSym :: forall a b. ToSymArgs arity a b -> (:*:) a c a -> (:*:) b d b
gtoSym ToSymArgs arity a b
args (a a
a :*: c a
c) = ToSymArgs arity a b -> a a -> b b
forall a b. ToSymArgs arity a b -> a a -> b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args a a
a b b -> d b -> (:*:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: ToSymArgs arity a b -> c a -> d b
forall a b. ToSymArgs arity a b -> c a -> d b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args c a
c
  {-# INLINE gtoSym #-}

instance (ToSym a b) => GToSym arity (K1 i a) (K1 i b) where
  gtoSym :: forall a b. ToSymArgs arity a b -> K1 i a a -> K1 i b b
gtoSym ToSymArgs arity a b
_ (K1 a
a) = b -> K1 i b b
forall k i c (p :: k). c -> K1 i c p
K1 (b -> K1 i b b) -> b -> K1 i b b
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. ToSym a b => a -> b
toSym a
a
  {-# INLINE gtoSym #-}

instance (GToSym arity f1 f2) => GToSym arity (M1 i c1 f1) (M1 i c2 f2) where
  gtoSym :: forall a b. ToSymArgs arity a b -> M1 i c1 f1 a -> M1 i c2 f2 b
gtoSym ToSymArgs arity a b
args (M1 f1 a
a) = f2 b -> M1 i c2 f2 b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f2 b -> M1 i c2 f2 b) -> f2 b -> M1 i c2 f2 b
forall a b. (a -> b) -> a -> b
$ ToSymArgs arity a b -> f1 a -> f2 b
forall a b. ToSymArgs arity a b -> f1 a -> f2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs arity a b
args f1 a
a
  {-# INLINE gtoSym #-}

instance GToSym Arity1 Par1 Par1 where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> Par1 a -> Par1 b
gtoSym (ToSymArgs1 a -> b
f) (Par1 a
a) = b -> Par1 b
forall p. p -> Par1 p
Par1 (b -> Par1 b) -> b -> Par1 b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
  {-# INLINE gtoSym #-}

instance (ToSym1 f1 f2) => GToSym Arity1 (Rec1 f1) (Rec1 f2) where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> Rec1 f1 a -> Rec1 f2 b
gtoSym (ToSymArgs1 a -> b
f) (Rec1 f1 a
a) = f2 b -> Rec1 f2 b
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (f2 b -> Rec1 f2 b) -> f2 b -> Rec1 f2 b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f1 a -> f2 b
forall b a. Mergeable b => (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f f1 a
a
  {-# INLINE gtoSym #-}

instance
  (ToSym1 f1 f2, GToSym Arity1 g1 g2, Mergeable1 g2) =>
  GToSym Arity1 (f1 :.: g1) (f2 :.: g2)
  where
  gtoSym :: forall a b. ToSymArgs Arity1 a b -> (:.:) f1 g1 a -> (:.:) f2 g2 b
gtoSym targs :: ToSymArgs Arity1 a b
targs@ToSymArgs1 {} (Comp1 f1 (g1 a)
a) = f2 (g2 b) -> (:.:) f2 g2 b
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f2 (g2 b) -> (:.:) f2 g2 b) -> f2 (g2 b) -> (:.:) f2 g2 b
forall a b. (a -> b) -> a -> b
$ (g1 a -> g2 b) -> f1 (g1 a) -> f2 (g2 b)
forall b a. Mergeable b => (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym (ToSymArgs Arity1 a b -> g1 a -> g2 b
forall a b. ToSymArgs Arity1 a b -> g1 a -> g2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs Arity1 a b
targs) f1 (g1 a)
a
  {-# INLINE gtoSym #-}

-- | Generic 'toSym' function.
genericToSym ::
  (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
  a ->
  b
genericToSym :: forall a b.
(Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
a -> b
genericToSym = Rep b Any -> b
forall a x. Generic a => Rep a x -> a
forall x. Rep b x -> b
to (Rep b Any -> b) -> (a -> Rep b Any) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSymArgs Arity0 Any Any -> Rep a Any -> Rep b Any
forall a b. ToSymArgs Arity0 a b -> Rep a a -> Rep b b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ToSymArgs Arity0 Any Any
forall _ _. ToSymArgs Arity0 _ _
ToSymArgs0 (Rep a Any -> Rep b Any) -> (a -> Rep a Any) -> a -> Rep b Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
{-# INLINE genericToSym #-}

-- | Generic 'liftToSym' function.
genericLiftToSym ::
  (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2), Mergeable b) =>
  (a -> b) ->
  f1 a ->
  f2 b
genericLiftToSym :: forall (f1 :: * -> *) (f2 :: * -> *) b a.
(Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2),
 Mergeable b) =>
(a -> b) -> f1 a -> f2 b
genericLiftToSym a -> b
f = Rep1 f2 b -> f2 b
forall a. Rep1 f2 a -> f2 a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f2 b -> f2 b) -> (f1 a -> Rep1 f2 b) -> f1 a -> f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSymArgs Arity1 a b -> Rep1 f1 a -> Rep1 f2 b
forall a b. ToSymArgs Arity1 a b -> Rep1 f1 a -> Rep1 f2 b
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToSym arity f1 f2 =>
ToSymArgs arity a b -> f1 a -> f2 b
gtoSym ((a -> b) -> ToSymArgs Arity1 a b
forall b a. Mergeable b => (a -> b) -> ToSymArgs Arity1 a b
ToSymArgs1 a -> b
f) (Rep1 f1 a -> Rep1 f2 b)
-> (f1 a -> Rep1 f1 a) -> f1 a -> Rep1 f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f1 a -> Rep1 f1 a
forall a. f1 a -> Rep1 f1 a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1
{-# INLINE genericLiftToSym #-}

instance
  ( Generic a,
    Generic b,
    GToSym Arity0 (Rep a) (Rep b),
    GMergeable Arity0 (Rep b)
  ) =>
  ToSym a (Default b)
  where
  toSym :: a -> Default b
toSym = b -> Default b
forall a. a -> Default a
Default (b -> Default b) -> (a -> b) -> a -> Default b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b.
(Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) =>
a -> b
genericToSym
  {-# INLINE toSym #-}

instance
  ( Generic1 f1,
    Generic1 f2,
    GToSym Arity1 (Rep1 f1) (Rep1 f2),
    ToSym a b,
    GMergeable Arity1 (Rep1 f2)
  ) =>
  ToSym (f1 a) (Default1 f2 b)
  where
  toSym :: f1 a -> Default1 f2 b
toSym = f1 a -> Default1 f2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1

instance
  ( Generic1 f1,
    Generic1 f2,
    GToSym Arity1 (Rep1 f1) (Rep1 f2),
    GMergeable Arity1 (Rep1 f2)
  ) =>
  ToSym1 f1 (Default1 f2)
  where
  liftToSym :: forall b a. Mergeable b => (a -> b) -> f1 a -> Default1 f2 b
liftToSym a -> b
f = f2 b -> Default1 f2 b
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (f2 b -> Default1 f2 b) -> (f1 a -> f2 b) -> f1 a -> Default1 f2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> f1 a -> f2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2),
 Mergeable b) =>
(a -> b) -> f1 a -> f2 b
genericLiftToSym a -> b
f
  {-# INLINE liftToSym #-}

#define CONCRETE_TOSYM(type) \
instance ToSym type type where \
  toSym = id

#define CONCRETE_TOSYM_BV(type) \
instance (KnownNat n, 1 <= n) => ToSym (type n) (type n) where \
  toSym = id

#if 1
CONCRETE_TOSYM(Bool)
CONCRETE_TOSYM(Integer)
CONCRETE_TOSYM(Char)
CONCRETE_TOSYM(Int)
CONCRETE_TOSYM(Int8)
CONCRETE_TOSYM(Int16)
CONCRETE_TOSYM(Int32)
CONCRETE_TOSYM(Int64)
CONCRETE_TOSYM(Word)
CONCRETE_TOSYM(Word8)
CONCRETE_TOSYM(Word16)
CONCRETE_TOSYM(Word32)
CONCRETE_TOSYM(Word64)
CONCRETE_TOSYM(Float)
CONCRETE_TOSYM(Double)
CONCRETE_TOSYM(B.ByteString)
CONCRETE_TOSYM(T.Text)
CONCRETE_TOSYM(FPRoundingMode)
CONCRETE_TOSYM_BV(IntN)
CONCRETE_TOSYM_BV(WordN)
CONCRETE_TOSYM(Monoid.All)
CONCRETE_TOSYM(Monoid.Any)
CONCRETE_TOSYM(Ordering)
#endif

instance (ValidFP eb sb) => ToSym (FP eb sb) (FP eb sb) where
  toSym :: FP eb sb -> FP eb sb
toSym = FP eb sb -> FP eb sb
forall a. a -> a
id

instance ToSym (a =-> b) (a =-> b) where
  toSym :: (a =-> b) -> a =-> b
toSym = (a =-> b) -> a =-> b
forall a. a -> a
id

instance ToSym (a --> b) (a --> b) where
  toSym :: (a --> b) -> a --> b
toSym = (a --> b) -> a --> b
forall a. a -> a
id

#define TO_SYM_SYMID_SIMPLE(symtype) \
instance ToSym symtype symtype where \
  toSym = id

#define TO_SYM_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToSym (symtype n) (symtype n) where \
  toSym = id

#define TO_SYM_SYMID_FUN(cop, op) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  ToSym (op sa sb) (op sa sb) where \
  toSym = id

#if 1
TO_SYM_SYMID_SIMPLE(SymBool)
TO_SYM_SYMID_SIMPLE(SymInteger)
TO_SYM_SYMID_SIMPLE(SymAlgReal)
TO_SYM_SYMID_BV(SymIntN)
TO_SYM_SYMID_BV(SymWordN)
TO_SYM_SYMID_FUN((=->), (=~>))
TO_SYM_SYMID_FUN((-->), (-~>))
TO_SYM_SYMID_SIMPLE(SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToSym (SymFP eb sb) (SymFP eb sb) where
  toSym :: SymFP eb sb -> SymFP eb sb
toSym = SymFP eb sb -> SymFP eb sb
forall a. a -> a
id

#define TO_SYM_FROMCON_SIMPLE(contype, symtype) \
instance ToSym contype symtype where \
  toSym = con

#define TO_SYM_FROMCON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (contype n) (symtype n) where \
  toSym = con

#define TO_SYM_FROMCON_FUN(conop, symop) \
instance (SupportedPrim (conop ca cb), SupportedNonFuncPrim ca, LinkedRep ca sa, LinkedRep cb sb) => \
  ToSym (conop ca cb) (symop sa sb) where \
  toSym = con

#if 1
TO_SYM_FROMCON_SIMPLE(Bool, SymBool)
TO_SYM_FROMCON_SIMPLE(Integer, SymInteger)
TO_SYM_FROMCON_SIMPLE(AlgReal, SymAlgReal)
TO_SYM_FROMCON_BV(IntN, SymIntN)
TO_SYM_FROMCON_BV(WordN, SymWordN)
TO_SYM_FROMCON_FUN((=->), (=~>))
TO_SYM_FROMCON_FUN((-->), (-~>))
TO_SYM_FROMCON_SIMPLE(FPRoundingMode, SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToSym (FP eb sb) (SymFP eb sb) where
  toSym :: FP eb sb -> SymFP eb sb
toSym = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con

#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (bv) where \
  toSym = fromIntegral

#if 1
TOSYM_MACHINE_INTEGER(Int8, SymIntN 8)
TOSYM_MACHINE_INTEGER(Int16, SymIntN 16)
TOSYM_MACHINE_INTEGER(Int32, SymIntN 32)
TOSYM_MACHINE_INTEGER(Int64, SymIntN 64)
TOSYM_MACHINE_INTEGER(Word8, SymWordN 8)
TOSYM_MACHINE_INTEGER(Word16, SymWordN 16)
TOSYM_MACHINE_INTEGER(Word32, SymWordN 32)
TOSYM_MACHINE_INTEGER(Word64, SymWordN 64)
TOSYM_MACHINE_INTEGER(Int, SymIntN $intBitwidthQ)
TOSYM_MACHINE_INTEGER(Word, SymWordN $intBitwidthQ)
#endif

instance ToSym Float SymFP32 where
  toSym :: Float -> SymFP32
toSym = FP 8 24 -> SymFP32
forall c t. Solvable c t => c -> t
con (FP 8 24 -> SymFP32) -> (Float -> FP 8 24) -> Float -> SymFP32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> FP 8 24
forall from to. BitCast from to => from -> to
bitCast
  {-# INLINE toSym #-}

instance ToSym Double SymFP64 where
  toSym :: Double -> SymFP64
toSym = FP 11 53 -> SymFP64
forall c t. Solvable c t => c -> t
con (FP 11 53 -> SymFP64) -> (Double -> FP 11 53) -> Double -> SymFP64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> FP 11 53
forall from to. BitCast from to => from -> to
bitCast
  {-# INLINE toSym #-}

instance
  (Integral b, Typeable b, Show b, ToSym a b) =>
  ToSym (Ratio a) (Ratio b)
  where
  toSym :: Ratio a -> Ratio b
toSym Ratio a
r = a -> b
forall a b. ToSym a b => a -> b
toSym (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
r) b -> b -> Ratio b
forall a. Integral a => a -> a -> Ratio a
% a -> b
forall a b. ToSym a b => a -> b
toSym (Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
r)
  {-# INLINE toSym #-}

instance ToSym Rational SymAlgReal where
  toSym :: Rational -> SymAlgReal
toSym Rational
v = AlgReal -> SymAlgReal
forall c t. Solvable c t => c -> t
con (Rational -> AlgReal
forall a. Fractional a => Rational -> a
fromRational Rational
v)

deriveBuiltins
  (ViaDefault ''ToSym)
  [''ToSym]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(),
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''NotRepresentableFPError,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

deriveBuiltins
  (ViaDefault1 ''ToSym1)
  [''ToSym, ''ToSym1]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

-- ExceptT
instance
  (ToSym1 m1 m2, ToSym e1 e2, ToSym a b) =>
  ToSym (ExceptT e1 m1 a) (ExceptT e2 m2 b)
  where
  toSym :: ExceptT e1 m1 a -> ExceptT e2 m2 b
toSym = ExceptT e1 m1 a -> ExceptT e2 m2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2, ToSym e1 e2) =>
  ToSym1 (ExceptT e1 m1) (ExceptT e2 m2)
  where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> ExceptT e1 m1 a -> ExceptT e2 m2 b
liftToSym a -> b
f (ExceptT m1 (Either e1 a)
v) = m2 (Either e2 b) -> ExceptT e2 m2 b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m2 (Either e2 b) -> ExceptT e2 m2 b)
-> m2 (Either e2 b) -> ExceptT e2 m2 b
forall a b. (a -> b) -> a -> b
$ (Either e1 a -> Either e2 b)
-> m1 (Either e1 a) -> m2 (Either e2 b)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> Either e1 a -> Either e2 b
forall b a. Mergeable b => (a -> b) -> Either e1 a -> Either e2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f) m1 (Either e1 a)
v
  {-# INLINE liftToSym #-}

-- MaybeT
instance
  (ToSym1 m1 m2, ToSym a b) =>
  ToSym (MaybeT m1 a) (MaybeT m2 b)
  where
  toSym :: MaybeT m1 a -> MaybeT m2 b
toSym = MaybeT m1 a -> MaybeT m2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2) =>
  ToSym1 (MaybeT m1) (MaybeT m2)
  where
  liftToSym :: forall b a. Mergeable b => (a -> b) -> MaybeT m1 a -> MaybeT m2 b
liftToSym a -> b
f (MaybeT m1 (Maybe a)
v) = m2 (Maybe b) -> MaybeT m2 b
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m2 (Maybe b) -> MaybeT m2 b) -> m2 (Maybe b) -> MaybeT m2 b
forall a b. (a -> b) -> a -> b
$ (Maybe a -> Maybe b) -> m1 (Maybe a) -> m2 (Maybe b)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> Maybe a -> Maybe b
forall b a. Mergeable b => (a -> b) -> Maybe a -> Maybe b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f) m1 (Maybe a)
v
  {-# INLINE liftToSym #-}

-- WriterT
instance
  (ToSym1 m1 m2, ToSym a b, ToSym s1 s2) =>
  ToSym (WriterLazy.WriterT s1 m1 a) (WriterLazy.WriterT s2 m2 b)
  where
  toSym :: WriterT s1 m1 a -> WriterT s2 m2 b
toSym = WriterT s1 m1 a -> WriterT s2 m2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2, ToSym s1 s2) =>
  ToSym1 (WriterLazy.WriterT s1 m1) (WriterLazy.WriterT s2 m2)
  where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> WriterT s1 m1 a -> WriterT s2 m2 b
liftToSym a -> b
f (WriterLazy.WriterT m1 (a, s1)
v) =
    m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m2 (b, s2) -> WriterT s2 m2 b) -> m2 (b, s2) -> WriterT s2 m2 b
forall a b. (a -> b) -> a -> b
$ ((a, s1) -> (b, s2)) -> m1 (a, s1) -> m2 (b, s2)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> (s1 -> s2) -> (a, s1) -> (b, s2)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
f s1 -> s2
forall a b. ToSym a b => a -> b
toSym) m1 (a, s1)
v
  {-# INLINE liftToSym #-}

instance
  (ToSym1 m1 m2, ToSym a b, ToSym s1 s2) =>
  ToSym (WriterStrict.WriterT s1 m1 a) (WriterStrict.WriterT s2 m2 b)
  where
  toSym :: WriterT s1 m1 a -> WriterT s2 m2 b
toSym = WriterT s1 m1 a -> WriterT s2 m2 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2, ToSym s1 s2) =>
  ToSym1 (WriterStrict.WriterT s1 m1) (WriterStrict.WriterT s2 m2)
  where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> WriterT s1 m1 a -> WriterT s2 m2 b
liftToSym a -> b
f (WriterStrict.WriterT m1 (a, s1)
v) =
    m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m2 (b, s2) -> WriterT s2 m2 b) -> m2 (b, s2) -> WriterT s2 m2 b
forall a b. (a -> b) -> a -> b
$ ((a, s1) -> (b, s2)) -> m1 (a, s1) -> m2 (b, s2)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> (s1 -> s2) -> (a, s1) -> (b, s2)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
f s1 -> s2
forall a b. ToSym a b => a -> b
toSym) m1 (a, s1)
v
  {-# INLINE liftToSym #-}

-- StateT
instance
  (ToSym1 m1 m2, ToSym a1 a2, Mergeable s) =>
  ToSym (StateLazy.StateT s m1 a1) (StateLazy.StateT s m2 a2)
  where
  toSym :: StateT s m1 a1 -> StateT s m2 a2
toSym = StateT s m1 a1 -> StateT s m2 a2
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2, Mergeable s) =>
  ToSym1 (StateLazy.StateT s m1) (StateLazy.StateT s m2)
  where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> StateT s m1 a -> StateT s m2 b
liftToSym a -> b
f (StateLazy.StateT s -> m1 (a, s)
f1) =
    (s -> m2 (b, s)) -> StateT s m2 b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT ((s -> m2 (b, s)) -> StateT s m2 b)
-> (s -> m2 (b, s)) -> StateT s m2 b
forall a b. (a -> b) -> a -> b
$ \s
s -> ((a, s) -> (b, s)) -> m1 (a, s) -> m2 (b, s)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> (s -> s) -> (a, s) -> (b, s)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
f s -> s
forall a. a -> a
id) (m1 (a, s) -> m2 (b, s)) -> m1 (a, s) -> m2 (b, s)
forall a b. (a -> b) -> a -> b
$ s -> m1 (a, s)
f1 s
s
  {-# INLINE liftToSym #-}

instance
  (ToSym1 m1 m2, ToSym a1 a2, Mergeable s) =>
  ToSym (StateStrict.StateT s m1 a1) (StateStrict.StateT s m2 a2)
  where
  toSym :: StateT s m1 a1 -> StateT s m2 a2
toSym = StateT s m1 a1 -> StateT s m2 a2
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym1 m1 m2, Mergeable s) =>
  ToSym1 (StateStrict.StateT s m1) (StateStrict.StateT s m2)
  where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> StateT s m1 a -> StateT s m2 b
liftToSym a -> b
f (StateStrict.StateT s -> m1 (a, s)
f1) =
    (s -> m2 (b, s)) -> StateT s m2 b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT ((s -> m2 (b, s)) -> StateT s m2 b)
-> (s -> m2 (b, s)) -> StateT s m2 b
forall a b. (a -> b) -> a -> b
$ \s
s -> ((a, s) -> (b, s)) -> m1 (a, s) -> m2 (b, s)
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> (s -> s) -> (a, s) -> (b, s)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToSym2 f1 f2 =>
(a -> b) -> (c -> d) -> f1 a c -> f2 b d
liftToSym2 a -> b
f s -> s
forall a. a -> a
id) (m1 (a, s) -> m2 (b, s)) -> m1 (a, s) -> m2 (b, s)
forall a b. (a -> b) -> a -> b
$ s -> m1 (a, s)
f1 s
s
  {-# INLINE liftToSym #-}

-- ReaderT
instance
  (ToSym s2 s1, ToSym1 m1 m2, ToSym a1 a2) =>
  ToSym (ReaderT s1 m1 a1) (ReaderT s2 m2 a2)
  where
  toSym :: ReaderT s1 m1 a1 -> ReaderT s2 m2 a2
toSym = ReaderT s1 m1 a1 -> ReaderT s2 m2 a2
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance
  (ToSym s2 s1, ToSym1 m1 m2, Mergeable1 m2) =>
  ToSym1 (ReaderT s1 m1) (ReaderT s2 m2)
  where
  liftToSym ::
    forall a b.
    (ToSym s2 s1, ToSym1 m1 m2, Mergeable1 m2, Mergeable b) =>
    (a -> b) ->
    ReaderT s1 m1 a ->
    ReaderT s2 m2 b
  liftToSym :: forall a b.
(ToSym s2 s1, ToSym1 m1 m2, Mergeable1 m2, Mergeable b) =>
(a -> b) -> ReaderT s1 m1 a -> ReaderT s2 m2 b
liftToSym a -> b
f (ReaderT s1 -> m1 a
f1) =
    forall (f :: * -> *) a r.
(Mergeable1 f, Mergeable a) =>
(Mergeable (f a) => r) -> r
resolveMergeable1 @m2 @b ((Mergeable (m2 b) => ReaderT s2 m2 b) -> ReaderT s2 m2 b)
-> (Mergeable (m2 b) => ReaderT s2 m2 b) -> ReaderT s2 m2 b
forall a b. (a -> b) -> a -> b
$
      (s2 -> m2 b) -> ReaderT s2 m2 b
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((s2 -> m2 b) -> ReaderT s2 m2 b)
-> (s2 -> m2 b) -> ReaderT s2 m2 b
forall a b. (a -> b) -> a -> b
$
        (m1 a -> m2 b) -> (s1 -> m1 a) -> s2 -> m2 b
forall b a. Mergeable b => (a -> b) -> (s1 -> a) -> s2 -> b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> m1 a -> m2 b
forall b a. Mergeable b => (a -> b) -> m1 a -> m2 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f) s1 -> m1 a
f1
  {-# INLINE liftToSym #-}

-- IdentityT
instance (ToSym1 m m1, ToSym a b) => ToSym (IdentityT m a) (IdentityT m1 b) where
  toSym :: IdentityT m a -> IdentityT m1 b
toSym = IdentityT m a -> IdentityT m1 b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance (ToSym1 m m1) => ToSym1 (IdentityT m) (IdentityT m1) where
  liftToSym :: forall b a.
Mergeable b =>
(a -> b) -> IdentityT m a -> IdentityT m1 b
liftToSym a -> b
f (IdentityT m a
v) = m1 b -> IdentityT m1 b
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m1 b -> IdentityT m1 b) -> m1 b -> IdentityT m1 b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> m a -> m1 b
forall b a. Mergeable b => (a -> b) -> m a -> m1 b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f m a
v
  {-# INLINE liftToSym #-}

-- Identity
instance {-# INCOHERENT #-} (ToSym a b) => ToSym (Identity a) (Identity b) where
  toSym :: Identity a -> Identity b
toSym = Identity a -> Identity b
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance {-# INCOHERENT #-} (ToSym a b) => ToSym a (Identity b) where
  toSym :: a -> Identity b
toSym = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> (a -> b) -> a -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
forall a b. ToSym a b => a -> b
toSym
  {-# INLINE toSym #-}

instance {-# INCOHERENT #-} (ToSym a b) => ToSym (Identity a) b where
  toSym :: Identity a -> b
toSym = a -> b
forall a b. ToSym a b => a -> b
toSym (a -> b) -> (Identity a -> a) -> Identity a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity
  {-# INLINE toSym #-}

instance ToSym1 Identity Identity where
  liftToSym :: forall b a. Mergeable b => (a -> b) -> Identity a -> Identity b
liftToSym a -> b
f (Identity a
v) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> b -> Identity b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
v
  {-# INLINE liftToSym #-}

-- Function
instance (ToSym b d, ToSym c a) => ToSym (a -> b) (c -> d) where
  toSym :: (a -> b) -> c -> d
toSym = (a -> b) -> c -> d
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToSym1 f1 f2, ToSym a b) =>
f1 a -> f2 b
toSym1
  {-# INLINE toSym #-}

instance (ToSym c a) => ToSym1 ((->) a) ((->) c) where
  liftToSym :: forall b a. Mergeable b => (a -> b) -> (a -> a) -> c -> b
liftToSym a -> b
l a -> a
f = a -> b
l (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f (a -> a) -> (c -> a) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> a
forall a b. ToSym a b => a -> b
toSym
  {-# INLINE liftToSym #-}

-- Product
deriving via
  (Default (Product l r a))
  instance
    (ToSym (l0 a0) (l a), ToSym (r0 a0) (r a)) =>
    ToSym (Product l0 r0 a0) (Product l r a)

deriving via
  (Default1 (Product l r))
  instance
    (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Product l0 r0) (Product l r)

-- Sum
deriving via
  (Default (Sum l r a))
  instance
    (ToSym (l0 a0) (l a), ToSym (r0 a0) (r a)) =>
    ToSym (Sum l0 r0 a0) (Sum l r a)

deriving via
  (Default1 (Sum l r))
  instance
    (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Sum l0 r0) (Sum l r)

-- Compose
deriving via
  (Default (Compose f g a))
  instance
    (ToSym (f0 (g0 a0)) (f (g a))) => ToSym (Compose f0 g0 a0) (Compose f g a)

instance
  (ToSym1 f0 f, ToSym1 g0 g) =>
  ToSym1 (Compose f0 g0) (Compose f g)
  where
  liftToSym ::
    forall a b.
    (ToSym1 f0 f, ToSym1 g0 g, Mergeable b) =>
    (a -> b) ->
    Compose f0 g0 a ->
    Compose f g b
  liftToSym :: forall a b.
(ToSym1 f0 f, ToSym1 g0 g, Mergeable b) =>
(a -> b) -> Compose f0 g0 a -> Compose f g b
liftToSym a -> b
f (Compose f0 (g0 a)
v) =
    forall (f :: * -> *) a r.
(Mergeable1 f, Mergeable a) =>
(Mergeable (f a) => r) -> r
resolveMergeable1 @g @b ((Mergeable (g b) => Compose f g b) -> Compose f g b)
-> (Mergeable (g b) => Compose f g b) -> Compose f g b
forall a b. (a -> b) -> a -> b
$ f (g b) -> Compose f g b
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g b) -> Compose f g b) -> f (g b) -> Compose f g b
forall a b. (a -> b) -> a -> b
$ (g0 a -> g b) -> f0 (g0 a) -> f (g b)
forall b a. Mergeable b => (a -> b) -> f0 a -> f b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym ((a -> b) -> g0 a -> g b
forall b a. Mergeable b => (a -> b) -> g0 a -> g b
forall (f1 :: * -> *) (f2 :: * -> *) b a.
(ToSym1 f1 f2, Mergeable b) =>
(a -> b) -> f1 a -> f2 b
liftToSym a -> b
f) f0 (g0 a)
v
  {-# INLINE liftToSym #-}

-- Const
deriving via
  (Default (Const a b))
  instance
    (ToSym a0 a) => ToSym (Const a0 b0) (Const a b)

deriving via
  (Default1 (Const a))
  instance
    (ToSym a0 a) => ToSym1 (Const a0) (Const a)

-- Alt
deriving via
  (Default (Alt f a))
  instance
    (ToSym (f0 a0) (f a)) => ToSym (Alt f0 a0) (Alt f a)

deriving via
  (Default1 (Alt f))
  instance
    (ToSym1 f0 f) => ToSym1 (Alt f0) (Alt f)

-- Ap
deriving via
  (Default (Ap f a))
  instance
    (ToSym (f0 a0) (f a)) => ToSym (Ap f0 a0) (Ap f a)

deriving via
  (Default1 (Ap f))
  instance
    (ToSym1 f0 f) => ToSym1 (Ap f0) (Ap f)

-- Generic
deriving via (Default (U1 p)) instance ToSym (U1 p0) (U1 p)

deriving via (Default (V1 p)) instance ToSym (V1 p0) (V1 p)

deriving via
  (Default (K1 i c p))
  instance
    (ToSym c0 c) => ToSym (K1 i0 c0 p0) (K1 i c p)

deriving via
  (Default (M1 i c f p))
  instance
    (ToSym (f0 p0) (f p)) => ToSym (M1 i0 c0 f0 p0) (M1 i c f p)

deriving via
  (Default ((f :+: g) p))
  instance
    (ToSym (f0 p0) (f p), ToSym (g0 p0) (g p)) =>
    ToSym ((f0 :+: g0) p0) ((f :+: g) p)

deriving via
  (Default ((f :*: g) p))
  instance
    (ToSym (f0 p0) (f p), ToSym (g0 p0) (g p)) =>
    ToSym ((f0 :*: g0) p0) ((f :*: g) p)

deriving via
  (Default (Par1 p))
  instance
    (ToSym p0 p) => ToSym (Par1 p0) (Par1 p)

deriving via
  (Default (Rec1 f p))
  instance
    (ToSym (f0 p0) (f p)) => ToSym (Rec1 f0 p0) (Rec1 f p)

deriving via
  (Default ((f :.: g) p))
  instance
    (ToSym (f0 (g0 p0)) (f (g p))) => ToSym ((f0 :.: g0) p0) ((f :.: g) p)

-- ToSym2
instance ToSym2 Either Either where
  liftToSym2 :: forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
liftToSym2 a -> b
f c -> d
_ (Left a
a) = b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> b -> Either b d
forall a b. (a -> b) -> a -> b
$ a -> b
f a
a
  liftToSym2 a -> b
_ c -> d
g (Right c
b) = d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> d -> Either b d
forall a b. (a -> b) -> a -> b
$ c -> d
g c
b
  {-# INLINE liftToSym2 #-}

instance ToSym2 (,) (,) where
  liftToSym2 :: forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
liftToSym2 a -> b
f c -> d
g (a
a, c
b) = (a -> b
f a
a, c -> d
g c
b)
  {-# INLINE liftToSym2 #-}

instance (ToSym a b) => ToSym2 ((,,) a) ((,,) b) where
  liftToSym2 :: forall a b c d. (a -> b) -> (c -> d) -> (a, a, c) -> (b, b, d)
liftToSym2 a -> b
f c -> d
g (a
a, a
b, c
c) = (a -> b
forall a b. ToSym a b => a -> b
toSym a
a, a -> b
f a
b, c -> d
g c
c)
  {-# INLINE liftToSym2 #-}

instance (ToSym a c, ToSym b d) => ToSym2 ((,,,) a b) ((,,,) c d) where
  liftToSym2 :: forall a b c d.
(a -> b) -> (c -> d) -> (a, b, a, c) -> (c, d, b, d)
liftToSym2 a -> b
f c -> d
g (a
a, b
b, a
c, c
d) = (a -> c
forall a b. ToSym a b => a -> b
toSym a
a, b -> d
forall a b. ToSym a b => a -> b
toSym b
b, a -> b
f a
c, c -> d
g c
d)
  {-# INLINE liftToSym2 #-}