Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Interaction.Options

Contents

Lenses for PragmaOptions
Boolean accessors to PragmaOptions collapsing default
Non-boolean accessors to PragmaOptions

Synopsis

data CommandLineOptions = Options {
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
- optDefaultLibs :: Bool
- optUseLibs :: Bool
- optTraceImports :: Integer
- optTrustedExecutables :: Map ExeName FilePath
- optPrintAgdaDir :: Bool
- optPrintVersion :: Maybe PrintAgdaVersion
- 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
- optDiagnosticsColour :: DiagnosticsColours
}
data PragmaOptions = PragmaOptions {
- _optShowImplicit :: WithDefault 'False
- _optShowGeneralized :: WithDefault 'True
- _optShowIrrelevant :: WithDefault 'False
- _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
- _optVerbose :: !Verbosity
- _optProfiling :: ProfileOptions
- _optProp :: WithDefault 'False
- _optLevelUniverse :: WithDefault 'False
- _optTwoLevel :: WithDefault 'False
- _optAllowUnsolved :: WithDefault 'False
- _optAllowIncompleteMatch :: WithDefault 'False
- _optPositivityCheck :: WithDefault 'True
- _optTerminationCheck :: WithDefault 'True
- _optTerminationDepth :: CutOff
- _optUniverseCheck :: WithDefault 'True
- _optOmegaInOmega :: WithDefault 'False
- _optCumulativity :: WithDefault 'False
- _optSizedTypes :: WithDefault 'False
- _optGuardedness :: WithDefault 'False
- _optInjectiveTypeConstructors :: WithDefault 'False
- _optUniversePolymorphism :: WithDefault 'True
- _optIrrelevantProjections :: WithDefault 'False
- _optExperimentalIrrelevance :: WithDefault 'False
- _optWithoutK :: WithDefault 'False
- _optCubicalCompatible :: WithDefault 'False
- _optCopatterns :: WithDefault 'True
- _optPatternMatching :: WithDefault 'True
- _optExactSplit :: WithDefault 'False
- _optHiddenArgumentPuns :: WithDefault 'False
- _optEta :: WithDefault 'True
- _optForcing :: WithDefault 'True
- _optProjectionLike :: WithDefault 'True
- _optErasure :: WithDefault 'False
- _optErasedMatches :: WithDefault 'True
- _optEraseRecordParameters :: WithDefault 'False
- _optRewriting :: WithDefault 'False
- _optCubical :: Maybe Cubical
- _optGuarded :: WithDefault 'False
- _optFirstOrder :: WithDefault 'False
- _optPostfixProjections :: WithDefault 'False
- _optKeepPatternVariables :: WithDefault 'False
- _optInferAbsurdClauses :: WithDefault 'True
- _optInstanceSearchDepth :: Int
- _optOverlappingInstances :: WithDefault 'False
- _optQualifiedInstances :: WithDefault 'True
- _optInversionMaxDepth :: Int
- _optSafe :: WithDefault 'False
- _optDoubleCheck :: WithDefault 'False
- _optSyntacticEquality :: !(Maybe Int)
- _optWarningMode :: WarningMode
- _optCompileMain :: WithDefault 'True
- _optCaching :: WithDefault 'True
- _optCountClusters :: WithDefault 'False
- _optAutoInline :: WithDefault 'False
- _optPrintPatternSynonyms :: WithDefault 'True
- _optFastReduce :: WithDefault 'True
- _optCallByName :: WithDefault 'False
- _optConfluenceCheck :: Maybe ConfluenceCheck
- _optCohesion :: WithDefault 'False
- _optFlatSplit :: WithDefault 'False
- _optImportSorts :: WithDefault 'True
- _optLoadPrimitives :: WithDefault 'True
- _optAllowExec :: WithDefault 'False
- _optSaveMetas :: WithDefault 'False
- _optShowIdentitySubstitutions :: WithDefault 'False
- _optKeepCoveringClauses :: WithDefault 'False
- _optLargeIndices :: WithDefault 'False
- _optForcedArgumentRecursion :: WithDefault 'True
}
data OptionWarning = OptionRenamed {
- oldOptionName :: String
- newOptionName :: String
}
optionWarningName :: OptionWarning -> WarningName
type Flag opts = opts -> OptM opts
data OptM a
runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)
data OptDescr a = Option [Char] [String] (ArgDescr a) String
data ArgDescr a
- = NoArg a
- | ReqArg (String -> a) String
- | OptArg (Maybe String -> a) String
type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
type VerboseKey = String
type VerboseLevel = Int
data WarningMode = WarningMode {
- _warningSet :: Set WarningName
- _warn2Error :: Bool
}
data ConfluenceCheck
- = LocalConfluenceCheck
- | GlobalConfluenceCheck
data PrintAgdaVersion
- = PrintAgdaVersion
- | PrintAgdaNumericVersion
data UnicodeOrAscii
- = UnicodeOk
- | AsciiOnly
data DiagnosticsColours
- = AlwaysColour
- | NeverColour
- | AutoColour
checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions
parsePragmaOptions :: OptionsPragma -> 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 :: PragmaOptions -> [String]
recheckBecausePragmaOptionsChanged :: PragmaOptions -> PragmaOptions -> Bool
data InfectiveCoinfective
- = Infective
- | Coinfective
data InfectiveCoinfectiveOption = ICOption {
- icOptionActive :: PragmaOptions -> Bool
- icOptionDescription :: String
- icOptionKind :: InfectiveCoinfective
- icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
- icOptionWarning :: TopLevelModuleName -> Doc
}
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
lensOptShowImplicit :: Lens' PragmaOptions _
lensOptShowIrrelevant :: Lens' PragmaOptions _
lensOptUseUnicode :: Lens' PragmaOptions _
lensOptVerbose :: Lens' PragmaOptions _
lensOptProfiling :: Lens' PragmaOptions _
lensOptProp :: Lens' PragmaOptions _
lensOptLevelUniverse :: Lens' PragmaOptions _
lensOptTwoLevel :: Lens' PragmaOptions _
lensOptAllowUnsolved :: Lens' PragmaOptions _
lensOptAllowIncompleteMatch :: Lens' PragmaOptions _
lensOptPositivityCheck :: Lens' PragmaOptions _
lensOptTerminationCheck :: Lens' PragmaOptions _
lensOptTerminationDepth :: Lens' PragmaOptions _
lensOptUniverseCheck :: Lens' PragmaOptions _
lensOptNoUniverseCheck :: Lens' PragmaOptions _
lensOptOmegaInOmega :: Lens' PragmaOptions _
lensOptCumulativity :: Lens' PragmaOptions _
lensOptSizedTypes :: Lens' PragmaOptions _
lensOptGuardedness :: Lens' PragmaOptions _
lensOptInjectiveTypeConstructors :: Lens' PragmaOptions _
lensOptUniversePolymorphism :: Lens' PragmaOptions _
lensOptIrrelevantProjections :: Lens' PragmaOptions _
lensOptExperimentalIrrelevance :: Lens' PragmaOptions _
lensOptWithoutK :: Lens' PragmaOptions _
lensOptCubicalCompatible :: Lens' PragmaOptions _
lensOptCopatterns :: Lens' PragmaOptions _
lensOptPatternMatching :: Lens' PragmaOptions _
lensOptExactSplit :: Lens' PragmaOptions _
lensOptHiddenArgumentPuns :: Lens' PragmaOptions _
lensOptEta :: Lens' PragmaOptions _
lensOptForcing :: Lens' PragmaOptions _
lensOptProjectionLike :: Lens' PragmaOptions _
lensOptErasure :: Lens' PragmaOptions _
lensOptErasedMatches :: Lens' PragmaOptions _
lensOptEraseRecordParameters :: Lens' PragmaOptions _
lensOptRewriting :: Lens' PragmaOptions _
lensOptCubical :: Lens' PragmaOptions _
lensOptGuarded :: Lens' PragmaOptions _
lensOptFirstOrder :: Lens' PragmaOptions _
lensOptPostfixProjections :: Lens' PragmaOptions _
lensOptKeepPatternVariables :: Lens' PragmaOptions _
lensOptInferAbsurdClauses :: Lens' PragmaOptions _
lensOptInstanceSearchDepth :: Lens' PragmaOptions _
lensOptOverlappingInstances :: Lens' PragmaOptions _
lensOptQualifiedInstances :: Lens' PragmaOptions _
lensOptInversionMaxDepth :: Lens' PragmaOptions _
lensOptSafe :: Lens' PragmaOptions _
lensOptDoubleCheck :: Lens' PragmaOptions _
lensOptSyntacticEquality :: Lens' PragmaOptions _
lensOptWarningMode :: Lens' PragmaOptions _
lensOptCompileMain :: Lens' PragmaOptions _
lensOptCaching :: Lens' PragmaOptions _
lensOptCountClusters :: Lens' PragmaOptions _
lensOptAutoInline :: Lens' PragmaOptions _
lensOptPrintPatternSynonyms :: Lens' PragmaOptions _
lensOptFastReduce :: Lens' PragmaOptions _
lensOptCallByName :: Lens' PragmaOptions _
lensOptConfluenceCheck :: Lens' PragmaOptions _
lensOptCohesion :: Lens' PragmaOptions _
lensOptFlatSplit :: Lens' PragmaOptions _
lensOptImportSorts :: Lens' PragmaOptions _
lensOptLoadPrimitives :: Lens' PragmaOptions _
lensOptAllowExec :: Lens' PragmaOptions _
lensOptSaveMetas :: Lens' PragmaOptions _
lensOptShowIdentitySubstitutions :: Lens' PragmaOptions _
lensOptKeepCoveringClauses :: Lens' PragmaOptions _
optShowImplicit :: PragmaOptions -> Bool
optShowGeneralized :: PragmaOptions -> Bool
optShowIrrelevant :: PragmaOptions -> Bool
optProp :: PragmaOptions -> Bool
optLevelUniverse :: PragmaOptions -> Bool
optTwoLevel :: PragmaOptions -> Bool
optAllowUnsolved :: PragmaOptions -> Bool
optAllowIncompleteMatch :: PragmaOptions -> Bool
optPositivityCheck :: PragmaOptions -> Bool
optTerminationCheck :: PragmaOptions -> Bool
optUniverseCheck :: PragmaOptions -> Bool
optOmegaInOmega :: PragmaOptions -> Bool
optCumulativity :: PragmaOptions -> Bool
optSizedTypes :: PragmaOptions -> Bool
optGuardedness :: PragmaOptions -> Bool
optInjectiveTypeConstructors :: PragmaOptions -> Bool
optUniversePolymorphism :: PragmaOptions -> Bool
optIrrelevantProjections :: PragmaOptions -> Bool
optExperimentalIrrelevance :: PragmaOptions -> Bool
optWithoutK :: PragmaOptions -> Bool
optCubicalCompatible :: PragmaOptions -> Bool
optCopatterns :: PragmaOptions -> Bool
optPatternMatching :: PragmaOptions -> Bool
optHiddenArgumentPuns :: PragmaOptions -> Bool
optEta :: PragmaOptions -> Bool
optForcing :: PragmaOptions -> Bool
optProjectionLike :: PragmaOptions -> Bool
optErasure :: PragmaOptions -> Bool
optErasedMatches :: PragmaOptions -> Bool
optEraseRecordParameters :: PragmaOptions -> Bool
optRewriting :: PragmaOptions -> Bool
optGuarded :: PragmaOptions -> Bool
optFirstOrder :: PragmaOptions -> Bool
optPostfixProjections :: PragmaOptions -> Bool
optKeepPatternVariables :: PragmaOptions -> Bool
optInferAbsurdClauses :: PragmaOptions -> Bool
optOverlappingInstances :: PragmaOptions -> Bool
optQualifiedInstances :: PragmaOptions -> Bool
optSafe :: PragmaOptions -> Bool
optDoubleCheck :: PragmaOptions -> Bool
optCompileNoMain :: PragmaOptions -> Bool
optCaching :: PragmaOptions -> Bool
optCountClusters :: PragmaOptions -> Bool
optAutoInline :: PragmaOptions -> Bool
optPrintPatternSynonyms :: PragmaOptions -> Bool
optFastReduce :: PragmaOptions -> Bool
optCallByName :: PragmaOptions -> Bool
optCohesion :: PragmaOptions -> Bool
optFlatSplit :: PragmaOptions -> Bool
optImportSorts :: PragmaOptions -> Bool
optLoadPrimitives :: PragmaOptions -> Bool
optAllowExec :: PragmaOptions -> Bool
optSaveMetas :: PragmaOptions -> Bool
optShowIdentitySubstitutions :: PragmaOptions -> Bool
optKeepCoveringClauses :: PragmaOptions -> Bool
optLargeIndices :: PragmaOptions -> Bool
optForcedArgumentRecursion :: PragmaOptions -> Bool
optConfluenceCheck :: PragmaOptions -> _
optCubical :: PragmaOptions -> _
optInstanceSearchDepth :: PragmaOptions -> _
optInversionMaxDepth :: PragmaOptions -> _
optProfiling :: PragmaOptions -> _
optSyntacticEquality :: PragmaOptions -> _
optTerminationDepth :: PragmaOptions -> _
optUseUnicode :: PragmaOptions -> UnicodeOrAscii
optVerbose :: PragmaOptions -> _
optWarningMode :: PragmaOptions -> _
class (Functor m, Applicative m, Monad m) => HasOptions m where
- pragmaOptions :: m PragmaOptions
- commandLineOptions :: m CommandLineOptions

