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

-- |
-- Module      :   Grisette.Internal.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.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 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 qualified Data.HashSet as HS
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down)
import Data.Ratio (Ratio, denominator, numerator)
import qualified Data.Text as T
import Data.Typeable (type (:~~:) (HRefl))
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default, unDefault),
    Default1 (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.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 (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.Model
  ( AnySymbolSet,
    SymbolSet (SymbolSet),
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( IsSymbolKind (decideSymbolKind),
    SymRep (SymType),
    SymbolKind,
    someTypedSymbol,
  )
import Grisette.Internal.SymPrim.Prim.TermUtils (extractTerm)
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 (=->) (TabularFun))
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
-- >>> 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 #-}

#define CONCRETE_EXTRACT_SYMBOLICS(type) \
instance ExtractSym type where \
  extractSymMaybe _ = return mempty

#define CONCRETE_EXTRACT_SYMBOLICS_BV(type) \
instance (KnownNat n, 1 <= n) => ExtractSym (type n) where \
  extractSymMaybe _ = return mempty

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

instance (ExtractSym a) => ExtractSym (Ratio a) where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
Ratio a -> Maybe (SymbolSet knd)
extractSymMaybe Ratio a
a =
    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 (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
a) Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> 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 (Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
a)
  {-# INLINE extractSymMaybe #-}

instance (ValidFP eb sb) => ExtractSym (FP eb sb) where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
FP eb sb -> Maybe (SymbolSet knd)
extractSymMaybe FP eb sb
_ = SymbolSet knd -> Maybe (SymbolSet knd)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return SymbolSet knd
forall a. Monoid a => a
mempty

#define EXTRACT_SYMBOLICS_SIMPLE(symtype) \
instance ExtractSym symtype where \
  extractSymMaybe :: \
    forall knd. (IsSymbolKind knd) => symtype -> Maybe (SymbolSet knd); \
  extractSymMaybe (symtype t) = \
    case decideSymbolKind @knd of\
      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \
      Right HRefl -> SymbolSet <$> extractTerm HS.empty t

#define EXTRACT_SYMBOLICS_BV(symtype) \
instance (KnownNat n, 1 <= n) => ExtractSym (symtype n) where \
  extractSymMaybe :: \
    forall knd. (IsSymbolKind knd) => symtype n -> Maybe (SymbolSet knd); \
  extractSymMaybe (symtype t) = \
    case decideSymbolKind @knd of\
      Left HRefl -> SymbolSet <$> extractTerm HS.empty t; \
      Right HRefl -> SymbolSet <$> extractTerm HS.empty t

#define EXTRACT_SYMBOLICS_FUN(op, cons) \
instance ExtractSym (op sa sb) where \
  extractSymMaybe :: \
    forall knd. (IsSymbolKind knd) => op sa sb -> Maybe (SymbolSet knd); \
  extractSymMaybe (cons t) = \
    case decideSymbolKind @knd of \
      Left HRefl -> Nothing; \
      Right HRefl -> SymbolSet <$> extractTerm HS.empty t

#if 1
EXTRACT_SYMBOLICS_SIMPLE(SymBool)
EXTRACT_SYMBOLICS_SIMPLE(SymInteger)
EXTRACT_SYMBOLICS_SIMPLE(SymFPRoundingMode)
EXTRACT_SYMBOLICS_SIMPLE(SymAlgReal)
EXTRACT_SYMBOLICS_BV(SymIntN)
EXTRACT_SYMBOLICS_BV(SymWordN)
EXTRACT_SYMBOLICS_FUN((=~>), SymTabularFun)
EXTRACT_SYMBOLICS_FUN((-~>), SymGeneralFun)
#endif

instance (ValidFP eb fb) => ExtractSym (SymFP eb fb) where
  extractSymMaybe ::
    forall knd. (IsSymbolKind knd) => SymFP eb fb -> Maybe (SymbolSet knd)
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
SymFP eb fb -> Maybe (SymbolSet knd)
extractSymMaybe (SymFP Term (FP eb fb)
t) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd of
      Left knd :~~: 'ConstantKind
HRefl -> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> Maybe (HashSet (SomeTypedSymbol knd)) -> Maybe (SymbolSet knd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet SomeTypedConstantSymbol
-> Term (FP eb fb) -> Maybe (HashSet (SomeTypedSymbol knd))
forall (knd :: SymbolKind) a.
(IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
HashSet SomeTypedConstantSymbol
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
extractTerm HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term (FP eb fb)
t
      Right knd :~~: 'AnyKind
HRefl -> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> Maybe (HashSet (SomeTypedSymbol knd)) -> Maybe (SymbolSet knd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet SomeTypedConstantSymbol
-> Term (FP eb fb) -> Maybe (HashSet (SomeTypedSymbol knd))
forall (knd :: SymbolKind) a.
(IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
HashSet SomeTypedConstantSymbol
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
extractTerm HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term (FP eb fb)
t

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

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

-- ExceptT
instance
  (ExtractSym1 m, ExtractSym e, ExtractSym a) =>
  ExtractSym (ExceptT e m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
ExceptT e m a -> Maybe (SymbolSet knd)
extractSymMaybe = ExceptT e m a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance
  (ExtractSym1 m, ExtractSym e) =>
  ExtractSym1 (ExceptT e m)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> ExceptT e m a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (ExceptT m (Either e a)
v) =
    (Either e a -> Maybe (SymbolSet knd))
-> m (Either e a) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> m 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)) -> Either e a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> Either e 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) m (Either e a)
v
  {-# INLINE liftExtractSymMaybe #-}

-- MaybeT
instance
  (ExtractSym1 m, ExtractSym a) =>
  ExtractSym (MaybeT m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
MaybeT m a -> Maybe (SymbolSet knd)
extractSymMaybe = MaybeT m a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance
  (ExtractSym1 m) =>
  ExtractSym1 (MaybeT m)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> MaybeT m a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (MaybeT m (Maybe a)
v) =
    (Maybe a -> Maybe (SymbolSet knd))
-> m (Maybe a) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> m 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)) -> Maybe a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> Maybe 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) m (Maybe a)
v
  {-# INLINE liftExtractSymMaybe #-}

-- WriterT
instance
  (ExtractSym1 m, ExtractSym w, ExtractSym a) =>
  ExtractSym (WriterLazy.WriterT w m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
WriterT w m a -> Maybe (SymbolSet knd)
extractSymMaybe = WriterT w m a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance
  (ExtractSym1 m, ExtractSym w) =>
  ExtractSym1 (WriterLazy.WriterT w m)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> WriterT w m a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (WriterLazy.WriterT m (a, w)
v) =
    ((a, w) -> Maybe (SymbolSet knd))
-> m (a, w) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> m 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))
-> (w -> Maybe (SymbolSet knd)) -> (a, w) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> (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)
f w -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
w -> Maybe (SymbolSet knd)
extractSymMaybe) m (a, w)
v
  {-# INLINE liftExtractSymMaybe #-}

instance
  (ExtractSym1 m, ExtractSym w, ExtractSym a) =>
  ExtractSym (WriterStrict.WriterT w m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
WriterT w m a -> Maybe (SymbolSet knd)
extractSymMaybe = WriterT w m a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance
  (ExtractSym1 m, ExtractSym w) =>
  ExtractSym1 (WriterStrict.WriterT w m)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> WriterT w m a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (WriterStrict.WriterT m (a, w)
v) =
    ((a, w) -> Maybe (SymbolSet knd))
-> m (a, w) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> m 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))
-> (w -> Maybe (SymbolSet knd)) -> (a, w) -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> (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)
f w -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
w -> Maybe (SymbolSet knd)
extractSymMaybe) m (a, w)
v
  {-# INLINE liftExtractSymMaybe #-}

-- IdentityT
instance
  (ExtractSym1 m, ExtractSym a) =>
  ExtractSym (IdentityT m a)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
IdentityT m a -> Maybe (SymbolSet knd)
extractSymMaybe = IdentityT m a -> Maybe (SymbolSet knd)
forall (f :: * -> *) a (knd :: SymbolKind).
(ExtractSym1 f, ExtractSym a, IsSymbolKind knd) =>
f a -> Maybe (SymbolSet knd)
extractSymMaybe1
  {-# INLINE extractSymMaybe #-}

instance (ExtractSym1 m) => ExtractSym1 (IdentityT m) where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> IdentityT m a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (IdentityT m a
v) = (a -> Maybe (SymbolSet knd)) -> m a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> m 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 m a
v
  {-# INLINE liftExtractSymMaybe #-}

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

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

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

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

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

instance
  (ExtractSym1 f, ExtractSym1 g) =>
  ExtractSym1 (Compose f g)
  where
  liftExtractSymMaybe :: forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> Compose f g a -> Maybe (SymbolSet knd)
liftExtractSymMaybe a -> Maybe (SymbolSet knd)
f (Compose f (g a)
l) =
    (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 ((a -> Maybe (SymbolSet knd)) -> g a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind) a.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd)) -> g 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) f (g a)
l
  {-# INLINE liftExtractSymMaybe #-}

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

deriving via
  (Default1 (Const a))
  instance
    (ExtractSym a) => ExtractSym1 (Const a)

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

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

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

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

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

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

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

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

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

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

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

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

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

-- ExtractSym2
instance ExtractSym2 Either where
  liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd))
-> Either a b
-> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
f b -> Maybe (SymbolSet knd)
_ (Left a
x) = a -> Maybe (SymbolSet knd)
f a
x
  liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
_ b -> Maybe (SymbolSet knd)
g (Right b
y) = b -> Maybe (SymbolSet knd)
g b
y
  {-# INLINE liftExtractSymMaybe2 #-}

instance ExtractSym2 (,) where
  liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd)) -> (a, b) -> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
f b -> Maybe (SymbolSet knd)
g (a
x, b
y) = a -> Maybe (SymbolSet knd)
f a
x Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> b -> Maybe (SymbolSet knd)
g b
y
  {-# INLINE liftExtractSymMaybe2 #-}

instance (ExtractSym a) => ExtractSym2 ((,,) a) where
  liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd))
