REPL: Edit width should be 80. NFCI

sauclovian-g · sauclovian-g · commit ece1b22915ee · 2025-10-31T15:41:39.000-04:00
diff --git a/saw-script/src/SAWScript/REPL.hs b/saw-script/src/SAWScript/REPL.hs
@@ -38,25 +38,26 @@ run mfile opts = do
   (_result, _rst') <- runREPL (repl mfile) rst
   return ()
 
--- | Function to enter a nested TopLevel REPL, passed down into the interpreter
---   to avoid cyclic dependencies.
+-- | Function to enter a nested TopLevel REPL, passed down into the
+--   interpreter to avoid cyclic dependencies.
 --
---   Note that there isn't any REPL state that needs to be transferred to the
---   nested instance, only the interpreter state.
+--   Note that there isn't any REPL state that needs to be transferred
+--   to the nested instance, only the interpreter state.
 --
 reenterTopLevel :: TopLevelRO -> TopLevelRW -> IO TopLevelRW
 reenterTopLevel ro rw = do
     let rst = resumeREPL ro rw Nothing
     (_result, rst') <- runREPL (repl Nothing) rst
     return $ rTopLevelRW rst'
 
--- | Function to enter a nested ProofScript REPL, passed down into the interpreter
---   to avoid cyclic dependencies.
+-- | Function to enter a nested ProofScript REPL, passed down into the
+--   interpreter to avoid cyclic dependencies.
 --
---   Note that there isn't any REPL state that needs to be transferred to the
---   nested instance, only the interpreter state.
+--   Note that there isn't any REPL state that needs to be transferred
+--   to the nested instance, only the interpreter state.
 --
-reenterProofScript :: TopLevelRO -> TopLevelRW -> ProofState -> IO (TopLevelRW, ProofState)
+reenterProofScript ::
+    TopLevelRO -> TopLevelRW -> ProofState -> IO (TopLevelRW, ProofState)
 reenterProofScript ro rw pst = do
     let rst = resumeREPL ro rw (Just pst)
     (_result, rst') <- runREPL (repl Nothing) rst
diff --git a/saw-script/src/SAWScript/REPL/Command.hs b/saw-script/src/SAWScript/REPL/Command.hs
@@ -77,8 +77,10 @@ failOn errs = case (reverse errs) of
         fail (Text.unpack lastMsg)
 
 cdCmd :: FilePath -> REPL ()
-cdCmd f | null f = liftIO $ putStrLn $ "Error: The :cd command requires a path argument"
-        | otherwise = do
+cdCmd f
+    | null f =
+        liftIO $ putStrLn "Error: The :cd command requires a path argument"
+    | otherwise = do
   exists <- liftIO $ doesDirectoryExist f
   if exists
     then liftIO $ setCurrentDirectory f
@@ -141,7 +143,9 @@ quitCmd =
 
 searchCmd :: Text -> REPL ()
 searchCmd str
-  | Text.null str = liftIO $ putStrLn $ "Error: The :search command requires at least one argument"
+  | Text.null str =
+      let msg = "Error: The :search command requires at least one argument" in
+      liftIO $ putStrLn msg
   | otherwise = do
 
      -- FUTURE: it would be nice to be able to use the words
@@ -162,7 +166,8 @@ searchCmd str
      rw <- getTopLevelRW
      let environ = rwEnviron rw
          rebindables = rwRebindables rw
-     errs_or_pat <- liftIO $ Loader.readSchemaPattern replFileName environ rebindables avail str
+     errs_or_pat <- liftIO $
+         Loader.readSchemaPattern replFileName environ rebindables avail str
      pat <- case errs_or_pat of
            Left errs -> failOn errs
            Right p -> return p
@@ -213,7 +218,8 @@ searchCmd str
                      " with unexpected lifecycle " <> Text.pack (show lc)
                  ]
          (visMatches, expMatches, depMatches) =
-             Map.foldrWithKey inspect (Map.empty, Map.empty, Map.empty) allMatches
+             let empty = (Map.empty, Map.empty, Map.empty) in
+             Map.foldrWithKey inspect empty allMatches
 
          printMatch (name, (lc, ty)) = do
            let ty' = PPS.pShowText ty
@@ -252,13 +258,13 @@ searchCmd str
      else do
          liftIO $ putStrLn "No matches."
          if not (Map.null expMatches) then do
-             liftIO $ putStrLn $ "The following experimental matches require " ++
-                             "enable_experimental:"
+             liftIO $ putStrLn $ "The following experimental matches " ++
+                                 " require enable_experimental:"
              printMatches expMatches
              alsoDeprecated
          else if not (Map.null depMatches) then do
              liftIO $ putStrLn $ "The following deprecated matches require " ++
-                             "enable_deprecated:"
+                                 "enable_deprecated:"
              printMatches depMatches
          else
              pure ()
@@ -280,13 +286,15 @@ tenvCmd = do
 
 typeOfCmd :: Text -> REPL ()
 typeOfCmd str
-  | Text.null str = liftIO $ putStrLn "Error: The :type command requires an argument"
+  | Text.null str =
+        liftIO $ putStrLn "Error: The :type command requires an argument"
   | otherwise = do
      rw <- getTopLevelRW
      let environ = rwEnviron rw
          rebindables = rwRebindables rw
          avail = rwPrimsAvail rw
-     errs_or_expr <- liftIO $ Loader.readExpression replFileName environ rebindables avail str
+     errs_or_expr <- liftIO $
+         Loader.readExpression replFileName environ rebindables avail str
      (schema, _expr) <- case errs_or_expr of
          Left errs -> failOn errs
          Right info -> return info
@@ -448,7 +456,8 @@ executeReplCommand cmd args0 =
           [] -> action ""
           [arg] -> action arg
           _ -> do
-              let msg = "The command " <> cName cmd <> " takes only one argument"
+              let msg = "The command " <> cName cmd <>
+                        " takes only one argument"
               liftIO $ TextIO.putStrLn msg
     in
     exceptionProtect $ case cBody cmd of
@@ -467,7 +476,9 @@ executeReplCommand cmd args0 =
 -- | Execute REPL :-command text.
 executeReplCommandText :: Text -> REPL ()
 executeReplCommandText text =
-    let textWords = filter (\w -> not $ Text.null w) $ Text.split isSpace text in
+    let textWords =
+           filter (\w -> not $ Text.null w) $ Text.split isSpace text
+    in
     case textWords of
         [] -> pure ()
         cmdName : args ->
@@ -476,8 +487,9 @@ executeReplCommandText text =
                     -- Historically SAW accepts ":?cmd" without a space
                     if Text.isPrefixOf ":?" cmdName then
                         executeReplCommandText $ ":? " <> Text.drop 2 cmdName
-                    else
-                        liftIO $ TextIO.putStrLn $ "Unknown command: " <> cmdName
+                    else do
+                        let msg = "Unknown command: " <> cmdName
+                        liftIO $ TextIO.putStrLn msg
                 [cmd] ->
                     executeReplCommand cmd args
                 cmds -> liftIO $ do
diff --git a/saw-script/src/SAWScript/REPL/Data.hs b/saw-script/src/SAWScript/REPL/Data.hs
@@ -50,13 +50,15 @@ import SAWScript.REPL.Monad
 getCryptolExprNames :: REPL [Text]
 getCryptolExprNames =
   do fNames <- fmap getNamingEnv getCryptolEnv
-     return (map (Text.pack . show . pp) (Map.keys (MN.namespaceMap NSValue fNames)))
+     let keys = Map.keys (MN.namespaceMap NSValue fNames)
+     return (map (Text.pack . show . pp) keys)
 
 -- | Get visible Cryptol type names.
 getCryptolTypeNames :: REPL [Text]
 getCryptolTypeNames =
   do fNames <- fmap getNamingEnv getCryptolEnv
-     return (map (Text.pack . show . pp) (Map.keys (MN.namespaceMap NSType fNames)))
+     let keys = Map.keys (MN.namespaceMap NSType fNames)
+     return (map (Text.pack . show . pp) keys)
 
 -- | Get visible variable names for Haskeline completion.
 getSAWScriptValueNames :: REPL [Text]
diff --git a/saw-script/src/SAWScript/REPL/Haskeline.hs b/saw-script/src/SAWScript/REPL/Haskeline.hs
@@ -7,7 +7,8 @@ License     : BSD3
 Maintainer  : saw@galois.com
 Stability   : provisional
 
-Haskeline interface layer with main REPL loop and tab completion support.
+Haskeline interface layer with main REPL loop and tab completion
+support.
 -}
 
 module SAWScript.REPL.Haskeline (repl) where
@@ -335,7 +336,8 @@ completeReplCommand text cursor =
             -- text on the line, the LHS of the return value should
             -- always be the LHS of the input cursor.
 
-            let completion cmd = appendCompletion (Text.length cmdPrefix, cName cmd)
+            let completion cmd =
+                    appendCompletion (Text.length cmdPrefix, cName cmd)
             let completions = map completion $ searchCommandsByPrefix cmdPrefix
             return (cursorLeftRaw cursor, completions)
         cmdName : args ->
@@ -354,8 +356,8 @@ completeReplCommand text cursor =
                     -- but you can only actually give it one. Should
                     -- strengthen the argument schema.
                     case cBody cmd of
-                        ExprArg _     -> completeSAWScriptValue (last args) cursor
-                        TypeArgs _    -> completeSAWScriptType (last args) cursor
+                        ExprArg _   -> completeSAWScriptValue (last args) cursor
+                        TypeArgs _  -> completeSAWScriptType (last args) cursor
                         FilenameArg _ -> completeFilename cursor
                         ShellArg _    -> completeFilename cursor
                         NoArg       _ -> return (cursorLeftRaw cursor, [])
diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs
@@ -30,7 +30,10 @@ module SAWScript.REPL.Monad (
   ) where
 
 import Control.Monad (void)
-import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), MonadMask(..), catchJust)
+import Control.Monad.Catch (
+    MonadThrow(..), MonadCatch(..), MonadMask(..),
+    catchJust
+ )
 import Control.Monad.State (MonadState(..), StateT(..), get, gets, modify)
 import Control.Monad.Except (runExceptT)
 import Control.Monad.IO.Class (MonadIO(..))
