Agda.Interaction.Options

Documentation

data CommandLineOptions

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

LensIncludePaths CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath]

setIncludePaths :: [FilePath] -> CommandLineOptions -> CommandLineOptions

mapIncludePaths :: ([FilePath] -> [FilePath]) -> CommandLineOptions -> CommandLineOptions

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> CommandLineOptions -> CommandLineOptions

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> CommandLineOptions -> CommandLineOptions

LensPersistentVerbosity CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions

LensPragmaOptions CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPragmaOptions :: CommandLineOptions -> PragmaOptions

setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions

lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions

LensSafeMode CommandLineOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: CommandLineOptions -> SafeMode

setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions

mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions

Generic CommandLineOptions

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> CommandLineOptions -> ShowS

show :: CommandLineOptions -> String

showList :: [CommandLineOptions] -> ShowS

NFData CommandLineOptions

Defined in Agda.Interaction.Options.Base

Methods

rnf :: CommandLineOptions -> ()

type Rep CommandLineOptions

Defined in Agda.Interaction.Options.Base

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-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

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

LensPersistentVerbosity PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions

LensSafeMode PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getSafeMode :: PragmaOptions -> SafeMode

setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions

mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions

LensVerbosity PragmaOptions

Defined in Agda.Interaction.Options.Lenses

Methods

getVerbosity :: PragmaOptions -> Verbosity

setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions

mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions

EmbPrj PragmaOptions

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: PragmaOptions -> S Int32

icod_ :: PragmaOptions -> S Int32

value :: Int32 -> R PragmaOptions

Generic PragmaOptions

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> PragmaOptions -> ShowS

show :: PragmaOptions -> String

showList :: [PragmaOptions] -> ShowS

NFData PragmaOptions

Defined in Agda.Interaction.Options.Base

Methods

rnf :: PragmaOptions -> ()

Eq PragmaOptions

Defined in Agda.Interaction.Options.Base

Methods

(==) :: PragmaOptions -> PragmaOptions -> Bool

(/=) :: PragmaOptions -> PragmaOptions -> Bool

type Rep PragmaOptions

Defined in Agda.Interaction.Options.Base

type Rep PragmaOptions = D1 ('MetaData "PragmaOptions" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-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

Warnings when parsing options.

Constructors

OptionRenamed

Fields

• oldOptionName :: String
• newOptionName :: String

Instances

Pretty OptionWarning

Defined in Agda.Interaction.Options.Base

Methods

pretty :: OptionWarning -> Doc

prettyPrec :: Int -> OptionWarning -> Doc

prettyList :: [OptionWarning] -> Doc

EmbPrj OptionWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: OptionWarning -> S Int32

icod_ :: OptionWarning -> S Int32

value :: Int32 -> R OptionWarning

Generic OptionWarning

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> OptionWarning -> ShowS

show :: OptionWarning -> String

showList :: [OptionWarning] -> ShowS

NFData OptionWarning

Defined in Agda.Interaction.Options.Base

Methods

rnf :: OptionWarning -> ()

type Rep OptionWarning

Defined in Agda.Interaction.Options.Base

type Rep OptionWarning = D1 ('MetaData "OptionWarning" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-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

type Flag opts = opts -> OptM opts

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

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

Instances

Applicative OptM

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

Defined in Agda.Interaction.Options.Base

Methods

fmap :: (a -> b) -> OptM a -> OptM b

(<$) :: a -> OptM b -> OptM a

Monad OptM

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)

data OptDescr a

Constructors

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

Instances

Functor OptDescr

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

Functor ArgDescr

Defined in System.Console.GetOpt

Methods

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

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

type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)

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

type VerboseLevel = Int

data WarningMode

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

EmbPrj WarningMode

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: WarningMode -> S Int32

icod_ :: WarningMode -> S Int32

value :: Int32 -> R WarningMode

Generic WarningMode

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

Defined in Agda.Interaction.Options.Warnings

Methods

showsPrec :: Int -> WarningMode -> ShowS

show :: WarningMode -> String

showList :: [WarningMode] -> ShowS

NFData WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

rnf :: WarningMode -> ()

Eq WarningMode

Defined in Agda.Interaction.Options.Warnings

Methods

(==) :: WarningMode -> WarningMode -> Bool

(/=) :: WarningMode -> WarningMode -> Bool

type Rep WarningMode

