Merge pull request #1270 from GaloisInc/issue1260

Convert some uses of `String` to `Text`

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -146,7 +146,7 @@ compMModule = mkModuleName ["CompM"]
 
 sawVectorDefinitionsModule :: TranslationConfiguration -> ModuleName
 sawVectorDefinitionsModule (TranslationConfiguration {..}) =
-  mkModuleName [vectorModule]
+  mkModuleName [Text.pack vectorModule]
 
 cryptolPrimitivesModule :: ModuleName
 cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"]

saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs

@@ -171,7 +171,7 @@ translateIdentWithArgs i args =
     UseRename targetModule targetName ->
       Coq.App (Coq.ExplVar $ identToCoq $
                mkIdent (fromMaybe (translateModuleName $ identModule i) targetModule)
-               targetName) <$>
+               (Text.pack targetName)) <$>
       mapM translateTerm args
     UseReplaceDropArgs n replacement
       | length args >= n -> Coq.App replacement <$> mapM translateTerm (drop n args)
@@ -186,9 +186,9 @@ translateIdent i = translateIdentWithArgs i []
 translateIdentToIdent :: TermTranslationMonad m => Ident -> m (Maybe Ident)
 translateIdentToIdent i =
   (atUseSite <$> findSpecialTreatment i) >>= \case
-    UsePreserve -> return $ Just (mkIdent translatedModuleName (identName i))
+    UsePreserve -> return $ Just (mkIdent translatedModuleName (identBaseName i))
     UseRename   targetModule targetName ->
-      return $ Just $ mkIdent (fromMaybe translatedModuleName targetModule) targetName
+      return $ Just $ mkIdent (fromMaybe translatedModuleName targetModule) (Text.pack targetName)
     UseReplaceDropArgs _ _ -> return Nothing
   where
     translatedModuleName = translateModuleName (identModule i)

saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RankNTypes #-}

saw-core/src/Verifier/SAW/Grammar.y

@@ -337,8 +337,8 @@ mkTupleProj t _ =
      return (badTerm (pos t))
 
 -- | Parse a term as a dotted list of strings
-parseModuleName :: Term -> Maybe [String]
-parseModuleName (RecordProj t str) = (++ [Text.unpack str]) <$> parseModuleName t
+parseModuleName :: Term -> Maybe [Text]
+parseModuleName (RecordProj t fname) = (++ [fname]) <$> parseModuleName t
 parseModuleName _ = Nothing
 
 -- | Parse a qualified recursor @M1.M2...Mn.d#rec@
@@ -359,7 +359,7 @@ parseTupleSelector t i =
 -- module name given first.
 mkPosModuleName :: [PosPair Text] -> PosPair ModuleName
 mkPosModuleName [] = error "internal: Unexpected empty module name"
-mkPosModuleName l = PosPair p (mkModuleName (fmap Text.unpack nms))
+mkPosModuleName l = PosPair p (mkModuleName nms)
   where nms = fmap val l
         p = pos (last l)
 }

saw-core/src/Verifier/SAW/Name.hs

@@ -25,7 +25,6 @@ module Verifier.SAW.Name
   , moduleNamePieces
    -- * Identifiers
   , Ident(identModule, identBaseName), identName, mkIdent
-  , mkIdentText
   , parseIdent
   , isIdent
   , identText
@@ -53,7 +52,6 @@ module Verifier.SAW.Name
 import           Control.Exception (assert)
 import           Data.Char
 import           Data.Hashable
-import qualified Data.List as L
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -91,10 +89,10 @@ moduleNamePieces (ModuleName x) = Text.splitOn (Text.pack ".") x
 
 -- | Create a module name given a list of strings with the top-most
 -- module name given first.
-mkModuleName :: [String] -> ModuleName
+mkModuleName :: [Text] -> ModuleName
 mkModuleName [] = error "internal: mkModuleName given empty module name"
