{-# 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 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
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Options
opts { optRawAgdaOptions :: [String]
optRawAgdaOptions = [String]
argvForAgda }

usageMessage :: String
usageMessage :: String
usageMessage = forall a. String -> [OptDescr a] -> String
usageInfo String
usage [OptDescr (Options -> Options)]
options 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 = forall a. Maybe a
Nothing, optRawAgdaOptions :: [String]
optRawAgdaOptions = [], optHelp :: Bool
optHelp = Bool
False }

options :: [OptDescr (Options -> Options)]
options :: [OptDescr (Options -> Options)]
options =
  [ forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'h']
           [String
"help"]
           (forall a. a -> ArgDescr a
NoArg (\Options
opts -> Options
opts { optHelp :: Bool
optHelp = Bool
True }))
           String
"print this help message"
  , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option
    [Char
'p']
    [String
"port"]
    (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 :: Maybe Int
optViaTCP = forall a. Read a => String -> Maybe a
readMaybe String
n }
        Maybe String
Nothing -> Options
opts { optViaTCP :: Maybe Int
optViaTCP = forall a. a -> Maybe a
Just Int
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 forall a.
ArgOrder a -> [OptDescr a] -> [String] -> ([a], [String], [String])
getOpt forall a. ArgOrder a
Permute [OptDescr (Options -> Options)]
options [String]
argv of
  ([Options -> Options]
o, [String]
n, []  ) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. a -> a
id) Options
defaultOptions [Options -> Options]
o, [String]
n)
  ([Options -> Options]
_, [String]
_, [String]
errs) -> forall a. IOError -> IO a
ioError forall a b. (a -> b) -> a -> b
$ String -> IOError
userError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
errs forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
1 forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
is String
"-RTS") [String]
argv
  | Bool
otherwise     = String
arg forall a. a -> [a] -> [a]
: [String] -> [String]
stripRTS [String]
argv
  where is :: String -> String -> Bool
is String
x String
arg = [String
x] forall a. Eq a => a -> a -> Bool
== 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') = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== String
"+AGDA") [String]
argv
      ([String]
forAgda, [String]
after) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
== String
"-AGDA") [String]
argv'
      forALS :: [String]
forALS           = [String]
before forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== String
"-AGDA") [String]
after
      forAgda' :: [String]
forAgda'         = forall a. (a -> Bool) -> [a] -> [a]
dropWhile (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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Config -> Config -> Bool
$c/= :: Config -> Config -> Bool
== :: Config -> Config -> Bool
$c== :: Config -> Config -> Bool
Eq, Int -> Config -> ShowS
[Config] -> ShowS
Config -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Config] -> ShowS
$cshowList :: [Config] -> ShowS
show :: Config -> String
$cshow :: Config -> String
showsPrec :: Int -> Config -> ShowS
$cshowsPrec :: Int -> Config -> ShowS
Show, 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
$cto :: forall x. Rep Config x -> Config
$cfrom :: forall x. Config -> Rep Config x
Generic)

instance FromJSON Config where
  parseJSON :: Value -> Parser Config
parseJSON (Object Object
v) = [String] -> Config
Config forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v 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 =
    forall a. String -> Parser a -> Parser a
prependFailure String
"parsing Config failed, " (forall a. String -> Value -> Parser a
typeMismatch String
"Object" Value
invalid)

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