Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Options

Synopsis

Documentation

data CommandLineOptions Source #

Constructors

Options 

Fields

Instances

Instances details
LensIncludePaths CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPersistentVerbosity CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

Generic CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep CommandLineOptions :: Type -> Type #

Show CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

NFData CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Methods

rnf :: CommandLineOptions -> () #

type Rep CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "Options" 'PrefixI 'True) ((((S1 ('MetaSel ('Just "optProgramName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "optInputFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath))) :*: (S1 ('MetaSel ('Just "optIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :*: (S1 ('MetaSel ('Just "optAbsoluteIncludePaths") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [AbsolutePath]) :*: S1 ('MetaSel ('Just "optLibraries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [LibName])))) :*: ((S1 ('MetaSel ('Just "optOverrideLibrariesFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath)) :*: (S1 ('MetaSel ('Just "optDefaultLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUseLibs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "optTrustedExecutables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ExeName FilePath)) :*: (S1 ('MetaSel ('Just "optPrintAgdaDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPrintVersion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "optPrintHelp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Help)) :*: (S1 ('MetaSel ('Just "optInteractive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optGHCiInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "optJSONInteraction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optOptimSmashing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optCompileDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe FilePath))))) :*: ((S1 ('MetaSel ('Just "optGenerateVimFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optIgnoreInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optIgnoreAllInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: (S1 ('MetaSel ('Just "optLocalInterfaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optPragmaOptions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PragmaOptions) :*: S1 ('MetaSel ('Just "optOnlyScopeChecking") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))))

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions 

Fields

Instances

Instances details
LensPersistentVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Generic PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep PragmaOptions :: Type -> Type #

Show PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

NFData PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Methods

rnf :: PragmaOptions -> () #

Eq PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

type Rep PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "PragmaOptions" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "optShowImplicit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optShowIrrelevant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUseUnicode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnicodeOrAscii))) :*: (S1 ('MetaSel ('Just "optVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Verbosity) :*: (S1 ('MetaSel ('Just "optProp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optTwoLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :*: ((S1 ('MetaSel ('Just "optAllowUnsolved") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optAllowIncompleteMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDisablePositivity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optTerminationDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CutOff)) :*: (S1 ('MetaSel ('Just "optCompletenessCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUniverseCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "optOmegaInOmega") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optSubtyping") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "optCumulativity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optSizedTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "optGuardedness") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :*: (S1 ('MetaSel ('Just "optInjectiveTypeConstructors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUniversePolymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optIrrelevantProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optExperimentalIrrelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optWithoutK") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "optCopatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPatternMatching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optExactSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optEta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))) :*: ((((S1 ('MetaSel ('Just "optForcing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optProjectionLike") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optRewriting") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optCubical") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Cubical)) :*: S1 ('MetaSel ('Just "optGuarded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optFirstOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPostfixProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optKeepPatternVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optInstanceSearchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "optOverlappingInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optQualifiedInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optInversionMaxDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "optSafe") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDoubleCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "optSyntacticEquality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optWarningMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningMode) :*: S1 ('MetaSel ('Just "optCompileNoMain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optCaching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optCountClusters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optAutoInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPrintPatternSynonyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optFastReduce") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optCallByName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optConfluenceCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ConfluenceCheck)))) :*: ((S1 ('MetaSel ('Just "optFlatSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optImportSorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optAllowExec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optShowIdentitySubstitutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))))

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

type OptM = Except String Source #

runOptM :: Monad m => OptM opts -> m (Either String opts) Source #

data OptDescr a #

Each OptDescr describes a single option.

The arguments to Option are:

  • list of short option characters
  • list of long option strings (without "--")
  • argument descriptor
  • explanation of option for user

Constructors

Option [Char] [String] (ArgDescr a) String 

Instances

Instances details
Functor OptDescr

Since: base-4.6.0.0

Instance details

Defined in System.Console.GetOpt

Methods

fmap :: (a -> b) -> OptDescr a -> OptDescr b #

(<$) :: a -> OptDescr b -> OptDescr a #

data ArgDescr a #

Describes whether an option takes an argument or not, and if so how the argument is injected into a value of type a.

Constructors

NoArg a

no argument expected

ReqArg (String -> a) String

option requires argument

OptArg (Maybe String -> a) String

optional argument

Instances

Instances details
Functor ArgDescr

Since: base-4.6.0.0

Instance details

Defined in System.Console.GetOpt

Methods

fmap :: (a -> b) -> ArgDescr a -> ArgDescr b #

(<$) :: a -> ArgDescr b -> ArgDescr a #

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.

Instances

Instances details
EmbPrj WarningMode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Generic WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Associated Types

type Rep WarningMode :: Type -> Type #

Show WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

NFData WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningMode -> () #

Eq WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode Source # 
Instance details

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

data ConfluenceCheck Source #

Instances

Instances details
EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Generic ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep ConfluenceCheck :: Type -> Type #

Show ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

NFData ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Methods

rnf :: ConfluenceCheck -> () #

Eq ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

type Rep ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Base" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data UnicodeOrAscii Source #

We want to know whether we are allowed to insert unicode characters or not.

Constructors

UnicodeOk 
AsciiOnly 

Instances

Instances details
EmbPrj UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Bounded UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Enum UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Generic UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Associated Types

type Rep UnicodeOrAscii :: Type -> Type #

Show UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

NFData UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

rnf :: UnicodeOrAscii -> () #

Eq UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

type Rep UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.6.2.1.20220320-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

checkOpts :: Flag CommandLineOptions Source #

Checks that the given options are consistent.

parsePragmaOptions Source #

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.

stripRTS :: [String] -> [String] Source #

Removes RTS options from a list of options.

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.

restartOptions :: [(PragmaOptions -> RestartCodomain, String)] Source #

If any these options have changed, then the file will be rechecked. Boolean options are negated to mention non-default options, where possible.

infectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

An infective option is an option that if used in one module, must be used in all modules that depend on this module.

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.

coinfectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

A coinfective option is an option that if used in one module, must be used in all modules that this module depends on.

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.

getOptSimple Source #

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 #

Instances

Instances details
HasOptions IM Source # 
Instance details

Defined in Agda.Interaction.Monad

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

HasOptions m => HasOptions (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasOptions m => HasOptions (BlockT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => HasOptions (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

HasOptions m => HasOptions (ListT m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (ChangeT m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (MaybeT m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (ExceptT e m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (IdentityT m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (ReaderT r m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

HasOptions m => HasOptions (StateT s m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions

(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source # 
Instance details

Defined in Agda.Interaction.Options.HasOptions