{-# 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.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)
import Grisette.Internal.SymPrim.GeneralFun (substTerm, type (-->))
import Grisette.Internal.SymPrim.Prim.Term
  ( IsSymbolKind,
    LinkedRep (underlyingTerm),
    SupportedPrim,
    SymbolKind,
    TypedSymbol,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
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" :: TypedAnySymbol 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, IsSymbolKind knd) =>
    TypedSymbol knd 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, IsSymbolKind knd) =>
    (TypedSymbol knd cb -> sb -> a -> a) ->
    TypedSymbol knd cb ->
    sb ->
    f a ->
    f a

-- | Lifting the standard 'substSym' to unary type constructors.
substSym1 ::
  (SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
  TypedSymbol knd cb ->
  sb ->
  f a ->
  f a
substSym1 :: forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1 = (TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd 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, IsSymbolKind knd) =>
    (TypedSymbol knd cb -> sb -> a -> a) ->
    (TypedSymbol knd cb -> sb -> b -> b) ->
    TypedSymbol knd 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, IsSymbolKind knd) =>
  TypedSymbol knd cb ->
  sb ->
  f a b ->
  f a b
substSym2 :: forall (f :: * -> * -> *) a b cb sb (knd :: SymbolKind).
(SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb,
 IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a b -> f a b
substSym2 = (TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> f a b
-> f a b
forall cb sb (knd :: SymbolKind) a b.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> f a b
-> f a b
forall (f :: * -> * -> *) cb sb (knd :: SymbolKind) a b.
(SubstSym2 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol knd cb -> sb -> a -> a
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
substSym TypedSymbol knd cb -> sb -> b -> b
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> b -> b
substSym

-- Derivations

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

data instance SubstSymArgs Arity0 _ _ _ _ = SubstSymArgs0

newtype instance SubstSymArgs Arity1 knd a cb sb
  = SubstSymArgs1 (TypedSymbol knd 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, IsSymbolKind knd) =>
    SubstSymArgs arity knd a cb sb ->
    TypedSymbol knd cb ->
    sb ->
    f a ->
    f a

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

instance GSubstSym arity U1 where
  gsubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> U1 a -> U1 a
gsubstSym SubstSymArgs arity knd a cb sb
_ TypedSymbol knd 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 (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> K1 i a a -> K1 i a a
gsubstSym SubstSymArgs arity knd a cb sb
_ TypedSymbol knd 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 knd cb -> sb -> a -> a
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
substSym TypedSymbol knd cb
sym sb
val a
v
  {-# INLINE gsubstSym #-}

instance (GSubstSym arity a) => GSubstSym arity (M1 i c a) where
  gsubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> M1 i c a a -> M1 i c a a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> (:*:) a b a -> (:*:) a b a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd cb
sym sb
val (a a
a :*: b a
b) =
    SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 knd a cb sb
-> TypedSymbol knd cb -> sb -> b a -> b a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> b a -> b a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> (:+:) a b a -> (:+:) a b a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> a a -> a a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd cb
sym sb
val a a
l
  gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd 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 knd a cb sb
-> TypedSymbol knd cb -> sb -> b a -> b a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> b a -> b a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs arity knd a cb sb
args TypedSymbol knd cb
sym sb
val b a
r
  {-# INLINE gsubstSym #-}

instance (SubstSym1 a) => GSubstSym Arity1 (Rec1 a) where
  gsubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> Rec1 a a -> Rec1 a a
gsubstSym (SubstSymArgs1 TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> a a -> a a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> a a -> a a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb
sym sb
val a a
v
  {-# INLINE gsubstSym #-}

instance GSubstSym Arity1 Par1 where
  gsubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> Par1 a -> Par1 a
gsubstSym (SubstSymArgs1 TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 knd cb -> sb -> a -> a
f TypedSymbol knd cb
sym sb
val a
v
  {-# INLINE gsubstSym #-}

instance
  (SubstSym1 f, GSubstSym Arity1 g) =>
  GSubstSym Arity1 (f :.: g)
  where
  gsubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> (:.:) f g a -> (:.:) f g a
gsubstSym SubstSymArgs Arity1 knd a cb sb
targs TypedSymbol knd 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 knd cb -> sb -> g a -> g a)
-> TypedSymbol knd cb -> sb -> f (g a) -> f (g a)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym (SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> g a -> g a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> g a -> g a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs Arity1 knd a cb sb
targs) TypedSymbol knd cb
sym sb
val f (g a)
x
  {-# INLINE gsubstSym #-}

-- | Generic 'substSym' function.
genericSubstSym ::
  (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb, IsSymbolKind knd) =>
  TypedSymbol knd cb ->
  sb ->
  a ->
  a
genericSubstSym :: forall a cb sb (knd :: SymbolKind).
(Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb,
 IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
genericSubstSym TypedSymbol knd 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 knd Any cb sb
-> TypedSymbol knd cb -> sb -> Rep a Any -> Rep a Any
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity0 knd a cb sb
-> TypedSymbol knd cb -> sb -> Rep a a -> Rep a a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym SubstSymArgs Arity0 knd Any cb sb
forall (_ :: SymbolKind) _ _ _. SubstSymArgs Arity0 _ _ _ _
SubstSymArgs0 TypedSymbol knd 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, IsSymbolKind knd) =>
  (TypedSymbol knd cb -> sb -> a -> a) ->
  TypedSymbol knd cb ->
  sb ->
  f a ->
  f a
genericLiftSubstSym :: forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb,
 IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
genericLiftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd a cb sb
-> TypedSymbol knd cb -> sb -> Rep1 f a -> Rep1 f a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs Arity1 knd a cb sb
-> TypedSymbol knd cb -> sb -> Rep1 f a -> Rep1 f a
forall arity (f :: * -> *) cb sb (knd :: SymbolKind) a.
(GSubstSym arity f, LinkedRep cb sb, IsSymbolKind knd) =>
SubstSymArgs arity knd a cb sb
-> TypedSymbol knd cb -> sb -> f a -> f a
gsubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> SubstSymArgs Arity1 knd a cb sb
forall (knd :: SymbolKind) a cb sb.
(TypedSymbol knd cb -> sb -> a -> a)
-> SubstSymArgs Arity1 knd a cb sb
SubstSymArgs1 TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> Default a -> Default a
substSym TypedSymbol knd 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 knd cb -> sb -> a -> a
forall a cb sb (knd :: SymbolKind).
(Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb,
 IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
genericSubstSym TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a
substSym = TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (Generic1 f, GSubstSym Arity1 (Rep1 f)) =>
  SubstSym1 (Default1 f)
  where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb,
 IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
genericLiftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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)
CONCRETE_SUBSTITUTESYM(AlgReal)
#endif

instance (ValidFP eb sb) => SubstSym (FP eb sb) where
  substSym :: forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> FP eb sb -> FP eb sb
substSym TypedSymbol knd 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_SIMPLE(SymAlgReal)
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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SymFP eb sb -> SymFP eb sb
substSym TypedSymbol knd 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 knd cb -> Term cb -> Term (FP eb sb) -> Term (FP eb sb)
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedSymbol knd 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,
    ''NotRepresentableFPError,
    ''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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> ExceptT e m a -> ExceptT e m a
substSym = TypedSymbol knd cb -> sb -> ExceptT e m a -> ExceptT e m a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym e) =>
  SubstSym1 (ExceptT e m)
  where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> ExceptT e m a -> ExceptT e m a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> Either e a -> Either e a)
-> TypedSymbol knd cb -> sb -> m (Either e a) -> m (Either e a)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Either e a -> Either e a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Either e a -> Either e a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> MaybeT m a -> MaybeT m a
substSym = TypedSymbol knd cb -> sb -> MaybeT m a -> MaybeT m a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m) =>
  SubstSym1 (MaybeT m)
  where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> MaybeT m a -> MaybeT m a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> Maybe a -> Maybe a)
-> TypedSymbol knd cb -> sb -> m (Maybe a) -> m (Maybe a)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Maybe a -> Maybe a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Maybe a -> Maybe a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
substSym = TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym s) =>
  SubstSym1 (WriterLazy.WriterT s m)
  where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> (a, s) -> (a, s))
-> TypedSymbol knd cb -> sb -> m (a, s) -> m (a, s)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> s -> s)
-> TypedSymbol knd cb
-> sb
-> (a, s)
-> (a, s)
forall cb sb (knd :: SymbolKind) a b.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> (a, b)
-> (a, b)
forall (f :: * -> * -> *) cb sb (knd :: SymbolKind) a b.
(SubstSym2 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb -> sb -> s -> s
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> s -> s
substSym) TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
substSym = TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance
  (SubstSym1 m, SubstSym s) =>
  SubstSym1 (WriterStrict.WriterT s m)
  where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> (a, s) -> (a, s))
-> TypedSymbol knd cb -> sb -> m (a, s) -> m (a, s)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> s -> s)
-> TypedSymbol knd cb
-> sb
-> (a, s)
-> (a, s)
forall cb sb (knd :: SymbolKind) a b.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> (a, b)
-> (a, b)
forall (f :: * -> * -> *) cb sb (knd :: SymbolKind) a b.
(SubstSym2 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> f a b
-> f a b
liftSubstSym2 TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb -> sb -> s -> s
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> s -> s
substSym) TypedSymbol knd 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 (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a
substSym = TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a
forall (f :: * -> *) a cb sb (knd :: SymbolKind).
(SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> f a -> f a
substSym1
  {-# INLINE substSym #-}

instance (SubstSym1 m) => SubstSym1 (IdentityT m) where
  liftSubstSym :: forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> m a -> m a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> Compose f g a -> Compose f g a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd 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 knd cb -> sb -> g a -> g a)
-> TypedSymbol knd cb -> sb -> f (g a) -> f (g a)
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym ((TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> g a -> g a
forall cb sb (knd :: SymbolKind) a.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> g a -> g a
forall (f :: * -> *) cb sb (knd :: SymbolKind) a.
(SubstSym1 f, LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> TypedSymbol knd cb -> sb -> f a -> f a
liftSubstSym TypedSymbol knd cb -> sb -> a -> a
f) TypedSymbol knd 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 (knd :: SymbolKind) a b.
(LinkedRep cb sb, IsSymbolKind knd) =>
(TypedSymbol knd cb -> sb -> a -> a)
-> (TypedSymbol knd cb -> sb -> b -> b)
-> TypedSymbol knd cb
-> sb
-> Either a b
-> Either a b
liftSubstSym2 TypedSymbol knd cb -> sb -> a -> a
f TypedSymbol knd cb -> sb -> b -> b
_ TypedSymbol knd 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 knd cb -> sb -> a -> a
f TypedSymbol knd cb
sym sb
val a
x
  liftSubstSym2 TypedSymbol knd cb -> sb -> a -> a
_ TypedSymbol knd cb -> sb -> b -> b
g TypedSymbol knd 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 knd cb -> sb -> b -> b
g TypedSymbol knd cb
sym sb
val b
y
  {-# INLINE liftSubstSym2 #-}

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

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

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