Skip to content

Commit

Permalink
Merge pull request #2188 from GaloisInc/dholland-textify
Browse files Browse the repository at this point in the history
Apply a round of String to Text modernization
  • Loading branch information
sauclovian-g authored Jan 21, 2025
2 parents 7d2e9d3 + 7fe49d6 commit 18daa7c
Show file tree
Hide file tree
Showing 22 changed files with 216 additions and 153 deletions.
2 changes: 1 addition & 1 deletion crux-mir-comp/src/Mir/Cryptol.hs
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ loadCryptolFunc col sig modulePath name = do
-- (m, _ce') <- liftIO $ SAW.loadCryptolModule sc ce (Text.unpack modulePath)
-- tt <- liftIO $ SAW.lookupCryptolModule m (Text.unpack name)
tt <- liftIO $ SAW.parseTypedTerm sc ce' $
SAW.InputText (Text.unpack name) "<string>" 1 1
SAW.InputText name "<string>" 1 1

case typecheckFnSig sig (toListFC Some argShps) (Some retShp) (SAW.ttType tt) of
Left err -> fail $ "error loading " ++ show name ++ ": " ++ err
Expand Down
3 changes: 2 additions & 1 deletion cryptol-saw-core/cryptol-saw-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ test-suite cryptol-saw-core-tc-test
cryptol,
cryptol-saw-core,
heredoc >= 0.2,
saw-core
saw-core,
text

GHC-options: -threaded
14 changes: 9 additions & 5 deletions cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ Stability : provisional
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Verifier.SAW.CryptolEnv
Expand Down Expand Up @@ -42,6 +43,7 @@ module Verifier.SAW.CryptolEnv

--import qualified Control.Exception as X
import Data.ByteString (ByteString)
import qualified Data.Text as Text
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
Expand Down Expand Up @@ -108,7 +110,7 @@ import Cryptol.ModuleSystem.Env (ModContextParams(NoParams))

-- | Parse input, together with information about where it came from.
data InputText = InputText
{ inpText :: String -- ^ Parse this
{ inpText :: Text -- ^ Parse this
, inpFile :: String -- ^ It came from this file (or thing)
, inpLine :: Int -- ^ On this line number
, inpCol :: Int -- ^ On this column number
Expand Down Expand Up @@ -252,12 +254,14 @@ ioParseSchema = ioParseGeneric P.parseSchemaWith

ioParseGeneric ::
(P.Config -> Text -> Either P.ParseError a) -> InputText -> IO a
ioParseGeneric parse inp = ioParseResult (parse cfg (pack str))
ioParseGeneric parse inp = ioParseResult (parse cfg str)
where
cfg = P.defaultConfig { P.cfgSource = inpFile inp }
str = concat [ replicate (inpLine inp - 1) '\n'
, replicate (inpCol inp - 1) ' '
, inpText inp ]
-- XXX this is kind of gross; maybe sometime we get a second parser
-- entry point that takes a start position... (this is saw-script #2175)
str = Text.concat [ Text.replicate (inpLine inp - 1) "\n"
, Text.replicate (inpCol inp - 1) " "
, inpText inp ]

ioParseResult :: Either P.ParseError a -> IO a
ioParseResult res = case res of
Expand Down
6 changes: 4 additions & 2 deletions cryptol-saw-core/test/CryptolVerifierTC.hs
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}

module Main where

import qualified Data.ByteString as BS
import qualified Data.ByteString.Char8 as BS8
import qualified Data.Map as Map
import Data.Text (Text)

import Text.Heredoc (there)

Expand Down Expand Up @@ -54,8 +56,8 @@ checkTranslation sc (name, term) =
putStrLn $ unlines $ TC.prettyTCError err
fail "internal type error"

superclassContents :: String
superclassContents :: Text
superclassContents = [there|test/superclass.cry|]

instanceContents :: String
instanceContents :: Text
instanceContents = [there|test/instance.cry|]
1 change: 1 addition & 0 deletions saw-script.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,7 @@ executable saw
, haskeline
, mtl
, QuickCheck
, text
, transformers
, saw-script
, saw-core
Expand Down
11 changes: 6 additions & 5 deletions saw/SAWScript/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ import Control.Monad (guard, void)
import Data.Char (isSpace,isPunctuation,isSymbol)
import Data.Function (on)
import Data.List (intercalate, nub)
import qualified Data.Text as Text
import System.FilePath((</>), isPathSeparator)
import System.Directory(getHomeDirectory,getCurrentDirectory,setCurrentDirectory,doesDirectoryExist)
import qualified Data.Map as Map
Expand Down Expand Up @@ -164,7 +165,7 @@ typeOfCmd :: String -> REPL ()
typeOfCmd str
| null str = do io $ putStrLn $ "[error] :type requires an argument"
| otherwise =
do let tokens = SAWScript.Lexer.lexSAW replFileName str
do let tokens = SAWScript.Lexer.lexSAW replFileName (Text.pack str)
expr <- case SAWScript.Parser.parseExpression tokens of
Left err -> fail (show err)
Right expr -> return expr
Expand All @@ -188,20 +189,20 @@ quitCmd = stop
envCmd :: REPL ()
envCmd = do
env <- getValueEnvironment
let showLName = SS.getVal
let showLName = Text.unpack . SS.getVal
io $ sequence_ [ putStrLn (showLName x ++ " : " ++ SS.pShow v) | (x, v) <- Map.assocs (rwValueTypes env) ]

tenvCmd :: REPL ()
tenvCmd = do
env <- getValueEnvironment
io $ sequence_ [ putStrLn (a ++ " : " ++ SS.pShow t) | (a, t) <- Map.assocs (rwNamedTypes env) ]
io $ sequence_ [ putStrLn (Text.unpack a ++ " : " ++ SS.pShow t) | (a, t) <- Map.assocs (rwNamedTypes env) ]

helpCmd :: String -> REPL ()
helpCmd cmd
| null cmd = io (mapM_ putStrLn (genHelp commandList))
| otherwise =
do env <- getEnvironment
case Map.lookup cmd (rwDocs env) of
case Map.lookup (Text.pack cmd) (rwDocs env) of
Just d -> io $ putStr d
-- FIXME? can we restore the ability to lookup doc strings from Cryptol?
-- | Just (ec,_) <- lookup cmd builtIns =
Expand Down Expand Up @@ -246,7 +247,7 @@ caveats:
we also hang onto the results and use them to seed the interpreter. -}
sawScriptCmd :: String -> REPL ()
sawScriptCmd str = do
let tokens = SAWScript.Lexer.lexSAW replFileName str
let tokens = SAWScript.Lexer.lexSAW replFileName (Text.pack str)
case SAWScript.Parser.parseStmtSemi tokens of
Left err -> io $ print err
Right stmt ->
Expand Down
3 changes: 2 additions & 1 deletion saw/SAWScript/REPL/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ import qualified Control.Monad.Fail as Fail
import Data.IORef (IORef, newIORef, readIORef, modifyIORef, writeIORef)
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Text as Text
import Data.Typeable (Typeable)
import System.Console.ANSI (setTitle)
import qualified Control.Exception as X
Expand Down Expand Up @@ -498,7 +499,7 @@ getSAWScriptNames :: REPL [String]
getSAWScriptNames = do
env <- getEnvironment
let rnames = Map.keys (rwValues env)
return (map getVal rnames)
return (map (Text.unpack . getVal) rnames)

-- User Environment Interaction ------------------------------------------------

Expand Down
21 changes: 13 additions & 8 deletions src/SAWScript/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -36,12 +36,13 @@ module SAWScript.AST
, tBlock, tContext, tVar
, isContext

, PrettyPrint(..), pShow, commaSepAll, prettyWholeModule
, PrettyPrint(..), pShow, pShowText, commaSepAll, prettyWholeModule
) where

import SAWScript.Token
import SAWScript.Position (Pos(..), Positioned(..), maxSpan)

import Data.Text (Text)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (intercalate)
Expand All @@ -52,13 +53,14 @@ import Data.Traversable (Traversable)
#endif
import qualified Prettyprinter as PP
import Prettyprinter (Pretty)
import qualified Prettyprinter.Render.Text as PPT

import qualified Cryptol.Parser.AST as P (ImportSpec(..), ModName)
import qualified Cryptol.Utils.Ident as P (identText, modNameChunks)

-- Names {{{

type Name = String
type Name = Text

-- }}}

Expand Down Expand Up @@ -110,10 +112,10 @@ instance Positioned Import where
data Expr
-- Constants
= Bool Pos Bool
| String Pos String
| String Pos Text
| Int Pos Integer
| Code (Located String)
| CType (Located String)
| Code (Located Text)
| CType (Located Text)
-- Structures
| Array Pos [Expr]
| Block Pos [Stmt]
Expand Down Expand Up @@ -167,9 +169,9 @@ instance Positioned Pattern where
data Stmt
= StmtBind Pos Pattern Expr
| StmtLet Pos DeclGroup
| StmtCode Pos (Located String)
| StmtCode Pos (Located Text)
| StmtImport Pos Import
| StmtTypedef Pos (Located String) Type
| StmtTypedef Pos (Located Text) Type
deriving Show

instance Positioned Stmt where
Expand Down Expand Up @@ -287,7 +289,7 @@ instance Pretty Expr where
String _ s -> PP.dquotes (PP.pretty s)
Int _ i -> PP.pretty i
Code ls -> PP.braces . PP.braces $ PP.pretty (getVal ls)
CType (Located string _ _) -> PP.braces . PP.pretty $ "|" ++ string ++ "|"
CType (Located string _ _) -> PP.braces . PP.pretty $ "|" <> string <> "|"
Array _ xs -> PP.list (map PP.pretty xs)
Block _ stmts ->
"do" PP.<+> PP.lbrace PP.<> PP.line' PP.<>
Expand Down Expand Up @@ -403,6 +405,9 @@ dissectLambda = \case
pShow :: PrettyPrint a => a -> String
pShow = show . pretty 0

pShowText :: PrettyPrint a => a -> Text
pShowText = PPT.renderStrict . PP.layoutPretty PP.defaultLayoutOptions . pretty 0

class PrettyPrint p where
pretty :: Int -> p -> PP.Doc ann

Expand Down
Loading

0 comments on commit 18daa7c

Please sign in to comment.