{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}

module Agda.Interaction.Command where

import Data.ByteString (ByteString)
import Data.HashMap.Strict (HashMap)
import GHC.Generics (Generic)
import System.FilePath

import Agda.Interaction.Command.EvalIn
import Agda.Interaction.Command.EvalTerm
import Agda.Interaction.Command.GiveMeta
import Agda.Interaction.Command.RefineMeta
import Agda.Interaction.Command.Reload
import Agda.Interaction.Command.RetryConstraints
import Agda.Interaction.Command.ShowConstraints
import Agda.Interaction.Command.ShowContext
import Agda.Interaction.Command.ShowMetas
import Agda.Interaction.Command.ShowScope
import Agda.Interaction.Command.TypeOf
import Agda.Interaction.Command.TypeIn

import Agda.Interaction.State
import Agda.TypeChecking.Monad.Base (TCEnv (..), TCM)
import Agda.Utils.FileName (AbsolutePath, filePath)

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

-- | Supported sub-commands for Agda.
data AgdaCommand
  = Reload | Help | Constraints | Context | Give | Refine | Meta | Load
  | Eval | TypeOf | TypeIn | WakeUp | Scope
  deriving (AgdaCommand -> AgdaCommand -> Bool
(AgdaCommand -> AgdaCommand -> Bool)
-> (AgdaCommand -> AgdaCommand -> Bool) -> Eq AgdaCommand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AgdaCommand -> AgdaCommand -> Bool
$c/= :: AgdaCommand -> AgdaCommand -> Bool
== :: AgdaCommand -> AgdaCommand -> Bool
$c== :: AgdaCommand -> AgdaCommand -> Bool
Eq, Int -> AgdaCommand -> ShowS
[AgdaCommand] -> ShowS
AgdaCommand -> String
(Int -> AgdaCommand -> ShowS)
-> (AgdaCommand -> String)
-> ([AgdaCommand] -> ShowS)
-> Show AgdaCommand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AgdaCommand] -> ShowS
$cshowList :: [AgdaCommand] -> ShowS
show :: AgdaCommand -> String
$cshow :: AgdaCommand -> String
showsPrec :: Int -> AgdaCommand -> ShowS
$cshowsPrec :: Int -> AgdaCommand -> ShowS
Show, (forall x. AgdaCommand -> Rep AgdaCommand x)
-> (forall x. Rep AgdaCommand x -> AgdaCommand)
-> Generic AgdaCommand
forall x. Rep AgdaCommand x -> AgdaCommand
forall x. AgdaCommand -> Rep AgdaCommand x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AgdaCommand x -> AgdaCommand
$cfrom :: forall x. AgdaCommand -> Rep AgdaCommand x
Generic)

-- | Map of supported Agda sub-commands. We use it instead of parser.
supportedCommands :: HashMap ByteString AgdaCommand
supportedCommands :: HashMap ByteString AgdaCommand
supportedCommands = [(ByteString, AgdaCommand)] -> HashMap ByteString AgdaCommand
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList
  [ (,) ByteString
"/reload" AgdaCommand
Reload
  , (,) ByteString
"/?" AgdaCommand
Help
  , (,) ByteString
"/constraints" AgdaCommand
Constraints
  , (,) ByteString
"/context" AgdaCommand
Context
  , (,) ByteString
"/give" AgdaCommand
Give
  , (,) ByteString
"/refine" AgdaCommand
Refine
  , (,) ByteString
"/meta" AgdaCommand
Meta
  , (,) ByteString
"/load" AgdaCommand
Load
  , (,) ByteString
"/eval" AgdaCommand
Eval
  , (,) ByteString
"/typeOf" AgdaCommand
TypeOf
  , (,) ByteString
"/typeIn" AgdaCommand
TypeIn
  , (,) ByteString
"/wakeup" AgdaCommand
WakeUp
  , (,) ByteString
"/scope" AgdaCommand
Scope
  ]

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

-- | Choose an action based on either 'AgdaCommand' or raw input.
chooseCommand :: AgdaState -> Either () AgdaCommand -> ByteString -> IO (TCM ByteString)
chooseCommand :: AgdaState
-> Either () AgdaCommand -> ByteString -> IO (TCM ByteString)
chooseCommand AgdaState
_state (Left ()
_) ByteString
input = TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString
evalTerm ByteString
input)
chooseCommand AgdaState
state (Right AgdaCommand
cmd) ByteString
input = do
  Maybe AbsolutePath
mfilePath <- TCEnv -> Maybe AbsolutePath
envCurrentPath (TCEnv -> Maybe AbsolutePath)
-> IO TCEnv -> IO (Maybe AbsolutePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AgdaState -> IO TCEnv
readTCEnv AgdaState
state
  case AgdaCommand
cmd of
    AgdaCommand
Constraints -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
showConstraints (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Context     -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
showContext (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Give        -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
giveMeta (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Refine      -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
refineMeta (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Scope       -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCM ByteString
showScope
    AgdaCommand
Meta        -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
showMetas (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Load        -> case Maybe AbsolutePath
mfilePath of
      Maybe AbsolutePath
Nothing   -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"Failed to load.")
      Just AbsolutePath
filepath -> do
        AbsolutePath -> ByteString -> IO ()
storeRequestContent AbsolutePath
filepath ByteString
input
        TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TCM ByteString -> IO (TCM ByteString))
-> TCM ByteString -> IO (TCM ByteString)
forall a b. (a -> b) -> a -> b
$ Maybe AbsolutePath -> TCM ByteString
reload (AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just AbsolutePath
filepath)
    AgdaCommand
Reload      -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe AbsolutePath -> TCM ByteString
reload Maybe AbsolutePath
mfilePath)
    AgdaCommand
WakeUp      -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCM ByteString
retryConstraints
    AgdaCommand
TypeOf      -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
typeOf (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
TypeIn      -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
typeIn (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
Eval        -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ByteString] -> TCM ByteString
evalIn (ByteString -> [ByteString]
BS8.words ByteString
input))
    AgdaCommand
_           -> TCM ByteString -> IO (TCM ByteString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
tbd)
  where
    tbd :: ByteString
tbd = [ByteString] -> ByteString
BS8.unwords
      [ ByteString
"Command"
      , String -> ByteString
BS8.pack (AgdaCommand -> String
forall a. Show a => a -> String
show AgdaCommand
cmd)
      , ByteString
"is not supported yet."
      ]

-- | Store raw user input in the file given by 'TCEnv'.
storeRequestContent :: AbsolutePath -> ByteString -> IO ()
storeRequestContent :: AbsolutePath -> ByteString -> IO ()
storeRequestContent AbsolutePath
absFilepath ByteString
content = do
  let moduleName :: ByteString
moduleName = (String -> ByteString
BS8.pack (String -> ByteString)
-> (AbsolutePath -> String) -> AbsolutePath -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
dropExtension ShowS -> (AbsolutePath -> String) -> AbsolutePath -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeFileName ShowS -> (AbsolutePath -> String) -> AbsolutePath -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> String
filePath) AbsolutePath
absFilepath
      moduleContent :: ByteString
moduleContent = [ByteString] -> ByteString
BS8.unlines
        [ [ByteString] -> ByteString
BS8.unwords [ ByteString
"module", ByteString
moduleName, ByteString
"where" ]
        , ByteString
""
        , ByteString
content
        ]
  String -> ByteString -> IO ()
BS8.writeFile (AbsolutePath -> String
filePath AbsolutePath
absFilepath) ByteString
moduleContent