✨ Improve SupportedNonFuncPrim/BasicSymPrim constraints, add constrai…

…nt tests for Prim, SymPrim and BasicSymPrim

CHANGELOG.md

@@ -24,6 +24,8 @@ Versioning](https://semver.org/spec/v2.0.0.html).
 - Added `AsMetadata` type class and `Metadata` pattern for embedding and
   extracting values from metadata represented as an S-expression.
   ([#277](https://github.com/lsrcz/grisette/pull/277))
+- Improved `SupportedNonFuncPrim` and `BasicSymPrim` constraints.
+  ([#278](https://github.com/lsrcz/grisette/pull/278))
 
 ### Changed
 - Derivation of `PPrint` no longer relies on `OverloadedStrings` extension.

grisette.cabal

@@ -462,6 +462,7 @@ test-suite spec
       Grisette.SymPrim.QuantifierTests
       Grisette.SymPrim.SomeBVTests
       Grisette.SymPrim.SymGeneralFunTests
+      Grisette.SymPrim.SymPrimConstraintTests
       Grisette.SymPrim.SymPrimTests
       Grisette.SymPrim.TabularFunTests
       Grisette.TestUtil.NoMerge

src/Grisette/Internal/SymPrim/FunInstanceGen.hs

@@ -22,7 +22,6 @@ module Grisette.Internal.SymPrim.FunInstanceGen
   )
 where
 
-import Data.Hashable (Hashable)
 import qualified Data.SBV as SBV
 import Grisette.Internal.SymPrim.Prim.Internal.Term
   ( IsSymbolKind,
@@ -73,7 +72,7 @@ import Language.Haskell.TH.Datatype.TyVarBndr
   ( plainTVInferred,
     plainTVSpecified,
   )
-import Type.Reflection (TypeRep, Typeable, typeRep, type (:~~:) (HRefl))
+import Type.Reflection (TypeRep, typeRep, type (:~~:) (HRefl))
 
 instanceWithOverlapDescD ::
   Maybe Overlap -> Q Cxt -> Q Type -> [DecsQ] -> DecsQ
@@ -219,17 +218,7 @@ supportedPrimFun
           |]
 
       constraints =
-        fmap concat
-          . traverse
-            ( \ty ->
-                sequence
-                  [ [t|SupportedNonFuncPrim $ty|],
-                    [t|Eq $ty|],
-                    [t|Show $ty|],
-                    [t|Hashable $ty|],
-                    [t|Typeable $ty|]
-                  ]
-            )
+        fmap concat . traverse (\ty -> sequence [[t|SupportedNonFuncPrim $ty|]])
       funType =
         foldl1 (\fty ty -> [t|$(varT funTypeName) $ty $fty|]) . reverse
       withPrims :: [Q Type] -> Q Exp

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

@@ -257,9 +257,7 @@ import GHC.IO (unsafePerformIO)
 import GHC.Stack (HasCallStack)
 import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
 import Grisette.Internal.Core.Data.Class.BitCast (BitCast, BitCastOr)
-import Grisette.Internal.Core.Data.Class.BitVector
-  ( SizedBV,
-  )
+import Grisette.Internal.Core.Data.Class.BitVector (SizedBV)
 import Grisette.Internal.Core.Data.Symbol
   ( Identifier,
     Symbol (IndexedSymbol, SimpleSymbol),
@@ -351,7 +349,16 @@ translateTypeError (Just reason) ta =
 
 -- | Type class for resolving the base type for the SBV type for the primitive
 -- type.
-class (SupportedPrim a, Ord a) => NonFuncSBVRep a where
+class
+  ( SupportedPrim a,
+    Ord a,
+    Eq a,
+    Show a,
+    Hashable a,
+    Typeable a
+  ) =>
+  NonFuncSBVRep a
+  where
   type NonFuncSBVBaseType a
 
 -- | Type class for resolving the constraint for a supported non-function

src/Grisette/Internal/SymPrim/SymPrim.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
 
 -- |
 -- Module      :   Grisette.Internal.SymPrim.SymPrim
@@ -19,7 +20,7 @@ import Data.Hashable (Hashable)
 import Data.Serialize (Serialize)
 import Grisette.Internal.Core.Data.Class.EvalSym (EvalSym)
 import Grisette.Internal.Core.Data.Class.ExtractSym (ExtractSym)
-import Grisette.Internal.Core.Data.Class.Function (Apply)
+import Grisette.Internal.Core.Data.Class.Function (Apply (FunType))
 import Grisette.Internal.Core.Data.Class.GenSym (GenSymSimple)
 import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp)
 import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
@@ -35,6 +36,7 @@ import Grisette.Internal.SymPrim.AllSyms (AllSyms)
 import Grisette.Internal.SymPrim.Prim.Internal.Term
   ( ConRep (ConType),
     LinkedRep,
+    SupportedNonFuncPrim,
   )
 import Language.Haskell.TH.Syntax (Lift)
 import Type.Reflection (Typeable)
@@ -78,10 +80,12 @@ type BasicSymPrim a =
   ( SymPrim a,
     SimpleMergeable a,
     GenSymSimple () a,
-    Apply a,
     Solvable (ConType a) a,
     ConRep a,
     LinkedRep (ConType a) a,
     ToCon a (ConType a),
-    ToSym (ConType a) a
+    ToSym (ConType a) a,
+    Apply a,
+    a ~ FunType a,
+    SupportedNonFuncPrim (ConType a)
   )

test/Grisette/SymPrim/SymPrimConstraintTests.hs

@@ -0,0 +1,97 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
+module Grisette.SymPrim.SymPrimConstraintTests
+  ( symBool,
+    symInteger,
+    symWordN8,
+    symIntN8,
+    symFP32,
+    symAlgReal,
+    someSymWordN,
+    someSymIntN,
+    bool,
+    integer,
+    wordN8,
+    intN8,
+    fp32,
+    algReal,
+    someWordN,
+    someIntN,
+  )
+where
+
+import Grisette
+  ( AlgReal,
+    BasicSymPrim,
+    FP32,
+    IntN8,
+    Prim,
+    SomeSymWordN,
+    SymAlgReal,
+    SymBool,
+    SymFP32,
+    SymIntN8,
+    SymInteger,
+    SymPrim,
+    SymWordN8,
+    WordN8,
+  )
+import Grisette.Internal.SymPrim.SomeBV (SomeIntN, SomeSymIntN, SomeWordN)
+
+data BasicSymPrimType a where
+  BasicSymPrimType :: (BasicSymPrim a) => BasicSymPrimType a
+
+symBool :: BasicSymPrimType SymBool
+symBool = BasicSymPrimType
+
+symInteger :: BasicSymPrimType SymInteger
+symInteger = BasicSymPrimType
+
+symWordN8 :: BasicSymPrimType SymWordN8
+symWordN8 = BasicSymPrimType
+
+symIntN8 :: BasicSymPrimType SymIntN8
+symIntN8 = BasicSymPrimType
+
+symFP32 :: BasicSymPrimType SymFP32
+symFP32 = BasicSymPrimType
+
+symAlgReal :: BasicSymPrimType SymAlgReal
+symAlgReal = BasicSymPrimType
+
+data SymPrimType a where
+  SymPrimType :: (SymPrim a) => SymPrimType a
+
+someSymWordN :: SymPrimType SomeSymWordN
+someSymWordN = SymPrimType
+
+someSymIntN :: SymPrimType SomeSymIntN
+someSymIntN = SymPrimType
+
+data PrimType a where
+  PrimType :: (Prim a) => PrimType a
+
+bool :: PrimType Bool
+bool = PrimType
+
+integer :: PrimType Integer
+integer = PrimType
+
+wordN8 :: PrimType WordN8
+wordN8 = PrimType
+
+intN8 :: PrimType IntN8
+intN8 = PrimType
+
+fp32 :: PrimType FP32
+fp32 = PrimType
+
+algReal :: PrimType AlgReal
+algReal = PrimType
+
+someWordN :: PrimType SomeWordN
+someWordN = PrimType
+
+someIntN :: PrimType SomeIntN
+someIntN = PrimType