Convert more uses of String to Text.

Author: Brian Huffman

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -10,6 +10,7 @@ module Verifier.SAW.TypedTerm where
 import Control.Monad (foldM)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 
 import Cryptol.ModuleSystem.Name (nameIdent)
 import qualified Cryptol.TypeCheck.AST as C
@@ -62,7 +63,7 @@ applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
 applyTypedTerms sc = foldM (applyTypedTerm sc)
 
 -- | Create an abstract defined constant with the specified name and body.
-defineTypedTerm :: SharedContext -> String -> TypedTerm -> IO TypedTerm
+defineTypedTerm :: SharedContext -> Text -> TypedTerm -> IO TypedTerm
 defineTypedTerm sc name (TypedTerm schema t) =
   do ty <- scTypeOf sc t
      TypedTerm schema <$> scConstant sc name t ty

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

@@ -49,6 +49,7 @@ import           Data.Ratio
 import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.Word(Word64)
+import           Data.Text (Text)
 import qualified Data.Text as Text
 
 import           What4.BaseTypes
@@ -148,7 +149,7 @@ baseSCType sym sc bt =
 
 -- | Create a new symbolic variable.
 sawCreateVar :: SAWCoreState n
-             -> String                                       -- ^ the name of the variable
+             -> Text -- ^ the name of the variable
              -> SC.Term
              -> IO SC.Term
 sawCreateVar st nm tp = do
@@ -539,7 +540,7 @@ evaluateExpr sym st sc cache = f []
         B.UninterpVarKind -> do
           tp <- baseSCType sym sc (B.bvarType bv)
           SAWExpr <$> sawCreateVar st nm tp
-            where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv
+            where nm = solverSymbolAsText $ B.bvarName bv
         B.LatchVarKind ->
           unsupported sym "SAW backend does not support latch variables"
         B.QuantifierVarKind -> do

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

@@ -8,11 +8,14 @@ Portability : non-portable (language extensions)
 -}
 
 module Verifier.SAW.Constant (scConst) where
+
+import Data.Text (Text)
+
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Rewriter
 import Verifier.SAW.Conversion
 
-scConst :: SharedContext -> String -> Term -> IO Term
+scConst :: SharedContext -> Text -> Term -> IO Term
 scConst sc name t = do
   ty <- scTypeOf sc t
   ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty

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

@@ -68,7 +68,6 @@ import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
-import qualified Data.Text as Text
 import Control.Monad.Trans.Writer.Strict
 import Numeric.Natural
 
@@ -222,7 +221,7 @@ scMatch sc pat term =
              let fvy = looseVars y `intersectBitSets` (completeBitSet depth)
              guard (fvy `unionBitSets` fvj == fvj)
              let fixVar t (nm, ty) =
