Changed the symbolic identifier type to Text

CHANGELOG.md

@@ -30,6 +30,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Reorganized the files for `MonadTrans`. ([#132](https://github.com/lsrcz/grisette/pull/132))
 - [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133))
 - The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133))
+- Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141))
 
 ## [0.3.1.1] -- 2023-09-29
 

src/Grisette/Backend/SBV/Data/SMT/Lowering.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}

src/Grisette/Core/Data/Class/GenSym.hs

@@ -214,15 +214,15 @@
 --     >>> nameWithInfo "a" (1 :: Int)
 --     a:1
 data FreshIdent where
-  FreshIdent :: String -> FreshIdent
-  FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
+  FreshIdent :: T.Text -> FreshIdent
+  FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent
 
 instance Show FreshIdent where
-  show (FreshIdent i) = i
-  show (FreshIdentWithInfo s i) = s ++ ":" ++ show i
+  show (FreshIdent i) = T.unpack i
+  show (FreshIdentWithInfo s i) = T.unpack s ++ ":" ++ show i
 
 instance IsString FreshIdent where
-  fromString = name
+  fromString = name . T.pack
 
 instance Eq FreshIdent where
   FreshIdent l == FreshIdent r = l == r
@@ -261,7 +261,7 @@
 --
 -- The user may need to use unique names to avoid unintentional identifier
 -- collision.
-name :: String -> FreshIdent
+name :: T.Text -> FreshIdent
 name = FreshIdent
 
 -- | Identifier with extra information.
@@ -270,7 +270,7 @@
 --
 -- The user may need to use unique names or additional information to avoid
 -- unintentional identifier collision.
-nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
+nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent
 nameWithInfo = FreshIdentWithInfo
 
 -- | Monad class for fresh symbolic value generation.

src/Grisette/Core/Data/Class/Solvable.hs

@@ -21,12 +21,14 @@ where
 import Control.DeepSeq (NFData)
 import Data.Hashable (Hashable)
 import Data.String (IsString)
+import qualified Data.Text as T
 import Data.Typeable (Typeable)
 import Language.Haskell.TH.Syntax (Lift)
 
 -- $setup
 -- >>> import Grisette.Core
 -- >>> import Grisette.IR.SymPrim
+-- >>> :set -XOverloadedStrings
 
 -- | The class defines the creation and pattern matching of solvable type
 -- values.
@@ -59,7 +61,7 @@ class (IsString t) => Solvable c t | t -> c where
   -- False
   -- >>> (ssym "a" :: SymBool) &&~ ssym "a"
   -- a
-  ssym :: String -> t
+  ssym :: T.Text -> t
 
   -- | Generate indexed symbolic constants.
   --
@@ -68,7 +70,7 @@ class (IsString t) => Solvable c t | t -> c where
   --
   -- >>> isym "a" 1 :: SymBool
   -- a@1
-  isym :: String -> Int -> t
+  isym :: T.Text -> Int -> t
 
   -- | Generate simply-named symbolic constants with some extra information for
   -- disambiguation.
@@ -78,7 +80,7 @@ class (IsString t) => Solvable c t | t -> c where
   --
   -- >>> sinfosym "a" "someInfo" :: SymInteger
   -- a:"someInfo"
-  sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> t
+  sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> t
 
   -- | Generate indexed symbolic constants with some extra information for
   -- disambiguation.
@@ -89,7 +91,7 @@ class (IsString t) => Solvable c t | t -> c where
   --
   -- >>> iinfosym "a" 1 "someInfo" :: SymInteger
   -- a@1:"someInfo"
-  iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> t
+  iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> Int -> a -> t
 
 -- | Extract the concrete value from a solvable value with 'conView'.
 --

src/Grisette/Core/Data/FileLocation.hs

@@ -25,6 +25,7 @@ where
 
 import Control.DeepSeq (NFData)
 import Data.Hashable (Hashable)
+import qualified Data.Text as T
 import Debug.Trace.LocationTH (__LOCATION__)
 import GHC.Generics (Generic)
 import Grisette.Core.Data.Class.GenSym (FreshIdent, nameWithInfo)
@@ -60,7 +61,7 @@ parseFileLocation str =
 -- a:<interactive>:...
 --
 -- The uniqueness is ensured for the call to 'nameWithLoc' at different location.
-nameWithLoc :: String -> SpliceQ FreshIdent
+nameWithLoc :: T.Text -> SpliceQ FreshIdent
 nameWithLoc s = [||nameWithInfo s (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __LOCATION__))||]
 
 -- | Generate simply-named symbolic variables. The file location will be
