{-# LANGUAGE DeriveGeneric #-}
module Options
  ( Options(..)
  , getOptionsFromArgv
  , usageMessage
  , Config(..)
  , initConfig
  ) where
import           Data.Aeson.Types        hiding ( Options
                                                , defaultOptions
                                                )
import           GHC.Generics                   ( Generic )
import           System.Console.GetOpt
import           System.Environment             ( getArgs )
import           Text.Read                      ( readMaybe )

getOptionsFromArgv :: IO Options
getOptionsFromArgv :: IO Options
getOptionsFromArgv = do
  -- extract options for Agda from ARGV 
  ([String]
argvForALS, [String]
argvForAgda) <- [String] -> ([String], [String])
extractAgdaOpts ([String] -> ([String], [String]))
-> IO [String] -> IO ([String], [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [String]
getArgs
  -- parse options for ALS 
  (Options
opts      , [String]
_          ) <- [String] -> IO (Options, [String])
parseOpts [String]
argvForALS
  -- save options for Agda back
  Options -> IO Options
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Options -> IO Options) -> Options -> IO Options
forall a b. (a -> b) -> a -> b
$ Options
opts { optRawAgdaOptions = argvForAgda }

usageMessage :: String
usageMessage :: String
usageMessage = String -> [OptDescr (Options -> Options)] -> String
forall a. String -> [OptDescr a] -> String
usageInfo String
usage [OptDescr (Options -> Options)]
options String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
usageAboutAgdaOptions

--------------------------------------------------------------------------------

-- | Command-line arguments
data Options = Options
  { Options -> Maybe Int
optViaTCP         :: Maybe Int
  , Options -> [String]
optRawAgdaOptions :: [String]
  , Options -> Bool
optHelp           :: Bool
  }

defaultOptions :: Options
defaultOptions :: Options
defaultOptions =
  Options { optViaTCP :: Maybe Int
optViaTCP = Maybe Int
forall a. Maybe a
Nothing, optRawAgdaOptions :: [String]
optRawAgdaOptions = [], optHelp :: Bool
optHelp = Bool
False }

options :: [OptDescr (Options -> Options)]
options :: [OptDescr (Options -> Options)]
options =
  [ String
-> [String]
-> ArgDescr (Options -> Options)
-> String
-> OptDescr (Options -> Options)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'h']
           [String
"help"]
           ((Options -> Options) -> ArgDescr (Options -> Options)
forall a. a -> ArgDescr a
NoArg (\Options
opts -> Options
opts { optHelp = True }))
           String
"print this help message"
  , String
-> [String]
-> ArgDescr (Options -> Options)
-> String
-> OptDescr (Options -> Options)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option
    [Char
'p']
    [String
"port"]
    ((Maybe String -> Options -> Options)
-> String -> ArgDescr (Options -> Options)
forall a. (Maybe String -> a) -> String -> ArgDescr a
OptArg
      (\Maybe String
port Options
opts -> case Maybe String
port of
        Just String
n  -> Options
opts { optViaTCP = readMaybe n }
        Maybe String
Nothing -> Options
opts { optViaTCP = Just 4096 }
      )
      String
"PORT"
    )
    String
"talk with the editor via TCP port (4096 as default)"
  ]

usage :: String
usage :: String
usage = String
"Agda Language Server v0.0.3.0 \nUsage: als [Options...]\n"

usageAboutAgdaOptions :: String
usageAboutAgdaOptions :: String
usageAboutAgdaOptions =
  String
"\n\
      \  +AGDA [Options for Agda ...] -AGDA\n\
      \    To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n\
      \    For example:\n\
      \      als -p=3000 +AGDA --cubical -AGDA\n\
      \    If you are using agda-mode on VS Code, put them in the Settings at:\n\
      \      agdaMode.connection.commandLineOptions\n\
      \"

parseOpts :: [String] -> IO (Options, [String])
parseOpts :: [String] -> IO (Options, [String])
parseOpts [String]
argv = case ArgOrder (Options -> Options)
-> [OptDescr (Options -> Options)]
-> [String]
-> ([Options -> Options], [String], [String])
forall a.
ArgOrder a -> [OptDescr a] -> [String] -> ([a], [String], [String])
getOpt ArgOrder (Options -> Options)
forall a. ArgOrder a
Permute [OptDescr (Options -> Options)]
options [String]
argv of
  ([Options -> Options]
o, [String]
n, []  ) -> (Options, [String]) -> IO (Options, [String])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Options -> (Options -> Options) -> Options)
-> Options -> [Options -> Options] -> Options
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((Options -> Options) -> Options -> Options)
-> Options -> (Options -> Options) -> Options
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Options -> Options) -> Options -> Options
forall a. a -> a
id) Options
defaultOptions [Options -> Options]
o, [String]
n)
  ([Options -> Options]
_, [String]
_, [String]
errs) -> IOError -> IO (Options, [String])
forall a. IOError -> IO a
ioError (IOError -> IO (Options, [String]))
-> IOError -> IO (Options, [String])
forall a b. (a -> b) -> a -> b
$ String -> IOError
userError (String -> IOError) -> String -> IOError
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
errs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [OptDescr (Options -> Options)] -> String
forall a. String -> [OptDescr a] -> String
usageInfo String
usage [OptDescr (Options -> Options)]
options


