Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




data PragmaOptions Source

Options which can be set in a pragma.




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?

optRewriting :: Bool

Can rewrite rules be added and used?

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 opts Source

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 IncludeDirs Source


 = 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 CommandLineOptions Source

Checks that the given options are consistent.

parsePragmaOptions Source


:: [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 opts Source

Parse options for a plugin.

defaultCutOff :: CutOff Source

The default termination depth.

standardOptions_ :: [OptDescr ()] Source

Used for printing usage info.

unsafePragmaOptions :: PragmaOptions -> [String] Source

Check for unsafe pramas. Gives a list of used unsafe flags.

isLiterate :: FilePath -> Bool Source

This should probably go somewhere else.

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

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 -> String Source

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

defaultLibDir :: IO FilePath Source

Returns the absolute default lib dir. This directory is used to store the Primitive.agda file.

getOptSimple Source


:: [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

Simple interface for System.Console.GetOpt Could be moved to Agda.Utils.Options (does not exist yet)