{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} module Agda.Interaction.Options ( CommandLineOptions(..) , PragmaOptions(..) , OptionsPragma , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..) , Verbosity , HtmlHighlight(..) , WarningMode(..) , checkOpts , parsePragmaOptions , parsePluginOptions , stripRTS , defaultOptions , defaultInteractionOptions , defaultVerbosity , defaultCutOff , defaultPragmaOptions , standardOptions_ , unsafePragmaOptions , restartOptions , infectiveOptions , coinfectiveOptions , safeFlag , mapFlag , usage , defaultLibDir -- Reused by PandocAgda , inputFlag , standardOptions, deadStandardOptions , getOptSimple ) where import Control.Monad ( (>=>), when ) import Control.Monad.Trans import Data.IORef import Data.Either import Data.Function import Data.Maybe import Data.List ( isSuffixOf , intercalate ) import Data.Set ( Set ) import qualified Data.Set as Set import System.Console.GetOpt ( getOpt', usageInfo, ArgOrder(ReturnInOrder) , OptDescr(..), ArgDescr(..) ) import System.Directory ( doesFileExist, doesDirectoryExist ) import Text.EditDistance import Agda.Termination.CutOff ( CutOff(..) ) import Agda.Interaction.Library import Agda.Interaction.Options.Help import Agda.Interaction.Options.IORefs import Agda.Interaction.Options.Warnings import Agda.Utils.Except ( ExceptT , MonadError(catchError, throwError) , runExceptT ) import Agda.Utils.FileName ( absolute, AbsolutePath, filePath ) import Agda.Utils.Functor ( (<&>) ) import Agda.Utils.Lens ( Lens', over ) import Agda.Utils.List ( groupOn, wordsBy ) import Agda.Utils.Monad ( ifM, readM ) import Agda.Utils.String ( indent ) import Agda.Utils.Trie ( Trie ) import qualified Agda.Utils.Trie as Trie import Agda.Utils.WithDefault import Agda.Version -- Paths_Agda.hs is in $(BUILD_DIR)/build/autogen/. import Paths_Agda ( getDataFileName ) import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO) -- OptDescr is a Functor -------------------------------------------------- type Verbosity = Trie String Int data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto deriving (Show, Eq) -- Don't forget to update -- doc/user-manual/tools/command-line-options.rst -- if you make changes to the command-line options! data CommandLineOptions = Options { optProgramName :: String , optInputFile :: Maybe FilePath , optIncludePaths :: [FilePath] , optAbsoluteIncludePaths :: [AbsolutePath] , optLibraries :: [LibName] , optOverrideLibrariesFile :: Maybe FilePath -- ^ Use this (if Just) instead of .agda/libraries , optDefaultLibs :: Bool -- ^ Use ~/.agda/defaults , optUseLibs :: Bool -- ^ look for .agda-lib files , optShowVersion :: Bool , optShowHelp :: Maybe Help , optInteractive :: Bool , optGHCiInteraction :: Bool , optJSONInteraction :: Bool , optOptimSmashing :: Bool , optCompileDir :: Maybe FilePath -- ^ In the absence of a path the project root is used. , optGenerateVimFile :: Bool , optGenerateLaTeX :: Bool , optGenerateHTML :: Bool , optHTMLHighlight :: HtmlHighlight , optDependencyGraph :: Maybe FilePath , optLaTeXDir :: FilePath , optHTMLDir :: FilePath , optCSSFile :: Maybe FilePath , optIgnoreInterfaces :: Bool , optIgnoreAllInterfaces :: Bool , optForcing :: Bool , optPragmaOptions :: PragmaOptions , optOnlyScopeChecking :: Bool -- ^ Should the top-level module only be scope-checked, and not -- type-checked? } deriving Show -- | Options which can be set in a pragma. data PragmaOptions = PragmaOptions { optShowImplicit :: Bool , optShowIrrelevant :: Bool , optUseUnicode :: Bool , optVerbose :: Verbosity , optProp :: Bool , optAllowUnsolved :: Bool , optDisablePositivity :: Bool , optTerminationCheck :: Bool , optTerminationDepth :: CutOff -- ^ Cut off structural order comparison at some depth in termination checker? , optCompletenessCheck :: Bool , optUniverseCheck :: Bool , optOmegaInOmega :: Bool , optSizedTypes :: WithDefault 'True , optGuardedness :: WithDefault 'True , optInjectiveTypeConstructors :: Bool , optUniversePolymorphism :: Bool , optIrrelevantProjections :: Bool , optExperimentalIrrelevance :: Bool -- ^ irrelevant levels, irrelevant data matching , optWithoutK :: WithDefault 'False , optCopatterns :: Bool -- ^ Allow definitions by copattern matching? , optPatternMatching :: Bool -- ^ Is pattern matching allowed in the current file? , optExactSplit :: Bool , optEta :: Bool , optRewriting :: Bool -- ^ Can rewrite rules be added and used? , optCubical :: Bool , optPostfixProjections :: Bool -- ^ Should system generated projections 'ProjSystem' be printed -- postfix (True) or prefix (False). , optInstanceSearchDepth :: Int , optOverlappingInstances :: Bool , optInversionMaxDepth :: Int , optSafe :: Bool , optDoubleCheck :: Bool , optSyntacticEquality :: Bool -- ^ Should conversion checker use syntactic equality shortcut? , optWarningMode :: WarningMode , optCompileNoMain :: Bool , optCaching :: Bool , optCountClusters :: Bool -- ^ Count extended grapheme clusters rather than code points when -- generating LaTeX. , optAutoInline :: Bool -- ^ Automatic compile-time inlining for simple definitions (unless marked -- NOINLINE). , optPrintPatternSynonyms :: Bool , optFastReduce :: Bool -- ^ Use the Agda abstract machine (fastReduce)? } deriving (Show, Eq) -- | The options from an @OPTIONS@ pragma. -- -- In the future it might be nice to switch to a more structured -- representation. Note that, currently, there is not a one-to-one -- correspondence between list elements and options. type OptionsPragma = [String] -- | Map a function over the long options. Also removes the short options. -- Will be used to add the plugin name to the plugin options. mapFlag :: (String -> String) -> OptDescr a -> OptDescr a mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr defaultVerbosity :: Verbosity defaultVerbosity = Trie.singleton [] 1 defaultInteractionOptions :: PragmaOptions defaultInteractionOptions = defaultPragmaOptions defaultOptions :: CommandLineOptions defaultOptions = Options { optProgramName = "agda" , optInputFile = Nothing , optIncludePaths = [] , optAbsoluteIncludePaths = [] , optLibraries = [] , optOverrideLibrariesFile = Nothing , optDefaultLibs = True , optUseLibs = True , optShowVersion = False , optShowHelp = Nothing , optInteractive = False , optGHCiInteraction = False , optJSONInteraction = False , optOptimSmashing = True , optCompileDir = Nothing , optGenerateVimFile = False , optGenerateLaTeX = False , optGenerateHTML = False , optHTMLHighlight = HighlightAll , optDependencyGraph = Nothing , optLaTeXDir = defaultLaTeXDir , optHTMLDir = defaultHTMLDir , optCSSFile = Nothing , optIgnoreInterfaces = False , optIgnoreAllInterfaces = False , optForcing = True , optPragmaOptions = defaultPragmaOptions , optOnlyScopeChecking = False } defaultPragmaOptions :: PragmaOptions defaultPragmaOptions = PragmaOptions { optShowImplicit = False , optShowIrrelevant = False , optUseUnicode = True , optVerbose = defaultVerbosity , optProp = False , optExperimentalIrrelevance = False , optIrrelevantProjections = False -- off by default in > 2.5.4, see issue #2170 , optAllowUnsolved = False , optDisablePositivity = False , optTerminationCheck = True , optTerminationDepth = defaultCutOff , optCompletenessCheck = True , optUniverseCheck = True , optOmegaInOmega = False , optSizedTypes = Default , optGuardedness = Default , optInjectiveTypeConstructors = False , optUniversePolymorphism = True , optWithoutK = Default , optCopatterns = True , optPatternMatching = True , optExactSplit = False , optEta = True , optRewriting = False , optCubical = False , optPostfixProjections = False , optInstanceSearchDepth = 500 , optOverlappingInstances = False , optInversionMaxDepth = 50 , optSafe = False , optDoubleCheck = False , optSyntacticEquality = True , optWarningMode = defaultWarningMode , optCompileNoMain = False , optCaching = True , optCountClusters = False , optAutoInline = True , optPrintPatternSynonyms = True , optFastReduce = True } -- | The default termination depth. defaultCutOff :: CutOff defaultCutOff = CutOff 0 -- minimum value -- | The default output directory for LaTeX. defaultLaTeXDir :: String defaultLaTeXDir = "latex" -- | The default output directory for HTML. defaultHTMLDir :: String defaultHTMLDir = "html" type OptM = ExceptT String IO runOptM :: OptM a -> IO (Either String a) runOptM = runExceptT {- | @f :: Flag opts@ is an action on the option record that results from parsing an option. @f opts@ produces either an error message or an updated options record -} type Flag opts = opts -> OptM opts -- | Checks that the given options are consistent. checkOpts :: Flag CommandLineOptions checkOpts opts | htmlRelated = throwError htmlRelatedMessage | not (matches [optGHCiInteraction, optJSONInteraction, isJust . optInputFile] <= 1) = throwError "Choose at most one: input file, --interactive, or --interaction-json.\n" | or [ p opts && matches ps > 1 | (p, ps) <- exclusive ] = throwError exclusiveMessage | otherwise = return opts where matches = length . filter ($ opts) optionChanged opt = ((/=) `on` opt) opts defaultOptions atMostOne = [ optGenerateHTML , isJust . optDependencyGraph ] ++ map fst exclusive exclusive = [ ( optOnlyScopeChecking , optGenerateVimFile : atMostOne ) , ( optInteractive , optGenerateLaTeX : atMostOne ) , ( optGHCiInteraction , optGenerateLaTeX : atMostOne ) , ( optJSONInteraction , optGenerateLaTeX : atMostOne ) ] exclusiveMessage = unlines $ [ "The options --interactive, --interaction, --interaction-json and" , "--only-scope-checking cannot be combined with each other or" , "with --html or --dependency-graph. Furthermore" , "--interactive and --interaction cannot be combined with" , "--latex, and --only-scope-checking cannot be combined with" , "--vim." ] htmlRelated = not (optGenerateHTML opts) && ( optionChanged optHTMLDir || optionChanged optHTMLHighlight || optionChanged optCSSFile ) htmlRelatedMessage = unlines $ [ "The options --html-highlight, --css-dir and --html-dir" , "only be used along with --html flag." ] -- | Check for unsafe pragmas. Gives a list of used unsafe flags. unsafePragmaOptions :: PragmaOptions -> [String] unsafePragmaOptions opts = [ "--allow-unsolved-metas" | optAllowUnsolved opts ] ++ [ "--no-positivity-check" | optDisablePositivity opts ] ++ [ "--no-termination-check" | not (optTerminationCheck opts) ] ++ [ "--type-in-type" | not (optUniverseCheck opts) ] ++ [ "--omega-in-omega" | optOmegaInOmega opts ] ++ -- [ "--sized-types" | optSizedTypes opts ] ++ [ "--sized-types and --guardedness" | collapseDefault (optSizedTypes opts) , collapseDefault (optGuardedness opts) ] ++ [ "--injective-type-constructors" | optInjectiveTypeConstructors opts ] ++ [ "--irrelevant-projections" | optIrrelevantProjections opts ] ++ [ "--experimental-irrelevance" | optExperimentalIrrelevance opts ] ++ [ "--rewriting" | optRewriting opts ] ++ [ "--cubical and --with-K" | optCubical opts , not (collapseDefault $ optWithoutK opts) ] ++ [] -- | If any these options have changed, then the file will be -- rechecked. Boolean options are negated to mention non-default -- options, where possible. restartOptions :: [(PragmaOptions -> RestartCodomain, String)] restartOptions = [ (C . optTerminationDepth, "--termination-depth") , (B . not . optUseUnicode, "--no-unicode") , (B . optAllowUnsolved, "--allow-unsolved-metas") , (B . optDisablePositivity, "--no-positivity-check") , (B . optTerminationCheck, "--no-termination-check") , (B . not . optUniverseCheck, "--type-in-type") , (B . optOmegaInOmega, "--omega-in-omega") , (B . not . collapseDefault . optSizedTypes, "--no-sized-types") , (B . not . collapseDefault . optGuardedness, "--no-guardedness") , (B . optInjectiveTypeConstructors, "--injective-type-constructors") , (B . optProp, "--prop") , (B . not . optUniversePolymorphism, "--no-universe-polymorphism") , (B . optIrrelevantProjections, "--irrelevant-projections") , (B . optExperimentalIrrelevance, "--experimental-irrelevance") , (B . collapseDefault . optWithoutK, "--without-K") , (B . optExactSplit, "--exact-split") , (B . not . optEta, "--no-eta-equality") , (B . optRewriting, "--rewriting") , (B . optCubical, "--cubical") , (B . optOverlappingInstances, "--overlapping-instances") , (B . optSafe, "--safe") , (B . optDoubleCheck, "--double-check") , (B . not . optSyntacticEquality, "--no-syntactic-equality") , (B . not . optAutoInline, "--no-auto-inline") , (B . not . optFastReduce, "--no-fast-reduce") , (I . optInstanceSearchDepth, "--instance-search-depth") , (I . optInversionMaxDepth, "--inversion-max-depth") , (W . optWarningMode, "--warning") ] -- to make all restart options have the same type data RestartCodomain = C CutOff | B Bool | I Int | W WarningMode deriving Eq -- | An infective option is an option that if used in one module, must -- be used in all modules that depend on this module. infectiveOptions :: [(PragmaOptions -> Bool, String)] infectiveOptions = [ (optCubical, "--cubical") , (optProp, "--prop") ] -- | A coinfective option is an option that if used in one module, must -- be used in all modules that this module depends on. coinfectiveOptions :: [(PragmaOptions -> Bool, String)] coinfectiveOptions = [ (optSafe, "--safe") , (collapseDefault . optWithoutK, "--without-K") , (not . optUniversePolymorphism, "--no-universe-polymorphism") , (not . collapseDefault . optSizedTypes, "--no-sized-types") , (not . collapseDefault . optGuardedness, "--no-guardedness") ] inputFlag :: FilePath -> Flag CommandLineOptions inputFlag f o = case optInputFile o of Nothing -> return $ o { optInputFile = Just f } Just _ -> throwError "only one input file allowed" versionFlag :: Flag CommandLineOptions versionFlag o = return $ o { optShowVersion = True } helpFlag :: Maybe String -> Flag CommandLineOptions helpFlag Nothing o = return $ o { optShowHelp = Just GeneralHelp } helpFlag (Just str) o = case string2HelpTopic str of Just hpt -> return $ o { optShowHelp = Just (HelpFor hpt) } Nothing -> throwError $ "unknown help topic " ++ str ++ " (available: " ++ intercalate ", " (map fst allHelpTopics) ++ ")" safeFlag :: Flag PragmaOptions safeFlag o = do let guardedness = optGuardedness o let sizedTypes = optSizedTypes o return $ o { optSafe = True , optGuardedness = setDefault False guardedness , optSizedTypes = setDefault False sizedTypes } doubleCheckFlag :: Flag PragmaOptions doubleCheckFlag o = return $ o { optDoubleCheck = True } noSyntacticEqualityFlag :: Flag PragmaOptions noSyntacticEqualityFlag o = return $ o { optSyntacticEquality = False } sharingFlag :: Bool -> Flag CommandLineOptions sharingFlag _ _ = throwError $ "Feature --sharing has been removed (in favor of the Agda abstract machine)." cachingFlag :: Bool -> Flag PragmaOptions cachingFlag b o = return $ o { optCaching = b } propFlag :: Flag PragmaOptions propFlag o = return $ o { optProp = True } noPropFlag :: Flag PragmaOptions noPropFlag o = return $ o { optProp = False } experimentalIrrelevanceFlag :: Flag PragmaOptions experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True } irrelevantProjectionsFlag :: Flag PragmaOptions irrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = True } noIrrelevantProjectionsFlag :: Flag PragmaOptions noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False } ignoreInterfacesFlag :: Flag CommandLineOptions ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True } ignoreAllInterfacesFlag :: Flag CommandLineOptions ignoreAllInterfacesFlag o = return $ o { optIgnoreAllInterfaces = True } allowUnsolvedFlag :: Flag PragmaOptions allowUnsolvedFlag o = do let upd = over warningSet (Set.\\ unsolvedWarnings) return $ o { optAllowUnsolved = True , optWarningMode = upd (optWarningMode o) } showImplicitFlag :: Flag PragmaOptions showImplicitFlag o = return $ o { optShowImplicit = True } showIrrelevantFlag :: Flag PragmaOptions showIrrelevantFlag o = return $ o { optShowIrrelevant = True } asciiOnlyFlag :: Flag PragmaOptions asciiOnlyFlag o = do lift $ writeIORef unicodeOrAscii AsciiOnly return $ o { optUseUnicode = False } ghciInteractionFlag :: Flag CommandLineOptions ghciInteractionFlag o = return $ o { optGHCiInteraction = True } jsonInteractionFlag :: Flag CommandLineOptions jsonInteractionFlag o = return $ o { optJSONInteraction = True } vimFlag :: Flag CommandLineOptions vimFlag o = return $ o { optGenerateVimFile = True } latexFlag :: Flag CommandLineOptions latexFlag o = return $ o { optGenerateLaTeX = True } onlyScopeCheckingFlag :: Flag CommandLineOptions onlyScopeCheckingFlag o = return $ o { optOnlyScopeChecking = True } countClustersFlag :: Flag PragmaOptions countClustersFlag o = #ifdef COUNT_CLUSTERS return $ o { optCountClusters = True } #else throwError "Cluster counting has not been enabled in this build of Agda." #endif noAutoInlineFlag :: Flag PragmaOptions noAutoInlineFlag o = return $ o { optAutoInline = False } noPrintPatSynFlag :: Flag PragmaOptions noPrintPatSynFlag o = return $ o { optPrintPatternSynonyms = False } noFastReduceFlag :: Flag PragmaOptions noFastReduceFlag o = return $ o { optFastReduce = False } latexDirFlag :: FilePath -> Flag CommandLineOptions latexDirFlag d o = return $ o { optLaTeXDir = d } noPositivityFlag :: Flag PragmaOptions noPositivityFlag o = do let upd = over warningSet (Set.delete NotStrictlyPositive_) return $ o { optDisablePositivity = True , optWarningMode = upd (optWarningMode o) } dontTerminationCheckFlag :: Flag PragmaOptions dontTerminationCheckFlag o = do let upd = over warningSet (Set.delete TerminationIssue_) return $ o { optTerminationCheck = False , optWarningMode = upd (optWarningMode o) } -- The option was removed. See Issue 1918. dontCompletenessCheckFlag :: Flag PragmaOptions dontCompletenessCheckFlag _ = throwError "The --no-coverage-check option has been removed." dontUniverseCheckFlag :: Flag PragmaOptions dontUniverseCheckFlag o = return $ o { optUniverseCheck = False } omegaInOmegaFlag :: Flag PragmaOptions omegaInOmegaFlag o = return $ o { optOmegaInOmega = True } etaFlag :: Flag PragmaOptions etaFlag o = return $ o { optEta = True } noEtaFlag :: Flag PragmaOptions noEtaFlag o = return $ o { optEta = False } sizedTypes :: Flag PragmaOptions sizedTypes o = return $ o { optSizedTypes = Value True } noSizedTypes :: Flag PragmaOptions noSizedTypes o = return $ o { optSizedTypes = Value False } guardedness :: Flag PragmaOptions guardedness o = return $ o { optGuardedness = Value True } noGuardedness :: Flag PragmaOptions noGuardedness o = return $ o { optGuardedness = Value False } injectiveTypeConstructorFlag :: Flag PragmaOptions injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True } guardingTypeConstructorFlag :: Flag PragmaOptions guardingTypeConstructorFlag _ = throwError $ "Experimental feature --guardedness-preserving-type-constructors has been removed." universePolymorphismFlag :: Flag PragmaOptions universePolymorphismFlag o = return $ o { optUniversePolymorphism = True } noUniversePolymorphismFlag :: Flag PragmaOptions noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False } noForcingFlag :: Flag CommandLineOptions noForcingFlag o = return $ o { optForcing = False } withKFlag :: Flag PragmaOptions withKFlag o = return $ o { optWithoutK = Value False } withoutKFlag :: Flag PragmaOptions withoutKFlag o = return $ o { optWithoutK = Value True } copatternsFlag :: Flag PragmaOptions copatternsFlag o = return $ o { optCopatterns = True } noCopatternsFlag :: Flag PragmaOptions noCopatternsFlag o = return $ o { optCopatterns = False } noPatternMatchingFlag :: Flag PragmaOptions noPatternMatchingFlag o = return $ o { optPatternMatching = False } exactSplitFlag :: Flag PragmaOptions exactSplitFlag o = do let upd = over warningSet (Set.insert CoverageNoExactSplit_) return $ o { optExactSplit = True , optWarningMode = upd (optWarningMode o) } noExactSplitFlag :: Flag PragmaOptions noExactSplitFlag o = do let upd = over warningSet (Set.delete CoverageNoExactSplit_) return $ o { optExactSplit = False , optWarningMode = upd (optWarningMode o) } rewritingFlag :: Flag PragmaOptions rewritingFlag o = return $ o { optRewriting = True } cubicalFlag :: Flag PragmaOptions cubicalFlag o = do let withoutK = optWithoutK o return $ o { optCubical = True , optWithoutK = setDefault True withoutK } postfixProjectionsFlag :: Flag PragmaOptions postfixProjectionsFlag o = return $ o { optPostfixProjections = True } instanceDepthFlag :: String -> Flag PragmaOptions instanceDepthFlag s o = do d <- integerArgument "--instance-search-depth" s return $ o { optInstanceSearchDepth = d } overlappingInstancesFlag :: Flag PragmaOptions overlappingInstancesFlag o = return $ o { optOverlappingInstances = True } noOverlappingInstancesFlag :: Flag PragmaOptions noOverlappingInstancesFlag o = return $ o { optOverlappingInstances = False } inversionMaxDepthFlag :: String -> Flag PragmaOptions inversionMaxDepthFlag s o = do d <- integerArgument "--inversion-max-depth" s return $ o { optInversionMaxDepth = d } interactiveFlag :: Flag CommandLineOptions interactiveFlag o = do prag <- allowUnsolvedFlag (optPragmaOptions o) return $ o { optInteractive = True , optPragmaOptions = prag } compileFlagNoMain :: Flag PragmaOptions compileFlagNoMain o = return $ o { optCompileNoMain = True } compileDirFlag :: FilePath -> Flag CommandLineOptions compileDirFlag f o = return $ o { optCompileDir = Just f } htmlFlag :: Flag CommandLineOptions htmlFlag o = return $ o { optGenerateHTML = True } htmlHighlightFlag :: String -> Flag CommandLineOptions htmlHighlightFlag "code" o = return $ o { optHTMLHighlight = HighlightCode } htmlHighlightFlag "all" o = return $ o { optHTMLHighlight = HighlightAll } htmlHighlightFlag "auto" o = return $ o { optHTMLHighlight = HighlightAuto } htmlHighlightFlag opt o = throwError $ "Invalid option <" ++ opt ++ ">, expected , or " dependencyGraphFlag :: FilePath -> Flag CommandLineOptions dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f } htmlDirFlag :: FilePath -> Flag CommandLineOptions htmlDirFlag d o = return $ o { optHTMLDir = d } cssFlag :: FilePath -> Flag CommandLineOptions cssFlag f o = return $ o { optCSSFile = Just f } includeFlag :: FilePath -> Flag CommandLineOptions includeFlag d o = return $ o { optIncludePaths = d : optIncludePaths o } libraryFlag :: String -> Flag CommandLineOptions libraryFlag s o = return $ o { optLibraries = optLibraries o ++ [s] } overrideLibrariesFileFlag :: String -> Flag CommandLineOptions overrideLibrariesFileFlag s o = do ifM (liftIO $ doesFileExist s) {-then-} (return $ o { optOverrideLibrariesFile = Just s }) {-else-} (throwError $ "Libraries file not found: " ++ s) noDefaultLibsFlag :: Flag CommandLineOptions noDefaultLibsFlag o = return $ o { optDefaultLibs = False } noLibsFlag :: Flag CommandLineOptions noLibsFlag o = return $ o { optUseLibs = False } verboseFlag :: String -> Flag PragmaOptions verboseFlag s o = do (k,n) <- parseVerbose s return $ o { optVerbose = Trie.insert k n $ optVerbose o } where parseVerbose s = case wordsBy (`elem` (":." :: String)) s of [] -> usage ss -> do n <- readM (last ss) `catchError` \_ -> usage return (init ss, n) usage = throwError "argument to verbose should be on the form x.y.z:N or N" warningModeFlag :: String -> Flag PragmaOptions warningModeFlag s o = case warningModeUpdate s of Just upd -> return $ o { optWarningMode = upd (optWarningMode o) } Nothing -> throwError $ "unknown warning flag " ++ s ++ ". See --help=warning." terminationDepthFlag :: String -> Flag PragmaOptions terminationDepthFlag s o = do k <- readM s `catchError` \_ -> usage when (k < 1) $ usage -- or: turn termination checking off for 0 return $ o { optTerminationDepth = CutOff $ k-1 } where usage = throwError "argument to termination-depth should be >= 1" integerArgument :: String -> String -> OptM Int integerArgument flag s = readM s `catchError` \_ -> throwError $ "option '" ++ flag ++ "' requires an integer argument" standardOptions :: [OptDescr (Flag CommandLineOptions)] standardOptions = [ Option ['V'] ["version"] (NoArg versionFlag) "show version number" , Option ['?'] ["help"] (OptArg helpFlag "TOPIC") ("show help for TOPIC (available: " ++ intercalate ", " (map fst allHelpTopics) ++ ")") , Option ['I'] ["interactive"] (NoArg interactiveFlag) "start in interactive mode" , Option [] ["interaction"] (NoArg ghciInteractionFlag) "for use with the Emacs mode" , Option [] ["interaction-json"] (NoArg jsonInteractionFlag) "for use with other editors such as Atom" , Option [] ["compile-dir"] (ReqArg compileDirFlag "DIR") ("directory for compiler output (default: the project root)") , Option [] ["vim"] (NoArg vimFlag) "generate Vim highlighting files" , Option [] ["latex"] (NoArg latexFlag) "generate LaTeX with highlighted source code" , Option [] ["latex-dir"] (ReqArg latexDirFlag "DIR") ("directory in which LaTeX files are placed (default: " ++ defaultLaTeXDir ++ ")") , 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 [] ["html-highlight"] (ReqArg htmlHighlightFlag "[code,all,auto]") ("whether to highlight only the code parts (code) or " ++ "the file as a whole (all) or " ++ "decide by source file type (auto)") , Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE") "generate a Dot file with a module dependency graph" , Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag) "ignore interface files (re-type check everything)" , Option ['i'] ["include-path"] (ReqArg includeFlag "DIR") "look for imports in DIR" , Option ['l'] ["library"] (ReqArg libraryFlag "LIB") "use library LIB" , Option [] ["library-file"] (ReqArg overrideLibrariesFileFlag "FILE") "use FILE instead of the standard libraries file" , Option [] ["no-libraries"] (NoArg noLibsFlag) "don't use any library files" , Option [] ["no-default-libraries"] (NoArg noDefaultLibsFlag) "don't use default libraries" , Option [] ["no-forcing"] (NoArg noForcingFlag) "disable the forcing optimisation" , Option [] ["only-scope-checking"] (NoArg onlyScopeCheckingFlag) "only scope-check the top-level module, do not type-check it" ] ++ map (fmap lensPragmaOptions) pragmaOptions -- | Defined locally here since module ''Agda.Interaction.Options.Lenses'' -- has cyclic dependency. lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions lensPragmaOptions f st = f (optPragmaOptions st) <&> \ opts -> st { optPragmaOptions = opts } -- | Command line options of previous versions of Agda. -- Should not be listed in the usage info, put parsed by GetOpt for good error messaging. deadStandardOptions :: [OptDescr (Flag CommandLineOptions)] deadStandardOptions = [ Option [] ["sharing"] (NoArg $ sharingFlag True) "DEPRECATED: does nothing" , Option [] ["no-sharing"] (NoArg $ sharingFlag False) "DEPRECATED: does nothing" , Option [] ["ignore-all-interfaces"] (NoArg ignoreAllInterfacesFlag) -- not deprecated! Just hidden "ignore all interface files (re-type check everything, including builtin files)" ] ++ map (fmap lensPragmaOptions) deadPragmaOptions pragmaOptions :: [OptDescr (Flag PragmaOptions)] pragmaOptions = [ Option [] ["show-implicit"] (NoArg showImplicitFlag) "show implicit arguments when printing" , Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag) "show irrelevant arguments when printing" , Option [] ["no-unicode"] (NoArg asciiOnlyFlag) "don't use unicode characters when printing terms" , Option ['v'] ["verbose"] (ReqArg verboseFlag "N") "set verbosity level to N" , Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag) "succeed and create interface file regardless of unsolved meta variables" , 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 [] ["termination-depth"] (ReqArg terminationDepthFlag "N") "allow termination checker to count decrease/increase upto N (default N=1)" , Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag) "ignore universe levels (this makes Agda inconsistent)" , Option [] ["omega-in-omega"] (NoArg omegaInOmegaFlag) "enable typing rule Setω : Setω (this makes Agda inconsistent)" , Option [] ["prop"] (NoArg propFlag) "enable the use of the Prop universe" , Option [] ["no-prop"] (NoArg noPropFlag) "disable the use of the Prop universe (default)" , Option [] ["sized-types"] (NoArg sizedTypes) "enable sized types (default, inconsistent with --guardedness)" , Option [] ["no-sized-types"] (NoArg noSizedTypes) "disable sized types" , Option [] ["guardedness"] (NoArg guardedness) "enable constructor-based guarded corecursion (default, inconsistent with --sized-types)" , Option [] ["no-guardedness"] (NoArg noGuardedness) "disable constructor-based guarded corecursion" , Option [] ["injective-type-constructors"] (NoArg injectiveTypeConstructorFlag) "enable injective type constructors (makes Agda anti-classical and possibly inconsistent)" , Option [] ["no-universe-polymorphism"] (NoArg noUniversePolymorphismFlag) "disable universe polymorphism" , Option [] ["universe-polymorphism"] (NoArg universePolymorphismFlag) "enable universe polymorphism (default)" , Option [] ["irrelevant-projections"] (NoArg irrelevantProjectionsFlag) "enable projection of irrelevant record fields and similar irrelevant definitions (inconsistent)" , Option [] ["no-irrelevant-projections"] (NoArg noIrrelevantProjectionsFlag) "disable projection of irrelevant record fields and similar irrelevant definitions (default)" , Option [] ["experimental-irrelevance"] (NoArg experimentalIrrelevanceFlag) "enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)" , Option [] ["with-K"] (NoArg withKFlag) "enable the K rule in pattern matching (default)" , Option [] ["without-K"] (NoArg withoutKFlag) "disable the K rule in pattern matching" , Option [] ["copatterns"] (NoArg copatternsFlag) "enable definitions by copattern matching (default)" , Option [] ["no-copatterns"] (NoArg noCopatternsFlag) "disable definitions by copattern matching" , Option [] ["no-pattern-matching"] (NoArg noPatternMatchingFlag) "disable pattern matching completely" , Option [] ["exact-split"] (NoArg exactSplitFlag) "require all clauses in a definition to hold as definitional equalities (unless marked CATCHALL)" , Option [] ["no-exact-split"] (NoArg noExactSplitFlag) "do not require all clauses in a definition to hold as definitional equalities (default)" , Option [] ["no-eta-equality"] (NoArg noEtaFlag) "default records to no-eta-equality" , Option [] ["rewriting"] (NoArg rewritingFlag) "enable declaration and use of REWRITE rules" , Option [] ["cubical"] (NoArg cubicalFlag) "enable cubical features (e.g. overloads lambdas for paths), implies --without-K" , Option [] ["postfix-projections"] (NoArg postfixProjectionsFlag) "make postfix projection notation the default" , Option [] ["instance-search-depth"] (ReqArg instanceDepthFlag "N") "set instance search depth to N (default: 500)" , Option [] ["overlapping-instances"] (NoArg overlappingInstancesFlag) "consider recursive instance arguments during pruning of instance candidates" , Option [] ["no-overlapping-instances"] (NoArg noOverlappingInstancesFlag) "don't consider recursive instance arguments during pruning of instance candidates (default)" , Option [] ["inversion-max-depth"] (ReqArg inversionMaxDepthFlag "N") "set maximum depth for pattern match inversion to N (default: 50)" , Option [] ["safe"] (NoArg safeFlag) "disable postulates, unsafe OPTION pragmas and primEraseEquality, implies --no-sized-types and --no-guardedness " , Option [] ["double-check"] (NoArg doubleCheckFlag) "enable double-checking of all terms using the internal typechecker" , Option [] ["no-syntactic-equality"] (NoArg noSyntacticEqualityFlag) "disable the syntactic equality shortcut in the conversion checker" , Option ['W'] ["warning"] (ReqArg warningModeFlag "FLAG") ("set warning flags. See --help=warning.") , Option [] ["no-main"] (NoArg compileFlagNoMain) "do not treat the requested module as the main module of a program when compiling" , Option [] ["caching"] (NoArg $ cachingFlag True) "enable caching of typechecking (default)" , Option [] ["no-caching"] (NoArg $ cachingFlag False) "disable caching of typechecking" , Option [] ["count-clusters"] (NoArg countClustersFlag) ("count extended grapheme clusters when " ++ "generating LaTeX (note that this flag " ++ #ifdef COUNT_CLUSTERS "is not enabled in all builds of Agda)" #else "has not been enabled in this build of Agda)" #endif ) , Option [] ["no-auto-inline"] (NoArg noAutoInlineFlag) ("disable automatic compile-time inlining " ++ "(only definitions marked INLINE will be inlined)") , Option [] ["no-print-pattern-synonyms"] (NoArg noPrintPatSynFlag) "expand pattern synonyms when printing terms" , Option [] ["no-fast-reduce"] (NoArg noFastReduceFlag) "disable reduction using the Agda Abstract Machine" ] -- | Pragma options of previous versions of Agda. -- Should not be listed in the usage info, put parsed by GetOpt for good error messaging. deadPragmaOptions :: [OptDescr (Flag PragmaOptions)] deadPragmaOptions = [ Option [] ["guardedness-preserving-type-constructors"] (NoArg guardingTypeConstructorFlag) "treat type constructors as inductive constructors when checking productivity" , Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag) "the option has been removed" ] -- | Used for printing usage info. -- Does not include the dead options. standardOptions_ :: [OptDescr ()] standardOptions_ = map (fmap $ const ()) standardOptions -- | Simple interface for System.Console.GetOpt -- Could be moved to Agda.Utils.Options (does not exist yet) getOptSimple :: [String] -- ^ command line argument words -> [OptDescr (Flag opts)] -- ^ options handlers -> (String -> Flag opts) -- ^ handler of non-options (only one is allowed) -> Flag opts -- ^ combined opts data structure transformer getOptSimple argv opts fileArg = \ defaults -> case getOpt' (ReturnInOrder fileArg) opts argv of (o, _, [] , [] ) -> foldl (>>=) (return defaults) o (_, _, unrecognized, errs) -> throwError $ umsg ++ emsg where ucap = "Unrecognized " ++ plural unrecognized "option" ++ ":" ecap = plural errs "Option error" ++ ":" umsg = if null unrecognized then "" else unlines $ ucap : map suggest unrecognized emsg = if null errs then "" else unlines $ ecap : errs plural [_] x = x plural _ x = x ++ "s" -- Suggest alternatives that are at most 3 typos away longopts :: [String] longopts = map ("--" ++) $ concat $ map (\ (Option _ long _ _) -> long) opts dist :: String -> String -> Int dist s t = restrictedDamerauLevenshteinDistance defaultEditCosts s t close :: String -> String -> Maybe (Int, String) close s t = let d = dist s t in if d <= 3 then Just (d, t) else Nothing closeopts :: String -> [(Int, String)] closeopts s = mapMaybe (close s) longopts alts :: String -> [[String]] alts s = map (map snd) $ groupOn fst $ closeopts s suggest :: String -> String suggest s = case alts s of [] -> s as : _ -> s ++ " (did you mean " ++ sugs as ++ " ?)" sugs :: [String] -> String sugs [a] = a sugs as = "any of " ++ intercalate " " as {- No longer used in favour of parseBackendOptions in Agda.Compiler.Backend -- | Parse the standard options. parseStandardOptions :: [String] -> OptM CommandLineOptions parseStandardOptions argv = parseStandardOptions' argv defaultOptions parseStandardOptions' :: [String] -> Flag CommandLineOptions parseStandardOptions' argv opts = do opts <- getOptSimple (stripRTS argv) (deadStandardOptions ++ standardOptions) inputFlag opts checkOpts opts -} -- | Parse options from an options pragma. parsePragmaOptions :: [String] -- ^ Pragma options. -> CommandLineOptions -- ^ Command-line options which should be updated. -> OptM PragmaOptions parsePragmaOptions argv opts = do ps <- getOptSimple argv (deadPragmaOptions ++ pragmaOptions) (\s _ -> throwError $ "Bad option in pragma: " ++ s) (optPragmaOptions opts) _ <- checkOpts (opts { optPragmaOptions = ps }) return ps -- | Parse options for a plugin. parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts parsePluginOptions argv opts = getOptSimple argv opts (\s _ -> throwError $ "Internal error: Flag " ++ s ++ " passed to a plugin") -- | The usage info message. The argument is the program name (probably -- agda). usage :: [OptDescr ()] -> String -> Help -> String usage options progName GeneralHelp = usageInfo (header progName) options where header progName = unlines [ "Agda version " ++ version, "" , "Usage: " ++ progName ++ " [OPTIONS...] [FILE]" ] usage options progName (HelpFor topic) = helpTopicUsage topic -- | Removes RTS options from a list of options. stripRTS :: [String] -> [String] stripRTS [] = [] stripRTS ("--RTS" : argv) = argv stripRTS (arg : argv) | is "+RTS" arg = stripRTS $ drop 1 $ dropWhile (not . is "-RTS") argv | otherwise = arg : stripRTS argv where is x arg = [x] == take 1 (words arg) ------------------------------------------------------------------------ -- Some paths -- | Returns the absolute default lib dir. This directory is used to -- store the Primitive.agda file. defaultLibDir :: IO FilePath defaultLibDir = do libdir <- fmap filePath (absolute =<< getDataFileName "lib") ifM (doesDirectoryExist libdir) (return libdir) (error $ "The lib directory " ++ libdir ++ " does not exist")