⚡ Remove the Hashable and Eq super class constraints from SupportedPrim

grisette.cabal

@@ -138,7 +138,6 @@ library
       Grisette.Internal.SymPrim.Prim.Internal.Unfold
       Grisette.Internal.SymPrim.Prim.Internal.Utils
       Grisette.Internal.SymPrim.Prim.Model
-      Grisette.Internal.SymPrim.Prim.ModelValue
       Grisette.Internal.SymPrim.Prim.SomeTerm
       Grisette.Internal.SymPrim.Prim.Term
       Grisette.Internal.SymPrim.Prim.TermUtils

src/Grisette/Internal/Core/Data/Class/PPrint.hs

@@ -144,9 +144,9 @@ import Grisette.Internal.SymPrim.Prim.Model
   ( Model (Model),
     SymbolSet (SymbolSet),
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue)
 import Grisette.Internal.SymPrim.Prim.Term
-  ( SomeTypedSymbol (SomeTypedSymbol),
+  ( ModelValue,
+    SomeTypedSymbol (SomeTypedSymbol),
     TypedSymbol (unTypedSymbol),
     prettyPrintTerm,
   )

src/Grisette/Internal/SymPrim/FunInstanceGen.hs

@@ -22,6 +22,7 @@ module Grisette.Internal.SymPrim.FunInstanceGen
   )
 where
 
+import Data.Hashable (Hashable)
 import qualified Data.SBV as SBV
 import Grisette.Internal.SymPrim.Prim.Internal.Term
   ( IsSymbolKind,
@@ -218,7 +219,16 @@ supportedPrimFun
             (typeRep :: TypeRep $(funType tyVars))
           |]
 
-      constraints = traverse (\ty -> [t|SupportedNonFuncPrim $ty|])
+      constraints =
+        fmap concat
+          . traverse
+            ( \ty ->
+                sequence
+                  [ [t|SupportedNonFuncPrim $ty|],
+                    [t|Eq $ty|],
+                    [t|Hashable $ty|]
+                  ]
+            )
       funType =
         foldl1 (\fty ty -> [t|$(varT funTypeName) $ty $fty|]) . reverse
       withPrims :: [Q Type] -> Q Exp

src/Grisette/Internal/SymPrim/Prim/Internal/Instances/SupportedPrim.hs

