Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.Options

Synopsis

- data CommandLineOptions = Options {
  - optProgramName :: String
  - optInputFile :: Maybe FilePath
  - optIncludePaths :: [FilePath]
  - optAbsoluteIncludePaths :: [AbsolutePath]
  - optLibraries :: [LibName]
  - optOverrideLibrariesFile :: Maybe FilePath
  - optDefaultLibs :: Bool
  - optUseLibs :: Bool
  - optTrustedExecutables :: Map ExeName FilePath
  - optPrintAgdaDir :: Bool
  - optPrintVersion :: Bool
  - optPrintHelp :: Maybe Help
  - optInteractive :: Bool
  - optGHCiInteraction :: Bool
  - optJSONInteraction :: Bool
  - optOptimSmashing :: Bool
  - optCompileDir :: Maybe FilePath
  - optGenerateVimFile :: Bool
  - optIgnoreInterfaces :: Bool
  - optIgnoreAllInterfaces :: Bool
  - optLocalInterfaces :: Bool
  - optPragmaOptions :: PragmaOptions
  - optOnlyScopeChecking :: Bool
  }
- data PragmaOptions = PragmaOptions {
  - optShowImplicit :: Bool
  - optShowIrrelevant :: Bool
  - optUseUnicode :: UnicodeOrAscii
  - optVerbose :: Verbosity
  - optProp :: Bool
  - optTwoLevel :: WithDefault 'False
  - optAllowUnsolved :: Bool
  - optAllowIncompleteMatch :: Bool
  - optDisablePositivity :: Bool
  - optTerminationCheck :: Bool
  - optTerminationDepth :: CutOff
  - optCompletenessCheck :: Bool
  - optUniverseCheck :: Bool
  - optOmegaInOmega :: Bool
  - optSubtyping :: WithDefault 'False
  - optCumulativity :: Bool
  - optSizedTypes :: WithDefault 'False
  - optGuardedness :: WithDefault 'False
  - optInjectiveTypeConstructors :: Bool
  - optUniversePolymorphism :: Bool
  - optIrrelevantProjections :: Bool
  - optExperimentalIrrelevance :: Bool
  - optWithoutK :: WithDefault 'False
  - optCopatterns :: Bool
  - optPatternMatching :: Bool
  - optExactSplit :: Bool
  - optEta :: Bool
  - optForcing :: Bool
  - optProjectionLike :: Bool
  - optRewriting :: Bool
  - optCubical :: Maybe Cubical
  - optGuarded :: Bool
  - optFirstOrder :: Bool
  - optPostfixProjections :: Bool
  - optKeepPatternVariables :: Bool
  - optInstanceSearchDepth :: Int
  - optOverlappingInstances :: Bool
  - optQualifiedInstances :: Bool
  - optInversionMaxDepth :: Int
  - optSafe :: Bool
  - optDoubleCheck :: Bool
  - optSyntacticEquality :: Bool
  - optWarningMode :: WarningMode
  - optCompileNoMain :: Bool
  - optCaching :: Bool
  - optCountClusters :: Bool
  - optAutoInline :: Bool
  - optPrintPatternSynonyms :: Bool
  - optFastReduce :: Bool
  - optCallByName :: Bool
  - optConfluenceCheck :: Maybe ConfluenceCheck
  - optFlatSplit :: Bool
  - optImportSorts :: Bool
  - optAllowExec :: Bool
  - optShowIdentitySubstitutions :: Bool
  }
- type OptionsPragma = [String]
- type Flag opts = opts -> OptM opts
- type OptM = Except String
- runOptM :: Monad m => OptM opts -> m (Either String opts)
- data OptDescr a = Option [Char] [String] (ArgDescr a) String
- data ArgDescr a
  - = NoArg a
  - | ReqArg (String -> a) String
  - | OptArg (Maybe String -> a) String
- type Verbosity = Trie VerboseKey VerboseLevel
- type VerboseKey = String
- type VerboseLevel = Int
- data WarningMode = WarningMode {
  - _warningSet :: Set WarningName
  - _warn2Error :: Bool
  }
