Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




data CommandLineOptions Source #


Show CommandLineOptions Source # 
LensPersistentVerbosity CommandLineOptions Source # 
LensIncludePaths CommandLineOptions Source # 
LensSafeMode CommandLineOptions Source # 
LensPragmaOptions CommandLineOptions Source # 

data PragmaOptions Source #

Options which can be set in a pragma.




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 -> OptM 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

checkOpts :: Flag CommandLineOptions Source #

Checks that the given options are consistent.

parseStandardOptions :: [String] -> OptM CommandLineOptions Source #

Parse the standard options.

parsePragmaOptions Source #


:: [String]

Pragma options.

-> CommandLineOptions

Command-line options which should be updated.

-> OptM 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 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)