@@ -45,6 +45,7 @@ import Grisette.Internal.SymPrim.FP
   )
 import Grisette.Internal.SymPrim.Prim.Internal.Term
   ( IsSymbolKind (decideSymbolKind),
+    ModelValue,
     NonFuncSBVRep (NonFuncSBVBaseType),
     SBVRep
       ( SBVType
@@ -86,8 +87,8 @@ import Grisette.Internal.SymPrim.Prim.Internal.Term
     pevalITEBasicTerm,
     pevalNotTerm,
     sbvFresh,
+    toModelValue,
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue (ModelValue, toModelValue)
 import Grisette.Internal.Utils.Parameterized (unsafeAxiom)
 
 defaultValueForInteger :: Integer

src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs

@@ -94,6 +94,9 @@ module Grisette.Internal.SymPrim.Prim.Internal.Term
     typeHashId,
     introSupportedPrimConstraint,
     pformatTerm,
+    ModelValue (..),
+    toModelValue,
+    unsafeFromModelValue,
 
     -- * Interning
     UTerm (..),
@@ -250,10 +253,6 @@ import Grisette.Internal.SymPrim.Prim.Internal.Utils
   ( WeakThreadId,
     myWeakThreadId,
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue
-  ( ModelValue,
-    toModelValue,
-  )
 import Language.Haskell.TH.Syntax (Lift (liftTyped))
 import Type.Reflection
   ( SomeTypeRep (SomeTypeRep),
@@ -394,8 +393,6 @@ class SupportedPrimConstraint t where
 class
   ( Lift t,
     Typeable t,
-    Hashable t,
-    Eq t,
     Show t,
     NFData t,
     SupportedPrimConstraint t,
@@ -404,8 +401,10 @@ class
   SupportedPrim t
   where
   sameCon :: t -> t -> Bool
+  default sameCon :: (Eq t) => t -> t -> Bool
   sameCon = (==)
   hashConWithSalt :: Int -> t -> Int
+  default hashConWithSalt :: (Hashable t) => Int -> t -> Int
   hashConWithSalt = hashWithSalt
   pformatCon :: t -> String
   default pformatCon :: (Show t) => t -> String
@@ -414,6 +413,7 @@ class
   pformatSym = showUntyped
   defaultValue :: t
   defaultValueDynamic :: proxy t -> ModelValue
+  default defaultValueDynamic :: (Hashable t) => proxy t -> ModelValue
   defaultValueDynamic _ = toModelValue (defaultValue @t)
   pevalITETerm :: Term Bool -> Term t -> Term t -> Term t
   pevalEqTerm :: Term t -> Term t -> Term Bool
@@ -461,6 +461,39 @@ class
   isFuncType :: Bool
   funcDummyConstraint :: SBVType t -> SBV.SBV Bool
 
+-- | A value with its type information.
+data ModelValue where
+  ModelValue :: forall v. (SupportedPrim v) => v -> ModelValue
+
+instance Show ModelValue where
+  show (ModelValue (v :: v)) = show v ++ " :: " ++ show (typeRep @v)
+
+instance Eq ModelValue where
+  (ModelValue (v1 :: v1)) == (ModelValue (v2 :: v2)) =
+    case eqTypeRep (typeRep @v1) (typeRep @v2) of
+      Just HRefl -> sameCon v1 v2
+      _ -> False
+
+instance Hashable ModelValue where
+  s `hashWithSalt` (ModelValue (v :: v)) =
+    (s `hashWithSalt` (typeRep @v)) `hashConWithSalt` v
+
+-- | Convert from a model value. Crashes if the types does not match.
+unsafeFromModelValue :: forall a. (Typeable a) => ModelValue -> a
+unsafeFromModelValue (ModelValue (v :: v)) =
+  case eqTypeRep (typeRep @v) (typeRep @a) of
+    Just HRefl -> v
+    _ ->
+      error $
+        "Bad model value type, expected type: "
+          ++ show (typeRep @a)
+          ++ ", but got: "
+          ++ show (typeRep @v)
+
+-- | Convert to a model value.
+toModelValue :: forall a. (SupportedPrim a) => a -> ModelValue
+toModelValue = ModelValue
+
 -- | Cast a typed symbol to a different kind. Check if the kind is compatible.
 castSomeTypedSymbol ::
   (IsSymbolKind knd') => SomeTypedSymbol knd -> Maybe (SomeTypedSymbol knd')

src/Grisette/Internal/SymPrim/Prim/Model.hs

@@ -69,20 +69,18 @@ import Grisette.Internal.SymPrim.Prim.Internal.Term
     Term,
     TypedAnySymbol,
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue
-  ( ModelValue,
-    toModelValue,
-    unsafeFromModelValue,
-  )
 import Grisette.Internal.SymPrim.Prim.Term
-  ( SomeTypedSymbol (SomeTypedSymbol),
+  ( ModelValue,
+    SomeTypedSymbol (SomeTypedSymbol),
     SupportedPrim (defaultValue, defaultValueDynamic),
     TypedSymbol (TypedSymbol, unTypedSymbol),
     conTerm,
     pevalEqTerm,
     showUntyped,
     someTypedSymbol,
     symTerm,
+    toModelValue,
+    unsafeFromModelValue,
     withSymbolSupported,
   )
 

src/Grisette/Internal/SymPrim/TabularFun.hs

@@ -107,7 +107,7 @@ instance (SupportedNonFuncPrim a, SupportedPrim b) => SBVRep (a =-> b) where
   type SBVType (a =-> b) = SBV.SBV (NonFuncSBVBaseType a) -> SBVType b
 
 instance
-  (SupportedPrim a, SupportedPrim b, SupportedPrim (a =-> b)) =>
+  (SupportedPrim a, SupportedPrim b, Eq a, SupportedPrim (a =-> b)) =>
   PEvalApplyTerm (a =-> b) a b
   where
   pevalApplyTerm = totalize2 doPevalApplyTerm applyTerm

test/Grisette/SymPrim/Prim/ModelTests.hs

@@ -29,7 +29,6 @@ import Grisette.Internal.SymPrim.Prim.Model
     equation,
     evalTerm,
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue (toModelValue)
 import Grisette.Internal.SymPrim.Prim.Term
   ( PEvalNumTerm (pevalAddNumTerm, pevalNegNumTerm),
     SupportedPrim (pevalITETerm),
@@ -38,6 +37,7 @@ import Grisette.Internal.SymPrim.Prim.Term
     pevalEqTerm,
     someTypedSymbol,
     ssymTerm,
+    toModelValue,
   )
 import Test.Framework (Test, testGroup)
 import Test.Framework.Providers.HUnit (testCase)

test/Grisette/SymPrim/SymPrimTests.hs

@@ -117,7 +117,6 @@ import Grisette.Internal.SymPrim.Prim.Model
   ( Model (Model),
     SymbolSet (SymbolSet),
   )
-import Grisette.Internal.SymPrim.Prim.ModelValue (toModelValue)
 import Grisette.Internal.SymPrim.Prim.Term
   ( LinkedRep (wrapTerm),
     PEvalApplyTerm (pevalApplyTerm),
@@ -169,6 +168,7 @@ import Grisette.Internal.SymPrim.Prim.Term
     pevalXorTerm,
     someTypedSymbol,
     ssymTerm,
+    toModelValue,
   )
 import Grisette.SymPrim
   ( ModelSymPair ((:=)),