Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Commit

Permalink
Supress defaulting warnings when loading cryptol modules.
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Aug 20, 2020
1 parent 0fe4d00 commit 2cea9b9
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Parser.Position as P
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Error as TE
import qualified Cryptol.TypeCheck.Infer as TI
import qualified Cryptol.TypeCheck.Kind as TK
import qualified Cryptol.TypeCheck.Monad as TM
Expand Down Expand Up @@ -592,7 +593,17 @@ defaultEvalOpts = E.EvalOpts quietLogger E.defaultPPOpts

moduleCmdResult :: M.ModuleRes a -> IO (a, ME.ModuleEnv)
moduleCmdResult (res, ws) = do
mapM_ (print . pp) ws
mapM_ (print . pp) (map 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 w =
case w of
MM.TypeCheckWarnings xs -> MM.TypeCheckWarnings (filter (notDefaulting . snd) xs)
MM.RenamerWarnings xs -> MM.RenamerWarnings xs

notDefaulting :: TE.Warning -> Bool
notDefaulting (TE.DefaultingTo {}) = False
notDefaulting _ = True

0 comments on commit 2cea9b9

Please sign in to comment.