Defined in Agda.Interaction.Options.Warnings

type Rep WarningMode = D1 ('MetaData "WarningMode" "Agda.Interaction.Options.Warnings" "Agda-2.6.3.20230930-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

Constructors

LocalConfluenceCheck

GlobalConfluenceCheck

Instances

EmbPrj ConfluenceCheck

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ConfluenceCheck -> S Int32

icod_ :: ConfluenceCheck -> S Int32

value :: Int32 -> R ConfluenceCheck

Generic ConfluenceCheck

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> ConfluenceCheck -> ShowS

show :: ConfluenceCheck -> String

showList :: [ConfluenceCheck] -> ShowS

NFData ConfluenceCheck

Defined in Agda.Interaction.Options.Base

Methods

rnf :: ConfluenceCheck -> ()

Eq ConfluenceCheck

Defined in Agda.Interaction.Options.Base

Methods

(==) :: ConfluenceCheck -> ConfluenceCheck -> Bool

(/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool

type Rep ConfluenceCheck

Defined in Agda.Interaction.Options.Base

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

data PrintAgdaVersion

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

Constructors

PrintAgdaVersion

Print Agda version information and exit.

PrintAgdaNumericVersion

Print Agda version number and exit.

Instances

Generic PrintAgdaVersion

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> PrintAgdaVersion -> ShowS

show :: PrintAgdaVersion -> String

showList :: [PrintAgdaVersion] -> ShowS

NFData PrintAgdaVersion

Defined in Agda.Interaction.Options.Base

Methods

rnf :: PrintAgdaVersion -> ()

type Rep PrintAgdaVersion

Defined in Agda.Interaction.Options.Base

type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: Type -> Type))

data UnicodeOrAscii

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

EmbPrj UnicodeOrAscii

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: UnicodeOrAscii -> S Int32

icod_ :: UnicodeOrAscii -> S Int32

value :: Int32 -> R UnicodeOrAscii

Boolean UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

fromBool :: Bool -> UnicodeOrAscii

true :: UnicodeOrAscii

false :: UnicodeOrAscii

not :: UnicodeOrAscii -> UnicodeOrAscii

