diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs index bd2a5b71cb..04d787652a 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs +++ b/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"] diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs index 4bbc3828d4..6542cc6352 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/Term.hs +++ b/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) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs index ad739a9881..90c517d667 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs +++ b/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 #-} diff --git a/saw-core/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y index 498f2a1065..acb06f2284 100644 --- a/saw-core/src/Verifier/SAW/Grammar.y +++ b/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) } diff --git a/saw-core/src/Verifier/SAW/Name.hs b/saw-core/src/Verifier/SAW/Name.hs index c2961e6e91..df3d5035b1 100644 --- a/saw-core/src/Verifier/SAW/Name.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/ParserUtils.hs b/saw-core/src/Verifier/SAW/ParserUtils.hs index f30eab06e9..20e015119b 100644 --- a/saw-core/src/Verifier/SAW/ParserUtils.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Prelude/Constants.hs b/saw-core/src/Verifier/SAW/Prelude/Constants.hs index fbc4163683..460b2c1170 100644 --- a/saw-core/src/Verifier/SAW/Prelude/Constants.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs index a7c241bf27..655ed48de0 100644 --- a/saw-core/src/Verifier/SAW/Typechecker.hs +++ b/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) diff --git a/saw-remote-api/src/SAWServer/Term.hs b/saw-remote-api/src/SAWServer/Term.hs index 5fd2a6f17b..084056a8c5 100644 --- a/saw-remote-api/src/SAWServer/Term.hs +++ b/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) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bf191a09ba..baf2f26fde 100644 --- a/src/SAWScript/Builtins.hs +++ b/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 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 88ff31e39c..300048710f 100644 --- a/src/SAWScript/Interpreter.hs +++ b/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 diff --git a/src/SAWScript/Prover/Rewrite.hs b/src/SAWScript/Prover/Rewrite.hs index 0b50a7dd25..7de2ebaea0 100644 --- a/src/SAWScript/Prover/Rewrite.hs +++ b/src/SAWScript/Prover/Rewrite.hs @@ -5,6 +5,8 @@ Maintainer : GaloisInc Stability : provisional -} +{-# LANGUAGE OverloadedStrings #-} + module SAWScript.Prover.Rewrite where import Verifier.SAW.Rewriter diff --git a/src/SAWScript/SBVParser.hs b/src/SAWScript/SBVParser.hs index 8176011aa9..ce2ff0ac94 100644 --- a/src/SAWScript/SBVParser.hs +++ b/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 diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index a237221cbe..0c3e9f6068 100644 --- a/src/SAWScript/Value.hs +++ b/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