-> (a, a, b)
-> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
f b -> Maybe (SymbolSet knd)
g (a
x, a
y, b
z) = 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 Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> a -> Maybe (SymbolSet knd)
f a
y Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> b -> Maybe (SymbolSet knd)
g b
z
  {-# INLINE liftExtractSymMaybe2 #-}

instance
  (ExtractSym a, ExtractSym b) =>
  ExtractSym2 ((,,,) a b)
  where
  liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b.
IsSymbolKind knd =>
(a -> Maybe (SymbolSet knd))
-> (b -> Maybe (SymbolSet knd))
-> (a, b, a, b)
-> Maybe (SymbolSet knd)
liftExtractSymMaybe2 a -> Maybe (SymbolSet knd)
f b -> Maybe (SymbolSet knd)
g (a
x, b
y, a
z, b
w) =
    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 Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> 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 b
y Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> a -> Maybe (SymbolSet knd)
f a
z Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> b -> Maybe (SymbolSet knd)
g b
w
  {-# INLINE liftExtractSymMaybe2 #-}

instance (ExtractSym a, ExtractSym b) => ExtractSym (a =-> b) where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
(a =-> b) -> Maybe (SymbolSet knd)
extractSymMaybe (TabularFun [(a, b)]
s b
t) =
    [(a, b)] -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
[(a, b)] -> Maybe (SymbolSet knd)
extractSymMaybe [(a, b)]
s Maybe (SymbolSet knd)
-> Maybe (SymbolSet knd) -> Maybe (SymbolSet knd)
forall a. Semigroup a => a -> a -> a
<> 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 b
t

instance (ExtractSym (SymType b)) => ExtractSym (a --> b) where
  extractSymMaybe :: forall knd. (IsSymbolKind knd) => (a --> b) -> Maybe (SymbolSet knd)
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
(a --> b) -> Maybe (SymbolSet knd)
extractSymMaybe (GeneralFun TypedConstantSymbol a
t Term b
f) =
    case forall (ty :: SymbolKind).
IsSymbolKind ty =>
Either (ty :~~: 'ConstantKind) (ty :~~: 'AnyKind)
decideSymbolKind @knd of
      Left knd :~~: 'ConstantKind
HRefl -> Maybe (SymbolSet knd)
forall a. Maybe a
Nothing
      Right knd :~~: 'AnyKind
HRefl -> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> Maybe (HashSet (SomeTypedSymbol knd)) -> Maybe (SymbolSet knd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet SomeTypedConstantSymbol
-> Term b -> Maybe (HashSet (SomeTypedSymbol knd))
forall (knd :: SymbolKind) a.
(IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
HashSet SomeTypedConstantSymbol
-> Term a -> Maybe (HashSet (SomeTypedSymbol knd))
extractTerm (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a. Hashable a => a -> HashSet a
HS.singleton (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol)
-> SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol a -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedConstantSymbol a
t) Term b
f