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

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Data.Class.ExtractSym
-- 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.ExtractSym
  ( -- * Extracting symbolic constant set from a value
    ExtractSym (..),
    ExtractSym1 (..),
    extractSymMaybe1,
    extractSym1,
    ExtractSym2 (..),
    extractSymMaybe2,
    extractSym2,

    -- * Generic 'ExtractSym'
    ExtractSymArgs (..),
    GExtractSym (..),
    genericExtractSymMaybe,
    genericLiftExtractSymMaybe,
  )
where

import Data.Kind (Type)
import Data.Maybe (fromJust)
import Generics.Deriving
  ( Default (unDefault),
    Default1 (unDefault1),
    Generic (Rep, from),
    Generic1 (Rep1, from1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
    type (:.:) (Comp1),
  )
import Grisette.Internal.SymPrim.Prim.Model
  ( AnySymbolSet,
    SymbolSet,
  )
import Grisette.Internal.SymPrim.Prim.Term (IsSymbolKind, SymbolKind)
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Lib.Base
-- >>> import Data.HashSet as HashSet
-- >>> import Data.List (sort)

-- | Extracts all the symbols (symbolic constants) that are transitively
-- contained in the given value.
--
-- >>> extractSym ("a" :: SymBool)
-- SymbolSet {a :: Bool}
--
-- >>> extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool])
-- SymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}
--
-- __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 ExtractSym via (Default X)
class ExtractSym a where
  extractSym :: a -> AnySymbolSet
  extractSym = Maybe AnySymbolSet -> AnySymbolSet
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe AnySymbolSet -> AnySymbolSet)
-> (a -> Maybe AnySymbolSet) -> a -> AnySymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe AnySymbolSet
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe
  {-# INLINE extractSym #-}
  extractSymMaybe :: (IsSymbolKind knd) => a -> Maybe (SymbolSet knd)

-- | Lifting of 'ExtractSym' to unary type constructors.
class
  (forall a. (ExtractSym a) => ExtractSym (f a)) =>
  ExtractSym1 f
  where
  -- | Lifts the 'extractSymMaybe' function to unary type constructors.
  liftExtractSymMaybe ::
    (IsSymbolKind knd) =>
    (a -> Maybe (SymbolSet knd)) ->
    f a ->
    Maybe (SymbolSet knd)

-- | Lift the standard 'extractSym' to unary type constructors.
extractSym1 ::
  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
  f a ->
  SymbolSet knd
extractSym1 :: forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> SymbolSet knd
extractSym1 = Maybe (SymbolSet knd) -> SymbolSet knd
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SymbolSet knd) -> SymbolSet knd)
-> (f a -> Maybe (SymbolSet knd)) -> f a -> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (f :: * -> *) (knd :: SymbolKind) a.
(ExtractSym1 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe
{-# INLINE extractSym1 #-}

-- | Lift the standard 'extractSymMaybe' to unary type constructors.
extractSymMaybe1 ::
  (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
  f a ->
  Maybe (SymbolSet knd)
extractSymMaybe1 :: forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1 = (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (f :: * -> *) (knd :: SymbolKind) a.
(ExtractSym1 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe
{-# INLINE extractSymMaybe1 #-}

-- | Lifting of 'ExtractSym' to binary type constructors.
class
  (forall a. (ExtractSym a) => ExtractSym1 (f a)) =>
  ExtractSym2 f
  where
  -- | Lifts the 'extractSymMaybe' function to binary type constructors.
  liftExtractSymMaybe2 ::
    (IsSymbolKind knd) =>
    (a -> Maybe (SymbolSet knd)) ->
    (b -> Maybe (SymbolSet knd)) ->
    f a b ->
    Maybe (SymbolSet knd)

-- | Lift the standard 'extractSym' to binary type constructors.
extractSym2 ::
  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>
  f a b ->
  SymbolSet knd
extractSym2 :: forall (f :: * -> * -> *) a b (knd :: SymbolKind).
(ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>
f a b -> SymbolSet knd
extractSym2 = Maybe (SymbolSet knd) -> SymbolSet knd
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (SymbolSet knd) -> SymbolSet knd)
-> (f a b -> Maybe (SymbolSet knd)) -> f a b -> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
forall (f :: * -> * -> *) (knd :: SymbolKind) a b.
(ExtractSym2 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe b -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
b -> Maybe (SymbolSet knd)
extractSymMaybe

-- | Lift the standard 'extractSymMaybe' to binary type constructors.
extractSymMaybe2 ::
  (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>
  f a b ->
  Maybe (SymbolSet knd)
extractSymMaybe2 :: forall (f :: * -> * -> *) a b (knd :: SymbolKind).
(ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) =>
f a b -> Maybe (SymbolSet knd)
extractSymMaybe2 = (a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
forall (f :: * -> * -> *) (knd :: SymbolKind) a b.
(ExtractSym2 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe b -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
b -> Maybe (SymbolSet knd)
extractSymMaybe
{-# INLINE extractSymMaybe2 #-}

-- Derivations

-- | The arguments to the generic 'extractSym' function.
data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type

data instance ExtractSymArgs Arity0 _ _ = ExtractSymArgs0

newtype instance ExtractSymArgs Arity1 knd a
  = ExtractSymArgs1 (a -> Maybe (SymbolSet knd))

-- | The class of types that can generically extract the symbols.
class GExtractSym arity f where
  gextractSymMaybe ::
    (IsSymbolKind knd) =>
    ExtractSymArgs arity knd a ->
    f a ->
    Maybe (SymbolSet knd)

instance GExtractSym arity V1 where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> V1 a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
_ V1 a
_ = SymbolSet knd -> Maybe (SymbolSet knd)
forall a. a -> Maybe a
Just SymbolSet knd
forall a. Monoid a => a
mempty
  {-# INLINE gextractSymMaybe #-}

instance GExtractSym arity U1 where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> U1 a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
_ U1 a
_ = SymbolSet knd -> Maybe (SymbolSet knd)
forall a. a -> Maybe a
Just SymbolSet knd
forall a. Monoid a => a
mempty
  {-# INLINE gextractSymMaybe #-}

instance (GExtractSym arity a) => GExtractSym arity (M1 i c a) where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> M1 i c a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args (M1 a a
x) = ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args a a
x
  {-# INLINE gextractSymMaybe #-}

instance (ExtractSym a) => GExtractSym arity (K1 i a) where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> K1 i a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
_ (K1 a
x) = a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
a -> Maybe (SymbolSet knd)
extractSymMaybe a
x
  {-# INLINE gextractSymMaybe #-}

instance
  (GExtractSym arity a, GExtractSym arity b) =>
  GExtractSym arity (a :+: b)
  where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> (:+:) a b a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args (L1 a a
x) = ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args a a
x
  gextractSymMaybe ExtractSymArgs arity knd a
args (R1 b a
x) = ExtractSymArgs arity knd a -> b a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> b a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args b a
x
  {-# INLINE gextractSymMaybe #-}

instance
  (GExtractSym arity a, GExtractSym arity b) =>
  GExtractSym arity (a :*: b)
  where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> (:*:) a b a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args (a a
x :*: b a
y) =
    ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args a a
x Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> ExtractSymArgs arity knd a -> b a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs arity knd a -> b a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs arity knd a
args b a
y
  {-# INLINE gextractSymMaybe #-}

instance GExtractSym Arity1 Par1 where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity1 knd a -> Par1 a -> Maybe (SymbolSet knd)
gextractSymMaybe (ExtractSymArgs1 a -> Maybe (SymbolSet knd)
f) (Par1 a
x) = a -> Maybe (SymbolSet knd)
f a
x
  {-# INLINE gextractSymMaybe #-}

instance (ExtractSym1 a) => GExtractSym Arity1 (Rec1 a) where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity1 knd a -> Rec1 a a -> Maybe (SymbolSet knd)
gextractSymMaybe (ExtractSymArgs1 a -> Maybe (SymbolSet knd)
f) (Rec1 a a
x) =
    (a -> Maybe (SymbolSet knd)) -> a a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> a a -> Maybe (SymbolSet knd)
forall (f :: * -> *) (knd :: SymbolKind) a.
(ExtractSym1 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f a a
x
  {-# INLINE gextractSymMaybe #-}

instance
  (ExtractSym1 f, GExtractSym Arity1 g) =>
  GExtractSym Arity1 (f :.: g)
  where
  gextractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity1 knd a -> (:.:) f g a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs Arity1 knd a
targs (Comp1 f (g a)
x) =
    (g a -> Maybe (SymbolSet knd)) -> f (g a) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (f :: * -> *) (knd :: SymbolKind) a.
(ExtractSym1 f, IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
liftExtractSymMaybe (ExtractSymArgs Arity1 knd a -> g a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity1 knd a -> g a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs Arity1 knd a
targs) f (g a)
x
  {-# INLINE gextractSymMaybe #-}

-- | Generic 'extractSym' function.
genericExtractSymMaybe ::
  (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) =>
  a ->
  Maybe (SymbolSet knd)
genericExtractSymMaybe :: forall a (knd :: SymbolKind).
(Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
genericExtractSymMaybe = ExtractSymArgs Arity0 knd Any -> Rep a Any -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity0 knd a -> Rep a a -> Maybe (SymbolSet knd)
gextractSymMaybe ExtractSymArgs Arity0 knd Any
forall (_ :: SymbolKind) _. ExtractSymArgs Arity0 _ _
ExtractSymArgs0 (Rep a Any -> Maybe (SymbolSet knd))
-> (a -> Rep a Any) -> a -> Maybe (SymbolSet knd)
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

-- | Generic 'liftExtractSymMaybe' function.
genericLiftExtractSymMaybe ::
  (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) =>
  (a -> Maybe (SymbolSet knd)) ->
  f a ->
  Maybe (SymbolSet knd)
genericLiftExtractSymMaybe :: forall (f :: * -> *) (knd :: SymbolKind) a.
(Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
genericLiftExtractSymMaybe a -> Maybe (SymbolSet knd)
f =
  ExtractSymArgs Arity1 knd a -> Rep1 f a -> Maybe (SymbolSet knd)
forall arity (f :: * -> *) (knd :: SymbolKind) a.
(GExtractSym arity f, IsSymbolKind knd) =>
ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
ExtractSymArgs Arity1 knd a -> Rep1 f a -> Maybe (SymbolSet knd)
gextractSymMaybe ((a -> Maybe (SymbolSet knd)) -> ExtractSymArgs Arity1 knd a
forall (knd :: SymbolKind) a.
(a -> Maybe (SymbolSet knd)) -> ExtractSymArgs Arity1 knd a
ExtractSymArgs1 a -> Maybe (SymbolSet knd)
f) (Rep1 f a -> Maybe (SymbolSet knd))
-> (f a -> Rep1 f a) -> f a -> Maybe (SymbolSet knd)
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

instance
  (Generic a, GExtractSym Arity0 (Rep a)) =>
  ExtractSym (Default a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
Default a -> Maybe (SymbolSet knd)
extractSymMaybe = a -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
genericExtractSymMaybe (a -> Maybe (SymbolSet knd))
-> (Default a -> a) -> Default a -> Maybe (SymbolSet knd)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault
  {-# INLINE extractSymMaybe #-}

instance
  (Generic1 f, GExtractSym Arity1 (Rep1 f), ExtractSym a) =>
  ExtractSym (Default1 f a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
Default1 f a -> Maybe (SymbolSet knd)
extractSymMaybe = Default1 f a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance
  (Generic1 f, GExtractSym Arity1 (Rep1 f)) =>
  ExtractSym1 (Default1 f)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> Default1 f a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f = (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
forall (f :: * -> *) (knd :: SymbolKind) a.
(Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) =>
(a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
genericLiftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (f a -> Maybe (SymbolSet knd))
-> (Default1 f a -> f a) -> Default1 f a -> Maybe (SymbolSet knd)
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 liftExtractSymMaybe #-}