From ab9d9f55b74b7c7a7fb9c43dfa3dffeb39703f17 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Wed, 24 May 2023 09:31:43 -0700 Subject: [PATCH 1/2] Avoid printing newlines when processing some type default warnings Before, SAW would filter out type-default warnings when processing Cryptol, but would always pretty-print the warnings' container (`TypeDefaultWarnings`), even if filtering rendered it empty. Printing an empty `TypeDefaultWarnings` amounts to displaying a newline. See #1407. --- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index e6b7570b52..a87fa91b3d 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -771,16 +771,19 @@ defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts moduleCmdResult :: M.ModuleRes a -> IO (a, ME.ModuleEnv) moduleCmdResult (res, ws) = do - mapM_ (print . pp) (map suppressDefaulting ws) + mapM_ (print . pp) (concatMap suppressDefaulting ws) case res of Right (a, me) -> return (a, me) Left err -> fail $ "Cryptol error:\n" ++ show (pp err) -- X.throwIO (ModuleSystemError err) where - suppressDefaulting :: MM.ModuleWarning -> MM.ModuleWarning + suppressDefaulting :: MM.ModuleWarning -> [MM.ModuleWarning] suppressDefaulting w = case w of - MM.TypeCheckWarnings nm xs -> MM.TypeCheckWarnings nm (filter (notDefaulting . snd) xs) - MM.RenamerWarnings xs -> MM.RenamerWarnings xs + MM.RenamerWarnings xs -> [MM.RenamerWarnings xs] + MM.TypeCheckWarnings nm xs -> + case filter (notDefaulting . snd) xs of + [] -> [] + xs' -> [MM.TypeCheckWarnings nm xs'] notDefaulting :: TE.Warning -> Bool notDefaulting (TE.DefaultingTo {}) = False From 3a2143e82793d3604cd5e1e4fe95045502c1dfb9 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Thu, 4 Jan 2024 08:13:58 -0800 Subject: [PATCH 2/2] cryptol-saw-core: documentation --- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index a87fa91b3d..d8011aac0f 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -776,6 +776,8 @@ moduleCmdResult (res, ws) = do Right (a, me) -> return (a, me) Left err -> fail $ "Cryptol error:\n" ++ show (pp err) -- X.throwIO (ModuleSystemError err) where + -- If all warnings are about type defaults, pretend there are no warnings at + -- all to avoid displaying an empty warning container. suppressDefaulting :: MM.ModuleWarning -> [MM.ModuleWarning] suppressDefaulting w = case w of