{-# 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 (..)) where

import Data.Hashable (Hashable (hashWithSalt))
import Data.Typeable (Proxy (Proxy), typeRep)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SupportedPrim,
    Term,
    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) =
    Term a -> (SomeTypeRep, Id)
forall t. Term t -> (SomeTypeRep, Id)
identityWithTypeRep Term a
t1 (SomeTypeRep, Id) -> (SomeTypeRep, Id) -> Bool
forall a. Eq a => a -> a -> Bool
== Term a -> (SomeTypeRep, Id)
forall t. Term t -> (SomeTypeRep, Id)
identityWithTypeRep Term a
t2

instance Hashable SomeTerm where
  hashWithSalt :: Id -> SomeTerm -> Id
hashWithSalt Id
s (SomeTerm Term a
t) = Id -> (SomeTypeRep, Id) -> Id
forall a. Hashable a => Id -> a -> Id
hashWithSalt Id
s ((SomeTypeRep, Id) -> Id) -> (SomeTypeRep, Id) -> Id
forall a b. (a -> b) -> a -> b
$ Term a -> (SomeTypeRep, Id)
forall t. Term t -> (SomeTypeRep, Id)
identityWithTypeRep 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]
++ SomeTypeRep -> String
forall a. Show a => a -> String
show (Proxy a -> SomeTypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">>"