-mkModuleName nms = assert (all isCtor nms) $ ModuleName (Text.pack s)
-  where s = L.intercalate "." (reverse nms)
+mkModuleName nms = assert (all (isCtor . Text.unpack) nms) $ ModuleName s
+  where s = Text.intercalate "." (reverse nms)
 
 preludeName :: ModuleName
 preludeName = mkModuleName ["Prelude"]
@@ -131,11 +129,8 @@ instance Read Ident where
     let (str1, str2) = break (not . isIdChar) str in
     [(parseIdent str1, str2)]
 
-mkIdent :: ModuleName -> String -> Ident
-mkIdent m s = Ident m (Text.pack s)
-
-mkIdentText :: ModuleName -> Text -> Ident
-mkIdentText m s = Ident m s
+mkIdent :: ModuleName -> Text -> Ident
+mkIdent m s = Ident m s
 
 -- | Parse a fully qualified identifier.
 parseIdent :: String -> Ident
@@ -146,9 +141,8 @@ parseIdent s0 =
       _ -> internalError $ "parseIdent given bad identifier " ++ show s0
   where breakEach s =
           case break (=='.') s of
-            (h,[]) -> [h]
-            (h,'.':r) -> h : breakEach r
-            _ -> internalError "parseIdent.breakEach failed"
+            (h, []) -> [Text.pack h]
+            (h, _ : r) -> Text.pack h : breakEach r
 
 instance IsString Ident where
   fromString = parseIdent

saw-core/src/Verifier/SAW/ParserUtils.hs

@@ -143,7 +143,7 @@ declareTypedNameFun sc_fun mnm nm apply_p tp =
   let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ Text.unpack nm in
   declareTermApplyFun th_nm (length $ fst $ Un.asPiList tp) $ \sc ts ->
   [| $(sc_fun) $(varE sc)
-   (mkIdent mnm $(stringE (Text.unpack nm)))
+   (mkIdent mnm (Text.pack $(stringE (Text.unpack nm))))
    $(ts) |]
 
 -- | Declare a Haskell function

saw-core/src/Verifier/SAW/Prelude/Constants.hs

@@ -7,6 +7,8 @@ Stability   : experimental
 Portability : non-portable (language extensions)
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Verifier.SAW.Prelude.Constants where
 
 import Verifier.SAW.Term.Functor

saw-core/src/Verifier/SAW/Typechecker.hs

@@ -43,7 +43,6 @@ import Prettyprinter hiding (Doc)
 import Verifier.SAW.Utils (internalError)
 
 import Verifier.SAW.Module
-import Verifier.SAW.Name (mkIdentText)
 import Verifier.SAW.Position
 import Verifier.SAW.Term.Functor
 import Verifier.SAW.Term.CtxTerm
@@ -178,7 +177,7 @@ typeInferCompleteTerm (matchAppliedRecursor -> Just (maybe_mnm, str, args)) =
          Just mnm -> return mnm
          Nothing -> getModuleName
      m <- liftTCM scFindModule mnm
-     let dt_ident = mkIdentText mnm str
+     let dt_ident = mkIdent mnm str
      dt <- case findDataType m str of
        Just d -> return d
        Nothing -> throwTCError $ NoSuchDataType dt_ident
