{-# LANGUAGE CPP #-}
module Options where
#if !MIN_VERSION_base(4,11,0)
import Data.Semigroup ( (<>) )
#endif
import Options.Applicative
import Options.Applicative.NonEmpty ( some1 )
import System.Environment ( getArgs )
import License ( copyright, license )
import Util
import Version ( version )
data Options = Options
{ Options -> List1 FilePath
optInputs :: List1 FilePath
}
self :: String
self :: FilePath
self = FilePath
"MiniAgda"
options :: IO Options
options :: IO Options
options = ParserResult Options -> IO Options
forall a. ParserResult a -> IO a
handleParseResult (ParserResult Options -> IO Options)
-> IO (ParserResult Options) -> IO Options
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do [FilePath] -> ParserResult Options
parseOptions ([FilePath] -> ParserResult Options)
-> IO [FilePath] -> IO (ParserResult Options)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [FilePath]
getArgs
parseOptions :: [String] -> ParserResult Options
parseOptions :: [FilePath] -> ParserResult Options
parseOptions = ParserPrefs
-> ParserInfo Options -> [FilePath] -> ParserResult Options
forall a.
ParserPrefs -> ParserInfo a -> [FilePath] -> ParserResult a
execParserPure ParserPrefs
defaultPrefs (ParserInfo Options -> [FilePath] -> ParserResult Options)
-> ParserInfo Options -> [FilePath] -> ParserResult Options
forall a b. (a -> b) -> a -> b
$ Parser Options -> InfoMod Options -> ParserInfo Options
forall a. Parser a -> InfoMod a -> ParserInfo a
info Parser Options
parser InfoMod Options
forall {a}. InfoMod a
description
where
parser :: Parser Options
parser = Parser Options
theOptions Parser Options -> Parser (Options -> Options) -> Parser Options
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**>
(Parser
((((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
-> ((Options -> Options) -> Options -> Options)
-> (Options -> Options)
-> Options
-> Options)
forall {a}. Parser (a -> a)
versionOption Parser
((((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
-> ((Options -> Options) -> Options -> Options)
-> (Options -> Options)
-> Options
-> Options)
-> Parser
(((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
-> Parser
(((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser
(((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
forall {a}. Parser (a -> a)
numericVersionOption Parser
(((Options -> Options) -> Options -> Options)
-> (Options -> Options) -> Options -> Options)
-> Parser ((Options -> Options) -> Options -> Options)
-> Parser ((Options -> Options) -> Options -> Options)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser ((Options -> Options) -> Options -> Options)
forall {a}. Parser (a -> a)
licenseOption Parser ((Options -> Options) -> Options -> Options)
-> Parser (Options -> Options) -> Parser (Options -> Options)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Options -> Options)
forall {a}. Parser (a -> a)
helper)
description :: InfoMod a
description = FilePath -> InfoMod a
forall a. FilePath -> InfoMod a
header FilePath
top InfoMod a -> InfoMod a -> InfoMod a
forall a. Semigroup a => a -> a -> a
<> FilePath -> InfoMod a
forall a. FilePath -> InfoMod a
footer FilePath
bot
top :: FilePath
top = [FilePath] -> FilePath
unwords
[ [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ FilePath
self, FilePath
":" ]
, FilePath
"A prototypical dependently typed pure language with sized types."
]
bot :: FilePath
bot = [FilePath] -> FilePath
unwords
[ FilePath
"Checks the given MiniAgda files in first-to-last order."
, FilePath
"Later files can refer to definitions made in earlier files."
]
versionOption :: Parser (a -> a)
versionOption =
FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a. FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
infoOption FilePath
versionLong
(Mod OptionFields (a -> a) -> Parser (a -> a))
-> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a b. (a -> b) -> a -> b
$ FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"version"
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> Char -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. HasName f => Char -> Mod f a
short Char
'V'
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Show version info."
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields (a -> a)
forall (f :: * -> *) a. Mod f a
hidden
versionText :: FilePath
versionText = [FilePath] -> FilePath
unwords [ FilePath
self, FilePath
"version", FilePath
version ]
versionLong :: FilePath
versionLong = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
"\n" ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$
[ FilePath
versionText
, FilePath
copyright
, FilePath
"This is free software under the MIT license."
]
numericVersionOption :: Parser (a -> a)
numericVersionOption =
FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a. FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
infoOption FilePath
version
(Mod OptionFields (a -> a) -> Parser (a -> a))
-> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a b. (a -> b) -> a -> b
$ FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"numeric-version"
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Show just version number."
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields (a -> a)
forall (f :: * -> *) a. Mod f a
hidden
licenseOption :: Parser (a -> a)
licenseOption =
FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a. FilePath -> Mod OptionFields (a -> a) -> Parser (a -> a)
infoOption FilePath
license
(Mod OptionFields (a -> a) -> Parser (a -> a))
-> Mod OptionFields (a -> a) -> Parser (a -> a)
forall a b. (a -> b) -> a -> b
$ FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"license"
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields (a -> a)
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Show the license text."
Mod OptionFields (a -> a)
-> Mod OptionFields (a -> a) -> Mod OptionFields (a -> a)
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields (a -> a)
forall (f :: * -> *) a. Mod f a
hidden
theOptions :: Parser Options
theOptions = List1 FilePath -> Options
Options
(List1 FilePath -> Options)
-> Parser (List1 FilePath) -> Parser Options
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (List1 FilePath)
oInputs
oInputs :: Parser (List1 FilePath)
oInputs :: Parser (List1 FilePath)
oInputs = Parser FilePath -> Parser (List1 FilePath)
forall a. Parser a -> Parser (NonEmpty a)
some1 (Parser FilePath -> Parser (List1 FilePath))
-> Parser FilePath -> Parser (List1 FilePath)
forall a b. (a -> b) -> a -> b
$
Mod ArgumentFields FilePath -> Parser FilePath
forall s. IsString s => Mod ArgumentFields s -> Parser s
strArgument
(Mod ArgumentFields FilePath -> Parser FilePath)
-> Mod ArgumentFields FilePath -> Parser FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> Mod ArgumentFields FilePath
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FILES"
Mod ArgumentFields FilePath
-> Mod ArgumentFields FilePath -> Mod ArgumentFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod ArgumentFields FilePath
forall (f :: * -> *) a. HasCompleter f => FilePath -> Mod f a
action FilePath
"file"
Mod ArgumentFields FilePath
-> Mod ArgumentFields FilePath -> Mod ArgumentFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod ArgumentFields FilePath
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Files to check (in first-to-last order)."