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

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

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

import Data.Kind (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.SymPrim.Prim.Term
  ( IsSymbolKind,
    LinkedRep,
    SymbolKind,
    TypedSymbol,
  )
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 #-}