{-# LANGUAGE CPP #-}

-- | Options given to @MiniAgda@.

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 )

-- | Options given to @MiniAgda@.
data Options = Options
  { Options -> List1 FilePath
optInputs :: List1 FilePath
      -- ^ The source files to type check, from first to last.
  }

self :: String
self :: FilePath
self = FilePath
"MiniAgda"

-- | Parse the options given on the command line.
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

-- | Pure parser for command line given by a list of strings.
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)."