{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.ToCon
-- 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.Core.Data.Class.ToCon
  ( -- * Converting to concrete values
    ToCon (..),
    ToCon1 (..),
    toCon1,
    ToCon2 (..),
    toCon2,

    -- * Generic 'ToCon'
    ToConArgs (..),
    GToCon (..),
    genericToCon,
    genericLiftToCon,
  )
where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity, runIdentity),
    IdentityT (IdentityT),
  )
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 qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics
  ( 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 GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving (Default (Default), Default1 (Default1))
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (conView),
    pattern Con,
  )
import Grisette.Internal.SymPrim.BV
  ( IntN (IntN),
    WordN (WordN),
  )
import Grisette.Internal.SymPrim.FP (FP, FP32, FP64, FPRoundingMode, ValidFP)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.IntBitwidth (intBitwidthQ)
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep,
    SupportedPrim,
  )
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.Core
-- >>> import Grisette.SymPrim

-- | Convert a symbolic value to concrete value if possible.
class ToCon a b where
  -- | Convert a symbolic value to concrete value if possible.
  -- If the symbolic value cannot be converted to concrete, the result will be 'Nothing'.
  --
  -- >>> toCon (ssym "a" :: SymInteger) :: Maybe Integer
  -- Nothing
  --
  -- >>> toCon (con 1 :: SymInteger) :: Maybe Integer
  -- Just 1
  --
  -- 'toCon' works on complex types too.
  --
  -- >>> toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]
  -- Just [1,2]
  --
  -- >>> toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]
  -- Nothing
  toCon :: a -> Maybe b

