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

Agda.Interaction.Options

Synopsis

Documentation

data CommandLineOptions Source #

Constructors

Options 

Fields

Instances

Instances details
LensIncludePaths CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPersistentVerbosity CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

Generic CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep CommandLineOptions :: Type -> Type

Show CommandLineOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Base

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

Instances

Instances details
LensPersistentVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity PragmaOptions Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

EmbPrj PragmaOptions Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

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

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

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

Instances

Instances details
Pretty OptionWarning Source # 
Instance details

Defined in Agda.Interaction.Options.Base

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

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

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

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 #

Instances

Instances details
EmbPrj ConfluenceCheck Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Generic ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep ConfluenceCheck :: Type -> Type

Show ConfluenceCheck Source # 
Instance details

Defined in Agda.Interaction.Options.Base

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

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

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

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

Enum UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Generic UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Associated Types

type Rep UnicodeOrAscii :: Type -> Type

Show UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

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

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 #

Instances

Instances details
Generic DiagnosticsColours Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep DiagnosticsColours :: Type -> Type

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.

defaultCutOff :: CutOff Source #

The default termination depth.

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

Generic InfectiveCoinfective Source # 
Instance details

Defined in Agda.Interaction.Options.Base

Associated Types

type Rep InfectiveCoinfective :: Type -> Type

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

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

infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption] Source #

Infective and coinfective options.

Note that --cubical and --erased-cubical are "jointly infective": if one of them is used in one module, then one or the other must be used in all modules that depend on this module.

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

Map a function over the long options. Also removes the short options. Will be used to add the plugin name to the plugin options.

usage :: [OptDescr ()] -> String -> Help -> String Source #

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

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

Command line options of previous versions of Agda. Should not be listed in the usage info, put parsed by GetOpt for good error messaging.

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

Boolean accessors to PragmaOptions collapsing default

optErasure :: PragmaOptions -> Bool Source #

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

Non-boolean accessors to PragmaOptions

class (Functor m, Applicative m, Monad m) => HasOptions m where Source #

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

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

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

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

Instances

Instances details
HasOptions IM Source # 
Instance details

Defined in Agda.Interaction.Monad

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

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

Defined in Agda.TypeChecking.Conversion.Pure

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Monad.Base

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

Defined in Agda.TypeChecking.Names

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions

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

Defined in Agda.Interaction.Options.HasOptions