@@ -78,7 +79,7 @@ nameWithLoc s = [||nameWithInfo s (parseFileLocation $$(liftSplice $ unsafeTExpC
 -- >>> let f _ = $$(slocsym "a") :: SymBool
 -- >>> f () == f ()
 -- True
-slocsym :: (Solvable c s) => String -> SpliceQ s
+slocsym :: (Solvable c s) => T.Text -> SpliceQ s
 slocsym nm = [||sinfosym nm (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __LOCATION__))||]
 
 -- | Generate indexed symbolic variables. The file location will be attached to identifier.
@@ -89,5 +90,5 @@ slocsym nm = [||sinfosym nm (parseFileLocation $$(liftSplice $ unsafeTExpCoerce
 -- Calling 'ilocsymb' with the same name and index at different location will
 -- always generate different symbolic constants. Calling 'slocsymb' at the same
 -- location for multiple times will generate the same symbolic constants.
-ilocsym :: (Solvable c s) => String -> Int -> SpliceQ s
+ilocsym :: (Solvable c s) => T.Text -> Int -> SpliceQ s
 ilocsym nm idx = [||iinfosym nm idx (parseFileLocation $$(liftSplice $ unsafeTExpCoerce __LOCATION__))||]

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs

@@ -78,6 +78,7 @@ import Data.Interned.Internal
   ( Cache (getCache),
     CacheState (CacheState),
   )
+import qualified Data.Text as T
 import GHC.IO (unsafeDupablePerformIO)
 import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
@@ -189,25 +190,25 @@ symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
 symTerm t = internTerm $ USymTerm t
 {-# INLINE symTerm #-}
 
-ssymTerm :: (SupportedPrim t, Typeable t) => String -> Term t
+ssymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Term t
 ssymTerm = symTerm . SimpleSymbol
 {-# INLINE ssymTerm #-}
 
-isymTerm :: (SupportedPrim t, Typeable t) => String -> Int -> Term t
+isymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Int -> Term t
 isymTerm str idx = symTerm $ IndexedSymbol str idx
 {-# INLINE isymTerm #-}
 
 sinfosymTerm ::
   (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
-  String ->
+  T.Text ->
   a ->
   Term t
 sinfosymTerm s info = symTerm $ WithInfo (SimpleSymbol s) info
 {-# INLINE sinfosymTerm #-}
 
 iinfosymTerm ::
   (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
-  String ->
+  T.Text ->
   Int ->
   a ->
   Term t

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot

@@ -57,6 +57,7 @@ where
 import Control.DeepSeq (NFData)
 import Data.Bits (Bits)
 import Data.Hashable (Hashable)
+import qualified Data.Text as T
 import Data.Typeable (Typeable)
 import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
@@ -100,16 +101,16 @@ constructTernary ::
   Term t
 conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
 symTerm :: (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
-ssymTerm :: (SupportedPrim t, Typeable t) => String -> Term t
-isymTerm :: (SupportedPrim t, Typeable t) => String -> Int -> Term t
+ssymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Term t
+isymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Int -> Term t
 sinfosymTerm ::
   (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
-  String ->
+  T.Text ->
   a ->
   Term t
 iinfosymTerm ::
   (SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
-  String ->
+  T.Text ->
   Int ->
   a ->
   Term t

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs

@@ -62,6 +62,7 @@
   )
 import Data.Kind (Constraint)
 import Data.String (IsString (fromString))
+import qualified Data.Text as T
 import Data.Typeable (Proxy (Proxy), cast)
 import GHC.Generics (Generic)
 import GHC.TypeNats (KnownNat, Nat, type (+), type (<=))
@@ -256,8 +257,8 @@
 -- >>> "a" :: TypedSymbol Bool
 -- a :: Bool
 data TypedSymbol t where
-  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t
-  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
+  SimpleSymbol :: (SupportedPrim t) => T.Text -> TypedSymbol t
+  IndexedSymbol :: (SupportedPrim t) => T.Text -> Int -> TypedSymbol t
   WithInfo ::
     forall t a.
     ( SupportedPrim t,
@@ -296,13 +297,13 @@
   liftTyped (WithInfo s1 i1) = [||WithInfo s1 i1||]
 
 instance Show (TypedSymbol t) where
-  show (SimpleSymbol str) = str ++ " :: " ++ show (typeRep @t)
-  show (IndexedSymbol str i) = str ++ "@" ++ show i ++ " :: " ++ show (typeRep @t)
+  show (SimpleSymbol str) = T.unpack str ++ " :: " ++ show (typeRep @t)
+  show (IndexedSymbol str i) = T.unpack str ++ "@" ++ show i ++ " :: " ++ show (typeRep @t)
   show (WithInfo s info) = showUntyped s ++ ":" ++ show info ++ " :: " ++ show (typeRep @t)
 
 showUntyped :: TypedSymbol t -> String
-showUntyped (SimpleSymbol str) = str
-showUntyped (IndexedSymbol str i) = str ++ "@" ++ show i
+showUntyped (SimpleSymbol str) = T.unpack str
+showUntyped (IndexedSymbol str i) = T.unpack str ++ "@" ++ show i
 showUntyped (WithInfo s info) = showUntyped s ++ ":" ++ show info
 
 instance Hashable (TypedSymbol t) where
@@ -316,7 +317,7 @@
   rnf (WithInfo s info) = rnf s `seq` rnf info
 
 instance (SupportedPrim t) => IsString (TypedSymbol t) where
-  fromString = SimpleSymbol
+  fromString = SimpleSymbol . T.pack
 
 withSymbolSupported :: TypedSymbol t -> ((SupportedPrim t) => a) -> a
 withSymbolSupported (SimpleSymbol _) a = a

src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot

@@ -33,6 +33,7 @@ import Data.Bits (Bits)
 import Data.Hashable (Hashable)
 import Data.Interned (Cache, Id)
 import Data.Kind (Constraint)
+import qualified Data.Text as T
 import GHC.TypeNats (KnownNat, type (+), type (<=))
 import Grisette.Core.Data.Class.BitVector
   ( BVSignConversion,
@@ -124,8 +125,8 @@ class
   pformatTernary :: tag -> Term arg1 -> Term arg2 -> Term arg3 -> String
 
 data TypedSymbol t where
-  SimpleSymbol :: (SupportedPrim t) => String -> TypedSymbol t
-  IndexedSymbol :: (SupportedPrim t) => String -> Int -> TypedSymbol t
+  SimpleSymbol :: (SupportedPrim t) => T.Text -> TypedSymbol t
+  IndexedSymbol :: (SupportedPrim t) => T.Text -> Int -> TypedSymbol t
   WithInfo ::
     forall t a.
     ( SupportedPrim t,

src/Grisette/IR/SymPrim/Data/SymPrim.hs

@@ -1045,15 +1045,15 @@ EQ_BV_SOME(SomeSymWordN, binSomeSymWordN)
 
 #define IS_STRING_SIMPLE(symtype) \
 instance IsString symtype where \
-  fromString = ssym
+  fromString = ssym . fromString
 
 #define IS_STRING_BV(symtype) \
 instance (KnownNat n, 1 <= n) => IsString (symtype n) where \
-  fromString = ssym
+  fromString = ssym . fromString
 
 #define IS_STRING_FUN(op, cons) \
 instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => IsString (sa op sb) where \
-  fromString = ssym
+  fromString = ssym . fromString
 
 #if 1
 IS_STRING_SIMPLE(SymBool)

test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -18,6 +19,7 @@ import qualified Data.HashMap.Strict as M
 import Data.Proxy (Proxy (Proxy))
 import qualified Data.SBV as SBV
 import qualified Data.SBV.Control as SBV
+import qualified Data.Text as T
 import GHC.Stack (HasCallStack)
 import Grisette.Backend.SBV.Data.SMT.Lowering (lowerSinglePrim)
 import Grisette.Backend.SBV.Data.SMT.Solving
@@ -231,7 +233,7 @@ testTernaryOpLowering ::
   ) =>
   GrisetteSMTConfig n ->
   (Term a -> Term b -> Term c -> Term d) ->
-  String ->
+  T.Text ->
   (TermTy n a -> TermTy n b -> TermTy n c -> TermTy n d) ->
   Assertion
 testTernaryOpLowering config f name sbvfun = do
@@ -250,7 +252,7 @@ testTernaryOpLowering config f name sbvfun = do
         satres <- SBV.checkSat
         case satres of
           SBV.Sat -> return ()
-          _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unsolvable formula"
+          _ -> lift $ assertFailure $ T.unpack $ "Lowering for " <> name <> " generated unsolvable formula"
       _ -> lift $ assertFailure "Failed to extract the term"
   SBV.runSMTWith (sbvConfig config) $ do
     (m, lt) <- lowerSinglePrim config fabc
@@ -271,7 +273,7 @@ testTernaryOpLowering config f name sbvfun = do
                 "Translation counter example found: "
                   ++ show (counterExampleA, counterExampleB, counterExampleC)
           SBV.Unsat -> return ()
-          _ -> lift $ assertFailure $ "Lowering for " ++ name ++ " generated unknown formula"
+          _ -> lift $ assertFailure $ T.unpack $ "Lowering for " <> name <> " generated unknown formula"
       _ -> lift $ assertFailure "Failed to extract the term"
 
 -- testTernaryOpLowering' ::