cryptol-2.12.0: cryptol/REPL/Haskeline.hs
-- |
-- 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 hiding ((</>))
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 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
data ReplMode
= InteractiveRepl -- ^ Interactive terminal session
| Batch FilePath -- ^ Execute from a batch file
| InteractiveBatch FilePath
-- ^ Execute from a batch file, but behave as though
-- lines are entered in an interactive session.
deriving (Show, Eq)
-- | One REPL invocation, either from a file or from the terminal.
crySession :: ReplMode -> Bool -> REPL CommandExitCode
crySession replMode stopOnError =
do settings <- io (setHistoryFile (replSettings isBatch))
let act = runInputTBehavior behavior settings (withInterrupt (loop 1))
if isBatch then asBatch act else act
where
(isBatch,behavior) = case replMode of
InteractiveRepl -> (False, defaultBehavior)
Batch path -> (True, useFile path)
InteractiveBatch path -> (False, useFile path)
loop :: Int -> InputT REPL CommandExitCode
loop lineNum =
do ln <- getInputLines =<< MTL.lift getPrompt
case ln of
NoMoreLines -> return CommandOk
Interrupted
| isBatch && stopOnError -> return CommandError
| otherwise -> loop lineNum
NextLine ls
| all (all isSpace) ls -> loop (lineNum + length ls)
| otherwise -> doCommand lineNum ls
run lineNum cmd =
case replMode of
InteractiveRepl -> runCommand lineNum Nothing cmd
InteractiveBatch _ -> runCommand lineNum Nothing cmd
Batch path -> runCommand lineNum (Just path) cmd
doCommand lineNum txt =
case parseCommand findCommandExact (unlines txt) of
Nothing | isBatch && stopOnError -> return CommandError
| otherwise -> loop (lineNum + length txt) -- say somtething?
Just cmd -> join $ MTL.lift $
do status <- handleInterrupt (handleCtrlC CommandError) (run lineNum cmd)
case status of
CommandError | isBatch && stopOnError -> return (return status)
_ -> do goOn <- shouldContinue
return (if goOn then loop (lineNum + length txt) 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 <- fmap (filter (/= '\r')) <$> 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 $ 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 (Batch file) True
else check others
loadMany [] = return CommandOk
loadMany (f : fs) = do status <- crySession (Batch f) True
case status of
CommandOk -> loadMany fs
_ -> return status
-- | Haskeline-specific repl implementation.
repl :: Cryptolrc -> ReplMode -> Bool -> Bool -> REPL () -> IO CommandExitCode
repl cryrc replMode callStacks stopOnError begin =
runREPL isBatch callStacks stdoutLogger replAction
where
-- this flag is used to suppress the logo and prompts
isBatch = case replMode of
InteractiveRepl -> False
Batch _ -> True
InteractiveBatch _ -> True
replAction =
do status <- loadCryRC cryrc
case status of
CommandOk -> begin >> crySession replMode 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
}