- data ConfluenceCheck
  - = LocalConfluenceCheck
  - | GlobalConfluenceCheck
- data UnicodeOrAscii
  - = UnicodeOk
  - | AsciiOnly
- checkOpts :: Flag CommandLineOptions
- parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
- parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
- stripRTS :: [String] -> [String]
- defaultOptions :: CommandLineOptions
- defaultInteractionOptions :: PragmaOptions
- defaultVerbosity :: Verbosity
- defaultCutOff :: CutOff
- defaultPragmaOptions :: PragmaOptions
- standardOptions_ :: [OptDescr ()]
- unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
- restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
- infectiveOptions :: [(PragmaOptions -> Bool, String)]
- coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
- 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
- class (Functor m, Applicative m, Monad m) => HasOptions m where
  - pragmaOptions :: m PragmaOptions
  - commandLineOptions :: m CommandLineOptions

# Documentation

data CommandLineOptions Source #

Constructors

Options |

Fields

- optProgramName :: String
- optInputFile :: Maybe FilePath
- optIncludePaths :: [FilePath]
- optAbsoluteIncludePaths :: [AbsolutePath]

  The list should not contain duplicates.

- optLibraries :: [LibName]
- optOverrideLibrariesFile :: Maybe FilePath

  Use this (if Just) instead of .agda/libraries

- optDefaultLibs :: Bool

  Use ~.agdadefaults

- optUseLibs :: Bool

  look for .agda-lib files

- optTrustedExecutables :: Map ExeName FilePath

  Map names of trusted executables to absolute paths

- optPrintAgdaDir :: Bool
- optPrintVersion :: Bool
- optPrintHelp :: Maybe Help
- optInteractive :: Bool

  Agda REPL (-I).

- optGHCiInteraction :: Bool
- optJSONInteraction :: Bool
- optOptimSmashing :: Bool
- 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?

#### Instances

Instances details

LensIncludePaths CommandLineOptions Source # |

Instance details

Defined in Agda.Interaction.Options.Lenses

Methods

getIncludePaths :: CommandLineOptions -> [FilePath] Source #

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

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

getAbsoluteIncludePaths :: CommandLineOptions -> [AbsolutePath] Source #

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

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

