content: -- |
  -- Module      :  Main
  -- Copyright   :  (c) 2013-2016 Galois, Inc.
  -- License     :  BSD3
  -- Maintainer  :  cryptol@galois.com
  -- Stability   :  provisional
  -- Portability :  portable
  
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedStrings #-}
  module Main where
  
  import OptParser
  
  import Cryptol.REPL.Command (loadCmd,loadPrelude,CommandResult(..))
  import Cryptol.REPL.Monad (REPL,updateREPLTitle,setUpdateREPLTitle,
                     io,prependSearchPath,setSearchPath,parseSearchPath)
  import qualified Cryptol.REPL.Monad as REPL
  import Cryptol.ModuleSystem.Env(ModulePath(..))
  import qualified Cryptol.Project as Project
  
  import REPL.Haskeline
  import REPL.Logo
  
  import Cryptol.Utils.PP
  import Cryptol.Version (displayVersion)
  
  import Control.Monad (when, void)
  import Data.Maybe (isJust, isNothing)
  import GHC.IO.Encoding (setLocaleEncoding, utf8)
  import System.Console.GetOpt
      (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)
  import System.Directory (getTemporaryDirectory, removeFile)
  import System.Environment (getArgs, getProgName, lookupEnv)
  import System.Exit (exitFailure,exitSuccess)
  import System.FilePath (searchPathSeparator, takeDirectory)
  import System.IO (hClose, hPutStr, openTempFile)
  
  
  import Prelude ()
  import Prelude.Compat
  
  data ColorMode = AutoColor | NoColor | AlwaysColor
    deriving (Show, Eq)
  
  data Options = Options
    { optLoad            :: [FilePath]
    , optVersion         :: Bool
    , optHelp            :: Bool
    , optBatch           :: ReplMode
    , optProject         :: Maybe FilePath
    , optProjectRefresh  :: Project.LoadProjectMode
    , optCallStacks      :: Bool
    , optCommands        :: [String]
    , optColorMode       :: ColorMode
    , optCryptolrc       :: Cryptolrc
    , optCryptolPathOnly :: Bool
    , optStopOnError     :: Bool
    , optNoUnicodeLogo   :: Bool
    } deriving (Show)
  
  defaultOptions :: Options
  defaultOptions  = Options
    { optLoad            = []
    , optVersion         = False
    , optHelp            = False
    , optBatch           = InteractiveRepl
    , optProject         = Nothing
    , optProjectRefresh  = Project.ModifiedMode
    , optCallStacks      = True
    , optCommands        = []
    , optColorMode       = AutoColor
    , optCryptolrc       = CryrcDefault
    , optCryptolPathOnly = False
    , optStopOnError     = False
    , optNoUnicodeLogo   = False
    }
  
  options :: [OptDescr (OptParser Options)]
  options  =
    [ Option "b" ["batch"] (ReqArg setBatchScript "FILE")
      "run the script provided and exit"
  
    , Option "" ["interactive-batch"] (ReqArg setInteractiveBatchScript "FILE")
      "run the script provided and exit, but behave as if running an interactive session"
  
    , Option "p" ["project"] (ReqArg setProject "CRYPROJECT")
      ("Load and verify a Cryptol project using the provided project "
        ++ "configuration file or directory containing 'cryproject.toml'")
    
    , Option "" ["refresh-project"] (NoArg setProjectRefresh)
      "Ignore a pre-existing cache file when loading a project."
  
    , Option "" ["untested-project"] (NoArg setProjectUntested)
      "Load all project files that don't have a test result."
  
    , Option "e" ["stop-on-error"] (NoArg setStopOnError)
      "stop script execution as soon as an error occurs."
  
    , Option "c" ["command"] (ReqArg addCommand "COMMAND")
      (concat [ "run the given command and then exit; if multiple --command "
              , "arguments are given, run them in the order they appear "
              , "on the command line (overrides --batch)"
              ])
  
    , Option "" ["color"] (ReqArg setColorMode "MODE")
      (concat [ "control the color output for the terminal, which may be "
              , "'auto', 'none' or 'always' (default: 'auto')"
              ])
  
    , Option "v" ["version"] (NoArg setVersion)
      "display version number"
  
    , Option "h" ["help"] (NoArg setHelp)
      "display this message"
  
    , Option "" ["no-call-stacks"] (NoArg setNoCallStacks)
      "Disable tracking of call stack information, which reduces interpreter overhead"
  
    , Option "" ["no-unicode-logo"] (NoArg setNoUnicodeLogo)
      "Don't use unicode characters in the REPL logo"
  
    , Option ""  ["ignore-cryptolrc"] (NoArg setCryrcDisabled)
      "disable reading of .cryptolrc files"
  
    , Option ""  ["cryptolrc-script"] (ReqArg addCryrc "FILE")
      "read additional .cryptolrc files"
  
    , Option ""  ["cryptolpath-only"] (NoArg setCryptolPathOnly)
      "only look for .cry files in CRYPTOLPATH; don't use built-in locations"
    ]
  
  -- | Set a single file to be loaded.  This should be extended in the future, if
  -- we ever plan to allow multiple files to be loaded at the same time.
  addFile :: String -> OptParser Options
  addFile path = modify $ \ opts -> opts { optLoad = [ path ] }
  
  -- | Add a command to be run on interpreter startup.
  addCommand :: String -> OptParser Options
  addCommand cmd =
    modify $ \ opts -> opts { optCommands = cmd : optCommands opts }
  
  -- | Stop script (batch mode) execution on first error.
  setStopOnError :: OptParser Options
  setStopOnError = modify $ \opts -> opts { optStopOnError = True }
  
  -- | Set a batch script to be run.
  setBatchScript :: String -> OptParser Options
  setBatchScript path = modify $ \ opts -> opts { optBatch = Batch path }
  
  -- | Set an interactive batch script
  setInteractiveBatchScript :: String -> OptParser Options
  setInteractiveBatchScript path = modify $ \ opts -> opts { optBatch = InteractiveBatch path }
  
  setProject :: String -> OptParser Options
  setProject path = modify $ \opts -> opts { optProject = Just path }
  
  setProjectRefresh :: OptParser Options
  setProjectRefresh = modify $ \opts -> opts { optProjectRefresh = Project.RefreshMode }
  
  setProjectUntested :: OptParser Options
  setProjectUntested = modify $ \opts -> opts { optProjectRefresh = Project.UntestedMode }
  
  -- | Set the color mode of the terminal output.
  setColorMode :: String -> OptParser Options
  setColorMode "auto"   = modify $ \ opts -> opts { optColorMode = AutoColor }
  setColorMode "none"   = modify $ \ opts -> opts { optColorMode = NoColor }
  setColorMode "always" = modify $ \ opts -> opts { optColorMode = AlwaysColor }
  setColorMode x        = OptFailure ["invalid color mode: " ++ x ++ "\n"]
  
  -- | Disable unicde characters in the REPL logo
  setNoUnicodeLogo :: OptParser Options
  setNoUnicodeLogo = modify $ \opts -> opts { optNoUnicodeLogo = True }
  
  -- | Signal that version should be displayed.
  setVersion :: OptParser Options
  setVersion  = modify $ \ opts -> opts { optVersion = True }
  
  -- | Signal that help should be displayed.
  setHelp :: OptParser Options
  setHelp  = modify $ \ opts -> opts { optHelp = True }
  
  -- | Disable .cryptolrc files entirely
  setCryrcDisabled :: OptParser Options
  setCryrcDisabled  = modify $ \ opts -> opts { optCryptolrc = CryrcDisabled }
  
  -- | Disable call stack tracking
  setNoCallStacks :: OptParser Options
  setNoCallStacks = modify $ \opts -> opts { optCallStacks = False }
  
  -- | Add another file to read as a @.cryptolrc@ file, unless @.cryptolrc@
  -- files have been disabled
  addCryrc :: String -> OptParser Options
  addCryrc path = modify $ \ opts ->
    case optCryptolrc opts of
      CryrcDefault  -> opts { optCryptolrc = CryrcFiles [path] }
      CryrcDisabled -> opts
      CryrcFiles xs -> opts { optCryptolrc = CryrcFiles (path:xs) }
  
  setCryptolPathOnly :: OptParser Options
  setCryptolPathOnly  = modify $ \opts -> opts { optCryptolPathOnly = True }
  
  -- | Parse arguments.
  parseArgs :: [String] -> Either [String] Options
  parseArgs args = case getOpt (ReturnInOrder addFile) options args of
    (ps,[],[]) -> runOptParser defaultOptions (mconcat ps)
    (_,_,errs) -> Left errs
  
  displayHelp :: [String] -> IO ()
  displayHelp errs = do
    prog <- getProgName
    let banner = "Usage: " ++ prog ++ " [OPTIONS]"
        paraLines = fsep . map text . words . unlines
        ppEnv (varname, desc) = hang varname 4 (paraLines $ desc)
        envs = [
            ( "CRYPTOLPATH"
            , [ "A `" ++ [searchPathSeparator] ++ "`-separated"
              , "list of directories to be searched for Cryptol modules in"
              , "addition to the default locations"
              ]
            )
          , ( "CRYPTOL_SAW"
            , [ "Sets the command to use when running SAW via the `:saw` command"
              ]
            )
          , ( "EDITOR"
            , [ "Sets the editor executable to use when opening an editor"
              , "via the `:edit` command"
              ]
            )
          , ( "SBV_{ABC,BITWUZLA,BOOLECTOR,CVC4,CVC5,MATHSAT,YICES,Z3}_OPTIONS"
            , [ "A string of command-line arguments to be passed to the"
              , "corresponding solver invoked for `:sat` and `:prove`"
              , "when using a prover via SBV"
              ]
            )
          ]
    putStrLn (usageInfo (concat (errs ++ [banner])) options)
    print $ hang "Influential environment variables:"
               4 (vcat (map ppEnv envs))
  main :: IO ()
  main  = do
    setLocaleEncoding utf8
    args <- getArgs
    case parseArgs args of
  
      Left errs -> do
        displayHelp errs
        exitFailure
  
      Right opts
        | optHelp opts    -> displayHelp []
        | optVersion opts -> displayVersion putStrLn
        | otherwise       -> do
            (opts', mCleanup) <- setupCmdScript opts
            (opts'', mConfig) <- setupProject opts'
            status <- repl (optCryptolrc opts'')
                           mConfig
                           (optProjectRefresh opts'')
                           (optBatch opts'')
                           (optCallStacks opts'')
                           (optStopOnError opts'')
                           (setupREPL opts'')
            case mCleanup of
              Nothing -> return ()
              Just cmdFile -> removeFile cmdFile
  
            if crSuccess status
              then exitSuccess
              else exitFailure
  
  setupCmdScript :: Options -> IO (Options, Maybe FilePath)
  setupCmdScript opts =
    case optCommands opts of
      [] -> return (opts, Nothing)
      cmds -> do
        tmpdir <- getTemporaryDirectory
        (path, h) <- openTempFile tmpdir "cmds.icry"
        hPutStr h (unlines cmds)
        hClose h
        when (optBatch opts /= InteractiveRepl) $
          putStrLn "[warning] --command argument specified; ignoring batch file"
        when (isJust (optProject opts)) $
          putStrLn $
            "[warning] --command argument specified; "
            ++ "ignoring project configuration file"
        return
          ( opts { optBatch = InteractiveBatch path, optProject = Nothing }
          , Just path )
  
  setupProject :: Options -> IO (Options, Maybe Project.Config)
  setupProject opts =
    case optProject opts of
      Nothing -> pure (opts, Nothing)
      Just path -> do
        when (optBatch opts /= InteractiveRepl) $
          putStrLn "[warning] --project argument specified; ignoring batch file"
        Project.loadConfig path >>= \case
          Left err -> do
            print $ pp err
            exitFailure
          Right config ->
            pure (opts { optBatch = InteractiveRepl }, Just config)
  
  setupREPL :: Options -> REPL ()
  setupREPL opts = do
    mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
    case mCryptolPath of
      Nothing -> return ()
      Just path | optCryptolPathOnly opts -> setSearchPath (parseSearchPath path)
                | otherwise               -> prependSearchPath (parseSearchPath path)
    smoke <- REPL.smokeTest
    case smoke of
      [] -> return ()
      _  -> io $ do
        print (hang "Errors encountered on startup; exiting:"
                  4 (vcat (map pp smoke)))
        exitFailure
  
    color <- case optColorMode opts of
      AlwaysColor -> return True
      NoColor     -> return False
      AutoColor   -> canDisplayColor
  
    let useUnicode = not (optNoUnicodeLogo opts)
    displayLogo color useUnicode
  
    setUpdateREPLTitle (shouldSetREPLTitle >>= \b -> when b setREPLTitle)
    updateREPLTitle
    case optBatch opts of
      -- add the directory containing the batch file to the module search path
      Batch file -> prependSearchPath [ takeDirectory file ]
      _ -> return ()
  
    when (isNothing (optProject opts)) $
      case optLoad opts of
        []  -> loadPrelude `REPL.catch` \x -> io $ print $ pp x
        [l] -> void (loadCmd l) `REPL.catch` \x -> do
                io $ print $ pp x
                -- If the requested file fails to load,
                -- load the prelude instead...
                loadPrelude `REPL.catch` \y -> do
                  io $ print $ pp y
                -- ... but make sure the loaded module is set to the file
                -- we tried, instead of the Prelude
                REPL.setEditPath l
                REPL.setLoadedMod REPL.LoadedModule
                  { REPL.lFocus = Nothing
                  , REPL.lPath = InFile l
                  }
        _   -> io $ putStrLn "Only one file may be loaded at the command line."
  