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

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SubstSym
-- 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.SubstSym
  ( -- * Substituting symbolic constants
    SubstSym (..),
    SubstSym1 (..),
    substSym1,
    SubstSym2 (..),
    substSym2,

    -- * Generic 'SubstSym'
    SubstSymArgs (..),
    GSubstSym (..),
    genericSubstSym,
    genericLiftSubstSym,
  )
where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    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.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default, unDefault),
    Default1 (Default1, unDefault1),
    Generic (Rep, from, to),
    Generic1 (Rep1, from1, to1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
import Grisette.Internal.SymPrim.GeneralFun (substTerm, type (-->))
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep (underlyingTerm),
    SupportedPrim,
    TypedSymbol,
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP
  ( SymFP (SymFP),
    SymFPRoundingMode (SymFPRoundingMode),
  )
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))
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

-- | Substitution of symbols (symbolic constants) to a symbolic value.
--
-- >>> a = "a" :: TypedSymbol Bool
-- >>> v = "x" .&& "y" :: SymBool
-- >>> substSym a v (["a" .&& "b", "a"] :: [SymBool])
-- [(&& (&& x y) b),(&& x y)]
--
-- __Note 1:__ This type class can be derived for algebraic data types.
-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.
--
-- > data X = ... deriving Generic deriving SubstSym via (Default X)
class SubstSym a where
  -- Substitute a symbolic constant to some symbolic value
  --
  -- >>> substSym "a" ("c" .&& "d" :: Sym Bool) ["a" .&& "b" :: Sym Bool, "a"]
  -- [(&& (&& c d) b),(&& c d)]
  substSym :: (LinkedRep cb sb) => TypedSymbol cb -> sb -> a -> a

-- | Lifting of 'SubstSym' to unary type constructors.
class
  (forall a. (SubstSym a) => SubstSym (f a)) =>
  SubstSym1 f
  where
  -- | Lift a symbol substitution function to unary type constructors.
  liftSubstSym ::
    (LinkedRep cb sb) =>
    (TypedSymbol cb -> sb -> a -> a) ->
    TypedSymbol cb ->
    sb ->
    f a ->
    f a

