{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

module Idris.Interaction.Command where

import Data.ByteString (ByteString)
import Data.Char (isSpace)
import Data.Coerce (coerce)
import Data.Text (unpack)
import Data.HashMap.Strict (HashMap)
import GHC.Generics (Generic)
import System.Directory
import System.FilePath (takeFileName)
import System.Exit (ExitCode (..))
import System.Process (readProcessWithExitCode)

import Proof.Assistant.Helpers
import Proof.Assistant.RefreshFile
import Proof.Assistant.Request
import Proof.Assistant.Settings

import qualified Data.ByteString.Char8 as BS8
import qualified Data.HashMap.Strict as HashMap

-- | Supported sub-commands for Idris 2.
data IdrisCommand
  = Load | TypeOf | Help
  deriving (IdrisCommand -> IdrisCommand -> Bool
(IdrisCommand -> IdrisCommand -> Bool)
-> (IdrisCommand -> IdrisCommand -> Bool) -> Eq IdrisCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IdrisCommand -> IdrisCommand -> Bool
$c/= :: IdrisCommand -> IdrisCommand -> Bool
== :: IdrisCommand -> IdrisCommand -> Bool
$c== :: IdrisCommand -> IdrisCommand -> Bool
Eq, Int -> IdrisCommand -> ShowS
[IdrisCommand] -> ShowS
IdrisCommand -> String
(Int -> IdrisCommand -> ShowS)
-> (IdrisCommand -> String)
-> ([IdrisCommand] -> ShowS)
-> Show IdrisCommand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IdrisCommand] -> ShowS
$cshowList :: [IdrisCommand] -> ShowS
show :: IdrisCommand -> String
$cshow :: IdrisCommand -> String
showsPrec :: Int -> IdrisCommand -> ShowS
$cshowsPrec :: Int -> IdrisCommand -> ShowS
Show, (forall x. IdrisCommand -> Rep IdrisCommand x)
-> (forall x. Rep IdrisCommand x -> IdrisCommand)
-> Generic IdrisCommand
forall x. Rep IdrisCommand x -> IdrisCommand
forall x. IdrisCommand -> Rep IdrisCommand x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IdrisCommand x -> IdrisCommand
$cfrom :: forall x. IdrisCommand -> Rep IdrisCommand x
Generic)

-- | Map of supported Idris 2 sub-commands. We use it instead of parser.
supportedCommands :: HashMap ByteString IdrisCommand
supportedCommands :: HashMap ByteString IdrisCommand
supportedCommands = [(ByteString, IdrisCommand)] -> HashMap ByteString IdrisCommand
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
  [ (,) ByteString
"/load" IdrisCommand
Load
  , (,) ByteString
"/?" IdrisCommand
Help
  , (,) ByteString
"/typeOf" IdrisCommand
TypeOf
  ]

