module Agda.Interaction.Options
( CommandLineOptions(..)
, Flag
, checkOpts
, parseStandardOptions
, parsePragmaOptions
, parsePluginOptions
, defaultOptions
, standardOptions_
, isLiterate
, mapFlag
, usage
, tests
) where
import Control.Monad.Error ( MonadError(catchError) )
import Data.List ( isSuffixOf )
import System.Console.GetOpt (getOpt, usageInfo, ArgOrder(ReturnInOrder)
, OptDescr(..), ArgDescr(..)
)
import Agda.Utils.TestHelpers ( runTests )
import Agda.Utils.QuickCheck ( quickCheck' )
import Agda.Utils.Monad ( readM )
import Agda.Utils.List ( wordsBy )
import Agda.Utils.Trie ( Trie )
import qualified Agda.Utils.Trie as Trie
isLiterate :: FilePath -> Bool
isLiterate file = ".lagda" `isSuffixOf` file
instance Functor OptDescr where
fmap f (Option short long arg descr) = Option short long (fmap f arg) descr
instance Functor ArgDescr where
fmap f (NoArg x) = NoArg (f x)
fmap f (ReqArg p s) = ReqArg (f . p) s
fmap f (OptArg p s) = OptArg (f . p) s
data CommandLineOptions =
Options { optProgramName :: String
, optInputFile :: Maybe FilePath
, optIncludeDirs :: [FilePath]
, optShowVersion :: Bool
, optShowHelp :: Bool
, optInteractive :: Bool
, optVerbose :: Trie String Int
, optProofIrrelevance :: Bool
, optAllowUnsolved :: Bool
, optShowImplicit :: Bool
, optRunTests :: Bool
, optCompile :: Bool
, optGenerateVimFile :: Bool
, optGenerateHTML :: Bool
, optHTMLDir :: FilePath
, optCSSFile :: Maybe FilePath
, optIgnoreInterfaces :: Bool
, optDisablePositivity :: Bool
, optCompileAlonzo :: Bool
, optCompileMAlonzo :: Bool
, optMAlonzoDir :: Maybe FilePath
, optTerminationCheck :: Bool
, optCompletenessCheck :: Bool
, optUnreachableCheck :: Bool
, optUniverseCheck :: Bool
, optSizedTypes :: Bool
, optUniversePolymorphism :: Bool
, optGhcFlags :: [String]
}
deriving Show
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr
defaultOptions :: CommandLineOptions
defaultOptions =
Options { optProgramName = "agda"
, optInputFile = Nothing
, optIncludeDirs = []
, optShowVersion = False
, optShowHelp = False
, optInteractive = False
, optVerbose = Trie.singleton [] 1
, optProofIrrelevance = False
, optAllowUnsolved = False
, optShowImplicit = False
, optRunTests = False
, optCompile = False
, optGenerateVimFile = False
, optGenerateHTML = False
, optHTMLDir = defaultHTMLDir
, optCSSFile = Nothing
, optIgnoreInterfaces = False
, optDisablePositivity = False
, optCompileAlonzo = False
, optCompileMAlonzo = False
, optMAlonzoDir = Nothing
, optTerminationCheck = True
, optCompletenessCheck = True
, optUnreachableCheck = True
, optUniverseCheck = True
, optSizedTypes = False
, optUniversePolymorphism = False
, optGhcFlags = []
}
defaultHTMLDir = "html"
prop_defaultOptions = case checkOpts defaultOptions of
Left _ -> False
Right _ -> True
type Flag opts = opts -> Either String opts
checkOpts :: Flag CommandLineOptions
checkOpts opts
| not (atMostOne compilerOpts) =
Left "At most one compiler may be used.\n"
| not (atMostOne $ optAllowUnsolved : compilerOpts) = Left
"Unsolved meta variables are not allowed when compiling.\n"
| not (atMostOne $ optInteractive : compilerOpts) =
Left "Choose at most one: compiler or interactive mode.\n"
| not (atMostOne [optGenerateHTML, optInteractive]) =
Left "Choose at most one: HTML generator or interactive mode.\n"
| not (atMostOne [optUniversePolymorphism, not . optUniverseCheck]) =
Left "Cannot have both universe polymorphism and type in type.\n"
| otherwise = Right opts
where
atMostOne bs = length (filter ($ opts) bs) <= 1
compilerOpts =
[ optCompile
, optCompileAlonzo
, optCompileMAlonzo
]
inputFlag :: FilePath -> CommandLineOptions -> Either String CommandLineOptions
inputFlag f o =
case optInputFile o of
Nothing -> checkOpts $ o { optInputFile = Just f }
Just _ -> fail "only one input file allowed"
versionFlag o = checkOpts $ o { optShowVersion = True }
helpFlag o = checkOpts $ o { optShowHelp = True }
proofIrrelevanceFlag o = checkOpts $ o { optProofIrrelevance = True }
ignoreInterfacesFlag o = checkOpts $ o { optIgnoreInterfaces = True }
allowUnsolvedFlag o = checkOpts $ o { optAllowUnsolved = True }
showImplicitFlag o = checkOpts $ o { optShowImplicit = True }
runTestsFlag o = checkOpts $ o { optRunTests = True }
vimFlag o = checkOpts $ o { optGenerateVimFile = True }
noPositivityFlag o = checkOpts $ o { optDisablePositivity = True }
dontTerminationCheckFlag o = checkOpts $ o { optTerminationCheck = False }
dontCompletenessCheckFlag o = checkOpts $ o { optCompletenessCheck = False }
noUnreachableCheckFlag o = checkOpts $ o { optUnreachableCheck = False }
dontUniverseCheckFlag o = checkOpts $ o { optUniverseCheck = False }
sizedTypes o = checkOpts $ o { optSizedTypes = True }
universePolymorphismFlag o = checkOpts $ o { optUniversePolymorphism = True }
interactiveFlag o = checkOpts $ o { optInteractive = True
, optAllowUnsolved = True
}
compileFlag o = checkOpts $ o { optCompileMAlonzo = True }
agateFlag o = checkOpts $ o { optCompile = True }
alonzoFlag o = checkOpts $ o { optCompileAlonzo = True }
malonzoFlag o = checkOpts $ o { optCompileMAlonzo = True }
malonzoDirFlag f o = checkOpts $ o { optMAlonzoDir = Just f }
ghcFlag f o = checkOpts $ o { optGhcFlags = f : optGhcFlags o }
htmlFlag o = checkOpts $ o { optGenerateHTML = True }
htmlDirFlag d o = checkOpts $ o { optHTMLDir = d }
cssFlag f o = checkOpts $ o { optCSSFile = Just f }
includeFlag d o = checkOpts $ o { optIncludeDirs = d : optIncludeDirs o }
verboseFlag s o =
do (k,n) <- parseVerbose s
checkOpts $ o { optVerbose = Trie.insert k n $ optVerbose o }
where
parseVerbose s = case wordsBy (`elem` ":.") s of
[] -> usage
ss -> do
n <- readM (last ss) `catchError` \_ -> usage
return (init ss, n)
usage = fail "argument to verbose should be on the form x.y.z:N or N"
integerArgument :: String -> String -> Either String Int
integerArgument flag s =
readM s `catchError` \_ ->
fail $ "option '" ++ flag ++ "' requires an integer argument"
standardOptions :: [OptDescr (Flag CommandLineOptions)]
standardOptions =
[ Option ['V'] ["version"] (NoArg versionFlag) "show version number"
, Option ['?'] ["help"] (NoArg helpFlag) "show this help"
, Option ['I'] ["interactive"] (NoArg interactiveFlag)
"start in interactive mode"
, Option ['c'] ["compile"] (NoArg compileFlag)
"compile program (experimental)"
, Option [] ["compile-dir"] (ReqArg malonzoDirFlag "DIR")
("directory for compiler output (default: the project root)")
, Option [] ["ghc-flag"] (ReqArg ghcFlag "GHC-FLAG")
"give the flag GHC-FLAG to GHC when compiling"
, Option [] ["test"] (NoArg runTestsFlag)
"run internal test suite"
, Option [] ["vim"] (NoArg vimFlag)
"generate Vim highlighting files"
, Option [] ["html"] (NoArg htmlFlag)
"generate HTML files with highlighted source code"
, Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR")
("directory in which HTML files are placed (default: " ++
defaultHTMLDir ++ ")")
, Option [] ["css"] (ReqArg cssFlag "URL")
"the CSS file used by the HTML files (can be relative)"
, Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)
"ignore interface files (re-type check everything)"
, Option ['i'] ["include-path"] (ReqArg includeFlag "DIR")
"look for imports in DIR"
] ++ pragmaOptions
pragmaOptions :: [OptDescr (Flag CommandLineOptions)]
pragmaOptions =
[ Option ['v'] ["verbose"] (ReqArg verboseFlag "N")
"set verbosity level to N"
, Option [] ["show-implicit"] (NoArg showImplicitFlag)
"show implicit arguments when printing"
, Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)
"allow unsolved meta variables (only needed in batch mode)"
, Option [] ["no-positivity-check"] (NoArg noPositivityFlag)
"do not warn about not strictly positive data types"
, Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag)
"do not warn about possibly nonterminating code"
, Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)
"do not warn about possibly incomplete pattern matches"
, Option [] ["no-unreachable-check"] (NoArg noUnreachableCheckFlag)
"do not warn about unreachable function clauses"
, Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag)
"ignore universe levels (this makes Agda inconsistent)"
, Option [] ["sized-types"] (NoArg sizedTypes)
"use sized datatypes"
, Option [] ["universe-polymorphism"] (NoArg universePolymorphismFlag)
"enable universe polymorphism (experimental feature)"
]
standardOptions_ :: [OptDescr ()]
standardOptions_ = map (fmap $ const ()) standardOptions
parseOptions' ::
String -> [String] -> opts ->
[OptDescr (Flag opts)] -> (String -> Flag opts) -> Either String opts
parseOptions' progName argv defaults opts fileArg =
case (getOpt (ReturnInOrder fileArg) opts argv) of
(o,_,[]) -> foldl (>>=) (return defaults) o
(_,_,errs) -> fail $ concat errs
parseStandardOptions :: String -> [String] -> Either String CommandLineOptions
parseStandardOptions progName argv =
parseOptions' progName argv defaultOptions standardOptions inputFlag
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptions
parsePragmaOptions argv opts =
parseOptions' progName argv opts pragmaOptions $
\s _ -> fail $ "Bad option in pragma: " ++ s
where
progName = optProgramName opts
parsePluginOptions ::
String -> [String] ->
opts -> [OptDescr (Flag opts)] ->
Either String opts
parsePluginOptions progName argv defaults opts =
parseOptions'
progName argv defaults opts
(\s _ -> fail $ "Internal error: Flag " ++ s ++ " passed to a plugin")
usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String
usage options pluginInfos progName =
usageInfo (header progName) options ++
"\nPlugins:\n" ++
indent (concatMap pluginMsg pluginInfos)
where
header progName = unlines [ "Agda"
, ""
, "Usage: " ++ progName ++ " [OPTIONS...] FILE"
]
indent = unlines . map (" " ++) . lines
pluginMsg (name, help, inherited, opts)
| null opts && null inherited = optHeader
| otherwise = usageInfo (optHeader ++
" Plugin-specific options:" ++
inheritedOptions inherited
) opts
where
optHeader = "\n" ++ name ++ "-plugin:\n" ++ indent help
inheritedOptions [] = ""
inheritedOptions pls =
"\n Inherits options from: " ++ unwords pls
tests :: IO Bool
tests = runTests "Agda.Interaction.Options"
[ quickCheck' prop_defaultOptions
]