Skip to content

Commit

Permalink
Merge pull request #2001 from GaloisInc/bugfix/excess-newline-printing
Browse files Browse the repository at this point in the history
Avoid printing newlines when processing some type default warnings
  • Loading branch information
samcowger authored Jan 4, 2024
2 parents 2d0e3d1 + 3a2143e commit 8e6371e
Showing 1 changed file with 9 additions and 4 deletions.
13 changes: 9 additions & 4 deletions cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -771,16 +771,21 @@ 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
-- 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
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
Expand Down

0 comments on commit 8e6371e

Please sign in to comment.