1-- | 2-- Module : REPL.Haskeline 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE CPP #-} 10{-# LANGUAGE MultiWayIf #-} 11{-# LANGUAGE PatternGuards #-} 12{-# OPTIONS_GHC -fno-warn-orphans #-} 13 14module REPL.Haskeline where 15 16import Cryptol.REPL.Command 17import Cryptol.REPL.Monad 18import Cryptol.REPL.Trie 19import Cryptol.Utils.PP 20import Cryptol.Utils.Logger(stdoutLogger) 21import Cryptol.Utils.Ident(modNameToText, interactiveName) 22 23import qualified Control.Exception as X 24import Control.Monad (guard, join) 25import qualified Control.Monad.Trans.Class as MTL 26#if !MIN_VERSION_haskeline(0,8,0) 27import Control.Monad.Trans.Control 28#endif 29import Data.Char (isAlphaNum, isSpace) 30import Data.Function (on) 31import Data.List (isPrefixOf,nub,sortBy,sort) 32import qualified Data.Set as Set 33import qualified Data.Text as T (unpack) 34import System.Console.ANSI (setTitle, hSupportsANSI) 35import System.Console.Haskeline 36import System.Directory ( doesFileExist 37 , getHomeDirectory 38 , getCurrentDirectory) 39import System.FilePath ((</>)) 40import System.IO (stdout) 41 42import Prelude () 43import Prelude.Compat 44 45 46data ReplMode 47 = InteractiveRepl -- ^ Interactive terminal session 48 | Batch FilePath -- ^ Execute from a batch file 49 | InteractiveBatch FilePath 50 -- ^ Execute from a batch file, but behave as though 51 -- lines are entered in an interactive session. 52 deriving (Show, Eq) 53 54-- | One REPL invocation, either from a file or from the terminal. 55crySession :: ReplMode -> Bool -> REPL CommandExitCode 56crySession replMode stopOnError = 57 do settings <- io (setHistoryFile (replSettings isBatch)) 58 let act = runInputTBehavior behavior settings (withInterrupt (loop 1)) 59 if isBatch then asBatch act else act 60 where 61 (isBatch,behavior) = case replMode of 62 InteractiveRepl -> (False, defaultBehavior) 63 Batch path -> (True, useFile path) 64 InteractiveBatch path -> (False, useFile path) 65 66 loop :: Int -> InputT REPL CommandExitCode 67 loop lineNum = 68 do ln <- getInputLines =<< MTL.lift getPrompt 69 case ln of 70 NoMoreLines -> return CommandOk 71 Interrupted 72 | isBatch && stopOnError -> return CommandError 73 | otherwise -> loop lineNum 74 NextLine ls 75 | all (all isSpace) ls -> loop (lineNum + length ls) 76 | otherwise -> doCommand lineNum ls 77 78 run lineNum cmd = 79 case replMode of 80 InteractiveRepl -> runCommand lineNum Nothing cmd 81 InteractiveBatch _ -> runCommand lineNum Nothing cmd 82 Batch path -> runCommand lineNum (Just path) cmd 83 84 doCommand lineNum txt = 85 case parseCommand findCommandExact (unlines txt) of 86 Nothing | isBatch && stopOnError -> return CommandError 87 | otherwise -> loop (lineNum + length txt) -- say somtething? 88 Just cmd -> join $ MTL.lift $ 89 do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd) 90 case status of 91 CommandError | isBatch && stopOnError -> return (return status) 92 _ -> do goOn <- shouldContinue 93 return (if goOn then loop (lineNum + length txt) else return status) 94 95 96data NextLine = NextLine [String] | NoMoreLines | Interrupted 97 98getInputLines :: String -> InputT REPL NextLine 99getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop [] 100 where 101 loop ls prompt = 102 do mb <- getInputLine prompt 103 let newPropmpt = map (\_ -> ' ') prompt 104 case mb of 105 Nothing -> return NoMoreLines 106 Just l 107 | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt 108 | otherwise -> return $ NextLine $ reverse $ l : ls 109 110loadCryRC :: Cryptolrc -> REPL CommandExitCode 111loadCryRC cryrc = 112 case cryrc of 113 CryrcDisabled -> return CommandOk 114 CryrcDefault -> check [ getCurrentDirectory, getHomeDirectory ] 115 CryrcFiles opts -> loadMany opts 116 where 117 check [] = return CommandOk 118 check (place : others) = 119 do dir <- io place 120 let file = dir </> ".cryptolrc" 121 present <- io (doesFileExist file) 122 if present 123 then crySession (Batch file) True 124 else check others 125 126 loadMany [] = return CommandOk 127 loadMany (f : fs) = do status <- crySession (Batch f) True 128 case status of 129 CommandOk -> loadMany fs 130 _ -> return status 131 132-- | Haskeline-specific repl implementation. 133repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode 134repl cryrc replMode callStacks stopOnError begin = 135 runREPL isBatch callStacks stdoutLogger replAction 136 137 where 138 -- this flag is used to suppress the logo and prompts 139 isBatch = case replMode of 140 InteractiveRepl -> False 141 Batch _ -> True 142 InteractiveBatch _ -> True 143 144 replAction = 145 do status <- loadCryRC cryrc 146 case status of 147 CommandOk -> begin >> crySession replMode stopOnError 148 _ -> return status 149 150-- | Try to set the history file. 151setHistoryFile :: Settings REPL -> IO (Settings REPL) 152setHistoryFile ss = 153 do dir <- getHomeDirectory 154 return ss { historyFile = Just (dir </> ".cryptol_history") } 155 `X.catch` \(X.SomeException {}) -> return ss 156 157-- | Haskeline settings for the REPL. 158replSettings :: Bool -> Settings REPL 159replSettings isBatch = Settings 160 { complete = cryptolCommand 161 , historyFile = Nothing 162 , autoAddHistory = not isBatch 163 } 164 165-- .cryptolrc ------------------------------------------------------------------ 166 167-- | Configuration of @.cryptolrc@ file behavior. The default option 168-- searches the following locations in order, and evaluates the first 169-- file that exists in batch mode on interpreter startup: 170-- 171-- 1. $PWD/.cryptolrc 172-- 2. $HOME/.cryptolrc 173-- 174-- If files are specified, they will all be evaluated, but none of the 175-- default files will be (unless they are explicitly specified). 176-- 177-- The disabled option inhibits any reading of any .cryptolrc files. 178data Cryptolrc = 179 CryrcDefault 180 | CryrcDisabled 181 | CryrcFiles [FilePath] 182 deriving (Show) 183 184-- Utilities ------------------------------------------------------------------- 185 186#if !MIN_VERSION_haskeline(0,8,0) 187instance MonadException REPL where 188 controlIO f = join $ liftBaseWith $ \f' -> 189 f $ RunIO $ \m -> restoreM <$> (f' m) 190#endif 191 192-- Titles ---------------------------------------------------------------------- 193 194mkTitle :: Maybe LoadedModule -> String 195mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm) 196 ++ "cryptol" 197 198setREPLTitle :: REPL () 199setREPLTitle = do 200 lm <- getLoadedMod 201 io (setTitle (mkTitle lm)) 202 203-- | In certain environments like Emacs, we shouldn't set the terminal 204-- title. Note: this does not imply we can't use color output. We can 205-- use ANSI color sequences in places like Emacs, but not terminal 206-- codes. 207-- 208-- This checks that @'stdout'@ is a proper terminal handle, and that the 209-- terminal mode is not @dumb@, which is set by Emacs and others. 210shouldSetREPLTitle :: REPL Bool 211shouldSetREPLTitle = io (hSupportsANSI stdout) 212 213-- | Whether we can display color titles. This checks that @'stdout'@ 214-- is a proper terminal handle, and that the terminal mode is not 215-- @dumb@, which is set by Emacs and others. 216canDisplayColor :: REPL Bool 217canDisplayColor = io (hSupportsANSI stdout) 218 219-- Completion ------------------------------------------------------------------ 220 221-- | Completion for cryptol commands. 222cryptolCommand :: CompletionFunc REPL 223cryptolCommand cursor@(l,r) 224 | ":" `isPrefixOf` l' 225 , Just (_,cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of 226 227 [c] | null rest && not (any isSpace l') -> do 228 return (l, cmdComp cmd c) 229 | otherwise -> do 230 (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) 231 return (unwords [rest', reverse cmd],cs) 232 233 cmds -> 234 return (l, concat [ cmdComp l' c | c <- cmds ]) 235 -- Complete all : commands when the line is just a : 236 | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ]) 237 | otherwise = completeExpr cursor 238 where 239 l' = sanitize (reverse l) 240 241-- | Generate completions from a REPL command definition. 242cmdComp :: String -> CommandDescr -> [Completion] 243cmdComp prefix c = do 244 cName <- cNames c 245 guard (prefix `isPrefixOf` cName) 246 return $ nameComp prefix cName 247 248-- | Dispatch to a completion function based on the kind of completion the 249-- command is expecting. 250cmdArgument :: CommandBody -> CompletionFunc REPL 251cmdArgument ct cursor@(l,_) = case ct of 252 ExprArg _ -> completeExpr cursor 253 DeclsArg _ -> (completeExpr +++ completeType) cursor 254 ExprTypeArg _ -> (completeExpr +++ completeType) cursor 255 ModNameArg _ -> completeModName cursor 256 FilenameArg _ -> completeFilename cursor 257 ShellArg _ -> completeFilename cursor 258 OptionArg _ -> completeOption cursor 259 HelpArg _ -> completeHelp cursor 260 NoArg _ -> return (l,[]) 261 FileExprArg _ -> completeExpr cursor 262 263-- | Additional keywords to suggest in the REPL 264-- autocompletion list. 265keywords :: [String] 266keywords = 267 [ "else" 268 , "if" 269 , "let" 270 , "then" 271 , "where" 272 ] 273 274-- | Complete a name from the expression environment. 275completeExpr :: CompletionFunc REPL 276completeExpr (l,_) = do 277 ns <- (keywords++) <$> getExprNames 278 let n = reverse (takeIdent l) 279 vars = sort $ filter (n `isPrefixOf`) ns 280 return (l,map (nameComp n) vars) 281 282-- | Complete a name from the type synonym environment. 283completeType :: CompletionFunc REPL 284completeType (l,_) = do 285 ns <- getTypeNames 286 let n = reverse (takeIdent l) 287 vars = filter (n `isPrefixOf`) ns 288 return (l,map (nameComp n) vars) 289 290-- | Complete a name for which we can show REPL help documentation. 291completeHelp :: CompletionFunc REPL 292completeHelp (l, _) = do 293 ns1 <- getExprNames 294 ns2 <- getTypeNames 295 let ns3 = concatMap cNames (nub (findCommand ":")) 296 let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3 297 let n = reverse l 298 case break isSpace n of 299 (":set", _ : n') -> 300 do let n'' = dropWhile isSpace n' 301 let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions) 302 return (l, map (nameComp n'') vars) 303 _ -> 304 do let vars = filter (n `isPrefixOf`) ns 305 return (l, map (nameComp n) vars) 306 307 308-- | Complete a name from the list of loaded modules. 309completeModName :: CompletionFunc REPL 310completeModName (l, _) = do 311 ms <- getModNames 312 let ns = map (T.unpack . modNameToText) (interactiveName : ms) 313 n = reverse (takeWhile (not . isSpace) l) 314 vars = filter (n `isPrefixOf`) ns 315 return (l, map (nameComp n) vars) 316 317-- | Generate a completion from a prefix and a name. 318nameComp :: String -> String -> Completion 319nameComp prefix c = Completion 320 { replacement = drop (length prefix) c 321 , display = c 322 , isFinished = True 323 } 324 325-- | Return longest identifier (possibly a qualified name) that is a 326-- prefix of the given string 327takeIdent :: String -> String 328takeIdent (c : cs) | isIdentChar c = c : takeIdent cs 329takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs 330takeIdent _ = [] 331 332isIdentChar :: Char -> Bool 333isIdentChar c = isAlphaNum c || c `elem` "_\'" 334 335-- | Join two completion functions together, merging and sorting their results. 336(+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL 337(as +++ bs) cursor = do 338 (_,acs) <- as cursor 339 (_,bcs) <- bs cursor 340 return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs)) 341 342 343-- | Complete an option from the options environment. 344-- 345-- XXX this can do better, as it has access to the expected form of the value 346completeOption :: CompletionFunc REPL 347completeOption cursor@(l,_) = return (fst cursor, map comp opts) 348 where 349 n = reverse l 350 opts = lookupTrie n userOptions 351 comp opt = Completion 352 { replacement = drop (length n) (optName opt) 353 , display = optName opt 354 , isFinished = False 355 } 356