packages feed

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
    }