-- | -- Module : REPL.Haskeline -- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable {-# LANGUAGE CPP #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE PatternGuards #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module REPL.Haskeline where import Cryptol.REPL.Command import Cryptol.REPL.Monad import Cryptol.REPL.Trie import Cryptol.Utils.PP import Cryptol.Utils.Logger(stdoutLogger) import Cryptol.Utils.Ident(modNameToText, interactiveName) import qualified Control.Exception as X import Control.Monad (guard, join) import qualified Control.Monad.Trans.Class as MTL #if !MIN_VERSION_haskeline(0,8,0) import Control.Monad.Trans.Control #endif import Data.Char (isAlphaNum, isSpace) import Data.Function (on) import Data.List (isPrefixOf,nub,sortBy,sort) import Data.Maybe(isJust) import qualified Data.Set as Set import qualified Data.Text as T (unpack) import System.Console.ANSI (setTitle, hSupportsANSI) import System.Console.Haskeline import System.Directory ( doesFileExist , getHomeDirectory , getCurrentDirectory) import System.FilePath (()) import System.IO (stdout) import Prelude () import Prelude.Compat -- | One REPL invocation, either from a file or from the terminal. crySession :: Maybe FilePath -> Bool -> REPL CommandExitCode crySession mbBatch stopOnError = do settings <- io (setHistoryFile (replSettings isBatch)) let act = runInputTBehavior behavior settings (withInterrupt loop) if isBatch then asBatch act else act where (isBatch,behavior) = case mbBatch of Nothing -> (False,defaultBehavior) Just path -> (True,useFile path) loop :: InputT REPL CommandExitCode loop = do ln <- getInputLines =<< MTL.lift getPrompt case ln of NoMoreLines -> return CommandOk Interrupted | isBatch && stopOnError -> return CommandError | otherwise -> loop NextLine line | all isSpace line -> loop | otherwise -> doCommand line doCommand txt = case parseCommand findCommandExact txt of Nothing | isBatch && stopOnError -> return CommandError | otherwise -> loop -- say somtething? Just cmd -> join $ MTL.lift $ do status <- handleInterrupt (handleCtrlC CommandError) (runCommand cmd) case status of CommandError | isBatch && stopOnError -> return (return status) _ -> do goOn <- shouldContinue return (if goOn then loop else return status) data NextLine = NextLine String | NoMoreLines | Interrupted getInputLines :: String -> InputT REPL NextLine getInputLines = handleInterrupt (MTL.lift (handleCtrlC Interrupted)) . loop [] where loop ls prompt = do mb <- getInputLine prompt let newPropmpt = map (\_ -> ' ') prompt case mb of Nothing -> return NoMoreLines Just l | not (null l) && last l == '\\' -> loop (init l : ls) newPropmpt | otherwise -> return $ NextLine $ unlines $ reverse $ l : ls loadCryRC :: Cryptolrc -> REPL CommandExitCode loadCryRC cryrc = case cryrc of CryrcDisabled -> return CommandOk CryrcDefault -> check [ getCurrentDirectory, getHomeDirectory ] CryrcFiles opts -> loadMany opts where check [] = return CommandOk check (place : others) = do dir <- io place let file = dir ".cryptolrc" present <- io (doesFileExist file) if present then crySession (Just file) True else check others loadMany [] = return CommandOk loadMany (f : fs) = do status <- crySession (Just f) True case status of CommandOk -> loadMany fs _ -> return status -- | Haskeline-specific repl implementation. repl :: Cryptolrc -> Maybe FilePath -> Bool -> REPL () -> IO CommandExitCode repl cryrc mbBatch stopOnError begin = runREPL (isJust mbBatch) stdoutLogger $ do status <- loadCryRC cryrc case status of CommandOk -> begin >> crySession mbBatch stopOnError _ -> return status -- | Try to set the history file. setHistoryFile :: Settings REPL -> IO (Settings REPL) setHistoryFile ss = do dir <- getHomeDirectory return ss { historyFile = Just (dir ".cryptol_history") } `X.catch` \(X.SomeException {}) -> return ss -- | Haskeline settings for the REPL. replSettings :: Bool -> Settings REPL replSettings isBatch = Settings { complete = cryptolCommand , historyFile = Nothing , autoAddHistory = not isBatch } -- .cryptolrc ------------------------------------------------------------------ -- | Configuration of @.cryptolrc@ file behavior. The default option -- searches the following locations in order, and evaluates the first -- file that exists in batch mode on interpreter startup: -- -- 1. $PWD/.cryptolrc -- 2. $HOME/.cryptolrc -- -- If files are specified, they will all be evaluated, but none of the -- default files will be (unless they are explicitly specified). -- -- The disabled option inhibits any reading of any .cryptolrc files. data Cryptolrc = CryrcDefault | CryrcDisabled | CryrcFiles [FilePath] deriving (Show) -- Utilities ------------------------------------------------------------------- #if !MIN_VERSION_haskeline(0,8,0) instance MonadException REPL where controlIO f = join $ liftBaseWith $ \f' -> f $ RunIO $ \m -> restoreM <$> (f' m) #endif -- Titles ---------------------------------------------------------------------- mkTitle :: Maybe LoadedModule -> String mkTitle lm = maybe "" (\ m -> pretty m ++ " - ") (lName =<< lm) ++ "cryptol" setREPLTitle :: REPL () setREPLTitle = do lm <- getLoadedMod io (setTitle (mkTitle lm)) -- | In certain environments like Emacs, we shouldn't set the terminal -- title. Note: this does not imply we can't use color output. We can -- use ANSI color sequences in places like Emacs, but not terminal -- codes. -- -- This checks that @'stdout'@ is a proper terminal handle, and that the -- terminal mode is not @dumb@, which is set by Emacs and others. shouldSetREPLTitle :: REPL Bool shouldSetREPLTitle = io (hSupportsANSI stdout) -- | Whether we can display color titles. This checks that @'stdout'@ -- is a proper terminal handle, and that the terminal mode is not -- @dumb@, which is set by Emacs and others. canDisplayColor :: REPL Bool canDisplayColor = io (hSupportsANSI stdout) -- Completion ------------------------------------------------------------------ -- | Completion for cryptol commands. cryptolCommand :: CompletionFunc REPL cryptolCommand cursor@(l,r) | ":" `isPrefixOf` l' , Just (cmd,rest) <- splitCommand l' = case nub (findCommand cmd) of [c] | null rest && not (any isSpace l') -> do return (l, cmdComp cmd c) | otherwise -> do (rest',cs) <- cmdArgument (cBody c) (reverse (sanitize rest),r) return (unwords [rest', reverse cmd],cs) cmds -> return (l, concat [ cmdComp l' c | c <- cmds ]) -- Complete all : commands when the line is just a : | ":" == l' = return (l, concat [ cmdComp l' c | c <- nub (findCommand ":") ]) | otherwise = completeExpr cursor where l' = sanitize (reverse l) -- | Generate completions from a REPL command definition. cmdComp :: String -> CommandDescr -> [Completion] cmdComp prefix c = do cName <- cNames c guard (prefix `isPrefixOf` cName) return $ nameComp prefix cName -- | Dispatch to a completion function based on the kind of completion the -- command is expecting. cmdArgument :: CommandBody -> CompletionFunc REPL cmdArgument ct cursor@(l,_) = case ct of ExprArg _ -> completeExpr cursor DeclsArg _ -> (completeExpr +++ completeType) cursor ExprTypeArg _ -> (completeExpr +++ completeType) cursor ModNameArg _ -> completeModName cursor FilenameArg _ -> completeFilename cursor ShellArg _ -> completeFilename cursor OptionArg _ -> completeOption cursor HelpArg _ -> completeHelp cursor NoArg _ -> return (l,[]) FileExprArg _ -> completeExpr cursor -- | Additional keywords to suggest in the REPL -- autocompletion list. keywords :: [String] keywords = [ "else" , "if" , "let" , "then" , "where" ] -- | Complete a name from the expression environment. completeExpr :: CompletionFunc REPL completeExpr (l,_) = do ns <- (keywords++) <$> getExprNames let n = reverse (takeIdent l) vars = sort $ filter (n `isPrefixOf`) ns return (l,map (nameComp n) vars) -- | Complete a name from the type synonym environment. completeType :: CompletionFunc REPL completeType (l,_) = do ns <- getTypeNames let n = reverse (takeIdent l) vars = filter (n `isPrefixOf`) ns return (l,map (nameComp n) vars) -- | Complete a name for which we can show REPL help documentation. completeHelp :: CompletionFunc REPL completeHelp (l, _) = do ns1 <- getExprNames ns2 <- getTypeNames let ns3 = concatMap cNames (nub (findCommand ":")) let ns = Set.toAscList (Set.fromList (ns1 ++ ns2)) ++ ns3 let n = reverse l case break isSpace n of (":set", _ : n') -> do let n'' = dropWhile isSpace n' let vars = map optName (lookupTrie (dropWhile isSpace n') userOptions) return (l, map (nameComp n'') vars) _ -> do let vars = filter (n `isPrefixOf`) ns return (l, map (nameComp n) vars) -- | Complete a name from the list of loaded modules. completeModName :: CompletionFunc REPL completeModName (l, _) = do ms <- getModNames let ns = map (T.unpack . modNameToText) (interactiveName : ms) n = reverse (takeWhile (not . isSpace) l) vars = filter (n `isPrefixOf`) ns return (l, map (nameComp n) vars) -- | Generate a completion from a prefix and a name. nameComp :: String -> String -> Completion nameComp prefix c = Completion { replacement = drop (length prefix) c , display = c , isFinished = True } -- | Return longest identifier (possibly a qualified name) that is a -- prefix of the given string takeIdent :: String -> String takeIdent (c : cs) | isIdentChar c = c : takeIdent cs takeIdent (':' : ':' : cs) = ':' : ':' : takeIdent cs takeIdent _ = [] isIdentChar :: Char -> Bool isIdentChar c = isAlphaNum c || c `elem` "_\'" -- | Join two completion functions together, merging and sorting their results. (+++) :: CompletionFunc REPL -> CompletionFunc REPL -> CompletionFunc REPL (as +++ bs) cursor = do (_,acs) <- as cursor (_,bcs) <- bs cursor return (fst cursor, sortBy (compare `on` replacement) (acs ++ bcs)) -- | Complete an option from the options environment. -- -- XXX this can do better, as it has access to the expected form of the value completeOption :: CompletionFunc REPL completeOption cursor@(l,_) = return (fst cursor, map comp opts) where n = reverse l opts = lookupTrie n userOptions comp opt = Completion { replacement = drop (length n) (optName opt) , display = optName opt , isFinished = False }