@@ -330,7 +329,7 @@ processDecls (Un.TypeDecl NoQualifier (PosPair p nm) tp :
 
      -- Step 4: add the definition to the current module
      mnm <- getModuleName
-     let ident = mkIdentText mnm nm
+     let ident = mkIdent mnm nm
      t <- liftTCM scConstant' (ModuleIdentifier ident) def_tm def_tp
      liftTCM scRegisterGlobal ident t
      liftTCM scModifyModule mnm $ \m ->
@@ -350,7 +349,7 @@ processDecls (Un.TypeDecl q (PosPair p nm) tp : rest) =
    do typed_tp <- typeInferComplete tp
       void $ ensureSort $ typedType typed_tp
       mnm <- getModuleName
-      let ident = mkIdentText mnm nm
+      let ident = mkIdent mnm nm
       let nmi = ModuleIdentifier ident
       i <- liftTCM scFreshGlobalVar
       liftTCM scRegisterName i nmi
@@ -406,7 +405,7 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
 
   -- Step 4: Add d as an empty datatype, so we can typecheck the constructors
   mnm <- getModuleName
-  let dtName = mkIdentText mnm nm
+  let dtName = mkIdent mnm nm
   let dt = DataType { dtCtors = [], .. }
   liftTCM scModifyModule mnm (\m -> beginDataType m dt)
 
@@ -432,8 +431,8 @@ processDecls (Un.DataDecl (PosPair p nm) param_ctx dt_tp c_decls : rest) =
             let tp = typedVal typed_tp in
             case mkCtorArgStruct dtName p_ctx ix_ctx tp of
               Just arg_struct ->
-                liftTCM scBuildCtor dtName (mkIdentText mnm c)
-                (map (mkIdentText mnm . fst) typed_ctors)
+                liftTCM scBuildCtor dtName (mkIdent mnm c)
+                (map (mkIdent mnm . fst) typed_ctors)
                 arg_struct
               Nothing -> err ("Malformed type form constructor: " ++ show c)
 

saw-remote-api/src/SAWServer/Term.hs

@@ -16,11 +16,11 @@ instance FromJSON JSONModuleName where
     where
       literal =
         withText "module name as string" $
-        pure . JSONModuleName . mkModuleName . map T.unpack . T.splitOn "."
+        pure . JSONModuleName . mkModuleName . T.splitOn "."
       structured =
         withArray "module name as list of parts" $ \v ->
         do parts <- traverse parseJSON (V.toList v)
-           pure $ JSONModuleName $ mkModuleName $ map T.unpack parts
+           pure $ JSONModuleName $ mkModuleName parts
 
 instance ToJSON JSONModuleName where
   toJSON (JSONModuleName n) = toJSON (show n)

src/SAWScript/Builtins.hs

@@ -39,10 +39,11 @@ import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Text (Text)
+import qualified Data.Text as Text
 import Data.Time.Clock
 import Data.Typeable
 
-import qualified Data.Text as Text
 import System.Directory
 import qualified System.Environment
 import qualified System.Exit as Exit
@@ -884,23 +885,21 @@ cryptolSimpset =
   do sc <- getSharedContext
      io $ Cryptol.mkCryptolSimpset sc
 
-addPreludeEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addPreludeEqs :: [Text] -> Simpset -> TopLevel Simpset
 addPreludeEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Prelude"])
 
-addCryptolEqs :: [String] -> Simpset
-              -> TopLevel Simpset
+addCryptolEqs :: [Text] -> Simpset -> TopLevel Simpset
 addCryptolEqs names ss = do
   sc <- getSharedContext
   eqRules <- io $ mapM (scEqRewriteRule sc) (map qualify names)
   return (addRules eqRules ss)
     where qualify = mkIdent (mkModuleName ["Cryptol"])
 
-add_core_defs :: String -> [String] -> Simpset -> TopLevel Simpset
+add_core_defs :: Text -> [Text] -> Simpset -> TopLevel Simpset
 add_core_defs modname names ss =
   do sc <- getSharedContext
      defs <- io $ mapM (getDef sc) names -- FIXME: warn if not found
@@ -912,12 +911,12 @@ add_core_defs modname names ss =
       scFindDef sc (qualify n) >>= \maybe_def ->
       case maybe_def of
         Just d -> return d
-        Nothing -> fail $ modname ++ " definition " ++ n ++ " not found"
+        Nothing -> fail $ Text.unpack $ modname <> " definition " <> n <> " not found"
 
-add_prelude_defs :: [String] -> Simpset -> TopLevel Simpset
+add_prelude_defs :: [Text] -> Simpset -> TopLevel Simpset
 add_prelude_defs = add_core_defs "Prelude"
 
-add_cryptol_defs :: [String] -> Simpset -> TopLevel Simpset
+add_cryptol_defs :: [Text] -> Simpset -> TopLevel Simpset
 add_cryptol_defs = add_core_defs "Cryptol"
 
 rewritePrim :: Simpset -> TypedTerm -> TopLevel TypedTerm

src/SAWScript/Interpreter.hs

@@ -42,6 +42,7 @@ import qualified Data.Map as Map
 import Data.Map ( Map )
 import qualified Data.Set as Set
 import Data.Set ( Set )
+import qualified Data.Text as Text
 import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath)
 import System.FilePath (takeDirectory, hasDrive, (</>))
 import System.Process (readProcess)