@@ -42,9 +45,14 @@ import CryptolSAWCore.CryptolEnv
 
 import SAWCentral.Options (Options)
 import SAWCentral.Proof (ProofState, ProofResult(..))
-import SAWCentral.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel)
-import SAWCentral.Value (ProofScript(..), showsProofResult,
-                         rwGetCryptolEnv, TopLevelShellHook, ProofScriptShellHook)
+import SAWCentral.TopLevel (
+    TopLevelRO(..), TopLevelRW(..), TopLevel(..),
+    runTopLevel
+ )
+import SAWCentral.Value (
+    ProofScript(..), showsProofResult,
+    rwGetCryptolEnv, TopLevelShellHook, ProofScriptShellHook
+ )
 
 import SAWScript.Panic (panic)
 import SAWScript.Interpreter (buildTopLevelEnv)
@@ -64,7 +72,9 @@ data REPLState = REPLState
   }
 
 -- | Create an initial, empty environment.
-initREPL :: Bool -> Options -> TopLevelShellHook -> ProofScriptShellHook -> IO REPLState
+initREPL ::
+    Bool -> Options -> TopLevelShellHook -> ProofScriptShellHook ->
+    IO REPLState
 initREPL isBatch opts tlhook pshook =
   do (ro, rw) <- buildTopLevelEnv opts [] tlhook pshook
      return REPLState
