Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data CommandLineOptions = Options {
- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]
- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath
- optDefaultLibs :: Bool
- optUseLibs :: Bool
- optTraceImports :: Integer
- optTrustedExecutables :: Map ExeName FilePath
- optPrintAgdaDir :: Bool
- optPrintVersion :: Maybe PrintAgdaVersion
- optPrintHelp :: Maybe Help
- optInteractive :: Bool
- optGHCiInteraction :: Bool
- optJSONInteraction :: Bool
- optExitOnError :: !Bool
- optCompileDir :: Maybe FilePath
- optGenerateVimFile :: Bool
- optIgnoreInterfaces :: Bool
- optIgnoreAllInterfaces :: Bool
- optLocalInterfaces :: Bool
- optPragmaOptions :: PragmaOptions
- optOnlyScopeChecking :: Bool
- optTransliterate :: Bool
- optDiagnosticsColour :: DiagnosticsColours
- data PragmaOptions = PragmaOptions {
- _optShowImplicit :: WithDefault 'False
- _optShowIrrelevant :: WithDefault 'False
- _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
- _optVerbose :: !Verbosity
- _optProfiling :: ProfileOptions
- _optProp :: WithDefault 'False
- _optLevelUniverse :: WithDefault 'False
- _optTwoLevel :: WithDefault 'False
- _optAllowUnsolved :: WithDefault 'False
- _optAllowIncompleteMatch :: WithDefault 'False
- _optPositivityCheck :: WithDefault 'True
- _optTerminationCheck :: WithDefault 'True
- _optTerminationDepth :: CutOff
- _optUniverseCheck :: WithDefault 'True
- _optOmegaInOmega :: WithDefault 'False
- _optCumulativity :: WithDefault 'False
- _optSizedTypes :: WithDefault 'False
- _optGuardedness :: WithDefault 'False
- _optInjectiveTypeConstructors :: WithDefault 'False
- _optUniversePolymorphism :: WithDefault 'True
- _optIrrelevantProjections :: WithDefault 'False
- _optExperimentalIrrelevance :: WithDefault 'False
- _optWithoutK :: WithDefault 'False
- _optCubicalCompatible :: WithDefault 'False
- _optCopatterns :: WithDefault 'True
- _optPatternMatching :: WithDefault 'True
- _optExactSplit :: WithDefault 'False
- _optHiddenArgumentPuns :: WithDefault 'False
- _optEta :: WithDefault 'True
- _optForcing :: WithDefault 'True
- _optProjectionLike :: WithDefault 'True
- _optErasure :: WithDefault 'False
- _optErasedMatches :: WithDefault 'True
- _optEraseRecordParameters :: WithDefault 'False
- _optRewriting :: WithDefault 'False
- _optCubical :: Maybe Cubical
- _optGuarded :: WithDefault 'False
- _optFirstOrder :: WithDefault 'False
- _optPostfixProjections :: WithDefault 'False
- _optKeepPatternVariables :: WithDefault 'False
- _optInferAbsurdClauses :: WithDefault 'True
- _optInstanceSearchDepth :: Int
- _optOverlappingInstances :: WithDefault 'False
- _optQualifiedInstances :: WithDefault 'True
- _optInversionMaxDepth :: Int
- _optSafe :: WithDefault 'False
- _optDoubleCheck :: WithDefault 'False
- _optSyntacticEquality :: !(Maybe Int)
- _optWarningMode :: WarningMode
- _optCompileMain :: WithDefault 'True
- _optCaching :: WithDefault 'True
- _optCountClusters :: WithDefault 'False
- _optAutoInline :: WithDefault 'False
- _optPrintPatternSynonyms :: WithDefault 'True
- _optFastReduce :: WithDefault 'True
- _optCallByName :: WithDefault 'False
- _optConfluenceCheck :: Maybe ConfluenceCheck
- _optCohesion :: WithDefault 'False
- _optFlatSplit :: WithDefault 'False
- _optImportSorts :: WithDefault 'True
- _optLoadPrimitives :: WithDefault 'True
- _optAllowExec :: WithDefault 'False
- _optSaveMetas :: WithDefault 'False
- _optShowIdentitySubstitutions :: WithDefault 'False
- _optKeepCoveringClauses :: WithDefault 'False
- _optLargeIndices :: WithDefault 'False
- _optForcedArgumentRecursion :: WithDefault 'True
- data OptionWarning = OptionRenamed {}
- optionWarningName :: OptionWarning -> WarningName
- type Flag opts = opts -> OptM opts
- data OptM a
- runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- data ArgDescr a
- type Verbosity = Maybe (Trie VerboseKeyItem VerboseLevel)
- type VerboseKey = String
- type VerboseLevel = Int
- data WarningMode = WarningMode {}
- data ConfluenceCheck
- data PrintAgdaVersion
- data UnicodeOrAscii
- data DiagnosticsColours
- checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions
- parsePragmaOptions :: OptionsPragma -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- parseVerboseKey :: VerboseKey -> [VerboseKeyItem]
- stripRTS :: [String] -> [String]
- defaultOptions :: CommandLineOptions
- defaultInteractionOptions :: PragmaOptions
- defaultCutOff :: CutOff
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: PragmaOptions -> [String]
- recheckBecausePragmaOptionsChanged :: PragmaOptions -> PragmaOptions -> Bool
- data InfectiveCoinfective
- data InfectiveCoinfectiveOption = ICOption {}
- infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption]
- safeFlag :: Flag PragmaOptions
- mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
- usage :: [OptDescr ()] -> String -> Help -> String
- inputFlag :: FilePath -> Flag CommandLineOptions
- standardOptions :: [OptDescr (Flag CommandLineOptions)]
- deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
- getOptSimple :: [String] -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
- lensOptShowImplicit :: Lens' PragmaOptions _
- lensOptShowIrrelevant :: Lens' PragmaOptions _
- lensOptUseUnicode :: Lens' PragmaOptions _
- lensOptVerbose :: Lens' PragmaOptions _
- lensOptProfiling :: Lens' PragmaOptions _
- lensOptProp :: Lens' PragmaOptions _
- lensOptLevelUniverse :: Lens' PragmaOptions _
- lensOptTwoLevel :: Lens' PragmaOptions _
- lensOptAllowUnsolved :: Lens' PragmaOptions _
- lensOptAllowIncompleteMatch :: Lens' PragmaOptions _
- lensOptPositivityCheck :: Lens' PragmaOptions _
- lensOptTerminationCheck :: Lens' PragmaOptions _
- lensOptTerminationDepth :: Lens' PragmaOptions _
- lensOptUniverseCheck :: Lens' PragmaOptions _
- lensOptNoUniverseCheck :: Lens' PragmaOptions _
- lensOptOmegaInOmega :: Lens' PragmaOptions _
- lensOptCumulativity :: Lens' PragmaOptions _
- lensOptSizedTypes :: Lens' PragmaOptions _
- lensOptGuardedness :: Lens' PragmaOptions _
- lensOptInjectiveTypeConstructors :: Lens' PragmaOptions _
- lensOptUniversePolymorphism :: Lens' PragmaOptions _
- lensOptIrrelevantProjections :: Lens' PragmaOptions _
- lensOptExperimentalIrrelevance :: Lens' PragmaOptions _
- lensOptWithoutK :: Lens' PragmaOptions _
- lensOptCubicalCompatible :: Lens' PragmaOptions _
- lensOptCopatterns :: Lens' PragmaOptions _
- lensOptPatternMatching :: Lens' PragmaOptions _
- lensOptExactSplit :: Lens' PragmaOptions _
- lensOptHiddenArgumentPuns :: Lens' PragmaOptions _
- lensOptEta :: Lens' PragmaOptions _
- lensOptForcing :: Lens' PragmaOptions _
- lensOptProjectionLike :: Lens' PragmaOptions _
- lensOptErasure :: Lens' PragmaOptions _
- lensOptErasedMatches :: Lens' PragmaOptions _
- lensOptEraseRecordParameters :: Lens' PragmaOptions _
- lensOptRewriting :: Lens' PragmaOptions _
- lensOptCubical :: Lens' PragmaOptions _
- lensOptGuarded :: Lens' PragmaOptions _
- lensOptFirstOrder :: Lens' PragmaOptions _
- lensOptPostfixProjections :: Lens' PragmaOptions _
- lensOptKeepPatternVariables :: Lens' PragmaOptions _
- lensOptInferAbsurdClauses :: Lens' PragmaOptions _
- lensOptInstanceSearchDepth :: Lens' PragmaOptions _
- lensOptOverlappingInstances :: Lens' PragmaOptions _
- lensOptQualifiedInstances :: Lens' PragmaOptions _
- lensOptInversionMaxDepth :: Lens' PragmaOptions _
- lensOptSafe :: Lens' PragmaOptions _
- lensOptDoubleCheck :: Lens' PragmaOptions _
- lensOptSyntacticEquality :: Lens' PragmaOptions _
- lensOptWarningMode :: Lens' PragmaOptions _
- lensOptCompileMain :: Lens' PragmaOptions _
- lensOptCaching :: Lens' PragmaOptions _
- lensOptCountClusters :: Lens' PragmaOptions _
- lensOptAutoInline :: Lens' PragmaOptions _
- lensOptPrintPatternSynonyms :: Lens' PragmaOptions _
- lensOptFastReduce :: Lens' PragmaOptions _
- lensOptCallByName :: Lens' PragmaOptions _
- lensOptConfluenceCheck :: Lens' PragmaOptions _
- lensOptCohesion :: Lens' PragmaOptions _
- lensOptFlatSplit :: Lens' PragmaOptions _
- lensOptImportSorts :: Lens' PragmaOptions _
- lensOptLoadPrimitives :: Lens' PragmaOptions _
- lensOptAllowExec :: Lens' PragmaOptions _
- lensOptSaveMetas :: Lens' PragmaOptions _
- lensOptShowIdentitySubstitutions :: Lens' PragmaOptions _
- lensOptKeepCoveringClauses :: Lens' PragmaOptions _
- optShowImplicit :: PragmaOptions -> Bool
- optShowIrrelevant :: PragmaOptions -> Bool
- optProp :: PragmaOptions -> Bool
- optLevelUniverse :: PragmaOptions -> Bool
- optTwoLevel :: PragmaOptions -> Bool
- optAllowUnsolved :: PragmaOptions -> Bool
- optAllowIncompleteMatch :: PragmaOptions -> Bool
- optPositivityCheck :: PragmaOptions -> Bool
- optTerminationCheck :: PragmaOptions -> Bool
- optUniverseCheck :: PragmaOptions -> Bool
- optOmegaInOmega :: PragmaOptions -> Bool
- optCumulativity :: PragmaOptions -> Bool
- optSizedTypes :: PragmaOptions -> Bool
- optGuardedness :: PragmaOptions -> Bool
- optInjectiveTypeConstructors :: PragmaOptions -> Bool
- optUniversePolymorphism :: PragmaOptions -> Bool
- optIrrelevantProjections :: PragmaOptions -> Bool
- optExperimentalIrrelevance :: PragmaOptions -> Bool
- optWithoutK :: PragmaOptions -> Bool
- optCubicalCompatible :: PragmaOptions -> Bool
- optCopatterns :: PragmaOptions -> Bool
- optPatternMatching :: PragmaOptions -> Bool
- optHiddenArgumentPuns :: PragmaOptions -> Bool
- optEta :: PragmaOptions -> Bool
- optForcing :: PragmaOptions -> Bool
- optProjectionLike :: PragmaOptions -> Bool
- optErasure :: PragmaOptions -> Bool
- optErasedMatches :: PragmaOptions -> Bool
- optEraseRecordParameters :: PragmaOptions -> Bool
- optRewriting :: PragmaOptions -> Bool
- optGuarded :: PragmaOptions -> Bool
- optFirstOrder :: PragmaOptions -> Bool
- optPostfixProjections :: PragmaOptions -> Bool
- optKeepPatternVariables :: PragmaOptions -> Bool
- optInferAbsurdClauses :: PragmaOptions -> Bool
- optOverlappingInstances :: PragmaOptions -> Bool
- optQualifiedInstances :: PragmaOptions -> Bool
- optSafe :: PragmaOptions -> Bool
- optDoubleCheck :: PragmaOptions -> Bool
- optCompileNoMain :: PragmaOptions -> Bool
- optCaching :: PragmaOptions -> Bool
- optCountClusters :: PragmaOptions -> Bool
- optAutoInline :: PragmaOptions -> Bool
- optPrintPatternSynonyms :: PragmaOptions -> Bool
- optFastReduce :: PragmaOptions -> Bool
- optCallByName :: PragmaOptions -> Bool
- optCohesion :: PragmaOptions -> Bool
- optFlatSplit :: PragmaOptions -> Bool
- optImportSorts :: PragmaOptions -> Bool
- optLoadPrimitives :: PragmaOptions -> Bool
- optAllowExec :: PragmaOptions -> Bool
- optSaveMetas :: PragmaOptions -> Bool
- optShowIdentitySubstitutions :: PragmaOptions -> Bool
- optKeepCoveringClauses :: PragmaOptions -> Bool
- optLargeIndices :: PragmaOptions -> Bool
- optForcedArgumentRecursion :: PragmaOptions -> Bool
- optConfluenceCheck :: PragmaOptions -> _
- optCubical :: PragmaOptions -> _
- optInstanceSearchDepth :: PragmaOptions -> _
- optInversionMaxDepth :: PragmaOptions -> _
- optProfiling :: PragmaOptions -> _
- optSyntacticEquality :: PragmaOptions -> _
- optTerminationDepth :: PragmaOptions -> _
- optUseUnicode :: PragmaOptions -> UnicodeOrAscii
- optVerbose :: PragmaOptions -> _
- optWarningMode :: PragmaOptions -> _
- class (Functor m, Applicative m, Monad m) => HasOptions m where
Documentation
data CommandLineOptions Source #
Instances
data PragmaOptions Source #
Options which can be set in a pragma.
PragmaOptions | |
|
Instances
data OptionWarning Source #
Warnings when parsing options.
Instances
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
The options parse monad OptM
collects warnings that are not discarded
when a fatal error occurrs
Describes whether an option takes an argument or not, and if so
how the argument is injected into a value of type 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.
Instances
data ConfluenceCheck Source #
Instances
EmbPrj ConfluenceCheck Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
Generic ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base type Rep ConfluenceCheck :: Type -> Type # from :: ConfluenceCheck -> Rep ConfluenceCheck x # to :: Rep ConfluenceCheck x -> ConfluenceCheck # | |
Show ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base showsPrec :: Int -> ConfluenceCheck -> ShowS # show :: ConfluenceCheck -> String # showList :: [ConfluenceCheck] -> ShowS # | |
NFData ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base rnf :: ConfluenceCheck -> () # | |
Eq ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool # (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool # | |
type Rep ConfluenceCheck Source # | |
Defined in Agda.Interaction.Options.Base |
data PrintAgdaVersion Source #
Options --version
and --numeric-version
(last wins).
PrintAgdaVersion | Print Agda version information and exit. |
PrintAgdaNumericVersion | Print Agda version number and exit. |
Instances
Generic PrintAgdaVersion Source # | |
Defined in Agda.Interaction.Options.Base type Rep PrintAgdaVersion :: Type -> Type # from :: PrintAgdaVersion -> Rep PrintAgdaVersion x # to :: Rep PrintAgdaVersion x -> PrintAgdaVersion # | |
Show PrintAgdaVersion Source # | |
Defined in Agda.Interaction.Options.Base showsPrec :: Int -> PrintAgdaVersion -> ShowS # show :: PrintAgdaVersion -> String # showList :: [PrintAgdaVersion] -> ShowS # | |
NFData PrintAgdaVersion Source # | |
Defined in Agda.Interaction.Options.Base rnf :: PrintAgdaVersion -> () # | |
type Rep PrintAgdaVersion Source # | |
Defined in Agda.Interaction.Options.Base |
data UnicodeOrAscii Source #
We want to know whether we are allowed to insert unicode characters or not.
Instances
data DiagnosticsColours Source #
Instances
Generic DiagnosticsColours Source # | |
Defined in Agda.Interaction.Options.Base type Rep DiagnosticsColours :: Type -> Type # from :: DiagnosticsColours -> Rep DiagnosticsColours x # to :: Rep DiagnosticsColours x -> DiagnosticsColours # | |
Show DiagnosticsColours Source # | |
Defined in Agda.Interaction.Options.Base showsPrec :: Int -> DiagnosticsColours -> ShowS # show :: DiagnosticsColours -> String # showList :: [DiagnosticsColours] -> ShowS # | |
NFData DiagnosticsColours Source # | |
Defined in Agda.Interaction.Options.Base rnf :: DiagnosticsColours -> () # | |
type Rep DiagnosticsColours Source # | |
Defined in Agda.Interaction.Options.Base type Rep DiagnosticsColours = D1 ('MetaData "DiagnosticsColours" "Agda.Interaction.Options.Base" "Agda-2.6.3.20230914-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).
:: 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 #
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 #
:: 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?
Instances
EmbPrj InfectiveCoinfective Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors | |
Generic InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base type Rep InfectiveCoinfective :: Type -> Type # from :: InfectiveCoinfective -> Rep InfectiveCoinfective x # to :: Rep InfectiveCoinfective x -> InfectiveCoinfective # | |
Show InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base showsPrec :: Int -> InfectiveCoinfective -> ShowS # show :: InfectiveCoinfective -> String # showList :: [InfectiveCoinfective] -> ShowS # | |
NFData InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base rnf :: InfectiveCoinfective -> () # | |
Eq InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base (==) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool # (/=) :: InfectiveCoinfective -> InfectiveCoinfective -> Bool # | |
type Rep InfectiveCoinfective Source # | |
Defined in Agda.Interaction.Options.Base |
data InfectiveCoinfectiveOption Source #
Descriptions of infective and coinfective options.
ICOption | |
|
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.
:: [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
lensOptProp :: Lens' PragmaOptions _ Source #
lensOptEta :: Lens' PragmaOptions _ Source #
lensOptSafe :: Lens' PragmaOptions _ Source #
Boolean accessors to PragmaOptions
collapsing default
optShowImplicit :: PragmaOptions -> Bool Source #
optProp :: PragmaOptions -> Bool Source #
optLevelUniverse :: PragmaOptions -> Bool Source #
optTwoLevel :: PragmaOptions -> Bool Source #
optAllowUnsolved :: PragmaOptions -> Bool Source #
optUniverseCheck :: PragmaOptions -> Bool Source #
optOmegaInOmega :: PragmaOptions -> Bool Source #
optCumulativity :: PragmaOptions -> Bool Source #
optSizedTypes :: PragmaOptions -> Bool Source #
optGuardedness :: PragmaOptions -> Bool Source #
optWithoutK :: PragmaOptions -> Bool Source #
optCopatterns :: PragmaOptions -> Bool Source #
optEta :: PragmaOptions -> Bool Source #
optForcing :: PragmaOptions -> Bool Source #
optErasure :: PragmaOptions -> Bool Source #
optErasure
is implied by optEraseRecordParameters
.
optErasure
is also implied by an explicitly given `--erased-matches`.
optErasedMatches :: PragmaOptions -> Bool Source #
optRewriting :: PragmaOptions -> Bool Source #
optGuarded :: PragmaOptions -> Bool Source #
optFirstOrder :: PragmaOptions -> Bool Source #
optSafe :: PragmaOptions -> Bool Source #
optDoubleCheck :: PragmaOptions -> Bool Source #
optCompileNoMain :: PragmaOptions -> Bool Source #
optCaching :: PragmaOptions -> Bool Source #
optCountClusters :: PragmaOptions -> Bool Source #
optAutoInline :: PragmaOptions -> Bool Source #
optFastReduce :: PragmaOptions -> Bool Source #
optCallByName :: PragmaOptions -> Bool Source #
optCohesion :: PragmaOptions -> Bool Source #
optCohesion
is implied by optFlatSplit
.
optFlatSplit :: PragmaOptions -> Bool Source #
optImportSorts :: PragmaOptions -> Bool Source #
optImportSorts
requires optLoadPrimitives
.
optAllowExec :: PragmaOptions -> Bool Source #
optSaveMetas :: PragmaOptions -> Bool Source #
optLargeIndices :: PragmaOptions -> Bool Source #
Non-boolean accessors to PragmaOptions
optConfluenceCheck :: PragmaOptions -> _ Source #
optCubical :: PragmaOptions -> _ Source #
optInstanceSearchDepth :: PragmaOptions -> _ Source #
optInversionMaxDepth :: PragmaOptions -> _ Source #
optProfiling :: PragmaOptions -> _ Source #
optSyntacticEquality :: PragmaOptions -> _ Source #
optTerminationDepth :: PragmaOptions -> _ Source #
optVerbose :: PragmaOptions -> _ Source #
optWarningMode :: PragmaOptions -> _ Source #
class (Functor m, Applicative m, Monad m) => HasOptions m where Source #
Nothing
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 #