-- | Lifting the standard 'substSym' to unary type constructors.
substSym1 ::
  (SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
  TypedSymbol cb ->
  sb ->
  f a ->
  f a
substSym1 :: forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1 = (TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substSym

-- | Lifting of 'SubstSym' to binary type constructors.
class
  (forall a. (SubstSym a) => SubstSym1 (f a)) =>
  SubstSym2 f
  where
  -- | Lift a symbol substitution function to binary type constructors.
  liftSubstSym2 ::
    (LinkedRep cb sb) =>
    (TypedSymbol cb -> sb -> a -> a) ->
    (TypedSymbol cb -> sb -> b -> b) ->
    TypedSymbol cb ->
    sb ->
    f a b ->
    f a b

-- | Lifting the standard 'substSym' to binary type constructors.
substSym2 ::
  (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb) =>
  TypedSymbol cb ->
  sb ->
  f a b ->
  f a b
substSym2 :: forall (f :: * -> * -> *) a b cb sb.
(SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a b -> f a b
substSym2 = (TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> f a b
-> f a b
forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> f a b
-> f a b
forall (f :: * -> * -> *) cb sb a b.
(SubstSym2 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substSym TypedSymbol cb -> sb -> b -> b
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> b -> b
substSym

-- Derivations

-- | The arguments to the generic 'substSym' function.
data family SubstSymArgs arity a cb sb :: Type

data instance SubstSymArgs Arity0 _ _ _ = SubstSymArgs0

newtype instance SubstSymArgs Arity1 a cb sb
  = SubstSymArgs1 (TypedSymbol cb -> sb -> a -> a)

-- | The class of types where we can generically substitute the symbols in a
-- value.
class GSubstSym arity f where
  gsubstSym ::
    (LinkedRep cb sb) =>
    SubstSymArgs arity a cb sb ->
    TypedSymbol cb ->
    sb ->
    f a ->
    f a

instance GSubstSym arity V1 where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> V1 a -> V1 a
gsubstSym SubstSymArgs arity a cb sb
_ TypedSymbol cb
_ sb
_ = V1 a -> V1 a
forall a. a -> a
id
  {-# INLINE gsubstSym #-}

instance GSubstSym arity U1 where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> U1 a -> U1 a
gsubstSym SubstSymArgs arity a cb sb
_ TypedSymbol cb
_ sb
_ = U1 a -> U1 a
forall a. a -> a
id
  {-# INLINE gsubstSym #-}

instance (SubstSym a) => GSubstSym arity (K1 i a) where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb
-> TypedSymbol cb -> sb -> K1 i a a -> K1 i a a
gsubstSym SubstSymArgs arity a cb sb
_ TypedSymbol cb
sym sb
val (K1 a
v) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substSym TypedSymbol cb
sym sb
val a
v
  {-# INLINE gsubstSym #-}

instance (GSubstSym arity a) => GSubstSym arity (M1 i c a) where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb
-> TypedSymbol cb -> sb -> M1 i c a a -> M1 i c a a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val (M1 a a
v) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val a a
v
  {-# INLINE gsubstSym #-}

instance (GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :*: b) where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb
-> TypedSymbol cb -> sb -> (:*:) a b a -> (:*:) a b a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val (a a
a :*: b a
b) =
    SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val a a
a a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> b a -> b a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> b a -> b a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val b a
b
  {-# INLINE gsubstSym #-}

instance (GSubstSym arity a, GSubstSym arity b) => GSubstSym arity (a :+: b) where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb
-> TypedSymbol cb -> sb -> (:+:) a b a -> (:+:) a b a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val (L1 a a
l) = a a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> a a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val a a
l
  gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val (R1 b a
r) = b a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> b a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> b a -> b a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> b a -> b a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity a cb sb
args TypedSymbol cb
sym sb
val b a
r
  {-# INLINE gsubstSym #-}

instance (SubstSym1 a) => GSubstSym Arity1 (Rec1 a) where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity1 a cb sb
-> TypedSymbol cb -> sb -> Rec1 a a -> Rec1 a a
gsubstSym (SubstSymArgs1 TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val (Rec1 a a
v) =
    a a -> Rec1 a a
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (a a -> Rec1 a a) -> a a -> Rec1 a a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> a a -> a a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> a a -> a a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a a
v
  {-# INLINE gsubstSym #-}

instance GSubstSym Arity1 Par1 where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity1 a cb sb
-> TypedSymbol cb -> sb -> Par1 a -> Par1 a
gsubstSym (SubstSymArgs1 TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val (Par1 a
v) = a -> Par1 a
forall p. p -> Par1 p
Par1 (a -> Par1 a) -> a -> Par1 a
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a
v
  {-# INLINE gsubstSym #-}

instance
  (SubstSym1 f, GSubstSym Arity1 g) =>
  GSubstSym Arity1 (f :.: g)
  where
  gsubstSym :: forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity1 a cb sb
-> TypedSymbol cb -> sb -> (:.:) f g a -> (:.:) f g a
gsubstSym SubstSymArgs Arity1 a cb sb
targs TypedSymbol cb
sym sb
val (Comp1 f (g a)
x) =
    f (g a) -> (:.:) f g a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g a) -> (:.:) f g a) -> f (g a) -> (:.:) f g a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> g a -> g a)
-> TypedSymbol cb -> sb -> f (g a) -> f (g a)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym (SubstSymArgs Arity1 a cb sb -> TypedSymbol cb -> sb -> g a -> g a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity1 a cb sb -> TypedSymbol cb -> sb -> g a -> g a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs Arity1 a cb sb
targs) TypedSymbol cb
sym sb
val f (g a)
x
  {-# INLINE gsubstSym #-}

-- | Generic 'substSym' function.
genericSubstSym ::
  (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb) =>
  TypedSymbol cb ->
  sb ->
  a ->
  a
genericSubstSym :: forall a cb sb.
(Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
genericSubstSym TypedSymbol cb
sym sb
val =
  Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubstSymArgs Arity0 Any cb sb
-> TypedSymbol cb -> sb -> Rep a Any -> Rep a Any
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity0 a cb sb
-> TypedSymbol cb -> sb -> Rep a a -> Rep a a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym SubstSymArgs Arity0 Any cb sb
forall _ _ _. SubstSymArgs Arity0 _ _ _
SubstSymArgs0 TypedSymbol cb
sym sb
val (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> a -> Rep a 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 genericSubstSym #-}

-- | Generic 'liftSubstSym' function.
genericLiftSubstSym ::
  (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb) =>
  (TypedSymbol cb -> sb -> a -> a) ->
  TypedSymbol cb ->
  sb ->
  f a ->
  f a
genericLiftSubstSym :: forall (f :: * -> *) cb sb a.
(Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
genericLiftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val =
  Rep1 f a -> f a
forall a. Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f a -> f a) -> (f a -> Rep1 f a) -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubstSymArgs Arity1 a cb sb
-> TypedSymbol cb -> sb -> Rep1 f a -> Rep1 f a
forall cb sb a.
LinkedRep cb sb =>
SubstSymArgs Arity1 a cb sb
-> TypedSymbol cb -> sb -> Rep1 f a -> Rep1 f a
forall arity (f :: * -> *) cb sb a.
(GSubstSym arity f, LinkedRep cb sb) =>
SubstSymArgs arity a cb sb -> TypedSymbol cb -> sb -> f a -> f a
gsubstSym ((TypedSymbol cb -> sb -> a -> a) -> SubstSymArgs Arity1 a cb sb
forall a cb sb.
(TypedSymbol cb -> sb -> a -> a) -> SubstSymArgs Arity1 a cb sb
SubstSymArgs1 TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val (Rep1 f a -> Rep1 f a) -> (f a -> Rep1 f a) -> f a -> Rep1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1
{-# INLINE genericLiftSubstSym #-}

instance
  (Generic a, GSubstSym Arity0 (Rep a)) =>
  SubstSym (Default a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> Default a -> Default a
substSym TypedSymbol cb
sym sb
val = a -> Default a
forall a. a -> Default a
Default (a -> Default a) -> (Default a -> a) -> Default a -> Default a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
genericSubstSym TypedSymbol cb
sym sb
val (a -> a) -> (Default a -> a) -> Default a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault
  {-# INLINE substSym #-}

instance
  (Generic1 f, GSubstSym Arity1 (Rep1 f), SubstSym a) =>
  SubstSym (Default1 f a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> Default1 f a -> Default1 f a
substSym = TypedSymbol cb -> sb -> Default1 f a -> Default1 f a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (Generic1 f, GSubstSym Arity1 (Rep1 f)) =>
  SubstSym1 (Default1 f)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Default1 f a -> Default1 f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val =
    f a -> Default1 f a
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (f a -> Default1 f a)
-> (Default1 f a -> f a) -> Default1 f a -> Default1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb a.
(Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
genericLiftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (f a -> f a) -> (Default1 f a -> f a) -> Default1 f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default1 f a -> f a
forall (f :: * -> *) a. Default1 f a -> f a
unDefault1
  {-# INLINE liftSubstSym #-}

#define CONCRETE_SUBSTITUTESYM(type) \
instance SubstSym type where \
  substSym _ _ = id

#define CONCRETE_SUBSTITUTESYM_BV(type) \
instance (KnownNat n, 1 <= n) => SubstSym (type n) where \
  substSym _ _ = id

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

instance (ValidFP eb sb) => SubstSym (FP eb sb) where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> FP eb sb -> FP eb sb
substSym TypedSymbol cb
_ sb
_ = FP eb sb -> FP eb sb
forall a. a -> a
id

#define SUBSTITUTE_SYM_SIMPLE(symtype) \
instance SubstSym symtype where \
  substSym sym v (symtype t) = symtype $ substTerm sym (underlyingTerm v) t

#define SUBSTITUTE_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => SubstSym (symtype n) where \
  substSym sym v (symtype t) = symtype $ substTerm sym (underlyingTerm v) t

#define SUBSTITUTE_SYM_FUN(cop, op, cons) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  SubstSym (op sa sb) where \
  substSym sym v (cons t) = cons $ substTerm sym (underlyingTerm v) t

#if 1
SUBSTITUTE_SYM_SIMPLE(SymBool)
SUBSTITUTE_SYM_SIMPLE(SymInteger)
SUBSTITUTE_SYM_BV(SymIntN)
SUBSTITUTE_SYM_BV(SymWordN)
SUBSTITUTE_SYM_FUN((=->), (=~>), SymTabularFun)
SUBSTITUTE_SYM_FUN((-->), (-~>), SymGeneralFun)
SUBSTITUTE_SYM_SIMPLE(SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => SubstSym (SymFP eb sb) where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> SymFP eb sb -> SymFP eb sb
substSym TypedSymbol cb
sym sb
v (SymFP Term (FP eb sb)
t) = Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> Term cb -> Term (FP eb sb) -> Term (FP eb sb)
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol cb
sym (sb -> Term cb
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sb
v) Term (FP eb sb)
t

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

deriveBuiltins
  (ViaDefault1 ''SubstSym1)
  [''SubstSym, ''SubstSym1]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

-- ExceptT
instance
  (SubstSym1 m, SubstSym e, SubstSym a) =>
  SubstSym (ExceptT e m a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a
substSym = TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym e) =>
  SubstSym1 (ExceptT e m)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (ExceptT m (Either e a)
v) =
    m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (Either e a) -> ExceptT e m a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> Either e a -> Either e a)
-> TypedSymbol cb -> sb -> m (Either e a) -> m (Either e a)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Either e a -> Either e a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Either e a -> Either e a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val m (Either e a)
v
  {-# INLINE liftSubstSym #-}

-- MaybeT
instance
  (SubstSym1 m, SubstSym a) =>
  SubstSym (MaybeT m a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a
substSym = TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m) =>
  SubstSym1 (MaybeT m)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (MaybeT m (Maybe a)
v) =
    m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (Maybe a) -> MaybeT m a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> Maybe a -> Maybe a)
-> TypedSymbol cb -> sb -> m (Maybe a) -> m (Maybe a)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Maybe a -> Maybe a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Maybe a -> Maybe a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val m (Maybe a)
v
  {-# INLINE liftSubstSym #-}

-- WriterT
instance
  (SubstSym1 m, SubstSym a, SubstSym s) =>
  SubstSym (WriterLazy.WriterT s m a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
substSym = TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym s) =>
  SubstSym1 (WriterLazy.WriterT s m)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (WriterLazy.WriterT m (a, s)
v) =
    m (a, s) -> WriterT s m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m (a, s) -> WriterT s m a) -> m (a, s) -> WriterT s m a
forall a b. (a -> b) -> a -> b
$
      (TypedSymbol cb -> sb -> (a, s) -> (a, s))
-> TypedSymbol cb -> sb -> m (a, s) -> m (a, s)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> s -> s)
-> TypedSymbol cb
-> sb
-> (a, s)
-> (a, s)
forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> (a, b)
-> (a, b)
forall (f :: * -> * -> *) cb sb a b.
(SubstSym2 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> s -> s
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> s -> s
substSym) TypedSymbol cb
sym sb
val m (a, s)
v
  {-# INLINE liftSubstSym #-}

instance
  (SubstSym1 m, SubstSym a, SubstSym s) =>
  SubstSym (WriterStrict.WriterT s m a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
substSym = TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym s) =>
  SubstSym1 (WriterStrict.WriterT s m)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (WriterStrict.WriterT m (a, s)
v) =
    m (a, s) -> WriterT s m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m (a, s) -> WriterT s m a) -> m (a, s) -> WriterT s m a
forall a b. (a -> b) -> a -> b
$
      (TypedSymbol cb -> sb -> (a, s) -> (a, s))
-> TypedSymbol cb -> sb -> m (a, s) -> m (a, s)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> s -> s)
-> TypedSymbol cb
-> sb
-> (a, s)
-> (a, s)
forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> (a, b)
-> (a, b)
forall (f :: * -> * -> *) cb sb a b.
(SubstSym2 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> s -> s
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> s -> s
substSym) TypedSymbol cb
sym sb
val m (a, s)
v
  {-# INLINE liftSubstSym #-}

-- IdentityT
instance
  (SubstSym1 m, SubstSym a) =>
  SubstSym (IdentityT m a)
  where
  substSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a
substSym = TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a
forall (f :: * -> *) a cb sb.
(SubstSym1 f, SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance (SubstSym1 m) => SubstSym1 (IdentityT m) where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (IdentityT m a
a) =
    m a -> IdentityT m a
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val m a
a
  {-# INLINE liftSubstSym #-}

-- Product
deriving via
  (Default (Product l r a))
  instance
    (SubstSym (l a), SubstSym (r a)) => SubstSym (Product l r a)

deriving via
  (Default1 (Product l r))
  instance
    (SubstSym1 l, SubstSym1 r) => SubstSym1 (Product l r)

-- Sum
deriving via
  (Default (Sum l r a))
  instance
    (SubstSym (l a), SubstSym (r a)) => SubstSym (Sum l r a)

deriving via
  (Default1 (Sum l r))
  instance
    (SubstSym1 l, SubstSym1 r) => SubstSym1 (Sum l r)

-- Compose
deriving via
  (Default (Compose f g a))
  instance
    (SubstSym (f (g a))) => SubstSym (Compose f g a)

instance
  (SubstSym1 f, SubstSym1 g) =>
  SubstSym1 (Compose f g)
  where
  liftSubstSym :: forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> Compose f g a -> Compose f g a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val (Compose f (g a)
x) =
    f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g a) -> Compose f g a) -> f (g a) -> Compose f g a
forall a b. (a -> b) -> a -> b
$ (TypedSymbol cb -> sb -> g a -> g a)
-> TypedSymbol cb -> sb -> f (g a) -> f (g a)
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> g a -> g a
forall cb sb a.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> g a -> g a
forall (f :: * -> *) cb sb a.
(SubstSym1 f, LinkedRep cb sb) =>
(TypedSymbol cb -> sb -> a -> a)
-> TypedSymbol cb -> sb -> f a -> f a
liftSubstSym TypedSymbol cb -> sb -> a -> a
f) TypedSymbol cb
sym sb
val f (g a)
x
  {-# INLINE liftSubstSym #-}

-- Const
deriving via
  (Default (Const a b))
  instance
    (SubstSym a) => SubstSym (Const a b)

deriving via
  (Default1 (Const a))
  instance
    (SubstSym a) => SubstSym1 (Const a)

-- Alt
deriving via
  (Default (Alt f a))
  instance
    (SubstSym (f a)) => SubstSym (Alt f a)

deriving via
  (Default1 (Alt f))
  instance
    (SubstSym1 f) => SubstSym1 (Alt f)

-- Ap
deriving via
  (Default (Ap f a))
  instance
    (SubstSym (f a)) => SubstSym (Ap f a)

deriving via
  (Default1 (Ap f))
  instance
    (SubstSym1 f) => SubstSym1 (Ap f)

-- Generic
deriving via (Default (U1 p)) instance SubstSym (U1 p)

deriving via (Default (V1 p)) instance SubstSym (V1 p)

deriving via
  (Default (K1 i c p))
  instance
    (SubstSym c) => SubstSym (K1 i c p)

deriving via
  (Default (M1 i c f p))
  instance
    (SubstSym (f p)) => SubstSym (M1 i c f p)

deriving via
  (Default ((f :+: g) p))
  instance
    (SubstSym (f p), SubstSym (g p)) => SubstSym ((f :+: g) p)

deriving via
  (Default ((f :*: g) p))
  instance
    (SubstSym (f p), SubstSym (g p)) => SubstSym ((f :*: g) p)

deriving via
  (Default (Par1 p))
  instance
    (SubstSym p) => SubstSym (Par1 p)

deriving via
  (Default (Rec1 f p))
  instance
    (SubstSym (f p)) => SubstSym (Rec1 f p)

deriving via
  (Default ((f :.: g) p))
  instance
    (SubstSym (f (g p))) => SubstSym ((f :.: g) p)

-- SubstSym2
instance SubstSym2 Either where
  liftSubstSym2 :: forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> Either a b
-> Either a b
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> b -> b
_ TypedSymbol cb
sym sb
val (Left a
x) = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a
x
  liftSubstSym2 TypedSymbol cb -> sb -> a -> a
_ TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val (Right b
y) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val b
y
  {-# INLINE liftSubstSym2 #-}

instance SubstSym2 (,) where
  liftSubstSym2 :: forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> (a, b)
-> (a, b)
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val (a
x, b
y) = (TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a
x, TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val b
y)
  {-# INLINE liftSubstSym2 #-}

instance (SubstSym a) => SubstSym2 ((,,) a) where
  liftSubstSym2 :: forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> (a, a, b)
-> (a, a, b)
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val (a
x, a
y, b
z) =
    (TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substSym TypedSymbol cb
sym sb
val a
x, TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a
y, TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val b
z)
  {-# INLINE liftSubstSym2 #-}

instance (SubstSym a, SubstSym b) => SubstSym2 ((,,,) a b) where
  liftSubstSym2 :: forall cb sb a b.
LinkedRep cb sb =>
(TypedSymbol cb -> sb -> a -> a)
-> (TypedSymbol cb -> sb -> b -> b)
-> TypedSymbol cb
-> sb
-> (a, b, a, b)
-> (a, b, a, b)
liftSubstSym2 TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val (a
x, b
y, a
z, b
w) =
    (TypedSymbol cb -> sb -> a -> a
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
substSym TypedSymbol cb
sym sb
val a
x, TypedSymbol cb -> sb -> b -> b
forall a cb sb.
(SubstSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb. LinkedRep cb sb => TypedSymbol cb -> sb -> b -> b
substSym TypedSymbol cb
sym sb
val b
y, TypedSymbol cb -> sb -> a -> a
f TypedSymbol cb
sym sb
val a
z, TypedSymbol cb -> sb -> b -> b
g TypedSymbol cb
sym sb
val b
w)
  {-# INLINE liftSubstSym2 #-}