@@ -171,7 +172,7 @@ interpret env expr =
     let ?fileReader = BS.readFile in
     case expr of
       SS.Bool b              -> return $ VBool b
-      SS.String s            -> return $ VString s
+      SS.String s            -> return $ VString (Text.pack s)
       SS.Int z               -> return $ VInteger z
       SS.Code str            -> do sc <- getSharedContext
                                    cenv <- fmap rwCryptol (getMergedEnv env)
@@ -605,7 +606,7 @@ set_color b = do
   putTopLevelRW rw { rwPPOpts = (rwPPOpts rw) { ppOptsColor = b' } }
 
 print_value :: Value -> TopLevel ()
-print_value (VString s) = printOutLnTop Info s
+print_value (VString s) = printOutLnTop Info (Text.unpack s)
 print_value (VTerm t) = do
   sc <- getSharedContext
   cenv <- fmap rwCryptol getTopLevelRW

src/SAWScript/Prover/Rewrite.hs

@@ -5,6 +5,8 @@ Maintainer  : GaloisInc
 Stability   : provisional
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module SAWScript.Prover.Rewrite where
 
 import Verifier.SAW.Rewriter

src/SAWScript/SBVParser.hs

@@ -128,7 +128,7 @@ parseSBVExpr opts sc unint nodes size (SBV.SBVApp operator sbvs) =
                Nothing ->
                    do printOutLn opts Warn ("WARNING: unknown uninterpreted function " ++ show (name, typ, size))
                       printOutLn opts Info ("Using Prelude." ++ name)
-                      scGlobalDef sc (mkIdent preludeName name)
+                      scGlobalDef sc (mkIdent preludeName (Text.pack name))
              args <- mapM (parseSBV sc nodes) sbvs
              let inSizes = map fst args
                  (TFun inTyp outTyp) = typ

src/SAWScript/Value.hs

@@ -111,7 +111,7 @@ import           What4.ProgramLoc (ProgramLoc(..))
 
 data Value
   = VBool Bool
-  | VString String
+  | VString Text
   | VInteger Integer
   | VArray [Value]
   | VTuple [Value]
@@ -529,7 +529,7 @@ extendEnv sc x mt md v rw =
          VCryptolModule m ->
            pure $ CEnv.bindCryptolModule (modname, m) ce
          VString s ->
-           do tt <- typedTermOfString sc s
+           do tt <- typedTermOfString sc (unpack s)
               pure $ CEnv.bindTypedTerm (ident, tt) ce
          _ ->
            pure ce
@@ -831,17 +831,17 @@ instance FromValue Cryptol.Schema where
     fromValue _ = error "fromValue Schema"
 
 instance IsValue String where
-    toValue n = VString n
+    toValue n = VString (pack n)
 
 instance FromValue String where
-    fromValue (VString n) = n
+    fromValue (VString n) = unpack n
     fromValue _ = error "fromValue String"
 
 instance IsValue Text where
-    toValue n = VString $ unpack n
+    toValue n = VString n
 
 instance FromValue Text where
-    fromValue (VString n) = pack n
+    fromValue (VString n) = n
     fromValue _ = error "fromValue Text"
 
 instance IsValue Integer where