@@ -93,7 +103,9 @@ resumeREPL ro rw mpst =
 
 -- | REPL monad context.
 newtype REPL a = REPL { unREPL :: StateT REPLState IO a }
-  deriving (Applicative, Functor, Monad, MonadThrow, MonadCatch, MonadMask, MonadFail)
+  deriving (
+      Applicative, Functor, Monad, MonadThrow, MonadCatch, MonadMask, MonadFail
+  )
 
 deriving instance MonadState REPLState REPL
 
@@ -119,7 +131,8 @@ liftProofScript m = do
     let pst = case mpst of
           Nothing -> panic "liftProofScript" ["Not in ProofScript mode"]
           Just ps -> ps
-    (result, pst') <- liftTopLevel $ runStateT (runExceptT (unProofScript m)) pst
+    (result, pst') <-
+        liftTopLevel $ runStateT (runExceptT (unProofScript m)) pst
     modify (\st -> st { rProofState = Just pst' })
     liftTopLevel $ case result of
        Left (stats, cex) ->
@@ -157,7 +170,8 @@ catchFail m k = catchJust sel m k
     sel e | isUserError e = Just (ioeGetErrorString e)
           | otherwise     = Nothing
 
--- | Handle any other exception (except that we ignore async exceptions and exitWith)
+-- | Handle any other exception (except that we ignore async
+--   exceptions and exitWith)
 catchOther :: REPL a -> (X.SomeException -> REPL a) -> REPL a
 catchOther m k = catchJust flt m k
  where