(&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

(||) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

IsBool UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

toBool :: UnicodeOrAscii -> Bool

ifThenElse :: UnicodeOrAscii -> b -> b -> b

fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii

fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

Bounded UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

minBound :: UnicodeOrAscii

maxBound :: UnicodeOrAscii

Enum UnicodeOrAscii

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

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

Defined in Agda.Syntax.Concrete.Glyph

Methods

showsPrec :: Int -> UnicodeOrAscii -> ShowS

show :: UnicodeOrAscii -> String

showList :: [UnicodeOrAscii] -> ShowS

NFData UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

rnf :: UnicodeOrAscii -> ()

Eq UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

(==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool

(/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool

type Rep UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

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

data DiagnosticsColours

Constructors

AlwaysColour

NeverColour

AutoColour

Instances

Generic DiagnosticsColours

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> DiagnosticsColours -> ShowS

show :: DiagnosticsColours -> String

showList :: [DiagnosticsColours] -> ShowS

NFData DiagnosticsColours

Defined in Agda.Interaction.Options.Base

Methods

rnf :: DiagnosticsColours -> ()

type Rep DiagnosticsColours

Defined in Agda.Interaction.Options.Base

type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-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

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

parsePragmaOptions

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

Parse options for a plugin.

parseVerboseKey :: VerboseKey -> [VerboseKeyItem]

stripRTS :: [String] -> [String]

Removes RTS options from a list of options.

defaultOptions :: CommandLineOptions

defaultInteractionOptions :: PragmaOptions

defaultCutOff :: CutOff

The default termination depth.

defaultPragmaOptions :: PragmaOptions

standardOptions_ :: [OptDescr ()]

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

unsafePragmaOptions :: PragmaOptions -> [String]

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

recheckBecausePragmaOptionsChanged

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

Infective or coinfective?

Constructors

Infective

Coinfective

Instances

EmbPrj InfectiveCoinfective

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: InfectiveCoinfective -> S Int32

icod_ :: InfectiveCoinfective -> S Int32

value :: Int32 -> R InfectiveCoinfective

Generic InfectiveCoinfective

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

Defined in Agda.Interaction.Options.Base

Methods

showsPrec :: Int -> InfectiveCoinfective -> ShowS

show :: InfectiveCoinfective -> String

showList :: [InfectiveCoinfective] -> ShowS

NFData InfectiveCoinfective

Defined in Agda.Interaction.Options.Base

Methods

rnf :: InfectiveCoinfective -> ()

Eq InfectiveCoinfective

Defined in Agda.Interaction.Options.Base

Methods

(==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool

(/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool

type Rep InfectiveCoinfective

Defined in Agda.Interaction.Options.Base

type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: Type -> Type))

data InfectiveCoinfectiveOption

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]

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

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

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

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

inputFlag :: FilePath -> Flag CommandLineOptions

standardOptions :: [OptDescr (Flag CommandLineOptions)]

deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]

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

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 _

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 _

Boolean accessors to PragmaOptions collapsing default

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

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

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

optCohesion is implied by optFlatSplit.

optFlatSplit :: PragmaOptions -> Bool

optImportSorts :: PragmaOptions -> Bool

optImportSorts requires optLoadPrimitives.

optLoadPrimitives :: PragmaOptions -> Bool

optAllowExec :: PragmaOptions -> Bool

optSaveMetas :: PragmaOptions -> Bool

optShowIdentitySubstitutions :: PragmaOptions -> Bool

optKeepCoveringClauses :: PragmaOptions -> Bool

optLargeIndices :: PragmaOptions -> Bool

optForcedArgumentRecursion :: PragmaOptions -> Bool

Non-boolean accessors to PragmaOptions

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

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions

Returns the pragma options which are currently in effect.

default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions

commandLineOptions :: m CommandLineOptions

Returns the command line options which are currently in effect.

default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions

Instances

HasOptions IM

Defined in Agda.Interaction.Monad

Methods

pragmaOptions :: IM PragmaOptions

commandLineOptions :: IM CommandLineOptions

HasOptions AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pragmaOptions :: AbsToCon PragmaOptions

commandLineOptions :: AbsToCon CommandLineOptions

HasOptions TerM

Defined in Agda.Termination.Monad

Methods

pragmaOptions :: TerM PragmaOptions

commandLineOptions :: TerM CommandLineOptions

HasOptions ReduceM

Defined in Agda.TypeChecking.Monad.Base

Methods

pragmaOptions :: ReduceM PragmaOptions

commandLineOptions :: ReduceM CommandLineOptions

HasOptions NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

pragmaOptions :: NLM PragmaOptions

commandLineOptions :: NLM CommandLineOptions

HasOptions m => HasOptions (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pragmaOptions :: PureConversionT m PragmaOptions

commandLineOptions :: PureConversionT m CommandLineOptions

HasOptions m => HasOptions (BlockT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

pragmaOptions :: BlockT m PragmaOptions

commandLineOptions :: BlockT m CommandLineOptions

MonadIO m => HasOptions (TCMT m)

Defined in Agda.TypeChecking.Monad.Base

Methods

pragmaOptions :: TCMT m PragmaOptions

commandLineOptions :: TCMT m CommandLineOptions

HasOptions m => HasOptions (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

pragmaOptions :: NamesT m PragmaOptions

commandLineOptions :: NamesT m CommandLineOptions

HasOptions m => HasOptions (ListT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ListT m PragmaOptions

commandLineOptions :: ListT m CommandLineOptions

HasOptions m => HasOptions (ChangeT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ChangeT m PragmaOptions

commandLineOptions :: ChangeT m CommandLineOptions

HasOptions m => HasOptions (MaybeT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: MaybeT m PragmaOptions

commandLineOptions :: MaybeT m CommandLineOptions

HasOptions m => HasOptions (ExceptT e m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ExceptT e m PragmaOptions

commandLineOptions :: ExceptT e m CommandLineOptions

HasOptions m => HasOptions (IdentityT m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: IdentityT m PragmaOptions

commandLineOptions :: IdentityT m CommandLineOptions

HasOptions m => HasOptions (ReaderT r m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: ReaderT r m PragmaOptions

commandLineOptions :: ReaderT r m CommandLineOptions

HasOptions m => HasOptions (StateT s m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: StateT s m PragmaOptions

commandLineOptions :: StateT s m CommandLineOptions

(HasOptions m, Monoid w) => HasOptions (WriterT w m)

Defined in Agda.Interaction.Options.HasOptions

Methods

pragmaOptions :: WriterT w m PragmaOptions

commandLineOptions :: WriterT w m CommandLineOptions