-- | Removes RTS options from a list of options (stolen from Agda)
stripRTS :: [String] -> [String]
stripRTS :: [String] -> [String]
stripRTS []               = []
stripRTS (String
"--RTS" : [String]
argv) = [String]
argv
stripRTS (String
arg : [String]
argv)
  | String -> String -> Bool
is String
"+RTS" String
arg = [String] -> [String]
stripRTS ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
1 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
is String
"-RTS") [String]
argv
  | Bool
otherwise     = String
arg String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
stripRTS [String]
argv
  where is :: String -> String -> Bool
is String
x String
arg = [String
x] [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
1 (String -> [String]
words String
arg)

-- | Extract Agda options (+AGDA ... -AGDA) from a list of options
extractAgdaOpts :: [String] -> ([String], [String])
extractAgdaOpts :: [String] -> ([String], [String])
extractAgdaOpts [String]
argv =
  let ([String]
before , [String]
argv') = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"+AGDA") [String]
argv
      ([String]
forAgda, [String]
after) = (String -> Bool) -> [String] -> ([String], [String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"-AGDA") [String]
argv'
      forALS :: [String]
forALS           = [String]
before [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"-AGDA") [String]
after
      forAgda' :: [String]
forAgda'         = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"+AGDA") [String]
forAgda
  in  ([String]
forALS, [String]
forAgda')

--------------------------------------------------------------------------------

newtype Config = Config { Config -> [String]
configRawAgdaOptions :: [String] }
  deriving (Config -> Config -> Bool
(Config -> Config -> Bool)
-> (Config -> Config -> Bool) -> Eq Config
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
/= :: Config -> Config -> Bool
Eq, Int -> Config -> String -> String
[Config] -> String -> String
Config -> String
(Int -> Config -> String -> String)
-> (Config -> String)
-> ([Config] -> String -> String)
-> Show Config
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Config -> String -> String
showsPrec :: Int -> Config -> String -> String
$cshow :: Config -> String
show :: Config -> String
$cshowList :: [Config] -> String -> String
showList :: [Config] -> String -> String
Show, (forall x. Config -> Rep Config x)
-> (forall x. Rep Config x -> Config) -> Generic Config
forall x. Rep Config x -> Config
forall x. Config -> Rep Config x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Config -> Rep Config x
from :: forall x. Config -> Rep Config x
$cto :: forall x. Rep Config x -> Config
to :: forall x. Rep Config x -> Config
Generic)

instance FromJSON Config where
  parseJSON :: Value -> Parser Config
parseJSON (Object Object
v) = [String] -> Config
Config ([String] -> Config) -> Parser [String] -> Parser Config
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Key -> Parser [String]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"commandLineOptions"
  -- We do not expect a non-Object value here.
  -- We could use empty to fail, but typeMismatch
  -- gives a much more informative error message.
  parseJSON Value
invalid =
    String -> Parser Config -> Parser Config
forall a. String -> Parser a -> Parser a
prependFailure String
"parsing Config failed, " (String -> Value -> Parser Config
forall a. String -> Value -> Parser a
typeMismatch String
"Object" Value
invalid)

initConfig :: Config
initConfig :: Config
initConfig = [String] -> Config
Config []