LensPersistentVerbosity CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: CommandLineOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> CommandLineOptions -> CommandLineOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> CommandLineOptions -> CommandLineOptions Source #
LensPragmaOptions CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPragmaOptions :: CommandLineOptions -> PragmaOptions Source # setPragmaOptions :: PragmaOptions -> CommandLineOptions -> CommandLineOptions Source # mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> CommandLineOptions -> CommandLineOptions Source # lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions Source #
LensSafeMode CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: CommandLineOptions -> SafeMode Source # setSafeMode :: SafeMode -> CommandLineOptions -> CommandLineOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> CommandLineOptions -> CommandLineOptions Source #
Generic CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep CommandLineOptions :: Type -> Type Source # Methods from :: CommandLineOptions -> Rep CommandLineOptions x Source # to :: Rep CommandLineOptions x -> CommandLineOptions Source #
Show CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> CommandLineOptions -> ShowS Source # show :: CommandLineOptions -> String Source # showList :: [CommandLineOptions] -> ShowS Source #
NFData CommandLineOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: CommandLineOptions -> () Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" '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 "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 Bool))))) :*: (((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 "optOptimSmashing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (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)))))))

data PragmaOptions Source #

Options which can be set in a pragma.

Constructors

PragmaOptions |

Fields

- optShowImplicit :: Bool
- optShowIrrelevant :: Bool
- optUseUnicode :: UnicodeOrAscii
- optVerbose :: Verbosity
- optProp :: Bool
- optTwoLevel :: WithDefault 'False
- optAllowUnsolved :: Bool
- optAllowIncompleteMatch :: Bool
- optDisablePositivity :: Bool
- optTerminationCheck :: Bool
- optTerminationDepth :: CutOff

  Cut off structural order comparison at some depth in termination checker?

- optCompletenessCheck :: Bool
- optUniverseCheck :: Bool
- optOmegaInOmega :: Bool
- optSubtyping :: WithDefault 'False
- optCumulativity :: Bool
- optSizedTypes :: WithDefault 'False
- optGuardedness :: WithDefault 'False
- optInjectiveTypeConstructors :: Bool
- optUniversePolymorphism :: Bool
- optIrrelevantProjections :: Bool
- optExperimentalIrrelevance :: Bool

  irrelevant levels, irrelevant data matching

- optWithoutK :: WithDefault 'False
- optCopatterns :: Bool

  Allow definitions by copattern matching?

- optPatternMatching :: Bool

  Is pattern matching allowed in the current file?

- optExactSplit :: Bool
- optEta :: Bool
- optForcing :: Bool

  Perform the forcing analysis on data constructors?

- optProjectionLike :: Bool

  Perform the projection-likeness analysis on functions?

- optRewriting :: Bool

  Can rewrite rules be added and used?

- optCubical :: Maybe Cubical
- optGuarded :: Bool
- optFirstOrder :: Bool

  Should we speculatively unify function applications as if they were injective?

- optPostfixProjections :: Bool

  Should system generated projections `ProjSystem` be printed postfix (True) or prefix (False).

- optKeepPatternVariables :: Bool

  Should case splitting replace variables with dot patterns (False) or keep them as variables (True).

- optInstanceSearchDepth :: Int
- optOverlappingInstances :: Bool
- optQualifiedInstances :: Bool

  Should instance search consider instances with qualified names?

- optInversionMaxDepth :: Int
- optSafe :: Bool
- optDoubleCheck :: Bool
- optSyntacticEquality :: Bool

  Should conversion checker use syntactic equality shortcut?

- optWarningMode :: WarningMode
- optCompileNoMain :: Bool
- optCaching :: Bool
- optCountClusters :: Bool

  Count extended grapheme clusters rather than code points when generating LaTeX.

- optAutoInline :: Bool

  Automatic compile-time inlining for simple definitions (unless marked NOINLINE).

- optPrintPatternSynonyms :: Bool
- optFastReduce :: Bool

  Use the Agda abstract machine (fastReduce)?

- optCallByName :: Bool

  Use call-by-name instead of call-by-need

- optConfluenceCheck :: Maybe ConfluenceCheck

  Check confluence of rewrite rules?

- optFlatSplit :: Bool

  Can we split on a (@flat x : A) argument?

- optImportSorts :: Bool

  Should every top-level module start with an implicit statement `open import Agda.Primitive using (Set; Prop)`?

- optAllowExec :: Bool
- optShowIdentitySubstitutions :: Bool

  Show identity substitutions when pretty-printing terms (i.e. always show all arguments of a metavariable)

#### Instances

Instances details

LensPersistentVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getPersistentVerbosity :: PragmaOptions -> PersistentVerbosity Source # setPersistentVerbosity :: PersistentVerbosity -> PragmaOptions -> PragmaOptions Source # mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PragmaOptions -> PragmaOptions Source #
LensSafeMode PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getSafeMode :: PragmaOptions -> SafeMode Source # setSafeMode :: SafeMode -> PragmaOptions -> PragmaOptions Source # mapSafeMode :: (SafeMode -> SafeMode) -> PragmaOptions -> PragmaOptions Source #
LensVerbosity PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Lenses Methods getVerbosity :: PragmaOptions -> Verbosity Source # setVerbosity :: Verbosity -> PragmaOptions -> PragmaOptions Source # mapVerbosity :: (Verbosity -> Verbosity) -> PragmaOptions -> PragmaOptions Source #
EmbPrj PragmaOptions Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: PragmaOptions -> S Int32 Source # icod_ :: PragmaOptions -> S Int32 Source # value :: Int32 -> R PragmaOptions Source #
Generic PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep PragmaOptions :: Type -> Type Source # Methods from :: PragmaOptions -> Rep PragmaOptions x Source # to :: Rep PragmaOptions x -> PragmaOptions Source #
Show PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> PragmaOptions -> ShowS Source # show :: PragmaOptions -> String Source # showList :: [PragmaOptions] -> ShowS Source #
NFData PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: PragmaOptions -> () Source #
Eq PragmaOptions Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods (==) :: PragmaOptions -> PragmaOptions -> Bool Source # (/=) :: PragmaOptions -> PragmaOptions -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "PragmaOptions" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "optShowImplicit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optShowIrrelevant") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUseUnicode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UnicodeOrAscii))) :*: (S1 ('MetaSel ('Just "optVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Verbosity) :*: (S1 ('MetaSel ('Just "optProp") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optTwoLevel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False))))) :*: ((S1 ('MetaSel ('Just "optAllowUnsolved") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optAllowIncompleteMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDisablePositivity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optTerminationDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CutOff)) :*: (S1 ('MetaSel ('Just "optCompletenessCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optUniverseCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "optOmegaInOmega") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optSubtyping") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)) :*: S1 ('MetaSel ('Just "optCumulativity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((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 Bool) :*: S1 ('MetaSel ('Just "optUniversePolymorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optIrrelevantProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optExperimentalIrrelevance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optWithoutK") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (WithDefault 'False)))) :*: ((S1 ('MetaSel ('Just "optCopatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPatternMatching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optExactSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optEta") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))) :*: ((((S1 ('MetaSel ('Just "optForcing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optProjectionLike") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optRewriting") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optCubical") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Cubical)) :*: S1 ('MetaSel ('Just "optGuarded") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optFirstOrder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPostfixProjections") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optKeepPatternVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optInstanceSearchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "optOverlappingInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optQualifiedInstances") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optInversionMaxDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "optSafe") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optDoubleCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "optSyntacticEquality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optWarningMode") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WarningMode) :*: S1 ('MetaSel ('Just "optCompileNoMain") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :*: ((S1 ('MetaSel ('Just "optCaching") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optCountClusters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optAutoInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optPrintPatternSynonyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :*: ((S1 ('MetaSel ('Just "optFastReduce") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "optCallByName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optConfluenceCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ConfluenceCheck)))) :*: ((S1 ('MetaSel ('Just "optFlatSplit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optImportSorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "optAllowExec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "optShowIdentitySubstitutions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))))

type OptionsPragma = [String] Source #

The options from an `OPTIONS` pragma.

In the future it might be nice to switch to a more structured representation. Note that, currently, there is not a one-to-one correspondence between list elements and options.

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

type OptM = Except String Source #

runOptM :: Monad m => OptM opts -> m (Either String opts) Source #

data OptDescr a Source #

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

Instances details

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

data ArgDescr a Source #

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

Instances details

Functor ArgDescr | Since: base-4.6.0.0
Instance details Defined in System.Console.GetOpt Methods fmap :: (a -> b) -> ArgDescr a -> ArgDescr b Source # (<$) :: a -> ArgDescr b -> ArgDescr a Source #

type Verbosity = Trie VerboseKey VerboseLevel Source #

type VerboseKey = String Source #

type VerboseLevel = Int Source #

data WarningMode Source #

A `WarningMode` has two components: a set of warnings to be displayed and a flag stating whether warnings should be turned into fatal errors.

Constructors

WarningMode |

Fields

- _warningSet :: Set WarningName
- _warn2Error :: Bool

#### Instances

Instances details

EmbPrj WarningMode Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: WarningMode -> S Int32 Source # icod_ :: WarningMode -> S Int32 Source # value :: Int32 -> R WarningMode Source #
Generic WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Associated Types type Rep WarningMode :: Type -> Type Source # Methods from :: WarningMode -> Rep WarningMode x Source # to :: Rep WarningMode x -> WarningMode Source #
Show WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods showsPrec :: Int -> WarningMode -> ShowS Source # show :: WarningMode -> String Source # showList :: [WarningMode] -> ShowS Source #
NFData WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods rnf :: WarningMode -> () Source #
Eq WarningMode Source # |
Instance details Defined in Agda.Interaction.Options.Warnings Methods (==) :: WarningMode -> WarningMode -> Bool Source # (/=) :: WarningMode -> WarningMode -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "WarningMode" 'PrefixI 'True) (S1 ('MetaSel ('Just "_warningSet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set WarningName)) :*: S1 ('MetaSel ('Just "_warn2Error") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))

data ConfluenceCheck Source #

Constructors

LocalConfluenceCheck |
GlobalConfluenceCheck |

#### Instances

Instances details

EmbPrj ConfluenceCheck Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ConfluenceCheck -> S Int32 Source # icod_ :: ConfluenceCheck -> S Int32 Source # value :: Int32 -> R ConfluenceCheck Source #
Generic ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Base Associated Types type Rep ConfluenceCheck :: Type -> Type Source # Methods from :: ConfluenceCheck -> Rep ConfluenceCheck x Source # to :: Rep ConfluenceCheck x -> ConfluenceCheck Source #
Show ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods showsPrec :: Int -> ConfluenceCheck -> ShowS Source # show :: ConfluenceCheck -> String Source # showList :: [ConfluenceCheck] -> ShowS Source #
NFData ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods rnf :: ConfluenceCheck -> () Source #
Eq ConfluenceCheck Source # |
Instance details Defined in Agda.Interaction.Options.Base Methods (==) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source # (/=) :: ConfluenceCheck -> ConfluenceCheck -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "LocalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GlobalConfluenceCheck" 'PrefixI 'False) (U1 :: Type -> Type))

data UnicodeOrAscii Source #

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

Constructors

UnicodeOk |
AsciiOnly |

#### 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 #
Bounded UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods minBound :: UnicodeOrAscii Source # maxBound :: UnicodeOrAscii Source #
Enum UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

succ :: UnicodeOrAscii -> UnicodeOrAscii Source #

pred :: UnicodeOrAscii -> UnicodeOrAscii Source #

toEnum :: Int -> UnicodeOrAscii Source #

fromEnum :: UnicodeOrAscii -> Int Source #

enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

enumFromThenTo :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] Source #

Generic UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Associated Types type Rep UnicodeOrAscii :: Type -> Type Source # Methods from :: UnicodeOrAscii -> Rep UnicodeOrAscii x Source # to :: Rep UnicodeOrAscii x -> UnicodeOrAscii Source #
Show UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods showsPrec :: Int -> UnicodeOrAscii -> ShowS Source # show :: UnicodeOrAscii -> String Source # showList :: [UnicodeOrAscii] -> ShowS Source #
NFData UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods rnf :: UnicodeOrAscii -> () Source #
Eq UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods (==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source # (/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source #
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.2.2-7KnEKyKhaJHFPwDzdI3vIK" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

checkOpts :: Flag CommandLineOptions Source #

Checks that the given options are consistent.

parsePragmaOptions Source #

Arguments

:: [String] | 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.

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

Removes RTS options from a list of options.

defaultOptions :: CommandLineOptions Source #

defaultInteractionOptions :: PragmaOptions Source #

defaultVerbosity :: Verbosity Source #

defaultCutOff :: CutOff Source #

The default termination depth.

defaultPragmaOptions :: PragmaOptions Source #

standardOptions_ :: [OptDescr ()] Source #

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

unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String] Source #

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

restartOptions :: [(PragmaOptions -> RestartCodomain, String)] Source #

If any these options have changed, then the file will be rechecked. Boolean options are negated to mention non-default options, where possible.

infectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

An infective option is an option that if used in one module, must be used in all modules that depend on this module.

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.

coinfectiveOptions :: [(PragmaOptions -> Bool, String)] Source #

A coinfective option is an option that if used in one module, must be used in all modules that this module depends on.

safeFlag :: Flag PragmaOptions Source #

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

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

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

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

inputFlag :: FilePath -> Flag CommandLineOptions Source #

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

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

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

getOptSimple Source #

Arguments

:: [String] | command line argument words
-> [OptDescr (Flag opts)] | options handlers
-> (String -> Flag opts) | handler of non-options (only one is allowed)
-> Flag opts | combined opts data structure transformer

Simple interface for System.Console.GetOpt Could be moved to Agda.Utils.Options (does not exist yet)

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

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

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

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

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

#### Instances

Instances details

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