SomeTerm.hs

{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# 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,
    termId,
    pattern SupportedTerm,
  )

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

instance Eq SomeTerm where
  (SomeTerm (t1 :: Term a)) == (SomeTerm (t2 :: Term b)) =
    case eqT @a @b of
      Just Refl -> t1 == t2
      Nothing -> False

instance Hashable SomeTerm where
  hashWithSalt s (SomeTerm t) = hashWithSalt s t

instance Show SomeTerm where
  show (SomeTerm (t :: Term a)) =
    "<<" ++ show t ++ " :: " ++ show (primTypeRep @a) ++ ">>"

-- | Wrap a symbolic term into t'SomeTerm'.
someTerm :: Term a -> SomeTerm
someTerm v@SupportedTerm = SomeTerm v
{-# INLINE someTerm #-}

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