diff --git a/cryptol/REPL/Command.hs b/cryptol/REPL/Command.hs index 5030a530..83837023 100644 --- a/cryptol/REPL/Command.hs +++ b/cryptol/REPL/Command.hs @@ -35,6 +35,7 @@ import REPL.Trie import qualified Cryptol.ModuleSystem as M import qualified Cryptol.ModuleSystem.Base as M (preludeName) import qualified Cryptol.ModuleSystem.NamingEnv as M +import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed)) import qualified Cryptol.Eval.Value as E import qualified Cryptol.Testing.Random as TestR @@ -691,18 +692,30 @@ liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleEnv moduleCmdResult :: M.ModuleRes a -> REPL a moduleCmdResult (res,ws0) = do - EnvBool yes <- getUser "warnDefaulting" + EnvBool warnDefaulting <- getUser "warnDefaulting" + EnvBool warnShadowing <- getUser "warnShadowing" + -- XXX: let's generalize this pattern let isDefaultWarn (T.DefaultingTo _ _) = True isDefaultWarn _ = False + filterDefaults w | warnDefaulting = Just w filterDefaults (M.TypeCheckWarnings xs) = case filter (not . isDefaultWarn . snd) xs of [] -> Nothing ys -> Just (M.TypeCheckWarnings ys) filterDefaults w = Just w - let ws = if yes then ws0 - else mapMaybe filterDefaults ws0 + isShadowWarn (M.SymbolShadowed _ _) = True + isShadowWarn _ = False + + filterShadowing w | warnShadowing = Just w + filterShadowing (M.RenamerWarnings xs) = + case filter (not . isShadowWarn) xs of + [] -> Nothing + ys -> Just (M.RenamerWarnings ys) + filterShadowing w = Just w + + let ws = mapMaybe filterDefaults . mapMaybe filterShadowing $ ws0 mapM_ (rPrint . pp) ws case res of Right (a,me') -> setModuleEnv me' >> return a diff --git a/cryptol/REPL/Monad.hs b/cryptol/REPL/Monad.hs index 9464d955..a28ca91a 100644 --- a/cryptol/REPL/Monad.hs +++ b/cryptol/REPL/Monad.hs @@ -521,6 +521,8 @@ userOptions = mkOptionMap "Use smt solver to filter conditional branches in proofs." , simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing) "Choose if we should display warnings when defaulting." + , simpleOpt "warnShadowing" (EnvBool True) (const $ return Nothing) + "Choose if we should display warnings when shadowing symbols." , simpleOpt "smtfile" (EnvString "-") (const $ return Nothing) "The file to use for SMT-Lib scripts (for debugging or offline proving)" , OptionDescr "mono-binds" (EnvBool True) (const $ return Nothing)