Documentation

data CommandLineOptions Source #

Constructors

Options

Fields

optProgramName :: String
optInputFile :: Maybe FilePath
optIncludePaths :: [FilePath]
optAbsoluteIncludePaths :: [AbsolutePath]
The list should not contain duplicates.
optLibraries :: [LibName]
optOverrideLibrariesFile :: Maybe FilePath
Use this (if Just) instead of ~/.agda/libraries.
optDefaultLibs :: Bool
Use ~/.agda/defaults.
optUseLibs :: Bool
look for .agda-lib files.
optTraceImports :: Integer
Configure notifications about imported modules.
optTrustedExecutables :: Map ExeName FilePath
Map names of trusted executables to absolute paths.
optPrintAgdaDir :: Bool
optPrintVersion :: Maybe PrintAgdaVersion
optPrintHelp :: Maybe Help
optInteractive :: Bool
Agda REPL (-I).
optGHCiInteraction :: Bool
optJSONInteraction :: Bool
optExitOnError :: !Bool
Exit if an interactive command fails.
optCompileDir :: Maybe FilePath
In the absence of a path the project root is used.
optGenerateVimFile :: Bool
optIgnoreInterfaces :: Bool
optIgnoreAllInterfaces :: Bool
optLocalInterfaces :: Bool
optPragmaOptions :: PragmaOptions
optOnlyScopeChecking :: Bool
Should the top-level module only be scope-checked, and not type-checked?
optTransliterate :: Bool
Should code points that are not supported by the locale be transliterated?
optDiagnosticsColour :: DiagnosticsColours
Configure colour output.

