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

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm (SomeTerm (..)) where

import Data.Hashable (Hashable (hashWithSalt))
import Data.Typeable (Proxy (Proxy), typeRep)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
  ( SupportedPrim,
    Term,
  )
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
  ( identityWithTypeRep,
  )

data SomeTerm where
  SomeTerm :: forall a. (SupportedPrim a) => Term a -> SomeTerm

instance Eq SomeTerm where
  (SomeTerm Term a
t1) == :: SomeTerm -> SomeTerm -> Bool
== (SomeTerm Term a
t2) = forall t. Term t -> (TypeRep, Id)
identityWithTypeRep Term a
t1 forall a. Eq a => a -> a -> Bool
== forall t. Term t -> (TypeRep, Id)
identityWithTypeRep Term a
t2

instance Hashable SomeTerm where
  hashWithSalt :: Id -> SomeTerm -> Id
hashWithSalt Id
s (SomeTerm Term a
t) = forall a. Hashable a => Id -> a -> Id
hashWithSalt Id
s forall a b. (a -> b) -> a -> b
$ forall t. Term t -> (TypeRep, Id)
identityWithTypeRep Term a
t

instance Show SomeTerm where
  show :: SomeTerm -> String
show (SomeTerm (Term a
t :: Term a)) = String
"<<" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
t forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy @a)) forall a. [a] -> [a] -> [a]
++ String
">>"