Agda.Interaction.Options

Documentation

data ArgDescr a

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

Constructors

NoArg a

no argument expected

ReqArg (String -> a) String

option requires argument

OptArg (Maybe String -> a) String

optional argument

Instances

Functor ArgDescr

Since: base-4.7.0.0

Defined in System.Console.GetOpt

Methods

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

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

data OptDescr a

Each OptDescr describes a single option.

The arguments to Option are:

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

Constructors

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

Instances

Functor OptDescr

Since: base-4.7.0.0

Defined in System.Console.GetOpt

Methods

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

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

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.

• optPrintAgdaDataDir :: Bool
• optPrintAgdaAppDir :: 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

Defined in Agda.Interaction.Options.Base

type Rep CommandLineOptions = D1 ('MetaData "CommandLineOptions" "Agda.Interaction.Options.Base" "Agda-2.6.4.2-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 "optPrintAgdaDataDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optPrintAgdaAppDir") '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)))))))

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.4.2-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 "optPrintAgdaDataDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optPrintAgdaAppDir") '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)))))))

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

defaultOptions :: CommandLineOptions

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

Defined in Agda.Interaction.Options.Warnings

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

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

Defined in Agda.Syntax.Concrete.Glyph

type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: 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.4.2-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

optUseUnicode :: PragmaOptions -> UnicodeOrAscii

defaultCutOff :: CutOff

The default termination depth.

optTerminationDepth :: PragmaOptions -> CutOff

optRewriting :: PragmaOptions -> Bool

optQualifiedInstances :: PragmaOptions -> Bool

optFirstOrder :: PragmaOptions -> Bool

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

optCubical :: PragmaOptions -> Maybe Cubical

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

Defined in Agda.Interaction.Options.Base

type Rep ConfluenceCheck = D1 ('MetaData "ConfluenceCheck" "Agda.Interaction.Options.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: 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.4.2-inplace" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

optInjectiveTypeConstructors :: PragmaOptions -> Bool

optCumulativity :: PragmaOptions -> Bool

optAllowExec :: PragmaOptions -> Bool

optCountClusters :: PragmaOptions -> Bool

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

Defined in Agda.Interaction.Options.Base

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

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

Defined in Agda.Interaction.Options.Base

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

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

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

Defined in Agda.Interaction.Options.Base

type Rep PrintAgdaVersion = D1 ('MetaData "PrintAgdaVersion" "Agda.Interaction.Options.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" 'PrefixI 'False) (U1 :: 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.4.2-inplace" 'False) (C1 ('MetaCons "PrintAgdaVersion" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrintAgdaNumericVersion" '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

Defined in Agda.Interaction.Options.Base

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

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

defaultInteractionOptions :: PragmaOptions

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

Defined in Agda.Interaction.Options.Base

type Rep InfectiveCoinfective = D1 ('MetaData "InfectiveCoinfective" "Agda.Interaction.Options.Base" "Agda-2.6.4.2-inplace" 'False) (C1 ('MetaCons "Infective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Coinfective" 'PrefixI 'False) (U1 :: 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.4.2-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)

lensOptShowImplicit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptShowIrrelevant :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptUseUnicode :: Functor f => (WithDefault' UnicodeOrAscii 'True -> f (WithDefault' UnicodeOrAscii 'True)) -> PragmaOptions -> f PragmaOptions

lensOptVerbose :: Functor f => (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions

lensOptProfiling :: Functor f => (ProfileOptions -> f ProfileOptions) -> PragmaOptions -> f PragmaOptions

lensOptProp :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptLevelUniverse :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptTwoLevel :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptAllowUnsolved :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptAllowIncompleteMatch :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptPositivityCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptTerminationCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptTerminationDepth :: Functor f => (CutOff -> f CutOff) -> PragmaOptions -> f PragmaOptions

lensOptUniverseCheck :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptNoUniverseCheck :: Functor f => (WithDefault' Bool 'True -> f (WithDefault' Bool 'True)) -> PragmaOptions -> f PragmaOptions

lensOptOmegaInOmega :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptCumulativity :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptSizedTypes :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptGuardedness :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptInjectiveTypeConstructors :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptUniversePolymorphism :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptIrrelevantProjections :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptExperimentalIrrelevance :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptWithoutK :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptCubicalCompatible :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptCopatterns :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptPatternMatching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptExactSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptHiddenArgumentPuns :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptEta :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptForcing :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptProjectionLike :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptErasure :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptErasedMatches :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptEraseRecordParameters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptRewriting :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptCubical :: Functor f => (Maybe Cubical -> f (Maybe Cubical)) -> PragmaOptions -> f PragmaOptions

lensOptGuarded :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptFirstOrder :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptPostfixProjections :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptKeepPatternVariables :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptInferAbsurdClauses :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptInstanceSearchDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions

lensOptOverlappingInstances :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptQualifiedInstances :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptInversionMaxDepth :: Functor f => (Int -> f Int) -> PragmaOptions -> f PragmaOptions

lensOptSafe :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptDoubleCheck :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptSyntacticEquality :: Functor f => (Maybe Int -> f (Maybe Int)) -> PragmaOptions -> f PragmaOptions

lensOptWarningMode :: Functor f => (WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions

lensOptCompileMain :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptCaching :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptCountClusters :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptAutoInline :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptPrintPatternSynonyms :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptFastReduce :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptCallByName :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptConfluenceCheck :: Functor f => (Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)) -> PragmaOptions -> f PragmaOptions

lensOptCohesion :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptFlatSplit :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptImportSorts :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptLoadPrimitives :: Functor f => (WithDefault 'True -> f (WithDefault 'True)) -> PragmaOptions -> f PragmaOptions

lensOptAllowExec :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptSaveMetas :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptShowIdentitySubstitutions :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions

lensOptKeepCoveringClauses :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f 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

optSizedTypes :: PragmaOptions -> Bool

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

optGuarded :: PragmaOptions -> Bool

optPostfixProjections :: PragmaOptions -> Bool

optKeepPatternVariables :: PragmaOptions -> Bool

optInferAbsurdClauses :: PragmaOptions -> Bool

optOverlappingInstances :: PragmaOptions -> Bool

optSafe :: PragmaOptions -> Bool

optDoubleCheck :: PragmaOptions -> Bool

optCompileNoMain :: PragmaOptions -> Bool

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

optSaveMetas :: PragmaOptions -> Bool

optShowIdentitySubstitutions :: PragmaOptions -> Bool

optKeepCoveringClauses :: PragmaOptions -> Bool

optLargeIndices :: PragmaOptions -> Bool

optForcedArgumentRecursion :: PragmaOptions -> Bool

optConfluenceCheck :: PragmaOptions -> Maybe ConfluenceCheck

optInstanceSearchDepth :: PragmaOptions -> Int

optInversionMaxDepth :: PragmaOptions -> Int

optProfiling :: PragmaOptions -> ProfileOptions

optSyntacticEquality :: PragmaOptions -> Maybe Int

optVerbose :: PragmaOptions -> Verbosity

optWarningMode :: PragmaOptions -> WarningMode

class (Functor m, Applicative m, Monad m) => HasOptions (m :: Type -> Type) where

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions

Returns the pragma options which are currently in effect.

default pragmaOptions :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions

commandLineOptions :: m CommandLineOptions

Returns the command line options which are currently in effect.

default commandLineOptions :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (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