Instances

Instances details

LensIncludePaths CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getIncludePaths :: CommandLineOptions -> [FilePath] Source # setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions Source # mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions Source # getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source # setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions Source # mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions Source #
LensPersistentVerbosity CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensPragmaOptions CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions Source #
LensSafeMode CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
Generic CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep CommandLineOptions :: Type -> Type Methods from :: CommandLineOptions -> Rep CommandLineOptions x to :: Rep CommandLineOptions x -> CommandLineOptions
Show CommandLineOptions Source #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> CommandLineOptions -> ShowS show :: CommandLineOptions -> String showList :: [CommandLineOptions] -> ShowS
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.4-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 "optTraceImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer))) :: ((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 (Maybe PrintAgdaVersion)) :: 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 "optExitOnError") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (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)) :: (S1 ('MetaSel ('Just "optTransliterate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDiagnosticsColour") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DiagnosticsColours)))))))

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions

Fields

_optShowImplicit :: WithDefault 'False
_optShowGeneralized :: WithDefault 'True
Show generalized parameters in Pi types
_optShowIrrelevant :: WithDefault 'False
_optUseUnicode :: WithDefault' UnicodeOrAscii 'True
_optVerbose :: !Verbosity
_optProfiling :: ProfileOptions
_optProp :: WithDefault 'False
_optLevelUniverse :: WithDefault 'False
_optTwoLevel :: WithDefault 'False
_optAllowUnsolved :: WithDefault 'False
_optAllowIncompleteMatch :: WithDefault 'False
_optPositivityCheck :: WithDefault 'True
_optTerminationCheck :: WithDefault 'True
_optTerminationDepth :: CutOff
Cut off structural order comparison at some depth in termination checker?
_optUniverseCheck :: WithDefault 'True
_optOmegaInOmega :: WithDefault 'False
_optCumulativity :: WithDefault 'False
_optSizedTypes :: WithDefault 'False
_optGuardedness :: WithDefault 'False
_optInjectiveTypeConstructors :: WithDefault 'False
_optUniversePolymorphism :: WithDefault 'True
_optIrrelevantProjections :: WithDefault 'False
_optExperimentalIrrelevance :: WithDefault 'False
irrelevant levels, irrelevant data matching
_optWithoutK :: WithDefault 'False
_optCubicalCompatible :: WithDefault 'False
_optCopatterns :: WithDefault 'True
Allow definitions by copattern matching?
_optPatternMatching :: WithDefault 'True
Is pattern matching allowed in the current file?
_optExactSplit :: WithDefault 'False
_optHiddenArgumentPuns :: WithDefault 'False
Should patterns of the form {x} or ⦃ x ⦄ be interpreted as puns?
_optEta :: WithDefault 'True
_optForcing :: WithDefault 'True
Perform the forcing analysis on data constructors?
_optProjectionLike :: WithDefault 'True
Perform the projection-likeness analysis on functions?
_optErasure :: WithDefault 'False
_optErasedMatches :: WithDefault 'True
Allow matching in erased positions for single-constructor, non-indexed data/record types. (This kind of matching is always allowed for record types with η-equality.)
_optEraseRecordParameters :: WithDefault 'False
Mark parameters of record modules as erased?
_optRewriting :: WithDefault 'False
Can rewrite rules be added and used?
_optCubical :: Maybe Cubical
_optGuarded :: WithDefault 'False
_optFirstOrder :: WithDefault 'False
Should we speculatively unify function applications as if they were injective?
_optPostfixProjections :: WithDefault 'False
Should system generated projections ProjSystem be printed postfix (True) or prefix (False).
_optKeepPatternVariables :: WithDefault 'False
Should case splitting replace variables with dot patterns (False) or keep them as variables (True).
_optInferAbsurdClauses :: WithDefault 'True
Should case splitting and coverage checking try to discharge absurd clauses? Default: True, but False might make coverage checking considerably faster in some cases.
_optInstanceSearchDepth :: Int
_optOverlappingInstances :: WithDefault 'False
_optQualifiedInstances :: WithDefault 'True
Should instance search consider instances with qualified names?
_optInversionMaxDepth :: Int
_optSafe :: WithDefault 'False
_optDoubleCheck :: WithDefault 'False
_optSyntacticEquality :: !(Maybe Int)
Should the conversion checker use the syntactic equality shortcut? Nothing means that it should. Just n, for a non-negative number n, means that syntactic equality checking gets n units of fuel. If the fuel becomes zero, then syntactic equality checking is turned off. The fuel counter is decreased in the failure continuation of checkSyntacticEquality.
_optWarningMode :: WarningMode
_optCompileMain :: WithDefault 'True
Treat the module given at the command line or via interaction as main module in compilation?
_optCaching :: WithDefault 'True
_optCountClusters :: WithDefault 'False
Count extended grapheme clusters rather than code points when generating LaTeX.
_optAutoInline :: WithDefault 'False
Automatic compile-time inlining for simple definitions (unless marked NOINLINE).
_optPrintPatternSynonyms :: WithDefault 'True
_optFastReduce :: WithDefault 'True
Use the Agda abstract machine (fastReduce)?
_optCallByName :: WithDefault 'False
Use call-by-name instead of call-by-need.
_optConfluenceCheck :: Maybe ConfluenceCheck
Check confluence of rewrite rules?
_optCohesion :: WithDefault 'False
Are the cohesion modalities available?
_optFlatSplit :: WithDefault 'False
Can we split on a (@flat x : A) argument?
_optImportSorts :: WithDefault 'True
Should every top-level module start with an implicit statement open import Agda.Primitive using (Set; Prop)?
_optLoadPrimitives :: WithDefault 'True
Should we load the primitive modules at all? This is a stronger form of optImportSorts.
_optAllowExec :: WithDefault 'False
Allow running external executables from meta programs.
_optSaveMetas :: WithDefault 'False
Save meta-variables to interface files.
_optShowIdentitySubstitutions :: WithDefault 'False
Show identity substitutions when pretty-printing terms (i.e. always show all arguments of a metavariable).
_optKeepCoveringClauses :: WithDefault 'False
Do not discard clauses constructed by the coverage checker (needed for some external backends).
_optLargeIndices :: WithDefault 'False
Allow large indices, and large forced arguments in constructors.
_optForcedArgumentRecursion :: WithDefault 'True
Allow recursion on forced constructor arguments.