-                   do v <- scFreshGlobal sc (Text.unpack nm) ty
+                   do v <- scFreshGlobal sc nm ty
                       let Just ec = R.asExtCns v
                       t' <- instantiateVar sc 0 v t
                       return (t', ec)
@@ -882,7 +881,7 @@ doHoistIfs sc ss hoistCache itePat = go
        goF _ (Pi nm tp body) = goBinder scPi nm tp body
 
        goBinder close nm tp body = do
-           (ec, body') <- scOpenTerm sc (Text.unpack nm) tp 0 body
+           (ec, body') <- scOpenTerm sc nm tp 0 body
            (body'', conds) <- go body'
            let (stuck, float) = List.partition (\(_,ecs) -> Set.member ec ecs) conds
 

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

@@ -392,17 +392,16 @@ scShowTerm sc opts t =
      pure (showTermWithNames opts env t)
 
 -- | Create a global variable with the given identifier (which may be "_") and type.
-scFreshEC :: SharedContext -> String -> a -> IO (ExtCns a)
-scFreshEC sc x tp = do
-  i   <- scFreshGlobalVar sc
-  let x' = Text.pack x
-  let uri = scFreshNameURI x' i
-  let nmi = ImportedName uri [x',Text.pack (x <> "#" <>  show i)]
-  scRegisterName sc i nmi
-  pure (EC i nmi tp)
+scFreshEC :: SharedContext -> Text -> a -> IO (ExtCns a)
+scFreshEC sc x tp =
+  do i <- scFreshGlobalVar sc
+     let uri = scFreshNameURI x i
+     let nmi = ImportedName uri [x, x <> "#" <>  Text.pack (show i)]
+     scRegisterName sc i nmi
+     pure (EC i nmi tp)
 
 -- | Create a global variable with the given identifier (which may be "_") and type.
-scFreshGlobal :: SharedContext -> String -> Term -> IO Term
+scFreshGlobal :: SharedContext -> Text -> Term -> IO Term
 scFreshGlobal sc x tp = scExtCns sc =<< scFreshEC sc x tp
 
 -- | Returns shared term associated with ident.
@@ -1213,7 +1212,7 @@ scSort sc s = scFlatTermF sc (Sort s)
 scNat :: SharedContext -> Natural -> IO Term
 scNat sc n = scFlatTermF sc (NatLit n)
 
--- | Create a literal term (of saw-core type @String@) from a 'String'.
+-- | Create a literal term (of saw-core type @String@) from a 'Text'.
 scString :: SharedContext -> Text -> IO Term
 scString sc s = scFlatTermF sc (StringLit s)
 
@@ -1324,7 +1323,7 @@ scFunAll :: SharedContext
          -> IO Term
 scFunAll sc argTypes resultType = foldrM (scFun sc) resultType argTypes
 
--- | Create a lambda term from a parameter name (as a 'String'), parameter type
+-- | Create a lambda term from a parameter name (as a 'LocalName'), parameter type
 -- (as a 'Term'), and a body. Regarding deBruijn indices, in the body of the
 -- function, an index of 0 refers to the bound parameter.
 scLambda :: SharedContext
@@ -1378,7 +1377,7 @@ scLocalVar sc i = scTermF sc (LocalVar i)
 -- indices. If the body contains any ExtCns variables, they will be
 -- abstracted over and reapplied to the resulting constant.
 scConstant :: SharedContext
-           -> String -- ^ The name
+           -> Text   -- ^ The name
            -> Term   -- ^ The body
            -> Term   -- ^ The type
            -> IO Term
@@ -2337,7 +2336,7 @@ scTreeSize = fst . go (0, Map.empty)
 -- | `openTerm sc nm ty i body` replaces the loose deBruijn variable `i`
 --   with a fresh external constant (with name `nm`, and type `ty`) in `body`.
 scOpenTerm :: SharedContext
-         -> String
+         -> Text
          -> Term
          -> DeBruijnIndex
          -> Term

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

@@ -26,7 +26,6 @@ import Data.Foldable ( traverse_ )
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Maybe ( maybeToList )
-import qualified Data.Text as T
 
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Utils.Ident (mkIdent)
@@ -120,7 +119,7 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty
     go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return
     -- TODO: do we really want two names here?
     go (SetupFresh name@(ServerName n) debugName ty) =
-      do t <- lift $ jvm_fresh_var (T.unpack debugName) ty
+      do t <- lift $ jvm_fresh_var debugName ty
          (env, cenv) <- get
          put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv)
          save name (Val (MS.SetupTerm t))

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

@@ -25,7 +25,6 @@ import Data.Aeson (FromJSON(..), withObject, (.:))
 import Data.ByteString (ByteString)
 import Data.Map (Map)
 import qualified Data.Map as Map
-import qualified Data.Text as T
 
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Utils.Ident (mkIdent)
@@ -102,7 +101,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
        Nothing -> return ()
   where
     setupFresh (ContractVar n dn ty) =
-      do t <- llvm_fresh_var (T.unpack dn) (llvmType ty)
+      do t <- llvm_fresh_var dn (llvmType ty)
          return (n, t)
 
     setupState allocs (env, cenv) vars =

src/SAWScript/Builtins.hs

@@ -130,7 +130,7 @@ showPrim v = do
   opts <- fmap rwPPOpts getTopLevelRW
   return (SV.showsPrecValue opts 0 v "")
 
-definePrim :: String -> TypedTerm -> TopLevel TypedTerm
+definePrim :: Text -> TypedTerm -> TopLevel TypedTerm
 definePrim name (TypedTerm schema rhs) =
   do sc <- getSharedContext
      ty <- io $ Cryptol.importSchema sc Cryptol.emptyEnv schema
@@ -526,7 +526,7 @@ goal_assume =
   do sc <- SV.scriptTopLevel getSharedContext
      execTactic (tacticAssume sc)
 
-goal_intro :: String -> ProofScript TypedTerm
+goal_intro :: Text -> ProofScript TypedTerm
 goal_intro s =
   do sc <- SV.scriptTopLevel getSharedContext
      execTactic (tacticIntro sc s)
@@ -986,7 +986,7 @@ check_goal =
 fixPos :: Pos
 fixPos = PosInternal "FIXME"
 
-freshSymbolicPrim :: String -> C.Schema -> TopLevel TypedTerm
+freshSymbolicPrim :: Text -> C.Schema -> TopLevel TypedTerm
 freshSymbolicPrim x schema@(C.Forall [] [] ct) = do
   sc <- getSharedContext
   cty <- io $ Cryptol.importType sc Cryptol.emptyEnv ct

src/SAWScript/Crucible/Common/Setup/Type.hs

@@ -35,6 +35,7 @@ module SAWScript.Crucible.Common.Setup.Type
 import           Control.Lens
 import           Control.Monad.State (StateT)
 import           Control.Monad.IO.Class (MonadIO(liftIO))
+import           Data.Text (Text)
 
 import qualified Cryptol.TypeCheck.Type as Cryptol (Type)
 import qualified Verifier.SAW.Cryptol as Cryptol (importType, emptyEnv)
@@ -101,7 +102,7 @@ addCondition cond = currentState . MS.csConditions %= (cond : )
 freshTypedExtCns ::
   MonadIO m =>
   SharedContext {- ^ shared context -} ->
-  String        {- ^ variable name  -} ->
+  Text          {- ^ variable name  -} ->
   Cryptol.Type  {- ^ variable type  -} ->
   CrucibleSetupT arch m TypedExtCns
 freshTypedExtCns sc name cty =
@@ -116,7 +117,7 @@ freshTypedExtCns sc name cty =
 freshVariable ::
   MonadIO m =>
   SharedContext {- ^ shared context -} ->
-  String        {- ^ variable name  -} ->
+  Text          {- ^ variable name  -} ->
   Cryptol.Type  {- ^ variable type  -} ->
   CrucibleSetupT arch m TypedTerm
 freshVariable sc name cty =

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -55,6 +55,7 @@ import qualified Data.Map as Map
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import qualified Data.Sequence as Seq
+import           Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Vector as V
 import           Data.Void (absurd)
@@ -955,7 +956,7 @@ typeOfJavaType jty =
 -- | Generate a fresh variable term. The name will be used when
 -- pretty-printing the variable in debug output.
 jvm_fresh_var ::
-  String              {- ^ variable name    -} ->
+  Text                {- ^ variable name    -} ->
   JavaType            {- ^ variable type    -} ->
   JVMSetupM TypedTerm {- ^ fresh typed term -}
 jvm_fresh_var name jty =

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -106,6 +106,7 @@ import qualified Data.HashMap.Strict as HashMap
 import qualified Data.Set as Set
 import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
+import           Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Vector as V
 import           Prettyprinter
@@ -1439,7 +1440,7 @@ setupArg sc sym ecRef tp = do
     freshGlobal cty sc_tp =
       do ecs <- readIORef ecRef
          let len = Seq.length ecs
-         ec <- scFreshEC sc ("arg_"++show len) sc_tp
+         ec <- scFreshEC sc ("arg_" <> Text.pack (show len)) sc_tp
          writeIORef ecRef (ecs Seq.|> TypedExtCns cty ec)
          scFlatTermF sc (ExtCns ec)
 
@@ -1649,7 +1650,7 @@ cryptolTypeOfActual dl mt =
 -- | Generate a fresh variable term. The name will be used when
 -- pretty-printing the variable in debug output.
 llvm_fresh_var ::
-  String                  {- ^ variable name    -} ->
+  Text                    {- ^ variable name    -} ->
   L.Type                  {- ^ variable type    -} ->
   LLVMCrucibleSetupM TypedTerm {- ^ fresh typed term -}
 llvm_fresh_var name lty =
@@ -1665,7 +1666,7 @@ llvm_fresh_var name lty =
        Just cty -> Setup.freshVariable sc name cty
 
 llvm_fresh_cryptol_var ::
-  String ->
+  Text ->
   Cryptol.Schema ->
   LLVMCrucibleSetupM TypedTerm
 llvm_fresh_cryptol_var name s =

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -10,6 +10,7 @@ Stability   : provisional
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}

src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs

@@ -202,7 +202,7 @@ buildArg arg idx
         $ arg ^. argSkelType . typeSkelLLVMType
       pure (Just val, Nothing, arg ^. argSkelName)
   where
-    ident = maybe ("arg" <> show idx) Text.unpack $ arg ^. argSkelName
+    ident = maybe ("arg" <> Text.pack (show idx)) id $ arg ^. argSkelName
 
 skeleton_prestate ::
   FunctionSkeleton ->
@@ -237,7 +237,7 @@ rebuildArg (arg, prearg) idx
             -> LLVM.Array (fromIntegral $ s ^. sizeGuessElems) pt
           | otherwise -> pt
         _ -> pt
-      ident = maybe ("arg" <> show idx) Text.unpack nm
+      ident = maybe ("arg" <> Text.pack (show idx)) id nm
     in do
       val' <- llvm_fresh_var ident t
       llvm_points_to True ptr $ anySetupTerm val'
@@ -255,7 +255,7 @@ skeleton_poststate skel prestate = do
   case skel ^. funSkelRet . typeSkelLLVMType of
     LLVM.PrimType LLVM.Void -> pure ()
     t -> do
-      ret <- llvm_fresh_var ("return value of " <> (Text.unpack $ skel ^. funSkelName)) t
+      ret <- llvm_fresh_var ("return value of " <> (skel ^. funSkelName)) t
       llvm_return $ anySetupTerm ret
   pure $ SkeletonState{..}
 

src/SAWScript/JavaExpr.hs

@@ -68,6 +68,7 @@ import Language.JVM.Common (ppFldId)
 
 import Data.List (intercalate)
 import Data.List.Split
+import Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Vector as V
 import Text.Read hiding (lift)
@@ -209,7 +210,7 @@ data LogicExpr =
             }
   deriving (Show)
 
-scJavaValue :: SharedContext -> Term -> String -> IO Term
+scJavaValue :: SharedContext -> Term -> Text -> IO Term
 scJavaValue sc ty name = do
   scFreshGlobal sc name ty
 

src/SAWScript/Proof.hs

@@ -188,7 +188,7 @@ evalProp sc unints (Prop p) =
          Just t -> pure t
          Nothing -> fail "goal_eval: expected EqTrue"
 
-     ecs <- traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args
+     ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args
      vars <- traverse (scExtCns sc) ecs
      t0 <- instantiateVarList sc 0 (reverse vars) body'
 
@@ -726,7 +726,7 @@ predicateToSATQuery sc unintSet tm0 =
           case evalFOT mmap tp of
             Nothing -> fail ("predicateToSATQuery: expected first order type: " ++ showTerm tp)
             Just fot ->
-              do ec  <- scFreshEC sc (Text.unpack lnm) tp
+              do ec  <- scFreshEC sc lnm tp
                  etm <- scExtCns sc ec
                  body' <- instantiateVar sc 0 etm body
                  processTerm mmap (Map.insert ec fot vars) body'
@@ -779,7 +779,7 @@ propToSATQuery sc unintSet prop =
               case evalFOT mmap tp of
                 Nothing -> fail ("propToSATQuery: expected first order type: " ++ showTerm tp)
                 Just fot ->
-                  do ec  <- scFreshEC sc (Text.unpack lnm) tp
+                  do ec  <- scFreshEC sc lnm tp
                      etm <- scExtCns sc ec
                      body' <- instantiateVar sc 0 etm body
                      processTerm mmap (Map.insert ec fot vars) xs body'
@@ -830,12 +830,12 @@ goalApply sc rule goal = applyFirst (asPiLists (unProp rule))
 --   for the binder.  Return the generated fresh term.
 tacticIntro :: (F.MonadFail m, MonadIO m) =>
   SharedContext ->
-  String {- ^ Name to give to the variable.  If empty, will be chosen automatically from the goal. -} ->
+  Text {- ^ Name to give to the variable.  If empty, will be chosen automatically from the goal. -} ->
   Tactic m TypedTerm
 tacticIntro sc usernm = Tactic \goal ->
   case asPi (unProp (goalProp goal)) of
     Just (nm, tp, body) ->
-      do let name = if null usernm then Text.unpack nm else usernm
+      do let name = if Text.null usernm then nm else usernm
          xv <- liftIO $ scFreshEC sc name tp
          x  <- liftIO $ scExtCns sc xv
          tt <- liftIO $ mkTypedTerm sc x

src/SAWScript/Prover/MRSolver.hs

@@ -13,7 +13,6 @@ import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Except
 import Data.Semigroup
-import qualified Data.Text as Text
 
 import Prettyprinter
 
@@ -614,7 +613,7 @@ askMRSolver sc smt_conf timeout t1 t2 =
        flip evalStateT init_st $ runExceptT $
        do mrSolveEq (Type tp1) (Type tp2)
           let (pi_args, ret_tp) = asPiList tp1
-          vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal (Text.unpack x) x_tp) pi_args
+          vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal x x_tp) pi_args
           case asCompMApp ret_tp of
             Just _ -> return ()
             Nothing -> throwError (NotCompFunType tp1)