Agda-2.4.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone

Agda.Interaction.Options

Synopsis

Documentation

data CommandLineOptions Source

Constructors

Options 

Fields

optProgramName :: String
 
optInputFile :: Maybe FilePath
 
optIncludeDirs :: IncludeDirs
 
optShowVersion :: Bool
 
optShowHelp :: Bool
 
optInteractive :: Bool
 
optRunTests :: Bool
 
optGHCiInteraction :: Bool
 
optCompile :: Bool
 
optCompileNoMain :: Bool
 
optEpicCompile :: Bool
 
optJSCompile :: Bool
 
optCompileDir :: Maybe FilePath

In the absence of a path the project root is used.

optGenerateVimFile :: Bool
 
optGenerateLaTeX :: Bool
 
optGenerateHTML :: Bool
 
optDependencyGraph :: Maybe FilePath
 
optLaTeXDir :: FilePath
 
optHTMLDir :: FilePath
 
optCSSFile :: Maybe FilePath
 
optIgnoreInterfaces :: Bool
 
optForcing :: Bool
 
optGhcFlags :: [String]
 
optPragmaOptions :: PragmaOptions
 
optEpicFlags :: [String]
 
optSafe :: Bool
 

data PragmaOptions Source

Options which can be set in a pragma.

Constructors

PragmaOptions 

Fields

optShowImplicit :: Bool
 
optShowIrrelevant :: Bool
 
optVerbose :: Verbosity
 
optProofIrrelevance :: Bool
 
optAllowUnsolved :: Bool
 
optDisablePositivity :: Bool
 
optTerminationCheck :: Bool
 
optTerminationDepth :: CutOff

Cut off structural order comparison at some depth in termination checker?

optCompletenessCheck :: Bool
 
optUniverseCheck :: Bool
 
optSizedTypes :: Bool
 
optInjectiveTypeConstructors :: Bool
 
optGuardingTypeConstructors :: Bool
 
optUniversePolymorphism :: Bool
 
optIrrelevantProjections :: Bool
 
optExperimentalIrrelevance :: Bool

irrelevant levels, irrelevant data matching

optWithoutK :: Bool
 
optCopatterns :: Bool

Allow definitions by copattern matching?

optPatternMatching :: Bool

Is pattern matching allowed in the current file?

type OptionsPragma = [String]Source

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 Flag opts = opts -> Either String optsSource

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 Verbosity = Trie String IntSource

type IncludeDirsSource

Arguments

 = Either [FilePath] [AbsolutePath]

Left is used temporarily, before the paths have been made absolute. An empty Left list is interpreted as [.] (see makeIncludeDirsAbsolute).

checkOpts :: Flag CommandLineOptionsSource

Checks that the given options are consistent.

parseStandardOptions :: [String] -> Either String CommandLineOptionsSource

Parse the standard options.

parsePragmaOptionsSource

Arguments

:: [String]

Pragma options.

-> CommandLineOptions

Command-line options which should be updated.

-> Either String PragmaOptions 

Parse options from an options pragma.

parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag optsSource

Parse options for a plugin.

defaultCutOff :: CutOffSource

The default termination depth.

standardOptions_ :: [OptDescr ()]Source

Used for printing usage info.

isLiterate :: FilePath -> BoolSource

This should probably go somewhere else.

mapFlag :: (String -> String) -> OptDescr a -> OptDescr aSource

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> StringSource

The usage info message. The argument is the program name (probably agda).

tests :: IO BoolSource