-- | Check user input to identify 'IdrisCommand'.
matchSupported :: ByteString -> Maybe IdrisCommand
matchSupported :: ByteString -> Maybe IdrisCommand
matchSupported = (ByteString -> HashMap ByteString IdrisCommand -> Maybe IdrisCommand
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HashMap.lookup` HashMap ByteString IdrisCommand
supportedCommands)

-- | Choose an action based on either 'IdrisCommand' or raw input.
chooseCommand
  :: ExternalInterpreterSettings
  -> InterpreterRequest
  -> Either () IdrisCommand -> ByteString -> IO (IO (ExitCode, String, String))
chooseCommand :: ExternalInterpreterSettings
-> InterpreterRequest
-> Either () IdrisCommand
-> ByteString
-> IO (IO (ExitCode, String, String))
chooseCommand ExternalInterpreterSettings
settings InterpreterRequest
request Either () IdrisCommand
ecmd ByteString
input = case Either () IdrisCommand
ecmd of
  Left () ->
    ExternalInterpreterSettings
-> InterpreterRequest
-> (String -> IO (ExitCode, String, String))
-> IO (IO (ExitCode, String, String))
withResource ExternalInterpreterSettings
settings InterpreterRequest
request
      ((String -> IO (ExitCode, String, String))
 -> IO (IO (ExitCode, String, String)))
-> (String -> IO (ExitCode, String, String))
-> IO (IO (ExitCode, String, String))
forall a b. (a -> b) -> a -> b
$ ExternalInterpreterSettings
-> String -> String -> IO (ExitCode, String, String)
runProcess ExternalInterpreterSettings
settings (ByteString -> String
BS8.unpack (ByteString -> String) -> ByteString -> String
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
validateCmd ByteString
input) (String -> IO (ExitCode, String, String))
-> ShowS -> String -> IO (ExitCode, String, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeFileName
  Right IdrisCommand
cmd -> case IdrisCommand
cmd of
    IdrisCommand
Load -> do
      (String
dir, String
path) <- ExternalInterpreterSettings
-> InterpreterRequest -> Maybe String -> IO (String, String)
refreshTmpFile ExternalInterpreterSettings
settings InterpreterRequest
request Maybe String
forall a. Maybe a
Nothing
      IO (ExitCode, String, String) -> IO (IO (ExitCode, String, String))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO (ExitCode, String, String)
 -> IO (IO (ExitCode, String, String)))
-> IO (ExitCode, String, String)
-> IO (IO (ExitCode, String, String))
forall a b. (a -> b) -> a -> b
$ String
-> IO (ExitCode, String, String) -> IO (ExitCode, String, String)
forall a. String -> IO a -> IO a
withCurrentDirectory String
dir (IO (ExitCode, String, String) -> IO (ExitCode, String, String))
-> IO (ExitCode, String, String) -> IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ ExternalInterpreterSettings
-> String -> String -> IO (ExitCode, String, String)
runProcess ExternalInterpreterSettings
settings String
"main" (ShowS
takeFileName String
path)
    IdrisCommand
TypeOf ->
      ExternalInterpreterSettings
-> InterpreterRequest
-> (String -> IO (ExitCode, String, String))
-> IO (IO (ExitCode, String, String))
withResource ExternalInterpreterSettings
settings InterpreterRequest
request
        ((String -> IO (ExitCode, String, String))
 -> IO (IO (ExitCode, String, String)))
-> (String -> IO (ExitCode, String, String))
-> IO (IO (ExitCode, String, String))
forall a b. (a -> b) -> a -> b
$ ExternalInterpreterSettings
-> String -> String -> IO (ExitCode, String, String)
runProcess ExternalInterpreterSettings
settings (String
":ti " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ByteString -> String
BS8.unpack ByteString
input) (String -> IO (ExitCode, String, String))
-> ShowS -> String -> IO (ExitCode, String, String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeFileName
    IdrisCommand
Help -> IO (ExitCode, String, String) -> IO (IO (ExitCode, String, String))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO (ExitCode, String, String)
 -> IO (IO (ExitCode, String, String)))
-> IO (ExitCode, String, String)
-> IO (IO (ExitCode, String, String))
forall a b. (a -> b) -> a -> b
$ String -> IO (ExitCode, String, String)
textResponse String
"TBD"

-- | Helper to wrap given text as stdout.
textResponse :: String -> IO (ExitCode, String, String)
textResponse :: String -> IO (ExitCode, String, String)
textResponse String
txt = (ExitCode, String, String) -> IO (ExitCode, String, String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExitCode
ExitSuccess, String
txt, String
"")

-- | Wrapper around temp directory that will try to identify whether associated file exists.
-- And if file exists given action will be performed.
withResource
  :: ExternalInterpreterSettings
  -> InterpreterRequest
  -> (FilePath -> IO (ExitCode, String, String))
  -> IO (IO (ExitCode, String, String))
withResource :: ExternalInterpreterSettings
-> InterpreterRequest
-> (String -> IO (ExitCode, String, String))
-> IO (IO (ExitCode, String, String))
withResource ExternalInterpreterSettings
settings InterpreterRequest
request String -> IO (ExitCode, String, String)
action = do
  String
tmpDir <- IO String
getTemporaryDirectory
  let path :: String
path = ExternalInterpreterSettings -> InterpreterRequest -> ShowS
getTempFilePath ExternalInterpreterSettings
settings InterpreterRequest
request String
tmpDir
  IO (ExitCode, String, String) -> IO (IO (ExitCode, String, String))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO (ExitCode, String, String)
 -> IO (IO (ExitCode, String, String)))
-> IO (ExitCode, String, String)
-> IO (IO (ExitCode, String, String))
forall a b. (a -> b) -> a -> b
$ String
-> IO (ExitCode, String, String) -> IO (ExitCode, String, String)
forall a. String -> IO a -> IO a
withCurrentDirectory String
tmpDir (IO (ExitCode, String, String) -> IO (ExitCode, String, String))
-> IO (ExitCode, String, String) -> IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ do
    Bool
exist <- String -> IO Bool
doesFileExist String
path
    if Bool
exist
      then String -> IO (ExitCode, String, String)
action String
path
      else String -> IO (ExitCode, String, String)
textResponse String
"Not found"

-- | Wrapper around CLI execution.
runProcess :: ExternalInterpreterSettings -> String -> FilePath -> IO (ExitCode, String, String)
runProcess :: ExternalInterpreterSettings
-> String -> String -> IO (ExitCode, String, String)
runProcess ExternalInterpreterSettings{Natural
String
ResourceSettings
Priority
Time
Executable
CmdArgs
$sel:inputSize:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Natural
$sel:fileExtension:ExternalInterpreterSettings :: ExternalInterpreterSettings -> String
$sel:tempFilePrefix:ExternalInterpreterSettings :: ExternalInterpreterSettings -> String
$sel:resources:ExternalInterpreterSettings :: ExternalInterpreterSettings -> ResourceSettings
$sel:priority:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Priority
$sel:time:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Time
$sel:executable:ExternalInterpreterSettings :: ExternalInterpreterSettings -> Executable
$sel:args:ExternalInterpreterSettings :: ExternalInterpreterSettings -> CmdArgs
inputSize :: Natural
fileExtension :: String
tempFilePrefix :: String
resources :: ResourceSettings
priority :: Priority
time :: Time
executable :: Executable
args :: CmdArgs
..} String
input String
path =
  String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode (Executable -> String
forall a. Coercible a Text => a -> String
t2s Executable
executable) [String]
fullArgs String
""
  where
    fullArgs :: [String]
fullArgs = (Text -> String
unpack (Text -> String) -> [Text] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CmdArgs -> [Text]
coerce CmdArgs
args) [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
input, String
path]

-- | We are trying to filter out some potentially dangerous operations such as @:x@.
validateCmd :: ByteString -> ByteString
validateCmd :: ByteString -> ByteString
validateCmd ByteString
xs =
  let cut :: ByteString -> ByteString
cut = if Int -> ByteString -> ByteString
BS8.take Int
1 ByteString
xs ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
":"
        then (Char -> Bool) -> ByteString -> ByteString
BS8.dropWhile Char -> Bool
isSpace (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ByteString -> ByteString
BS8.dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)
        else ByteString -> ByteString
forall a. a -> a
id
  in ByteString -> ByteString
cut ByteString
xs