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