{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.SomeTerm
-- 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.SymPrim.Prim.SomeTerm
  ( SomeTerm (..),
    someTerm,
    someTermId,
  )
where

import Data.Hashable (Hashable (hashWithSalt))
import Data.Typeable (eqT, type (:~:) (Refl))
import Grisette.Internal.SymPrim.Prim.Internal.Caches (Id)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SupportedPrim (primTypeRep),
    Term,
    introSupportedPrimConstraint,
    termId,
    withSupportedPrimTypeable,
  )

-- | Existential wrapper for symbolic Grisette terms.
data SomeTerm where
  SomeTerm :: forall a. (SupportedPrim a) => Term a -> SomeTerm

instance Eq SomeTerm where
  (SomeTerm (Term a
t1 :: Term a)) == :: SomeTerm -> SomeTerm -> Bool
== (SomeTerm (Term a
t2 :: Term b)) =
    forall a b. SupportedPrim a => (Typeable a => b) -> b
withSupportedPrimTypeable @a ((Typeable a => Bool) -> Bool) -> (Typeable a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
      forall a b. SupportedPrim a => (Typeable a => b) -> b
withSupportedPrimTypeable @b ((Typeable a => Bool) -> Bool) -> (Typeable a => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
        case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @a @b of
          Just a :~: a
Refl -> Term a
t1 Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
Term a
t2
          Maybe (a :~: a)
Nothing -> Bool
False

instance Hashable SomeTerm where
  hashWithSalt :: Int -> SomeTerm -> Int
hashWithSalt Int
s (SomeTerm Term a
t) = Int -> Term a -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Term a
t

instance Show SomeTerm where
  show :: SomeTerm -> String
show (SomeTerm (Term a
t :: Term a)) =
    String
"<<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall t. SupportedPrim t => TypeRep t
primTypeRep @a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">>"

-- | Wrap a symbolic term into t'SomeTerm'.
someTerm :: Term a -> SomeTerm
someTerm :: forall a. Term a -> SomeTerm
someTerm Term a
v = Term a -> ((SupportedPrim a, Typeable a) => SomeTerm) -> SomeTerm
forall t a. Term t -> ((SupportedPrim t, Typeable t) => a) -> a
introSupportedPrimConstraint Term a
v (((SupportedPrim a, Typeable a) => SomeTerm) -> SomeTerm)
-> ((SupportedPrim a, Typeable a) => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
v
{-# INLINE someTerm #-}

-- | Get the unique identifier of a symbolic term.
someTermId :: SomeTerm -> Id
someTermId :: SomeTerm -> Id
someTermId (SomeTerm Term a
t) = Term a -> Id
forall t. Term t -> Id
termId Term a
t
{-# INLINE someTermId #-}