instance {-# INCOHERENT #-} ToCon v v where
  toCon :: v -> Maybe v
toCon = v -> Maybe v
forall v. v -> Maybe v
Just

-- | Lifting of 'ToCon' to unary type constructors.
class (forall a b. (ToCon a b) => ToCon (f1 a) (f2 b)) => ToCon1 f1 f2 where
  -- | Lift a conversion to concrete function to unary type constructors.
  liftToCon :: (a -> Maybe b) -> f1 a -> Maybe (f2 b)

-- | Lift the standard 'toCon' to unary type constructors.
toCon1 :: (ToCon1 f1 f2, ToCon a b) => f1 a -> Maybe (f2 b)
toCon1 :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1 = (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon
{-# INLINE toCon1 #-}

-- | Lifting of 'ToCon' to binary type constructors.
class (forall a b. (ToCon a b) => ToCon1 (f1 a) (f2 b)) => ToCon2 f1 f2 where
  -- | Lift conversion to concrete functions to binary type constructors.
  liftToCon2 :: (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)

-- | Lift the standard 'toCon' to binary type constructors.
toCon2 :: (ToCon2 f1 f2, ToCon a b, ToCon c d) => f1 a c -> Maybe (f2 b d)
toCon2 :: forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
(ToCon2 f1 f2, ToCon a b, ToCon c d) =>
f1 a c -> Maybe (f2 b d)
toCon2 = (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToCon2 f1 f2 =>
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
liftToCon2 a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon c -> Maybe d
forall a b. ToCon a b => a -> Maybe b
toCon
{-# INLINE toCon2 #-}

-- Derivations

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

data instance ToConArgs Arity0 _ _ = ToConArgs0

newtype instance ToConArgs Arity1 a b
  = ToConArgs1 (a -> Maybe b)

-- | The class of types that can be generically converted to concrete values.
class GToCon arity f1 f2 where
  gtoCon :: ToConArgs arity a b -> f1 a -> Maybe (f2 b)

instance GToCon arity V1 V1 where
  gtoCon :: forall a b. ToConArgs arity a b -> V1 a -> Maybe (V1 b)
gtoCon ToConArgs arity a b
_ V1 a
_ = [Char] -> Maybe (V1 b)
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"
  {-# INLINE gtoCon #-}

instance GToCon arity U1 U1 where
  gtoCon :: forall a b. ToConArgs arity a b -> U1 a -> Maybe (U1 b)
gtoCon ToConArgs arity a b
_ U1 a
_ = U1 b -> Maybe (U1 b)
forall v. v -> Maybe v
Just U1 b
forall k (p :: k). U1 p
U1
  {-# INLINE gtoCon #-}

instance
  (GToCon arity a b, GToCon arity c d) =>
  GToCon arity (a :*: c) (b :*: d)
  where
  gtoCon :: forall a b.
ToConArgs arity a b -> (:*:) a c a -> Maybe ((:*:) b d b)
gtoCon ToConArgs arity a b
args (a a
a :*: c a
c) = do
    b b
a' <- ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
    d b
c' <- ToConArgs arity a b -> c a -> Maybe (d b)
forall a b. ToConArgs arity a b -> c a -> Maybe (d b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args c a
c
    (:*:) b d b -> Maybe ((:*:) b d b)
forall v. v -> Maybe v
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) b d b -> Maybe ((:*:) b d b))
-> (:*:) b d b -> Maybe ((:*:) b d b)
forall a b. (a -> b) -> a -> b
$ b b
a' b b -> d b -> (:*:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: d b
c'
  {-# INLINE gtoCon #-}

instance
  (GToCon arity a b, GToCon arity c d) =>
  GToCon arity (a :+: c) (b :+: d)
  where
  gtoCon :: forall a b.
ToConArgs arity a b -> (:+:) a c a -> Maybe ((:+:) b d b)
gtoCon ToConArgs 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) -> Maybe (b b) -> Maybe ((:+:) b d b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
  gtoCon ToConArgs arity a b
args (R1 c a
a) = d b -> (:+:) b d b
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (d b -> (:+:) b d b) -> Maybe (d b) -> Maybe ((:+:) b d b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> c a -> Maybe (d b)
forall a b. ToConArgs arity a b -> c a -> Maybe (d b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args c a
a
  {-# INLINE gtoCon #-}

instance (GToCon arity a b) => GToCon arity (M1 i c1 a) (M1 i c2 b) where
  gtoCon :: forall a b.
ToConArgs arity a b -> M1 i c1 a a -> Maybe (M1 i c2 b b)
gtoCon ToConArgs arity a b
args (M1 a a
a) = b b -> M1 i c2 b b
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (b b -> M1 i c2 b b) -> Maybe (b b) -> Maybe (M1 i c2 b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToConArgs arity a b -> a a -> Maybe (b b)
forall a b. ToConArgs arity a b -> a a -> Maybe (b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs arity a b
args a a
a
  {-# INLINE gtoCon #-}

instance (ToCon a b) => GToCon arity (K1 i a) (K1 i b) where
  gtoCon :: forall a b. ToConArgs arity a b -> K1 i a a -> Maybe (K1 i b b)
gtoCon ToConArgs 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) -> Maybe b -> Maybe (K1 i b b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
a
  {-# INLINE gtoCon #-}

instance GToCon Arity1 Par1 Par1 where
  gtoCon :: forall a b. ToConArgs Arity1 a b -> Par1 a -> Maybe (Par1 b)
gtoCon (ToConArgs1 a -> Maybe b
f) (Par1 a
a) = b -> Par1 b
forall p. p -> Par1 p
Par1 (b -> Par1 b) -> Maybe b -> Maybe (Par1 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a
  {-# INLINE gtoCon #-}

instance (ToCon1 f1 f2) => GToCon Arity1 (Rec1 f1) (Rec1 f2) where
  gtoCon :: forall a b. ToConArgs Arity1 a b -> Rec1 f1 a -> Maybe (Rec1 f2 b)
gtoCon (ToConArgs1 a -> Maybe 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) -> Maybe (f2 b) -> Maybe (Rec1 f2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f f1 a
a
  {-# INLINE gtoCon #-}

instance
  (ToCon1 f1 f2, GToCon Arity1 g1 g2) =>
  GToCon Arity1 (f1 :.: g1) (f2 :.: g2)
  where
  gtoCon :: forall a b.
ToConArgs Arity1 a b -> (:.:) f1 g1 a -> Maybe ((:.:) f2 g2 b)
gtoCon ToConArgs Arity1 a b
targs (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)
-> Maybe (f2 (g2 b)) -> Maybe ((:.:) f2 g2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g1 a -> Maybe (g2 b)) -> f1 (g1 a) -> Maybe (f2 (g2 b))
forall a b. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon (ToConArgs Arity1 a b -> g1 a -> Maybe (g2 b)
forall a b. ToConArgs Arity1 a b -> g1 a -> Maybe (g2 b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs Arity1 a b
targs) f1 (g1 a)
a
  {-# INLINE gtoCon #-}

-- | Generic 'toCon' function.
genericToCon ::
  (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
  a ->
  Maybe b
genericToCon :: forall a b.
(Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
a -> Maybe b
genericToCon = (Rep b Any -> b) -> Maybe (Rep b Any) -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep b Any -> b
forall a x. Generic a => Rep a x -> a
forall x. Rep b x -> b
to (Maybe (Rep b Any) -> Maybe b)
-> (a -> Maybe (Rep b Any)) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToConArgs Arity0 Any Any -> Rep a Any -> Maybe (Rep b Any)
forall a b. ToConArgs Arity0 a b -> Rep a a -> Maybe (Rep b b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ToConArgs Arity0 Any Any
forall _ _. ToConArgs Arity0 _ _
ToConArgs0 (Rep a Any -> Maybe (Rep b Any))
-> (a -> Rep a Any) -> a -> Maybe (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 genericToCon #-}

-- | Generic 'liftToCon' function.
genericLiftToCon ::
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
  (a -> Maybe b) ->
  f1 a ->
  Maybe (f2 b)
genericLiftToCon :: forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
genericLiftToCon a -> Maybe b
f = (Rep1 f2 b -> f2 b) -> Maybe (Rep1 f2 b) -> Maybe (f2 b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 (Maybe (Rep1 f2 b) -> Maybe (f2 b))
-> (f1 a -> Maybe (Rep1 f2 b)) -> f1 a -> Maybe (f2 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToConArgs Arity1 a b -> Rep1 f1 a -> Maybe (Rep1 f2 b)
forall a b. ToConArgs Arity1 a b -> Rep1 f1 a -> Maybe (Rep1 f2 b)
forall arity (f1 :: * -> *) (f2 :: * -> *) a b.
GToCon arity f1 f2 =>
ToConArgs arity a b -> f1 a -> Maybe (f2 b)
gtoCon ((a -> Maybe b) -> ToConArgs Arity1 a b
forall a b. (a -> Maybe b) -> ToConArgs Arity1 a b
ToConArgs1 a -> Maybe b
f) (Rep1 f1 a -> Maybe (Rep1 f2 b))
-> (f1 a -> Rep1 f1 a) -> f1 a -> Maybe (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 genericLiftToCon #-}

instance
  (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
  ToCon a (Default b)
  where
  toCon :: a -> Maybe (Default b)
toCon = (b -> Default b) -> Maybe b -> Maybe (Default b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Default b
forall a. a -> Default a
Default (Maybe b -> Maybe (Default b))
-> (a -> Maybe b) -> a -> Maybe (Default b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
forall a b.
(Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) =>
a -> Maybe b
genericToCon
  {-# INLINE toCon #-}

instance
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2), ToCon a b) =>
  ToCon (f1 a) (Default1 f2 b)
  where
  toCon :: f1 a -> Maybe (Default1 f2 b)
toCon = f1 a -> Maybe (Default1 f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1

instance
  (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
  ToCon1 f1 (Default1 f2)
  where
  liftToCon :: forall a b. (a -> Maybe b) -> f1 a -> Maybe (Default1 f2 b)
liftToCon a -> Maybe b
f = (f2 b -> Default1 f2 b) -> Maybe (f2 b) -> Maybe (Default1 f2 b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f2 b -> Default1 f2 b
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (Maybe (f2 b) -> Maybe (Default1 f2 b))
-> (f1 a -> Maybe (f2 b)) -> f1 a -> Maybe (Default1 f2 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe b) -> f1 a -> Maybe (f2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
genericLiftToCon a -> Maybe b
f
  {-# INLINE liftToCon #-}

#define CONCRETE_TOCON(type) \
instance ToCon type type where \
  toCon = Just

#define CONCRETE_TOCON_BV(type) \
instance (KnownNat n, 1 <= n) => ToCon (type n) (type n) where \
  toCon = Just

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

instance (ValidFP eb sb) => ToCon (FP eb sb) (FP eb sb) where
  toCon :: FP eb sb -> Maybe (FP eb sb)
toCon = FP eb sb -> Maybe (FP eb sb)
forall v. v -> Maybe v
Just

#define TO_CON_SYMID_SIMPLE(symtype) \
instance ToCon symtype symtype where \
  toCon = Just

#define TO_CON_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (symtype n) where \
  toCon = Just

#define TO_CON_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToCon (a op b) (a op b) where \
  toCon = Just

#if 1
TO_CON_SYMID_SIMPLE(SymBool)
TO_CON_SYMID_SIMPLE(SymInteger)
TO_CON_SYMID_BV(SymIntN)
TO_CON_SYMID_BV(SymWordN)
TO_CON_SYMID_FUN(=~>)
TO_CON_SYMID_FUN(-~>)
TO_CON_SYMID_SIMPLE(SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToCon (SymFP eb sb) (SymFP eb sb) where
  toCon :: SymFP eb sb -> Maybe (SymFP eb sb)
toCon = SymFP eb sb -> Maybe (SymFP eb sb)
forall v. v -> Maybe v
Just

#define TO_CON_FROMSYM_SIMPLE(contype, symtype) \
instance ToCon symtype contype where \
  toCon = conView

#define TO_CON_FROMSYM_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (contype n) where \
  toCon = conView

#define TO_CON_FROMSYM_FUN(conop, symop) \
instance (SupportedPrim (conop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  ToCon (symop sa sb) (conop ca cb) where \
  toCon = conView

#if 1
TO_CON_FROMSYM_SIMPLE(Bool, SymBool)
TO_CON_FROMSYM_SIMPLE(Integer, SymInteger)
TO_CON_FROMSYM_BV(IntN, SymIntN)
TO_CON_FROMSYM_BV(WordN, SymWordN)
TO_CON_FROMSYM_FUN((=->), (=~>))
TO_CON_FROMSYM_FUN((-->), (-~>))
TO_CON_FROMSYM_SIMPLE(FPRoundingMode, SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToCon (SymFP eb sb) (FP eb sb) where
  toCon :: SymFP eb sb -> Maybe (FP eb sb)
toCon = SymFP eb sb -> Maybe (FP eb sb)
forall c t. Solvable c t => t -> Maybe c
conView

#define TOCON_MACHINE_INTEGER(sbvw, bvw, n, int) \
instance ToCon (sbvw n) int where \
  toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
  toCon _ = Nothing

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

instance ToCon SymFP32 Float where
  toCon :: SymFP32 -> Maybe Float
toCon (Con (FP32
fp :: FP32)) = Float -> Maybe Float
forall v. v -> Maybe v
Just (Float -> Maybe Float) -> Float -> Maybe Float
forall a b. (a -> b) -> a -> b
$ FP32 -> Float
forall from to. BitCast from to => from -> to
bitCast FP32
fp
  toCon SymFP32
_ = Maybe Float
forall a. Maybe a
Nothing

instance ToCon SymFP64 Double where
  toCon :: SymFP64 -> Maybe Double
toCon (Con (FP64
fp :: FP64)) = Double -> Maybe Double
forall v. v -> Maybe v
Just (Double -> Maybe Double) -> Double -> Maybe Double
forall a b. (a -> b) -> a -> b
$ FP64 -> Double
forall from to. BitCast from to => from -> to
bitCast FP64
fp
  toCon SymFP64
_ = Maybe Double
forall a. Maybe a
Nothing

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

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

-- ExceptT
instance
  (ToCon1 m1 m2, ToCon e1 e2, ToCon a b) =>
  ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b)
  where
  toCon :: ExceptT e1 m1 a -> Maybe (ExceptT e2 m2 b)
toCon = ExceptT e1 m1 a -> Maybe (ExceptT e2 m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1
  {-# INLINE toCon #-}

instance
  (ToCon1 m1 m2, ToCon e1 e2) =>
  ToCon1 (ExceptT e1 m1) (ExceptT e2 m2)
  where
  liftToCon :: forall a b.
(a -> Maybe b) -> ExceptT e1 m1 a -> Maybe (ExceptT e2 m2 b)
liftToCon a -> Maybe 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)
-> Maybe (m2 (Either e2 b)) -> Maybe (ExceptT e2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Either e1 a -> Maybe (Either e2 b))
-> m1 (Either e1 a) -> Maybe (m2 (Either e2 b))
forall a b. (a -> Maybe b) -> m1 a -> Maybe (m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon ((a -> Maybe b) -> Either e1 a -> Maybe (Either e2 b)
forall a b. (a -> Maybe b) -> Either e1 a -> Maybe (Either e2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f) m1 (Either e1 a)
v
  {-# INLINE liftToCon #-}

-- MaybeT
instance
  (ToCon1 m1 m2, ToCon a b) =>
  ToCon (MaybeT m1 a) (MaybeT m2 b)
  where
  toCon :: MaybeT m1 a -> Maybe (MaybeT m2 b)
toCon = MaybeT m1 a -> Maybe (MaybeT m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1
  {-# INLINE toCon #-}

instance
  (ToCon1 m1 m2) =>
  ToCon1 (MaybeT m1) (MaybeT m2)
  where
  liftToCon :: forall a b. (a -> Maybe b) -> MaybeT m1 a -> Maybe (MaybeT m2 b)
liftToCon a -> Maybe 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)
-> Maybe (m2 (Maybe b)) -> Maybe (MaybeT m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe a -> Maybe (Maybe b))
-> m1 (Maybe a) -> Maybe (m2 (Maybe b))
forall a b. (a -> Maybe b) -> m1 a -> Maybe (m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon ((a -> Maybe b) -> Maybe a -> Maybe (Maybe b)
forall a b. (a -> Maybe b) -> Maybe a -> Maybe (Maybe b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f) m1 (Maybe a)
v
  {-# INLINE liftToCon #-}

-- WriterT
instance
  (ToCon1 m1 m2, ToCon a b, ToCon s1 s2) =>
  ToCon (WriterLazy.WriterT s1 m1 a) (WriterLazy.WriterT s2 m2 b)
  where
  toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
toCon (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)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (a, s1)
v

instance
  (ToCon1 m1 m2, ToCon s1 s2) =>
  ToCon1 (WriterLazy.WriterT s1 m1) (WriterLazy.WriterT s2 m2)
  where
  liftToCon :: forall a b.
(a -> Maybe b) -> WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
liftToCon a -> Maybe 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)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((a, s1) -> Maybe (b, s2)) -> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. (a -> Maybe b) -> m1 a -> Maybe (m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon ((a -> Maybe b) -> (s1 -> Maybe s2) -> (a, s1) -> Maybe (b, s2)
forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> (a, c) -> Maybe (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToCon2 f1 f2 =>
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
liftToCon2 a -> Maybe b
f s1 -> Maybe s2
forall a b. ToCon a b => a -> Maybe b
toCon) m1 (a, s1)
v

instance
  (ToCon1 m1 m2, ToCon a b, ToCon s1 s2) =>
  ToCon (WriterStrict.WriterT s1 m1 a) (WriterStrict.WriterT s2 m2 b)
  where
  toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
toCon (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)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (a, s1)
v

instance
  (ToCon1 m1 m2, ToCon s1 s2) =>
  ToCon1 (WriterStrict.WriterT s1 m1) (WriterStrict.WriterT s2 m2)
  where
  liftToCon :: forall a b.
(a -> Maybe b) -> WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
liftToCon a -> Maybe 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)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((a, s1) -> Maybe (b, s2)) -> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. (a -> Maybe b) -> m1 a -> Maybe (m2 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon ((a -> Maybe b) -> (s1 -> Maybe s2) -> (a, s1) -> Maybe (b, s2)
forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> (a, c) -> Maybe (b, d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
ToCon2 f1 f2 =>
(a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
liftToCon2 a -> Maybe b
f s1 -> Maybe s2
forall a b. ToCon a b => a -> Maybe b
toCon) m1 (a, s1)
v

-- IdentityT
instance
  (ToCon1 m m1, ToCon a b) =>
  ToCon (IdentityT m a) (IdentityT m1 b)
  where
  toCon :: IdentityT m a -> Maybe (IdentityT m1 b)
toCon = IdentityT m a -> Maybe (IdentityT m1 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1
  {-# INLINE toCon #-}

instance
  (ToCon1 m m1) =>
  ToCon1 (IdentityT m) (IdentityT m1)
  where
  liftToCon :: forall a b.
(a -> Maybe b) -> IdentityT m a -> Maybe (IdentityT m1 b)
liftToCon a -> Maybe b
f (IdentityT m a
a) = m1 b -> IdentityT m1 b
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m1 b -> IdentityT m1 b) -> Maybe (m1 b) -> Maybe (IdentityT m1 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Maybe b) -> m a -> Maybe (m1 b)
forall a b. (a -> Maybe b) -> m a -> Maybe (m1 b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f m a
a
  {-# INLINE liftToCon #-}

-- Identity
instance {-# INCOHERENT #-} (ToCon a b) => ToCon (Identity a) (Identity b) where
  toCon :: Identity a -> Maybe (Identity b)
toCon = Identity a -> Maybe (Identity b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1

instance {-# INCOHERENT #-} (ToCon a b) => ToCon (Identity a) b where
  toCon :: Identity a -> Maybe b
toCon = a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon (a -> Maybe b) -> (Identity a -> a) -> Identity a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity

instance {-# INCOHERENT #-} (ToCon a b) => ToCon a (Identity b) where
  toCon :: a -> Maybe (Identity b)
toCon = (b -> Identity b) -> Maybe b -> Maybe (Identity b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Identity b
forall a. a -> Identity a
Identity (Maybe b -> Maybe (Identity b))
-> (a -> Maybe b) -> a -> Maybe (Identity b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon

instance ToCon1 Identity Identity where
  liftToCon :: forall a b. (a -> Maybe b) -> Identity a -> Maybe (Identity b)
liftToCon a -> Maybe b
f (Identity a
a) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> Maybe b -> Maybe (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a

-- Special
instance
  (ToCon (m1 (Either e1 a)) (Either e2 b)) =>
  ToCon (ExceptT e1 m1 a) (Either e2 b)
  where
  toCon :: ExceptT e1 m1 a -> Maybe (Either e2 b)
toCon (ExceptT m1 (Either e1 a)
v) = m1 (Either e1 a) -> Maybe (Either e2 b)
forall a b. ToCon a b => a -> Maybe b
toCon m1 (Either e1 a)
v

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

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

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

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

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

instance
  (ToCon1 f0 f, ToCon1 g0 g) =>
  ToCon1 (Compose f0 g0) (Compose f g)
  where
  liftToCon :: forall a b.
(a -> Maybe b) -> Compose f0 g0 a -> Maybe (Compose f g b)
liftToCon a -> Maybe b
f (Compose f0 (g0 a)
a) = 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)
-> Maybe (f (g b)) -> Maybe (Compose f g b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (g0 a -> Maybe (g b)) -> f0 (g0 a) -> Maybe (f (g b))
forall a b. (a -> Maybe b) -> f0 a -> Maybe (f b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon ((a -> Maybe b) -> g0 a -> Maybe (g b)
forall a b. (a -> Maybe b) -> g0 a -> Maybe (g b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
ToCon1 f1 f2 =>
(a -> Maybe b) -> f1 a -> Maybe (f2 b)
liftToCon a -> Maybe b
f) f0 (g0 a)
a
  {-# INLINE liftToCon #-}

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

deriving via
  (Default1 (Const a))
  instance
    (ToCon a0 a) => ToCon1 (Const a0) (Const a)

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

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

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

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

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

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

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

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

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

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

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

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

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

-- ToCon2
instance ToCon2 Either Either where
  liftToCon2 :: forall a b c d.
(a -> Maybe b)
-> (c -> Maybe d) -> Either a c -> Maybe (Either b d)
liftToCon2 a -> Maybe b
f c -> Maybe d
_ (Left a
a) = b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> Maybe b -> Maybe (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a
  liftToCon2 a -> Maybe b
_ c -> Maybe d
g (Right c
b) = d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> Maybe d -> Maybe (Either b d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Maybe d
g c
b
  {-# INLINE liftToCon2 #-}

instance ToCon2 (,) (,) where
  liftToCon2 :: forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> (a, c) -> Maybe (b, d)
liftToCon2 a -> Maybe b
f c -> Maybe d
g (a
a, c
b) = (,) (b -> d -> (b, d)) -> Maybe b -> Maybe (d -> (b, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
f a
a Maybe (d -> (b, d)) -> Maybe d -> Maybe (b, d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Maybe d
g c
b
  {-# INLINE liftToCon2 #-}

instance (ToCon a b) => ToCon2 ((,,) a) ((,,) b) where
  liftToCon2 :: forall a b c d.
(a -> Maybe b) -> (c -> Maybe d) -> (a, a, c) -> Maybe (b, b, d)
liftToCon2 a -> Maybe b
f c -> Maybe d
g (a
a, a
b, c
c) = (,,) (b -> b -> d -> (b, b, d))
-> Maybe b -> Maybe (b -> d -> (b, b, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
a Maybe (b -> d -> (b, b, d)) -> Maybe b -> Maybe (d -> (b, b, d))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> Maybe b
f a
b Maybe (d -> (b, b, d)) -> Maybe d -> Maybe (b, b, d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Maybe d
g c
c
  {-# INLINE liftToCon2 #-}

instance (ToCon a c, ToCon b d) => ToCon2 ((,,,) a b) ((,,,) c d) where
  liftToCon2 :: forall a b c d.
(a -> Maybe b)
-> (c -> Maybe d) -> (a, b, a, c) -> Maybe (c, d, b, d)
liftToCon2 a -> Maybe b
f c -> Maybe d
g (a
a, b
b, a
c, c
d) = (,,,) (c -> d -> b -> d -> (c, d, b, d))
-> Maybe c -> Maybe (d -> b -> d -> (c, d, b, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe c
forall a b. ToCon a b => a -> Maybe b
toCon a
a Maybe (d -> b -> d -> (c, d, b, d))
-> Maybe d -> Maybe (b -> d -> (c, d, b, d))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> Maybe d
forall a b. ToCon a b => a -> Maybe b
toCon b
b Maybe (b -> d -> (c, d, b, d))
-> Maybe b -> Maybe (d -> (c, d, b, d))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> Maybe b
f a
c Maybe (d -> (c, d, b, d)) -> Maybe d -> Maybe (c, d, b, d)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> c -> Maybe d
g c
d
  {-# INLINE liftToCon2 #-}