| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Options
Synopsis
- data CommandLineOptions = Options {
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
- optDefaultLibs :: Bool
- optUseLibs :: Bool
- optTrustedExecutables :: Map ExeName FilePath
- optPrintAgdaDir :: Bool
- optPrintVersion :: Bool
- optPrintHelp :: Maybe Help
- optInteractive :: Bool
- optGHCiInteraction :: Bool
- optJSONInteraction :: Bool
- optExitOnError :: !Bool
- optCompileDir :: Maybe FilePath
- optGenerateVimFile :: Bool
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optLocalInterfaces :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool
- optTransliterate :: Bool
- data PragmaOptions = PragmaOptions {
- optShowImplicit :: Bool
- optShowIrrelevant :: Bool
- optUseUnicode :: UnicodeOrAscii
- optVerbose :: !Verbosity
- optProfiling :: ProfileOptions
- optProp :: Bool
- optTwoLevel :: WithDefault 'False
- optAllowUnsolved :: Bool
- optAllowIncompleteMatch :: Bool
- optDisablePositivity :: Bool
- optTerminationCheck :: Bool
- optTerminationDepth :: CutOff
- optUniverseCheck :: Bool
- optOmegaInOmega :: Bool
- optCumulativity :: Bool
- optSizedTypes :: WithDefault 'False
- optGuardedness :: WithDefault 'False
- optInjectiveTypeConstructors :: Bool
- optUniversePolymorphism :: Bool
- optIrrelevantProjections :: Bool
- optExperimentalIrrelevance :: Bool
- optWithoutK :: WithDefault 'False
- optCubicalCompatible :: WithDefault 'False
- optCopatterns :: Bool
- optPatternMatching :: Bool
- optExactSplit :: Bool
- optEta :: Bool
- optForcing :: Bool
- optProjectionLike :: Bool
- optEraseRecordParameters :: Bool
- optRewriting :: Bool
- optCubical :: Maybe Cubical
- optGuarded :: Bool
- optFirstOrder :: Bool
- optPostfixProjections :: Bool
- optKeepPatternVariables :: Bool
- optInstanceSearchDepth :: Int
- optOverlappingInstances :: Bool
- optQualifiedInstances :: Bool
- optInversionMaxDepth :: Int
- optSafe :: Bool
- optDoubleCheck :: Bool
- optSyntacticEquality :: !(Maybe Int)
- optWarningMode :: WarningMode
- optCompileNoMain :: Bool
- optCaching :: Bool
- optCountClusters :: Bool
- optAutoInline :: Bool
- optPrintPatternSynonyms :: Bool
- optFastReduce :: Bool
- optCallByName :: Bool
- optConfluenceCheck :: Maybe ConfluenceCheck
- optCohesion :: Bool
- optFlatSplit :: WithDefault 'False
- optImportSorts :: Bool
- optLoadPrimitives :: Bool
- optAllowExec :: Bool
- optSaveMetas :: WithDefault 'False
- optShowIdentitySubstitutions :: Bool
- optKeepCoveringClauses :: Bool
- type OptionsPragma = [String]
- type Flag opts = opts -> OptM opts
- type OptM = Except String
- runOptM :: Monad m => OptM opts -> m (Either String opts)
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- data ArgDescr a
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
- data WarningMode = WarningMode {}
- data ConfluenceCheck
- data UnicodeOrAscii
- checkOpts :: Flag CommandLineOptions
- parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- parseVerboseKey :: VerboseKey -> [VerboseKeyItem]
- stripRTS :: [String] -> [String]
- defaultOptions :: CommandLineOptions
- defaultInteractionOptions :: PragmaOptions
- defaultCutOff :: CutOff
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
- recheckBecausePragmaOptionsChanged :: PragmaOptions -> PragmaOptions -> Bool
- data InfectiveCoinfective
- data InfectiveCoinfectiveOption = ICOption {}
- infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption]
- safeFlag :: Flag PragmaOptions
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> String -> Help -> String
- inputFlag :: FilePath -> Flag CommandLineOptions
- standardOptions :: [OptDescr (Flag CommandLineOptions)]
- deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
- getOptSimple :: [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
- class (Functor m, Applicative m, Monad m) => HasOptions m where
Documentation
data CommandLineOptions Source #
Constructors
Instances
data PragmaOptions Source #
Options which can be set in a pragma.
Constructors
| PragmaOptions | |
Fields
| |
Instances
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
Describes whether an option takes an argument or not, and if so
how the argument is injected into a value of type a.
type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel) Source #
Nothing is used if no verbosity options have been given,
thus making it possible to handle the default case relatively
quickly. Note that Nothing corresponds to a trie with
verbosity level 1 for the empty path.
type VerboseKey = String Source #
type VerboseLevel = Int Source #
data WarningMode Source #
A WarningMode has two components: a set of warnings to be displayed
and a flag stating whether warnings should be turned into fatal errors.
Constructors
| WarningMode | |
Fields
| |
Instances
data ConfluenceCheck Source #
Constructors
| LocalConfluenceCheck | |
| GlobalConfluenceCheck |
Instances
| EmbPrj ConfluenceCheck Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
| Generic ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base Associated Types type Rep ConfluenceCheck :: Type -> Type # Methods from :: ConfluenceCheck -> Rep ConfluenceCheck x # to :: Rep ConfluenceCheck x -> ConfluenceCheck # | |
| Show ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> ConfluenceCheck -> ShowS # show :: ConfluenceCheck -> String # showList :: [ConfluenceCheck] -> ShowS # | |
| NFData ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base Methods rnf :: ConfluenceCheck -> () # | |
| Eq ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool # (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool # | |
| type Rep ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base | |
data UnicodeOrAscii Source #
We want to know whether we are allowed to insert unicode characters or not.
Instances
checkOpts :: Flag CommandLineOptions Source #
Checks that the given options are consistent.
Arguments
| :: [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.
parseVerboseKey :: VerboseKey -> [VerboseKeyItem] Source #
defaultCutOff :: CutOff Source #
The default termination depth.
standardOptions_ :: [OptDescr ()] Source #
Used for printing usage info. Does not include the dead options.
unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String] Source #
Check for unsafe pragmas. Gives a list of used unsafe flags.
recheckBecausePragmaOptionsChanged Source #
Arguments
| :: PragmaOptions | The options that were used to check the file. |
| -> PragmaOptions | The options that are currently in effect. |
| -> Bool |
This function returns True if the file should be rechecked.
data InfectiveCoinfective Source #
Infective or coinfective?
Constructors
| Infective | |
| Coinfective |
Instances
| EmbPrj InfectiveCoinfective Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
| Generic InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base Associated Types type Rep InfectiveCoinfective :: Type -> Type # Methods from :: InfectiveCoinfective -> Rep InfectiveCoinfective x # to :: Rep InfectiveCoinfective x -> InfectiveCoinfective # | |
| Show InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> InfectiveCoinfective -> ShowS # show :: InfectiveCoinfective -> String # showList :: [InfectiveCoinfective] -> ShowS # | |
| NFData InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base Methods rnf :: InfectiveCoinfective -> () # | |
| Eq InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base Methods (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool # (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool # | |
| type Rep InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base | |
data InfectiveCoinfectiveOption Source #
Descriptions of infective and coinfective options.
Constructors
| ICOption | |
Fields
| |
infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption] Source #
Infective and coinfective options.
Note that --cubical and --erased-cubical are "jointly
infective": if one of them is used in one module, then one or the
other must be used in all modules that depend on this module.
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 -> Help -> String Source #
The usage info message. The argument is the program name (probably agda).
deadStandardOptions :: [OptDescr (Flag CommandLineOptions)] Source #
Command line options of previous versions of Agda. Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
Arguments
| :: [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)
class (Functor m, Applicative m, Monad m) => HasOptions m where Source #
Minimal complete definition
Nothing
Methods
pragmaOptions :: m PragmaOptions Source #
Returns the pragma options which are currently in effect.
default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions Source #
commandLineOptions :: m CommandLineOptions Source #
Returns the command line options which are currently in effect.
default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions Source #