Switch StringLit to use Text instead of String.

GaloisInc · Jan 17, 2021 · 8034ecb · 8034ecb
1 parent 333c2a0
commit 8034ecb
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 6 deletions.
diff --git a/saw-core/src/Verifier/SAW/Recognizer.hs b/saw-core/src/Verifier/SAW/Recognizer.hs
@@ -75,6 +75,7 @@ import Control.Lens
 import Control.Monad
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 import Numeric.Natural (Natural)
 
 import Verifier.SAW.Term.Functor
@@ -287,7 +288,7 @@ asUnsignedConcreteBv term = do
   (n :*: v) <- asBvNat term
   return $ mod v (2 ^ n)
 
-asStringLit :: Recognizer Term String
+asStringLit :: Recognizer Term Text
 asStringLit t = do StringLit i <- asFTermF t; return i
 
 asLambda :: Recognizer Term (LocalName, Term, Term)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -1246,7 +1246,7 @@ scNat :: SharedContext -> Natural -> IO Term
 scNat sc n = scFlatTermF sc (NatLit n)
 
 -- | Create a literal term (of saw-core type @String@) from a 'String'.
-scString :: SharedContext -> String -> IO Term
+scString :: SharedContext -> Text -> IO Term
 scString sc s = scFlatTermF sc (StringLit s)
 
 -- | Create a term representing the primitive saw-core type @String@.

diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs
@@ -31,6 +31,7 @@ import Control.Monad.Fix (MonadFix(mfix))
 import Data.Bits
 import Data.Map (Map)
 import qualified Data.Map as Map
+import qualified Data.Text as Text
 import Data.Traversable
 import Data.Vector (Vector)
 import qualified Data.Vector as V
@@ -1209,7 +1210,7 @@ errorOp =
   constFun $
   strictFun $ \x ->
   case x of
-    VString s -> Prim.userError s
+    VString s -> Prim.userError (Text.unpack s)
     _ -> Prim.userError "unknown error"
 
 ------------------------------------------------------------

diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs
@@ -27,6 +27,7 @@ import Control.Monad (foldM, liftM, mapM)
 import Data.Kind (Type)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Vector (Vector)
 import qualified Data.Vector as V
@@ -59,7 +60,7 @@ data Value l
   | VInt (VInt l)
   | VIntMod !Natural (VInt l)
   | VArray (VArray l)
-  | VString !String
+  | VString !Text
   | VFloat !Float
   | VDouble !Double
   | VRecordValue ![(FieldName, Thunk l)]

diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs
@@ -332,7 +332,7 @@ data FlatTermF e
     -- | Array value includes type of elements followed by elements.
   | ArrayValue e (Vector e)
     -- | String literal
-  | StringLit !String
+  | StringLit !Text
 
     -- | An external constant with a name.
   | ExtCns !(ExtCns e)

diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs
@@ -264,7 +264,7 @@ typeInferCompleteTerm (Un.TypeConstraint t _ tp) =
 typeInferCompleteTerm (Un.NatLit _ i) =
   typeInferComplete (NatLit i :: FlatTermF TypedTerm)
 typeInferCompleteTerm (Un.StringLit _ str) =
-  typeInferComplete (StringLit str :: FlatTermF TypedTerm)
+  typeInferComplete (StringLit (Text.pack str) :: FlatTermF TypedTerm)
 typeInferCompleteTerm (Un.VecLit _ []) = throwTCError EmptyVectorLit
 typeInferCompleteTerm (Un.VecLit _ ts) =
   do typed_ts <- mapM typeInferComplete ts