Instances

Instances details

LensPersistentVerbosity PragmaOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode PragmaOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensVerbosity PragmaOptions Source #
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #
EmbPrj PragmaOptions Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Int32 Source # icod_ :: PragmaOptions -> S Int32 Source # value :: Int32 -> R PragmaOptions Source #
Generic PragmaOptions Source #
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep PragmaOptions :: Type -> Type Methods from :: PragmaOptions -> Rep PragmaOptions x to :: Rep PragmaOptions x -> PragmaOptions
Show PragmaOptions Source #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> PragmaOptions -> ShowS show :: PragmaOptions -> String showList :: [PragmaOptions] -> ShowS
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 Methods (==) :: PragmaOptions -> PragmaOptions -> Bool (/=) :: PragmaOptions -> PragmaOptions -> Bool
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.4-inplace" 'False) (C1 ('MetaCons "PragmaOptions" 'PrefixI 'True) ((((((S1 ('MetaSel ('Just "_optShowImplicit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optShowGeneralized") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :: (S1 ('MetaSel ('Just "_optShowIrrelevant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optUseUnicode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault' UnicodeOrAscii 'True)))) :: ((S1 ('MetaSel ('Just "_optVerbose") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Verbosity) :: S1 ('MetaSel ('Just "_optProfiling") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProfileOptions)) :: (S1 ('MetaSel ('Just "_optProp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optLevelUniverse") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :: (((S1 ('MetaSel ('Just "_optTwoLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optAllowUnsolved") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optAllowIncompleteMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optPositivityCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :: ((S1 ('MetaSel ('Just "_optTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optTerminationDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CutOff)) :: (S1 ('MetaSel ('Just "_optUniverseCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: (S1 ('MetaSel ('Just "_optOmegaInOmega") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optCumulativity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))))) :: ((((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 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optUniversePolymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :: ((S1 ('MetaSel ('Just "_optIrrelevantProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optExperimentalIrrelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optWithoutK") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optCubicalCompatible") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :: (((S1 ('MetaSel ('Just "_optCopatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optPatternMatching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :: (S1 ('MetaSel ('Just "_optExactSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optHiddenArgumentPuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :: ((S1 ('MetaSel ('Just "_optEta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optForcing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :: (S1 ('MetaSel ('Just "_optProjectionLike") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: (S1 ('MetaSel ('Just "_optErasure") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optErasedMatches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))))))) :: (((((S1 ('MetaSel ('Just "_optEraseRecordParameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optRewriting") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optCubical") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Cubical)) :: S1 ('MetaSel ('Just "_optGuarded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :: ((S1 ('MetaSel ('Just "_optFirstOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optPostfixProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optKeepPatternVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optInferAbsurdClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))))) :: (((S1 ('MetaSel ('Just "_optInstanceSearchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "_optOverlappingInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optQualifiedInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optInversionMaxDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :: ((S1 ('MetaSel ('Just "_optSafe") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optDoubleCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optSyntacticEquality") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Int)) :: (S1 ('MetaSel ('Just "_optWarningMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningMode) :: S1 ('MetaSel ('Just "_optCompileMain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))))))) :: ((((S1 ('MetaSel ('Just "_optCaching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optCountClusters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optAutoInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optPrintPatternSynonyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)))) :: ((S1 ('MetaSel ('Just "_optFastReduce") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optCallByName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optConfluenceCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ConfluenceCheck)) :: S1 ('MetaSel ('Just "_optCohesion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :: (((S1 ('MetaSel ('Just "_optFlatSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optImportSorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))) :: (S1 ('MetaSel ('Just "_optLoadPrimitives") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True)) :: S1 ('MetaSel ('Just "_optAllowExec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :: ((S1 ('MetaSel ('Just "_optSaveMetas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: S1 ('MetaSel ('Just "_optShowIdentitySubstitutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))) :: (S1 ('MetaSel ('Just "_optKeepCoveringClauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :: (S1 ('MetaSel ('Just "_optLargeIndices") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "_optForcedArgumentRecursion") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'True))))))))))

data OptionWarning Source #

Warnings when parsing options.

Constructors

OptionRenamed
Fields oldOptionName :: String newOptionName :: String

Instances

Instances details

Pretty OptionWarning Source #
Instance details Defined in Agda.Interaction.Options.Base Methods pretty :: OptionWarning -> Doc Source # prettyPrec :: Int -> OptionWarning -> Doc Source # prettyList :: [OptionWarning] -> Doc Source #
EmbPrj OptionWarning Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: OptionWarning -> S Int32 Source # icod_ :: OptionWarning -> S Int32 Source # value :: Int32 -> R OptionWarning Source #
Generic OptionWarning Source #
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep OptionWarning :: Type -> Type Methods from :: OptionWarning -> Rep OptionWarning x to :: Rep OptionWarning x -> OptionWarning
Show OptionWarning Source #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> OptionWarning -> ShowS show :: OptionWarning -> String showList :: [OptionWarning] -> ShowS
NFData OptionWarning Source #
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: OptionWarning -> ()
type Rep OptionWarning Source #
Instance details Defined in Agda.Interaction.Options.Base type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "OptionRenamed" 'PrefixI 'True) (S1 ('MetaSel ('Just "oldOptionName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "newOptionName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

optionWarningName :: OptionWarning -> WarningName Source #

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

data OptM a Source #

The options parse monad OptM collects warnings that are not discarded when a fatal error occurrs

Instances

Instances details

Applicative OptM Source #
Instance details Defined in Agda.Interaction.Options.Base Methods pure :: a -> OptM a (<>) :: OptM (a -> b) -> OptM a -> OptM b # liftA2 :: (a -> b -> c) -> OptM a -> OptM b -> OptM c (>) :: OptM a -> OptM b -> OptM b (<*) :: OptM a -> OptM b -> OptM a
Functor OptM Source #
Instance details Defined in Agda.Interaction.Options.Base Methods fmap :: (a -> b) -> OptM a -> OptM b (<$) :: a -> OptM b -> OptM a #
Monad OptM Source #
Instance details Defined in Agda.Interaction.Options.Base Methods (>>=) :: OptM a -> (a -> OptM b) -> OptM b (>>) :: OptM a -> OptM b -> OptM b return :: a -> OptM a

runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings) Source #

data OptDescr a #

Constructors

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

Instances

Instances details

Functor OptDescr
Instance details Defined in System.Console.GetOpt Methods fmap :: (a -> b) -> OptDescr a -> OptDescr b (<$) :: a -> OptDescr b -> OptDescr a #

data ArgDescr a #

Constructors

NoArg a
ReqArg (String -> a) String
OptArg (Maybe String -> a) String

Instances

Instances details

Functor ArgDescr
Instance details Defined in System.Console.GetOpt Methods fmap :: (a -> b) -> ArgDescr a -> ArgDescr b (<$) :: a -> ArgDescr b -> ArgDescr 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 _warningSet :: Set WarningName _warn2Error :: Bool

Instances

Instances details

EmbPrj WarningMode Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source #
Generic WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Associated Types type Rep WarningMode :: Type -> Type Methods from :: WarningMode -> Rep WarningMode x to :: Rep WarningMode x -> WarningMode
Show WarningMode Source #
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS show :: WarningMode -> String showList :: [WarningMode] -> ShowS
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 Methods (==) :: WarningMode -> WarningMode -> Bool (/=) :: WarningMode -> WarningMode -> Bool
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.4-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 #

Constructors

LocalConfluenceCheck
GlobalConfluenceCheck

Instances

Instances details

EmbPrj ConfluenceCheck Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Int32 Source # icod_ :: ConfluenceCheck -> S Int32 Source # value :: Int32 -> R ConfluenceCheck Source #
Generic ConfluenceCheck Source #
Instance details 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 #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> ConfluenceCheck -> ShowS show :: ConfluenceCheck -> String showList :: [ConfluenceCheck] -> ShowS
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 Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool
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.4-inplace" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data PrintAgdaVersion Source #

Options --version and --numeric-version (last wins).

Constructors

PrintAgdaVersion	Print Agda version information and exit.
PrintAgdaNumericVersion	Print Agda version number and exit.

Instances

Instances details

Generic PrintAgdaVersion Source #
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep PrintAgdaVersion :: Type -> Type Methods from :: PrintAgdaVersion -> Rep PrintAgdaVersion x to :: Rep PrintAgdaVersion x -> PrintAgdaVersion
Show PrintAgdaVersion Source #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> PrintAgdaVersion -> ShowS show :: PrintAgdaVersion -> String showList :: [PrintAgdaVersion] -> ShowS
NFData PrintAgdaVersion Source #
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: PrintAgdaVersion -> ()
type Rep PrintAgdaVersion Source #
Instance details Defined in Agda.Interaction.Options.Base type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Base" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

data UnicodeOrAscii Source #

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

Constructors

UnicodeOk	`true`: Unicode characters are allowed.
AsciiOnly	'false: Stick to ASCII.

Instances

Instances details

EmbPrj UnicodeOrAscii Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: UnicodeOrAscii -> S Int32 Source # icod_ :: UnicodeOrAscii -> S Int32 Source # value :: Int32 -> R UnicodeOrAscii Source #
Boolean UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods fromBool :: Bool -> UnicodeOrAscii Source # true :: UnicodeOrAscii Source # false :: UnicodeOrAscii Source # not :: UnicodeOrAscii -> UnicodeOrAscii Source # (&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source # (\|\|) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source # implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source # butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #
IsBool UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods toBool :: UnicodeOrAscii -> Bool Source # ifThenElse :: UnicodeOrAscii -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii Source # fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #
Bounded UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods minBound :: UnicodeOrAscii maxBound :: UnicodeOrAscii
Enum UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods succ :: UnicodeOrAscii -> UnicodeOrAscii pred :: UnicodeOrAscii -> UnicodeOrAscii toEnum :: Int -> UnicodeOrAscii fromEnum :: UnicodeOrAscii -> Int enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] enumFromThenTo :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii]
Generic UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Associated Types type Rep UnicodeOrAscii :: Type -> Type Methods from :: UnicodeOrAscii -> Rep UnicodeOrAscii x to :: Rep UnicodeOrAscii x -> UnicodeOrAscii
Show UnicodeOrAscii Source #
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods showsPrec :: Int -> UnicodeOrAscii -> ShowS show :: UnicodeOrAscii -> String showList :: [UnicodeOrAscii] -> ShowS
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 Methods (==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool (/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool
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.4-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

data DiagnosticsColours Source #

Constructors

AlwaysColour
NeverColour
AutoColour

Instances

Instances details

Generic DiagnosticsColours Source #
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep DiagnosticsColours :: Type -> Type Methods from :: DiagnosticsColours -> Rep DiagnosticsColours x to :: Rep DiagnosticsColours x -> DiagnosticsColours
Show DiagnosticsColours Source #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> DiagnosticsColours -> ShowS show :: DiagnosticsColours -> String showList :: [DiagnosticsColours] -> ShowS
NFData DiagnosticsColours Source #
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: DiagnosticsColours -> ()
type Rep DiagnosticsColours Source #
Instance details Defined in Agda.Interaction.Options.Base type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Base" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "AlwaysColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NeverColour" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AutoColour" 'PrefixI 'False) (U1 :: Type -> Type)))

checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions Source #

Checks that the given options are consistent. Also makes adjustments (e.g. when one option implies another).

parsePragmaOptions Source #

Arguments

:: OptionsPragma	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 #

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

Removes RTS options from a list of options.

defaultOptions :: CommandLineOptions Source #

defaultInteractionOptions :: PragmaOptions Source #

defaultCutOff :: CutOff Source #

The default termination depth.

defaultPragmaOptions :: PragmaOptions Source #

standardOptions_ :: [OptDescr ()] Source #

Used for printing usage info. Does not include the dead options.

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

Instances details

EmbPrj InfectiveCoinfective Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: InfectiveCoinfective -> S Int32 Source # icod_ :: InfectiveCoinfective -> S Int32 Source # value :: Int32 -> R InfectiveCoinfective Source #
Generic InfectiveCoinfective Source #
Instance details 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 #
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> InfectiveCoinfective -> ShowS show :: InfectiveCoinfective -> String showList :: [InfectiveCoinfective] -> ShowS
NFData InfectiveCoinfective Source #
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: InfectiveCoinfective -> ()
Eq InfectiveCoinfective Source #
Instance details Defined in Agda.Interaction.Options.Base Methods (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
type Rep InfectiveCoinfective Source #
Instance details Defined in Agda.Interaction.Options.Base type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Base" "Agda-2.6.4-inplace" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

data InfectiveCoinfectiveOption Source #

Descriptions of infective and coinfective options.

Constructors

ICOption

Fields

icOptionActive :: PragmaOptions -> Bool
Is the option active?
icOptionDescription :: String
A description of the option (typically a flag that activates the option).
icOptionKind :: InfectiveCoinfective
Is the option (roughly speaking) infective or coinfective?
icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
This function returns True exactly when, from the perspective of the option in question, the options in the current module (the first argument) are compatible with the options in a given imported module (the second argument).
icOptionWarning :: TopLevelModuleName -> Doc
A warning message that should be used if this option is not used correctly. The given module name is the name of an imported module for which icOptionOK failed.

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.

safeFlag :: Flag PragmaOptions Source #

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

inputFlag :: FilePath -> Flag CommandLineOptions Source #

standardOptions :: [OptDescr (Flag CommandLineOptions)] Source #

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)

Lenses for `PragmaOptions`

lensOptShowImplicit :: Lens' PragmaOptions _ Source #

lensOptShowIrrelevant :: Lens' PragmaOptions _ Source #

lensOptUseUnicode :: Lens' PragmaOptions _ Source #

lensOptVerbose :: Lens' PragmaOptions _ Source #

lensOptProfiling :: Lens' PragmaOptions _ Source #

lensOptProp :: Lens' PragmaOptions _ Source #

lensOptLevelUniverse :: Lens' PragmaOptions _ Source #

lensOptTwoLevel :: Lens' PragmaOptions _ Source #

lensOptAllowUnsolved :: Lens' PragmaOptions _ Source #

lensOptAllowIncompleteMatch :: Lens' PragmaOptions _ Source #

lensOptPositivityCheck :: Lens' PragmaOptions _ Source #

lensOptTerminationCheck :: Lens' PragmaOptions _ Source #

lensOptTerminationDepth :: Lens' PragmaOptions _ Source #

lensOptUniverseCheck :: Lens' PragmaOptions _ Source #

lensOptNoUniverseCheck :: Lens' PragmaOptions _ Source #

lensOptOmegaInOmega :: Lens' PragmaOptions _ Source #

lensOptCumulativity :: Lens' PragmaOptions _ Source #

lensOptSizedTypes :: Lens' PragmaOptions _ Source #

lensOptGuardedness :: Lens' PragmaOptions _ Source #

lensOptInjectiveTypeConstructors :: Lens' PragmaOptions _ Source #

lensOptUniversePolymorphism :: Lens' PragmaOptions _ Source #

lensOptIrrelevantProjections :: Lens' PragmaOptions _ Source #

lensOptExperimentalIrrelevance :: Lens' PragmaOptions _ Source #

lensOptWithoutK :: Lens' PragmaOptions _ Source #

lensOptCubicalCompatible :: Lens' PragmaOptions _ Source #

lensOptCopatterns :: Lens' PragmaOptions _ Source #

lensOptPatternMatching :: Lens' PragmaOptions _ Source #

lensOptExactSplit :: Lens' PragmaOptions _ Source #

lensOptHiddenArgumentPuns :: Lens' PragmaOptions _ Source #

lensOptEta :: Lens' PragmaOptions _ Source #

lensOptForcing :: Lens' PragmaOptions _ Source #

lensOptProjectionLike :: Lens' PragmaOptions _ Source #

lensOptErasure :: Lens' PragmaOptions _ Source #

lensOptErasedMatches :: Lens' PragmaOptions _ Source #

lensOptEraseRecordParameters :: Lens' PragmaOptions _ Source #

lensOptRewriting :: Lens' PragmaOptions _ Source #

lensOptCubical :: Lens' PragmaOptions _ Source #

lensOptGuarded :: Lens' PragmaOptions _ Source #

lensOptFirstOrder :: Lens' PragmaOptions _ Source #

lensOptPostfixProjections :: Lens' PragmaOptions _ Source #

lensOptKeepPatternVariables :: Lens' PragmaOptions _ Source #

lensOptInferAbsurdClauses :: Lens' PragmaOptions _ Source #

lensOptInstanceSearchDepth :: Lens' PragmaOptions _ Source #

lensOptOverlappingInstances :: Lens' PragmaOptions _ Source #

lensOptQualifiedInstances :: Lens' PragmaOptions _ Source #

lensOptInversionMaxDepth :: Lens' PragmaOptions _ Source #

lensOptSafe :: Lens' PragmaOptions _ Source #

lensOptDoubleCheck :: Lens' PragmaOptions _ Source #

lensOptSyntacticEquality :: Lens' PragmaOptions _ Source #

lensOptWarningMode :: Lens' PragmaOptions _ Source #

lensOptCompileMain :: Lens' PragmaOptions _ Source #

lensOptCaching :: Lens' PragmaOptions _ Source #

lensOptCountClusters :: Lens' PragmaOptions _ Source #

lensOptAutoInline :: Lens' PragmaOptions _ Source #

lensOptPrintPatternSynonyms :: Lens' PragmaOptions _ Source #

lensOptFastReduce :: Lens' PragmaOptions _ Source #

lensOptCallByName :: Lens' PragmaOptions _ Source #

lensOptConfluenceCheck :: Lens' PragmaOptions _ Source #

lensOptCohesion :: Lens' PragmaOptions _ Source #

lensOptFlatSplit :: Lens' PragmaOptions _ Source #

lensOptImportSorts :: Lens' PragmaOptions _ Source #

lensOptLoadPrimitives :: Lens' PragmaOptions _ Source #

lensOptAllowExec :: Lens' PragmaOptions _ Source #

lensOptSaveMetas :: Lens' PragmaOptions _ Source #

lensOptShowIdentitySubstitutions :: Lens' PragmaOptions _ Source #

lensOptKeepCoveringClauses :: Lens' PragmaOptions _ Source #

Boolean accessors to `PragmaOptions` collapsing default

optShowImplicit :: PragmaOptions -> Bool Source #

optShowGeneralized :: PragmaOptions -> Bool Source #

optShowIrrelevant :: PragmaOptions -> Bool Source #

optProp :: PragmaOptions -> Bool Source #

optLevelUniverse :: PragmaOptions -> Bool Source #

optTwoLevel :: PragmaOptions -> Bool Source #

optAllowUnsolved :: PragmaOptions -> Bool Source #

optAllowIncompleteMatch :: PragmaOptions -> Bool Source #

optPositivityCheck :: PragmaOptions -> Bool Source #

optTerminationCheck :: PragmaOptions -> Bool Source #

optUniverseCheck :: PragmaOptions -> Bool Source #

optOmegaInOmega :: PragmaOptions -> Bool Source #

optCumulativity :: PragmaOptions -> Bool Source #

optSizedTypes :: PragmaOptions -> Bool Source #

optGuardedness :: PragmaOptions -> Bool Source #

optInjectiveTypeConstructors :: PragmaOptions -> Bool Source #

optUniversePolymorphism :: PragmaOptions -> Bool Source #

optIrrelevantProjections :: PragmaOptions -> Bool Source #

optExperimentalIrrelevance :: PragmaOptions -> Bool Source #

optWithoutK :: PragmaOptions -> Bool Source #

optCubicalCompatible :: PragmaOptions -> Bool Source #

optCopatterns :: PragmaOptions -> Bool Source #

optPatternMatching :: PragmaOptions -> Bool Source #

optHiddenArgumentPuns :: PragmaOptions -> Bool Source #

optEta :: PragmaOptions -> Bool Source #

optForcing :: PragmaOptions -> Bool Source #

optProjectionLike :: PragmaOptions -> Bool Source #

optErasure :: PragmaOptions -> Bool Source #

optErasure is implied by optEraseRecordParameters. optErasure is also implied by an explicitly given `--erased-matches`.

optErasedMatches :: PragmaOptions -> Bool Source #

optEraseRecordParameters :: PragmaOptions -> Bool Source #

optRewriting :: PragmaOptions -> Bool Source #

optGuarded :: PragmaOptions -> Bool Source #

optFirstOrder :: PragmaOptions -> Bool Source #

optPostfixProjections :: PragmaOptions -> Bool Source #

optKeepPatternVariables :: PragmaOptions -> Bool Source #

optInferAbsurdClauses :: PragmaOptions -> Bool Source #

optOverlappingInstances :: PragmaOptions -> Bool Source #

optQualifiedInstances :: PragmaOptions -> Bool Source #

optSafe :: PragmaOptions -> Bool Source #

optDoubleCheck :: PragmaOptions -> Bool Source #

optCompileNoMain :: PragmaOptions -> Bool Source #

optCaching :: PragmaOptions -> Bool Source #

optCountClusters :: PragmaOptions -> Bool Source #

optAutoInline :: PragmaOptions -> Bool Source #

optPrintPatternSynonyms :: PragmaOptions -> Bool Source #

optFastReduce :: PragmaOptions -> Bool Source #

optCallByName :: PragmaOptions -> Bool Source #

optCohesion :: PragmaOptions -> Bool Source #

optCohesion is implied by optFlatSplit.

optFlatSplit :: PragmaOptions -> Bool Source #

optImportSorts :: PragmaOptions -> Bool Source #

optImportSorts requires optLoadPrimitives.

optLoadPrimitives :: PragmaOptions -> Bool Source #

optAllowExec :: PragmaOptions -> Bool Source #

optSaveMetas :: PragmaOptions -> Bool Source #

optShowIdentitySubstitutions :: PragmaOptions -> Bool Source #

optKeepCoveringClauses :: PragmaOptions -> Bool Source #

optLargeIndices :: PragmaOptions -> Bool Source #

optForcedArgumentRecursion :: PragmaOptions -> Bool Source #

Non-boolean accessors to `PragmaOptions`

optConfluenceCheck :: PragmaOptions -> _ Source #

optCubical :: PragmaOptions -> _ Source #

optInstanceSearchDepth :: PragmaOptions -> _ Source #

optInversionMaxDepth :: PragmaOptions -> _ Source #

optProfiling :: PragmaOptions -> _ Source #

optSyntacticEquality :: PragmaOptions -> _ Source #

optTerminationDepth :: PragmaOptions -> _ Source #

optUseUnicode :: PragmaOptions -> UnicodeOrAscii Source #

optVerbose :: PragmaOptions -> _ Source #

optWarningMode :: PragmaOptions -> _ Source #

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 Methods pragmaOptions :: IM PragmaOptions Source # commandLineOptions :: IM CommandLineOptions Source #
HasOptions AbsToCon Source #
Instance details Defined in Agda.Syntax.Translation.AbstractToConcrete Methods pragmaOptions :: AbsToCon PragmaOptions Source # commandLineOptions :: AbsToCon CommandLineOptions Source #
HasOptions TerM Source #
Instance details Defined in Agda.Termination.Monad Methods pragmaOptions :: TerM PragmaOptions Source # commandLineOptions :: TerM CommandLineOptions Source #
HasOptions ReduceM Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ReduceM PragmaOptions Source # commandLineOptions :: ReduceM CommandLineOptions Source #
HasOptions NLM Source #
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods pragmaOptions :: NLM PragmaOptions Source # commandLineOptions :: NLM CommandLineOptions Source #
HasOptions m => HasOptions (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods pragmaOptions :: PureConversionT m PragmaOptions Source # commandLineOptions :: PureConversionT m CommandLineOptions Source #
HasOptions m => HasOptions (BlockT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: BlockT m PragmaOptions Source # commandLineOptions :: BlockT m CommandLineOptions Source #
MonadIO m => HasOptions (TCMT m) Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: TCMT m PragmaOptions Source # commandLineOptions :: TCMT m CommandLineOptions Source #
HasOptions m => HasOptions (NamesT m) Source #
Instance details Defined in Agda.TypeChecking.Names Methods pragmaOptions :: NamesT m PragmaOptions Source # commandLineOptions :: NamesT m CommandLineOptions Source #
HasOptions m => HasOptions (ListT m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ListT m PragmaOptions Source # commandLineOptions :: ListT m CommandLineOptions Source #
HasOptions m => HasOptions (ChangeT m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ChangeT m PragmaOptions Source # commandLineOptions :: ChangeT m CommandLineOptions Source #
HasOptions m => HasOptions (MaybeT m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: MaybeT m PragmaOptions Source # commandLineOptions :: MaybeT m CommandLineOptions Source #
HasOptions m => HasOptions (ExceptT e m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source #
HasOptions m => HasOptions (IdentityT m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: IdentityT m PragmaOptions Source # commandLineOptions :: IdentityT m CommandLineOptions Source #
HasOptions m => HasOptions (ReaderT r m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: ReaderT r m PragmaOptions Source # commandLineOptions :: ReaderT r m CommandLineOptions Source #
HasOptions m => HasOptions (StateT s m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: StateT s m PragmaOptions Source # commandLineOptions :: StateT s m CommandLineOptions Source #
(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source #
Instance details Defined in Agda.Interaction.Options.HasOptions Methods pragmaOptions :: WriterT w m PragmaOptions Source # commandLineOptions :: WriterT w m CommandLineOptions Source #

Documentation

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Lenses for PragmaOptions

Boolean accessors to PragmaOptions collapsing default

Non-boolean accessors to PragmaOptions

Instances

Lenses for `PragmaOptions`

Boolean accessors to `PragmaOptions` collapsing default

Non-boolean accessors to `PragmaOptions`