1-- | 2-- Module : Cryptol.REPL.Monad 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE DeriveDataTypeable #-} 10{-# LANGUAGE LambdaCase #-} 11{-# LANGUAGE MultiParamTypeClasses #-} 12{-# LANGUAGE PatternGuards #-} 13{-# LANGUAGE RecordWildCards #-} 14{-# LANGUAGE TypeFamilies #-} 15{-# LANGUAGE ViewPatterns #-} 16{-# LANGUAGE FlexibleInstances #-} 17 18module Cryptol.REPL.Monad ( 19 -- * REPL Monad 20 REPL(..), runREPL 21 , io 22 , raise 23 , stop 24 , catch 25 , finally 26 , rPutStrLn 27 , rPutStr 28 , rPrint 29 30 -- ** Errors 31 , REPLException(..) 32 , rethrowEvalError 33 34 -- ** Environment 35 , getFocusedEnv 36 , getModuleEnv, setModuleEnv 37 , getDynEnv, setDynEnv 38 , getCallStacks 39 , uniqify, freshName 40 , whenDebug 41 , getEvalOptsAction 42 , getPPValOpts 43 , getExprNames 44 , getTypeNames 45 , getPropertyNames 46 , getModNames 47 , LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod 48 , setEditPath, getEditPath, clearEditPath 49 , setSearchPath, prependSearchPath 50 , getPrompt 51 , shouldContinue 52 , unlessBatch 53 , asBatch 54 , validEvalContext 55 , updateREPLTitle 56 , setUpdateREPLTitle 57 58 -- ** Config Options 59 , EnvVal(..) 60 , OptionDescr(..) 61 , setUser, getUser, getKnownUser, tryGetUser 62 , userOptions 63 , userOptionsWithAliases 64 , getUserSatNum 65 , getUserShowProverStats 66 , getUserProverValidate 67 , parsePPFloatFormat 68 , getProverConfig 69 70 -- ** Configurable Output 71 , getPutStr 72 , getLogger 73 , setPutStr 74 75 -- ** Smoke Test 76 , smokeTest 77 , Smoke(..) 78 79 ) where 80 81import Cryptol.REPL.Trie 82 83import Cryptol.Eval (EvalErrorEx, Unsupported, WordTooWide,EvalOpts(..)) 84import qualified Cryptol.ModuleSystem as M 85import qualified Cryptol.ModuleSystem.Env as M 86import qualified Cryptol.ModuleSystem.Name as M 87import qualified Cryptol.ModuleSystem.NamingEnv as M 88import Cryptol.Parser (ParseError,ppError) 89import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError) 90import Cryptol.Parser.NoPat (Error) 91import Cryptol.Parser.Position (emptyRange, Range(from)) 92import qualified Cryptol.TypeCheck.AST as T 93import qualified Cryptol.TypeCheck as T 94import qualified Cryptol.IR.FreeVars as T 95import qualified Cryptol.Utils.Ident as I 96import Cryptol.Utils.PP 97import Cryptol.Utils.Panic (panic) 98import Cryptol.Utils.Logger(Logger, logPutStr, funLogger) 99import qualified Cryptol.Parser.AST as P 100import Cryptol.Symbolic (SatNum(..)) 101import Cryptol.Symbolic.SBV (SBVPortfolioException) 102import Cryptol.Symbolic.What4 (W4Exception) 103import qualified Cryptol.Symbolic.SBV as SBV (proverNames, setupProver, defaultProver, SBVProverConfig) 104import qualified Cryptol.Symbolic.What4 as W4 (proverNames, setupProver, W4ProverConfig) 105 106import Control.Monad (ap,unless,when) 107import Control.Monad.Base 108import qualified Control.Monad.Catch as Ex 109import Control.Monad.IO.Class 110import Control.Monad.Trans.Control 111import Data.Char (isSpace, toLower) 112import Data.IORef 113 (IORef,newIORef,readIORef,modifyIORef,atomicModifyIORef) 114import Data.List (intercalate, isPrefixOf, unfoldr, sortBy) 115import Data.Maybe (catMaybes) 116import Data.Ord (comparing) 117import Data.Typeable (Typeable) 118import System.Directory (findExecutable) 119import qualified Control.Exception as X 120import qualified Data.Map as Map 121import qualified Data.Set as Set 122import Text.Read (readMaybe) 123 124import Data.SBV (SBVException) 125 126import Prelude () 127import Prelude.Compat 128 129-- REPL Environment ------------------------------------------------------------ 130 131-- | This indicates what the user would like to work on. 132data LoadedModule = LoadedModule 133 { lName :: Maybe P.ModName -- ^ Working on this module. 134 , lPath :: M.ModulePath -- ^ Working on this file. 135 } 136 137-- | REPL RW Environment. 138data RW = RW 139 { eLoadedMod :: Maybe LoadedModule 140 -- ^ This is the name of the currently "focused" module. 141 -- This is what we reload (:r) 142 143 , eEditFile :: Maybe FilePath 144 -- ^ This is what we edit (:e) 145 146 , eContinue :: Bool 147 -- ^ Should we keep going when we encounter an error, or give up. 148 149 , eIsBatch :: Bool 150 -- ^ Are we in batch mode. 151 152 , eModuleEnv :: M.ModuleEnv 153 -- ^ The current environment of all things loaded. 154 155 , eUserEnv :: UserEnv 156 -- ^ User settings 157 158 , eLogger :: Logger 159 -- ^ Use this to send messages to the user 160 161 , eCallStacks :: Bool 162 163 , eUpdateTitle :: REPL () 164 -- ^ Execute this every time we load a module. 165 -- This is used to change the title of terminal when loading a module. 166 167 , eProverConfig :: Either SBV.SBVProverConfig W4.W4ProverConfig 168 } 169 170-- | Initial, empty environment. 171defaultRW :: Bool -> Bool ->Logger -> IO RW 172defaultRW isBatch callStacks l = do 173 env <- M.initialModuleEnv 174 return RW 175 { eLoadedMod = Nothing 176 , eEditFile = Nothing 177 , eContinue = True 178 , eIsBatch = isBatch 179 , eModuleEnv = env 180 , eUserEnv = mkUserEnv userOptions 181 , eLogger = l 182 , eCallStacks = callStacks 183 , eUpdateTitle = return () 184 , eProverConfig = Left SBV.defaultProver 185 } 186 187-- | Build up the prompt for the REPL. 188mkPrompt :: RW -> String 189mkPrompt rw 190 | eIsBatch rw = "" 191 | detailedPrompt = withEdit ++ "> " 192 | otherwise = modLn ++ "> " 193 where 194 detailedPrompt = False 195 196 modLn = 197 case lName =<< eLoadedMod rw of 198 Nothing -> show (pp I.preludeName) 199 Just m 200 | M.isLoadedParamMod m (M.meLoadedModules (eModuleEnv rw)) -> 201 modName ++ "(parameterized)" 202 | otherwise -> modName 203 where modName = pretty m 204 205 withFocus = 206 case eLoadedMod rw of 207 Nothing -> modLn 208 Just m -> 209 case (lName m, lPath m) of 210 (Nothing, M.InFile f) -> ":r to reload " ++ show f ++ "\n" ++ modLn 211 _ -> modLn 212 213 withEdit = 214 case eEditFile rw of 215 Nothing -> withFocus 216 Just e 217 | Just (M.InFile f) <- lPath <$> eLoadedMod rw 218 , f == e -> withFocus 219 | otherwise -> ":e to edit " ++ e ++ "\n" ++ withFocus 220 221 222 223-- REPL Monad ------------------------------------------------------------------ 224 225-- | REPL_ context with InputT handling. 226newtype REPL a = REPL { unREPL :: IORef RW -> IO a } 227 228-- | Run a REPL action with a fresh environment. 229runREPL :: Bool -> Bool -> Logger -> REPL a -> IO a 230runREPL isBatch callStacks l m = do 231 ref <- newIORef =<< defaultRW isBatch callStacks l 232 unREPL m ref 233 234instance Functor REPL where 235 {-# INLINE fmap #-} 236 fmap f m = REPL (\ ref -> fmap f (unREPL m ref)) 237 238instance Applicative REPL where 239 {-# INLINE pure #-} 240 pure = return 241 {-# INLINE (<*>) #-} 242 (<*>) = ap 243 244instance Monad REPL where 245 {-# INLINE return #-} 246 return x = REPL (\_ -> return x) 247 248 {-# INLINE (>>=) #-} 249 m >>= f = REPL $ \ref -> do 250 x <- unREPL m ref 251 unREPL (f x) ref 252 253instance MonadIO REPL where 254 liftIO = io 255 256instance MonadBase IO REPL where 257 liftBase = liftIO 258 259instance MonadBaseControl IO REPL where 260 type StM REPL a = a 261 liftBaseWith f = REPL $ \ref -> 262 f $ \m -> unREPL m ref 263 restoreM x = return x 264 265instance M.FreshM REPL where 266 liftSupply f = modifyRW $ \ RW { .. } -> 267 let (a,s') = f (M.meSupply eModuleEnv) 268 in (RW { eModuleEnv = eModuleEnv { M.meSupply = s' }, .. },a) 269 270instance Ex.MonadThrow REPL where 271 throwM e = liftIO $ X.throwIO e 272 273instance Ex.MonadCatch REPL where 274 catch op handler = control $ \runInBase -> Ex.catch (runInBase op) (runInBase . handler) 275 276instance Ex.MonadMask REPL where 277 mask op = REPL $ \ref -> Ex.mask $ \u -> unREPL (op (q u)) ref 278 where q u (REPL b) = REPL (\ref -> u (b ref)) 279 280 uninterruptibleMask op = REPL $ \ref -> 281 Ex.uninterruptibleMask $ \u -> unREPL (op (q u)) ref 282 where q u (REPL b) = REPL (\ref -> u (b ref)) 283 284 generalBracket acq rls op = control $ \runInBase -> 285 Ex.generalBracket (runInBase acq) 286 (\saved -> \e -> runInBase (restoreM saved >>= \a -> rls a e)) 287 (\saved -> runInBase (restoreM saved >>= op)) 288 289-- Exceptions ------------------------------------------------------------------ 290 291-- | REPL exceptions. 292data REPLException 293 = ParseError ParseError 294 | FileNotFound FilePath 295 | DirectoryNotFound FilePath 296 | NoPatError [Error] 297 | NoIncludeError [IncludeError] 298 | EvalError EvalErrorEx 299 | TooWide WordTooWide 300 | Unsupported Unsupported 301 | ModuleSystemError NameDisp M.ModuleError 302 | EvalPolyError T.Schema 303 | TypeNotTestable T.Type 304 | EvalInParamModule [M.Name] 305 | SBVError String 306 | SBVException SBVException 307 | SBVPortfolioException SBVPortfolioException 308 | W4Exception W4Exception 309 deriving (Show,Typeable) 310 311instance X.Exception REPLException 312 313instance PP REPLException where 314 ppPrec _ re = case re of 315 ParseError e -> ppError e 316 FileNotFound path -> sep [ text "File" 317 , text ("`" ++ path ++ "'") 318 , text"not found" 319 ] 320 DirectoryNotFound path -> sep [ text "Directory" 321 , text ("`" ++ path ++ "'") 322 , text"not found or not a directory" 323 ] 324 NoPatError es -> vcat (map pp es) 325 NoIncludeError es -> vcat (map ppIncludeError es) 326 ModuleSystemError ns me -> fixNameDisp ns (pp me) 327 EvalError e -> pp e 328 Unsupported e -> pp e 329 TooWide e -> pp e 330 EvalPolyError s -> text "Cannot evaluate polymorphic value." 331 $$ text "Type:" <+> pp s 332 TypeNotTestable t -> text "The expression is not of a testable type." 333 $$ text "Type:" <+> pp t 334 EvalInParamModule xs -> 335 text "Expression depends on definitions from a parameterized module:" 336 $$ nest 2 (vcat (map pp xs)) 337 SBVError s -> text "SBV error:" $$ text s 338 SBVException e -> text "SBV exception:" $$ text (show e) 339 SBVPortfolioException e -> text "SBV exception:" $$ text (show e) 340 W4Exception e -> text "What4 exception:" $$ text (show e) 341 342-- | Raise an exception. 343raise :: REPLException -> REPL a 344raise exn = io (X.throwIO exn) 345 346 347catch :: REPL a -> (REPLException -> REPL a) -> REPL a 348catch m k = REPL (\ ref -> rethrowEvalError (unREPL m ref) `X.catch` \ e -> unREPL (k e) ref) 349 350finally :: REPL a -> REPL b -> REPL a 351finally m1 m2 = REPL (\ref -> unREPL m1 ref `X.finally` unREPL m2 ref) 352 353 354rethrowEvalError :: IO a -> IO a 355rethrowEvalError m = 356 run `X.catch` rethrow 357 `X.catch` rethrowTooWide 358 `X.catch` rethrowUnsupported 359 where 360 run = do 361 a <- m 362 return $! a 363 364 rethrow :: EvalErrorEx -> IO a 365 rethrow exn = X.throwIO (EvalError exn) 366 367 rethrowTooWide :: WordTooWide -> IO a 368 rethrowTooWide exn = X.throwIO (TooWide exn) 369 370 rethrowUnsupported :: Unsupported -> IO a 371 rethrowUnsupported exn = X.throwIO (Unsupported exn) 372 373 374-- Primitives ------------------------------------------------------------------ 375 376 377io :: IO a -> REPL a 378io m = REPL (\ _ -> m) 379 380getRW :: REPL RW 381getRW = REPL readIORef 382 383modifyRW :: (RW -> (RW,a)) -> REPL a 384modifyRW f = REPL (\ ref -> atomicModifyIORef ref f) 385 386modifyRW_ :: (RW -> RW) -> REPL () 387modifyRW_ f = REPL (\ ref -> modifyIORef ref f) 388 389-- | Construct the prompt for the current environment. 390getPrompt :: REPL String 391getPrompt = mkPrompt `fmap` getRW 392 393getCallStacks :: REPL Bool 394getCallStacks = eCallStacks <$> getRW 395 396-- Get the setting we should use for displaying values. 397getPPValOpts :: REPL PPOpts 398getPPValOpts = 399 do base <- getKnownUser "base" 400 ascii <- getKnownUser "ascii" 401 infLength <- getKnownUser "infLength" 402 403 fpBase <- getKnownUser "fpBase" 404 fpFmtTxt <- getKnownUser "fpFormat" 405 let fpFmt = case parsePPFloatFormat fpFmtTxt of 406 Just f -> f 407 Nothing -> panic "getPPOpts" 408 [ "Failed to parse fp-format" ] 409 410 return PPOpts { useBase = base 411 , useAscii = ascii 412 , useInfLength = infLength 413 , useFPBase = fpBase 414 , useFPFormat = fpFmt 415 } 416 417getEvalOptsAction :: REPL (IO EvalOpts) 418getEvalOptsAction = REPL $ \rwRef -> pure $ 419 do ppOpts <- unREPL getPPValOpts rwRef 420 l <- unREPL getLogger rwRef 421 return EvalOpts { evalPPOpts = ppOpts, evalLogger = l } 422 423clearLoadedMod :: REPL () 424clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw }) 425 updateREPLTitle 426 where upd x = x { lName = Nothing } 427 428-- | Set the name of the currently focused file, loaded via @:r@. 429setLoadedMod :: LoadedModule -> REPL () 430setLoadedMod n = do 431 modifyRW_ (\ rw -> rw { eLoadedMod = Just n }) 432 updateREPLTitle 433 434getLoadedMod :: REPL (Maybe LoadedModule) 435getLoadedMod = eLoadedMod `fmap` getRW 436 437 438 439-- | Set the path for the ':e' command. 440-- Note that this does not change the focused module (i.e., what ":r" reloads) 441setEditPath :: FilePath -> REPL () 442setEditPath p = modifyRW_ $ \rw -> rw { eEditFile = Just p } 443 444getEditPath :: REPL (Maybe FilePath) 445getEditPath = eEditFile <$> getRW 446 447clearEditPath :: REPL () 448clearEditPath = modifyRW_ $ \rw -> rw { eEditFile = Nothing } 449 450setSearchPath :: [FilePath] -> REPL () 451setSearchPath path = do 452 me <- getModuleEnv 453 setModuleEnv $ me { M.meSearchPath = path } 454 455prependSearchPath :: [FilePath] -> REPL () 456prependSearchPath path = do 457 me <- getModuleEnv 458 setModuleEnv $ me { M.meSearchPath = path ++ M.meSearchPath me } 459 460getProverConfig :: REPL (Either SBV.SBVProverConfig W4.W4ProverConfig) 461getProverConfig = eProverConfig <$> getRW 462 463shouldContinue :: REPL Bool 464shouldContinue = eContinue `fmap` getRW 465 466stop :: REPL () 467stop = modifyRW_ (\ rw -> rw { eContinue = False }) 468 469unlessBatch :: REPL () -> REPL () 470unlessBatch body = do 471 rw <- getRW 472 unless (eIsBatch rw) body 473 474-- | Run a computation in batch mode, restoring the previous isBatch 475-- flag afterwards 476asBatch :: REPL a -> REPL a 477asBatch body = do 478 wasBatch <- eIsBatch `fmap` getRW 479 modifyRW_ $ (\ rw -> rw { eIsBatch = True }) 480 a <- body 481 modifyRW_ $ (\ rw -> rw { eIsBatch = wasBatch }) 482 return a 483 484-- | Is evaluation enabled. If the currently focused module is 485-- parameterized, then we cannot evalute. 486validEvalContext :: T.FreeVars a => a -> REPL () 487validEvalContext a = 488 do me <- eModuleEnv <$> getRW 489 let ds = T.freeVars a 490 badVals = foldr badName Set.empty (T.valDeps ds) 491 bad = foldr badName badVals (T.tyDeps ds) 492 493 badName nm bs = 494 case M.nameInfo nm of 495 M.Declared m _ 496 | M.isLoadedParamMod m (M.meLoadedModules me) -> Set.insert nm bs 497 _ -> bs 498 499 unless (Set.null bad) $ 500 raise (EvalInParamModule (Set.toList bad)) 501 502 503 504-- | Update the title 505updateREPLTitle :: REPL () 506updateREPLTitle = unlessBatch $ do 507 rw <- getRW 508 eUpdateTitle rw 509 510-- | Set the function that will be called when updating the title 511setUpdateREPLTitle :: REPL () -> REPL () 512setUpdateREPLTitle m = modifyRW_ (\rw -> rw { eUpdateTitle = m }) 513 514-- | Set the REPL's string-printer 515setPutStr :: (String -> IO ()) -> REPL () 516setPutStr fn = modifyRW_ $ \rw -> rw { eLogger = funLogger fn } 517 518-- | Get the REPL's string-printer 519getPutStr :: REPL (String -> IO ()) 520getPutStr = 521 do rw <- getRW 522 return (logPutStr (eLogger rw)) 523 524getLogger :: REPL Logger 525getLogger = eLogger <$> getRW 526 527 528-- | Use the configured output action to print a string 529rPutStr :: String -> REPL () 530rPutStr str = do 531 f <- getPutStr 532 io (f str) 533 534-- | Use the configured output action to print a string with a trailing newline 535rPutStrLn :: String -> REPL () 536rPutStrLn str = rPutStr $ str ++ "\n" 537 538-- | Use the configured output action to print something using its Show instance 539rPrint :: Show a => a -> REPL () 540rPrint x = rPutStrLn (show x) 541 542getFocusedEnv :: REPL M.ModContext 543getFocusedEnv = M.focusedEnv <$> getModuleEnv 544 545-- | Get visible variable names. 546-- This is used for command line completition. 547getExprNames :: REPL [String] 548getExprNames = 549 do fNames <- M.mctxNames <$> getFocusedEnv 550 return (map (show . pp) (Map.keys (M.neExprs fNames))) 551 552-- | Get visible type signature names. 553-- This is used for command line completition. 554getTypeNames :: REPL [String] 555getTypeNames = 556 do fNames <- M.mctxNames <$> getFocusedEnv 557 return (map (show . pp) (Map.keys (M.neTypes fNames))) 558 559-- | Return a list of property names, sorted by position in the file. 560getPropertyNames :: REPL ([(M.Name,M.IfaceDecl)],NameDisp) 561getPropertyNames = 562 do fe <- getFocusedEnv 563 let xs = M.ifDecls (M.mctxDecls fe) 564 ps = sortBy (comparing (from . M.nameLoc . fst)) 565 [ (x,d) | (x,d) <- Map.toList xs, 566 T.PragmaProperty `elem` M.ifDeclPragmas d ] 567 568 return (ps, M.mctxNameDisp fe) 569 570getModNames :: REPL [I.ModName] 571getModNames = 572 do me <- getModuleEnv 573 return (map T.mName (M.loadedModules me)) 574 575getModuleEnv :: REPL M.ModuleEnv 576getModuleEnv = eModuleEnv `fmap` getRW 577 578setModuleEnv :: M.ModuleEnv -> REPL () 579setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me }) 580 581getDynEnv :: REPL M.DynamicEnv 582getDynEnv = (M.meDynEnv . eModuleEnv) `fmap` getRW 583 584setDynEnv :: M.DynamicEnv -> REPL () 585setDynEnv denv = do 586 me <- getModuleEnv 587 setModuleEnv (me { M.meDynEnv = denv }) 588 589 590-- | Given an existing qualified name, prefix it with a 591-- relatively-unique string. We make it unique by prefixing with a 592-- character @#@ that is not lexically valid in a module name. 593uniqify :: M.Name -> REPL M.Name 594 595uniqify name = 596 case M.nameInfo name of 597 M.Declared ns s -> 598 M.liftSupply (M.mkDeclared ns s (M.nameIdent name) (M.nameFixity name) (M.nameLoc name)) 599 600 M.Parameter -> 601 panic "[REPL] uniqify" ["tried to uniqify a parameter: " ++ pretty name] 602 603 604-- uniqify (P.QName Nothing name) = do 605-- i <- eNameSupply `fmap` getRW 606-- modifyRW_ (\rw -> rw { eNameSupply = i+1 }) 607-- let modname' = P.mkModName [ '#' : ("Uniq_" ++ show i) ] 608-- return (P.QName (Just modname') name) 609 610-- uniqify qn = 611-- panic "[REPL] uniqify" ["tried to uniqify a qualified name: " ++ pretty qn] 612 613 614-- | Generate a fresh name using the given index. The name will reside within 615-- the "<interactive>" namespace. 616freshName :: I.Ident -> M.NameSource -> REPL M.Name 617freshName i sys = 618 M.liftSupply (M.mkDeclared I.interactiveName sys i Nothing emptyRange) 619 620 621-- User Environment Interaction ------------------------------------------------ 622 623-- | User modifiable environment, for things like numeric base. 624type UserEnv = Map.Map String EnvVal 625 626data EnvVal 627 = EnvString String 628 | EnvProg String [String] 629 | EnvNum !Int 630 | EnvBool Bool 631 deriving (Show) 632 633-- | Generate a UserEnv from a description of the options map. 634mkUserEnv :: OptionMap -> UserEnv 635mkUserEnv opts = Map.fromList $ do 636 opt <- leaves opts 637 return (optName opt, optDefault opt) 638 639-- | Set a user option. 640setUser :: String -> String -> REPL () 641setUser name val = case lookupTrieExact name userOptionsWithAliases of 642 643 [opt] -> setUserOpt opt 644 [] -> rPutStrLn ("Unknown env value `" ++ name ++ "`") 645 _ -> rPutStrLn ("Ambiguous env value `" ++ name ++ "`") 646 647 where 648 setUserOpt opt = case optDefault opt of 649 EnvString _ -> doCheck (EnvString val) 650 651 EnvProg _ _ -> 652 case splitOptArgs val of 653 prog:args -> doCheck (EnvProg prog args) 654 [] -> rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`") 655 656 EnvNum _ -> case reads val of 657 [(x,_)] -> doCheck (EnvNum x) 658 _ -> rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`") 659 660 EnvBool _ 661 | any (`isPrefixOf` val) ["enable", "on", "yes", "true"] -> 662 writeEnv (EnvBool True) 663 | any (`isPrefixOf` val) ["disable", "off", "no", "false"] -> 664 writeEnv (EnvBool False) 665 | otherwise -> 666 rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`") 667 where 668 doCheck v = do (r,ws) <- optCheck opt v 669 case r of 670 Just err -> rPutStrLn err 671 Nothing -> do mapM_ rPutStrLn ws 672 writeEnv v 673 writeEnv ev = 674 do optEff opt ev 675 modifyRW_ (\rw -> rw { eUserEnv = Map.insert (optName opt) ev (eUserEnv rw) }) 676 677splitOptArgs :: String -> [String] 678splitOptArgs = unfoldr (parse "") 679 where 680 681 parse acc (c:cs) | isQuote c = quoted (c:acc) cs 682 | not (isSpace c) = parse (c:acc) cs 683 | otherwise = result acc cs 684 parse acc [] = result acc [] 685 686 quoted acc (c:cs) | isQuote c = parse (c:acc) cs 687 | otherwise = quoted (c:acc) cs 688 quoted acc [] = result acc [] 689 690 result [] [] = Nothing 691 result [] cs = parse [] (dropWhile isSpace cs) 692 result acc cs = Just (reverse acc, dropWhile isSpace cs) 693 694 isQuote :: Char -> Bool 695 isQuote c = c `elem` ("'\"" :: String) 696 697 698-- | Get a user option, using Maybe for failure. 699tryGetUser :: String -> REPL (Maybe EnvVal) 700tryGetUser name = do 701 rw <- getRW 702 return (Map.lookup name (eUserEnv rw)) 703 704-- | Get a user option, when it's known to exist. Fail with panic when it 705-- doesn't. 706getUser :: String -> REPL EnvVal 707getUser name = do 708 mb <- tryGetUser name 709 case mb of 710 Just ev -> return ev 711 Nothing -> panic "[REPL] getUser" ["option `" ++ name ++ "` does not exist"] 712 713getKnownUser :: IsEnvVal a => String -> REPL a 714getKnownUser x = fromEnvVal <$> getUser x 715 716class IsEnvVal a where 717 fromEnvVal :: EnvVal -> a 718 719instance IsEnvVal Bool where 720 fromEnvVal x = case x of 721 EnvBool b -> b 722 _ -> badIsEnv "Bool" 723 724instance IsEnvVal Int where 725 fromEnvVal x = case x of 726 EnvNum b -> b 727 _ -> badIsEnv "Num" 728 729instance IsEnvVal (String,[String]) where 730 fromEnvVal x = case x of 731 EnvProg b bs -> (b,bs) 732 _ -> badIsEnv "Prog" 733 734instance IsEnvVal String where 735 fromEnvVal x = case x of 736 EnvString b -> b 737 _ -> badIsEnv "String" 738 739badIsEnv :: String -> a 740badIsEnv x = panic "fromEnvVal" [ "[REPL] Expected a `" ++ x ++ "` value." ] 741 742 743getUserShowProverStats :: REPL Bool 744getUserShowProverStats = getKnownUser "proverStats" 745 746getUserProverValidate :: REPL Bool 747getUserProverValidate = getKnownUser "proverValidate" 748 749-- Environment Options --------------------------------------------------------- 750 751type OptionMap = Trie OptionDescr 752 753mkOptionMap :: [OptionDescr] -> OptionMap 754mkOptionMap = foldl insert emptyTrie 755 where 756 insert m d = insertTrie (optName d) d m 757 758-- | Returns maybe an error, and some warnings 759type Checker = EnvVal -> REPL (Maybe String, [String]) 760 761noCheck :: Checker 762noCheck _ = return (Nothing, []) 763 764noWarns :: Maybe String -> REPL (Maybe String, [String]) 765noWarns mb = return (mb, []) 766 767data OptionDescr = OptionDescr 768 { optName :: String 769 , optAliases :: [String] 770 , optDefault :: EnvVal 771 , optCheck :: Checker 772 , optHelp :: String 773 , optEff :: EnvVal -> REPL () 774 } 775 776simpleOpt :: String -> [String] -> EnvVal -> Checker -> String -> OptionDescr 777simpleOpt optName optAliases optDefault optCheck optHelp = 778 OptionDescr { optEff = \ _ -> return (), .. } 779 780userOptionsWithAliases :: OptionMap 781userOptionsWithAliases = foldl insert userOptions (leaves userOptions) 782 where 783 insert m d = foldl (\m' n -> insertTrie n d m') m (optAliases d) 784 785userOptions :: OptionMap 786userOptions = mkOptionMap 787 [ simpleOpt "base" [] (EnvNum 16) checkBase 788 "The base to display words at (2, 8, 10, or 16)." 789 , simpleOpt "debug" [] (EnvBool False) noCheck 790 "Enable debugging output." 791 , simpleOpt "ascii" [] (EnvBool False) noCheck 792 "Whether to display 7- or 8-bit words using ASCII notation." 793 , simpleOpt "infLength" ["inf-length"] (EnvNum 5) checkInfLength 794 "The number of elements to display for infinite sequences." 795 , simpleOpt "tests" [] (EnvNum 100) noCheck 796 "The number of random tests to try with ':check'." 797 , simpleOpt "satNum" ["sat-num"] (EnvString "1") checkSatNum 798 "The maximum number of :sat solutions to display (\"all\" for no limit)." 799 , simpleOpt "prover" [] (EnvString "z3") checkProver $ 800 "The external SMT solver for ':prove' and ':sat'\n(" ++ proverListString ++ ")." 801 , simpleOpt "warnDefaulting" ["warn-defaulting"] (EnvBool False) noCheck 802 "Choose whether to display warnings when defaulting." 803 , simpleOpt "warnShadowing" ["warn-shadowing"] (EnvBool True) noCheck 804 "Choose whether to display warnings when shadowing symbols." 805 , simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck 806 "Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator." 807 , simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck 808 "The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout." 809 , OptionDescr "monoBinds" ["mono-binds"] (EnvBool True) noCheck 810 "Whether or not to generalize bindings in a 'where' clause." $ 811 \case EnvBool b -> do me <- getModuleEnv 812 setModuleEnv me { M.meMonoBinds = b } 813 _ -> return () 814 815 , OptionDescr "tcSolver" ["tc-solver"] (EnvProg "z3" [ "-smt2", "-in" ]) 816 noCheck -- TODO: check for the program in the path 817 "The solver that will be used by the type checker." $ 818 \case EnvProg prog args -> do me <- getModuleEnv 819 let cfg = M.meSolverConfig me 820 setModuleEnv me { M.meSolverConfig = 821 cfg { T.solverPath = prog 822 , T.solverArgs = args } } 823 _ -> return () 824 825 , OptionDescr "tcDebug" ["tc-debug"] (EnvNum 0) 826 noCheck 827 (unlines 828 [ "Enable type-checker debugging output:" 829 , " * 0 no debug output" 830 , " * 1 show type-checker debug info" 831 , " * >1 show type-checker debug info and interactions with SMT solver"]) $ 832 \case EnvNum n -> do me <- getModuleEnv 833 let cfg = M.meSolverConfig me 834 setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = n } } 835 _ -> return () 836 , OptionDescr "coreLint" ["core-lint"] (EnvBool False) 837 noCheck 838 "Enable sanity checking of type-checker." $ 839 let setIt x = do me <- getModuleEnv 840 setModuleEnv me { M.meCoreLint = x } 841 in \case EnvBool True -> setIt M.CoreLint 842 EnvBool False -> setIt M.NoCoreLint 843 _ -> return () 844 845 , simpleOpt "hashConsing" ["hash-consing"] (EnvBool True) noCheck 846 "Enable hash-consing in the What4 symbolic backends." 847 848 , simpleOpt "proverStats" ["prover-stats"] (EnvBool True) noCheck 849 "Enable prover timing statistics." 850 851 , simpleOpt "proverValidate" ["prover-validate"] (EnvBool False) noCheck 852 "Validate :sat examples and :prove counter-examples for correctness." 853 854 , simpleOpt "showExamples" ["show-examples"] (EnvBool True) noCheck 855 "Print the (counter) example after :sat or :prove" 856 857 , simpleOpt "fpBase" ["fp-base"] (EnvNum 16) checkBase 858 "The base to display floating point numbers at (2, 8, 10, or 16)." 859 860 , simpleOpt "fpFormat" ["fp-format"] (EnvString "free") checkPPFloatFormat 861 $ unlines 862 [ "Specifies the format to use when showing floating point numbers:" 863 , " * free show using as many digits as needed" 864 , " * free+exp like `free` but always show exponent" 865 , " * .NUM show NUM (>=1) digits after floating point" 866 , " * NUM show using NUM (>=1) significant digits" 867 , " * NUM+exp like NUM but always show exponent" 868 ] 869 870 , simpleOpt "ignoreSafety" ["ignore-safety"] (EnvBool False) noCheck 871 "Ignore safety predicates when performing :sat or :prove checks" 872 ] 873 874 875parsePPFloatFormat :: String -> Maybe PPFloatFormat 876parsePPFloatFormat s = 877 case s of 878 "free" -> Just $ FloatFree AutoExponent 879 "free+exp" -> Just $ FloatFree ForceExponent 880 '.' : xs -> FloatFrac <$> readMaybe xs 881 _ | (as,res) <- break (== '+') s 882 , Just n <- readMaybe as 883 , Just e <- case res of 884 "+exp" -> Just ForceExponent 885 "" -> Just AutoExponent 886 _ -> Nothing 887 -> Just (FloatFixed n e) 888 _ -> Nothing 889 890checkPPFloatFormat :: Checker 891checkPPFloatFormat val = 892 case val of 893 EnvString s | Just _ <- parsePPFloatFormat s -> noWarns Nothing 894 _ -> noWarns $ Just "Failed to parse `fp-format`" 895 896 897 898-- | Check the value to the `base` option. 899checkBase :: Checker 900checkBase val = case val of 901 EnvNum n 902 | n `elem` [2,8,10,16] -> noWarns Nothing 903 | otherwise -> noWarns $ Just "base must be 2, 8, 10, or 16" 904 _ -> noWarns $ Just "unable to parse a value for base" 905 906checkInfLength :: Checker 907checkInfLength val = case val of 908 EnvNum n 909 | n >= 0 -> noWarns Nothing 910 | otherwise -> noWarns $ Just "the number of elements should be positive" 911 _ -> noWarns $ Just "unable to parse a value for infLength" 912 913checkProver :: Checker 914checkProver val = case val of 915 EnvString (map toLower -> s) 916 | s `elem` W4.proverNames -> 917 io (W4.setupProver s) >>= \case 918 Left msg -> noWarns (Just msg) 919 Right (ws, cfg) -> 920 do modifyRW_ (\rw -> rw{ eProverConfig = Right cfg }) 921 return (Nothing, ws) 922 | s `elem` SBV.proverNames -> 923 io (SBV.setupProver s) >>= \case 924 Left msg -> noWarns (Just msg) 925 Right (ws, cfg) -> 926 do modifyRW_ (\rw -> rw{ eProverConfig = Left cfg }) 927 return (Nothing, ws) 928 929 | otherwise -> 930 noWarns $ Just $ "Prover must be " ++ proverListString 931 932 _ -> noWarns $ Just "unable to parse a value for prover" 933 934allProvers :: [String] 935allProvers = SBV.proverNames ++ W4.proverNames 936 937proverListString :: String 938proverListString = concatMap (++ ", ") (init allProvers) ++ "or " ++ last allProvers 939 940checkSatNum :: Checker 941checkSatNum val = case val of 942 EnvString "all" -> noWarns Nothing 943 EnvString s -> 944 case readMaybe s :: Maybe Int of 945 Just n | n >= 1 -> noWarns Nothing 946 _ -> noWarns $ Just "must be an integer > 0 or \"all\"" 947 _ -> noWarns $ Just "unable to parse a value for satNum" 948 949getUserSatNum :: REPL SatNum 950getUserSatNum = do 951 s <- getKnownUser "satNum" 952 case s of 953 "all" -> return AllSat 954 _ | Just n <- readMaybe s -> return (SomeSat n) 955 _ -> panic "REPL.Monad.getUserSatNum" 956 [ "invalid satNum option" ] 957 958-- Environment Utilities ------------------------------------------------------- 959 960whenDebug :: REPL () -> REPL () 961whenDebug m = do 962 b <- getKnownUser "debug" 963 when b m 964 965-- Smoke Testing --------------------------------------------------------------- 966 967smokeTest :: REPL [Smoke] 968smokeTest = catMaybes <$> sequence tests 969 where 970 tests = [ z3exists ] 971 972type SmokeTest = REPL (Maybe Smoke) 973 974data Smoke 975 = Z3NotFound 976 deriving (Show, Eq) 977 978instance PP Smoke where 979 ppPrec _ smoke = 980 case smoke of 981 Z3NotFound -> text . intercalate " " $ [ 982 "[error] z3 is required to run Cryptol, but was not found in the" 983 , "system path. See the Cryptol README for more on how to install z3." 984 ] 985 986z3exists :: SmokeTest 987z3exists = do 988 mPath <- io $ findExecutable "z3" 989 case mPath of 990 Nothing -> return (Just Z3NotFound) 991 Just _ -> return Nothing 992