    {-# LANGUAGE CPP       #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE PartialTypeSignatures #-}

    {-# OPTIONS_GHC -Wno-partial-type-signatures #-}
    {-# OPTIONS_GHC -Wno-missing-signatures #-}

    module Agda.Interaction.Options.Base
        ( CommandLineOptions(..)
        , PragmaOptions(..)
        , OptionError
        , OptionWarning(..), optionWarningName
        , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
        , Verbosity, VerboseKey, VerboseLevel
        , ConfluenceCheck(..)
        , DiagnosticsColours(..)
        , EmacsModeCommand(..)
        , PrintAgdaVersion(..)
        , UnicodeOrAscii(..)
        , WarningMode(..)
        , checkOpts
        , parsePragmaOptions
        , parsePluginOptions
        , parseVerboseKey
        , stripRTS
        , defaultOptions
        , defaultInteractionOptions
        , defaultCutOff
        , defaultPragmaOptions
        , standardOptions_
        , unsafePragmaOptions
        , recheckBecausePragmaOptionsChanged
        , InfectiveCoinfective(..)
        , InfectiveCoinfectiveOption(..)
        , infectiveCoinfectiveOptions
        , ImpliedPragmaOption(..)
        , impliedPragmaOptions
        , safeFlag
        , mapFlag
        , usage
        -- Reused by PandocAgda
        , inputFlag
        , standardOptions, deadStandardOptions
        , getOptSimple
        -- * Lenses for 'PragmaOptions'
        , lensOptShowImplicit
        , lensOptShowIrrelevant
        , lensOptUseUnicode
        , lensOptVerbose
        , lensOptProfiling
        , lensOptProp
        , lensOptLevelUniverse
        , lensOptTwoLevel
        , lensOptAllowUnsolved
        , lensOptAllowIncompleteMatch
        , lensOptPositivityCheck
        , lensOptTerminationCheck
        , lensOptTerminationDepth
        , lensOptUniverseCheck, lensOptNoUniverseCheck
        , lensOptOmegaInOmega
        , lensOptCumulativity
        , lensOptSizedTypes
        , lensOptGuardedness
        , lensOptInjectiveTypeConstructors
        , lensOptUniversePolymorphism
        , lensOptIrrelevantProjections
        , lensOptExperimentalIrrelevance
        , lensOptExperimentalLazyInstances
        , lensOptWithoutK
        , lensOptCubicalCompatible
        , lensOptCopatterns
        , lensOptPatternMatching
        , lensOptExactSplit
        , lensOptHiddenArgumentPuns
        , lensOptEta
        , lensOptForcing
        , lensOptProjectionLike
        , lensOptErasure
        , lensOptErasedMatches
        , lensOptEraseRecordParameters
        , lensOptRewriting
        , lensOptCubical
        , lensOptGuarded
        , lensOptFirstOrder
        , lensOptRequireUniqueMetaSolutions
        , lensOptPostfixProjections
        , lensOptKeepPatternVariables
        , lensOptInferAbsurdClauses
        , lensOptInstanceSearchDepth
        , lensOptBacktrackingInstances
        , lensOptQualifiedInstances
        , lensOptInversionMaxDepth
        , lensOptSafe
        , lensOptDoubleCheck
        , lensOptSyntacticEquality
        , lensOptWarningMode
        , lensOptCompileMain
        , lensOptCaching
        , lensOptCountClusters
        , lensOptAutoInline
        , lensOptPrintPatternSynonyms
        , lensOptFastReduce
        , lensOptCallByName
        , lensOptConfluenceCheck
        , lensOptCohesion
        , lensOptFlatSplit
        , lensOptPolarity
        , lensOptImportSorts
        , lensOptLoadPrimitives
        , lensOptAllowExec
        , lensOptSaveMetas
        , lensOptShowIdentitySubstitutions
        , lensOptKeepCoveringClauses
        -- * Boolean accessors to 'PragmaOptions' collapsing default
        , optShowImplicit
        , optShowGeneralized
        , optShowIrrelevant
        , optProp
        , optLevelUniverse
        , optTwoLevel
        , optAllowUnsolved
        , optAllowIncompleteMatch
        , optPositivityCheck
        , optTerminationCheck
        , optUniverseCheck
        , optOmegaInOmega
        , optCumulativity
        , optSizedTypes
        , optGuardedness
        , optInjectiveTypeConstructors
        , optUniversePolymorphism
        , optIrrelevantProjections
        , optExperimentalIrrelevance
        , optWithoutK
        , optCubicalCompatible
        , optCopatterns
        , optPatternMatching
        , optHiddenArgumentPuns
        , optEta
        , optForcing
        , optProjectionLike
        , optErasure
        , optErasedMatches
        , optEraseRecordParameters
        , optRewriting
        , optGuarded
        , optFirstOrder
        , optRequireUniqueMetaSolutions
        , optPostfixProjections
        , optKeepPatternVariables
        , optInferAbsurdClauses
        , optBacktrackingInstances
        , optQualifiedInstances
        , optSafe
        , optDoubleCheck
        , optCompileNoMain
        , optCaching
        , optCountClusters
        , optAutoInline
        , optPrintPatternSynonyms
        , optFastReduce
        , optCallByName
        , optCohesion
        , optFlatSplit
        , optPolarity
        , optImportSorts
        , optLoadPrimitives
        , optAllowExec
        , optSaveMetas
        , optShowIdentitySubstitutions
        , optKeepCoveringClauses
        , optLargeIndices
        , optForcedArgumentRecursion
        -- * Non-boolean accessors to 'PragmaOptions'
        , optConfluenceCheck
        , optCubical
        , optInstanceSearchDepth
        , optInversionMaxDepth
        , optProfiling
        , optSyntacticEquality
        , optTerminationDepth
        , optUseUnicode
        , optVerbose
        , optWarningMode
        ) where

    import Prelude hiding ( null, not, (&&), (||) )

    import Control.DeepSeq
    import Control.Monad        ( (>=>), when, unless, void )
    import Control.Monad.Except ( ExceptT, MonadError(throwError), runExceptT )
    import Control.Monad.Writer ( Writer, runWriter, MonadWriter(..) )

    import Data.Function            ( (&) )
    import Data.List                ( intercalate )
    import Data.Maybe
    import Data.Map                 ( Map )
    import qualified Data.Map as Map
    import Data.Set                 ( Set )
    import qualified Data.Set as Set
    import qualified Data.Text as T

    import GHC.Generics (Generic)

    import Agda.Utils.GetOpt        ( getOpt', usageInfo, ArgOrder(ReturnInOrder)
                                    , OptDescr(..), ArgDescr(..)
                                    )
    import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)

    import Text.EditDistance
    import Text.Read                ( readMaybe )

    import Agda.Termination.CutOff  ( CutOff(..), defaultCutOff )

    import Agda.Interaction.Library ( ExeName, LibName, OptionsPragma(..), parseLibName )
    import Agda.Interaction.Options.Help
      ( Help(HelpFor, GeneralHelp)
      , string2HelpTopic
      , allHelpTopics
      , helpTopicUsage
      )
    import Agda.Interaction.Options.Types
    import Agda.Interaction.Options.Warnings

    import Agda.Syntax.Concrete.Glyph ( unsafeSetUnicodeOrAscii, UnicodeOrAscii(..) )
    import Agda.Syntax.Common (Cubical(..))
    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)

    import qualified Agda.Setup.EmacsMode as EmacsMode

    import Agda.Utils.Boolean
    import Agda.Utils.FileName      ( AbsolutePath )
    import Agda.Utils.Function      ( applyWhen, applyUnless )
    import Agda.Utils.Functor       ( (<&>) )
    import Agda.Utils.Lens          ( Lens', (^.), over, set )
    import Agda.Utils.List          ( headWithDefault, initLast1 )
    import Agda.Utils.List1         ( List1, String1, pattern (:|), toList )
    import qualified Agda.Utils.List1        as List1
    import qualified Agda.Utils.Maybe.Strict as Strict
    import Agda.Utils.Monad         ( tell1 )
    import Agda.Utils.Null
    import Agda.Utils.ProfileOptions
    import Agda.Utils.String        ( unwords1 )
    import qualified Agda.Utils.String       as String
    import Agda.Utils.Trie          ( Trie )
    import qualified Agda.Utils.Trie as Trie
    import Agda.Utils.TypeLits
    import Agda.Utils.WithDefault

    import Agda.Utils.Impossible

    import Agda.Version

    parseVerboseKey :: VerboseKey -> [VerboseKeyItem]
    parseVerboseKey :: String -> [VerboseKeyItem]
    parseVerboseKey = (Char -> Bool) -> String -> [VerboseKeyItem]
    forall a. (a -> Bool) -> [a] -> [List1 a]
    List1.wordsBy (Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Char
    '.', Char
    ':'])

    data ImpliedPragmaOption where
      ImpliesPragmaOption
        :: String -> Bool -> (PragmaOptions -> WithDefault a)
        -> String -> Bool -> (PragmaOptions -> WithDefault b)
        -> ImpliedPragmaOption
        -- ^ The first option having the given value implies the second option having its given value.
        --   For instance, `ImpliesPragmaOption "lossy-unification" True _optFirstOrder
        --                                      "require-unique-meta-solutions" False _optRequireUniqueMetaSolutions`
        --   encodes the fact that --lossy-unification implies --no-require-unique-meta-solutions.

    impliedPragmaOptions :: [ImpliedPragmaOption]
    impliedPragmaOptions :: [ImpliedPragmaOption]
    impliedPragmaOptions =
      [ (String
    "erase-record-parameters", PragmaOptions -> WithDefault 'False
    _optEraseRecordParameters) (String, PragmaOptions -> WithDefault 'False)
    -> (String, PragmaOptions -> WithDefault 'False)
    -> ImpliedPragmaOption
    forall {a :: Bool} {b :: Bool}.
    (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    "erasure",                          PragmaOptions -> WithDefault 'False
    _optErasure)
      , (String
    "erased-matches",          PragmaOptions -> WithDefault' Bool 'True
    _optErasedMatches)         (String, PragmaOptions -> WithDefault' Bool 'True)
    -> (String, PragmaOptions -> WithDefault 'False)
    -> ImpliedPragmaOption
    forall {a :: Bool} {b :: Bool}.
    (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    "erasure",                          PragmaOptions -> WithDefault 'False
    _optErasure)
      , (String
    "flat-split",              PragmaOptions -> WithDefault 'False
    _optFlatSplit)             (String, PragmaOptions -> WithDefault 'False)
    -> (String, PragmaOptions -> WithDefault 'False)
    -> ImpliedPragmaOption
    forall {a :: Bool} {b :: Bool}.
    (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    "cohesion",                         PragmaOptions -> WithDefault 'False
    _optCohesion)
      , (String
    "no-load-primitives",      PragmaOptions -> WithDefault' Bool 'True
    _optLoadPrimitives)        (String, PragmaOptions -> WithDefault' Bool 'True)
    -> (String, PragmaOptions -> WithDefault' Bool 'True)
    -> ImpliedPragmaOption
    forall {a :: Bool} {b :: Bool}.
    (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    "no-import-sorts",                  PragmaOptions -> WithDefault' Bool 'True
    _optImportSorts)
      , (String
    "lossy-unification",       PragmaOptions -> WithDefault 'False
    _optFirstOrder)            (String, PragmaOptions -> WithDefault 'False)
    -> (String, PragmaOptions -> WithDefault' Bool 'True)
    -> ImpliedPragmaOption
    forall {a :: Bool} {b :: Bool}.
    (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    "no-require-unique-meta-solutions", PragmaOptions -> WithDefault' Bool 'True
    _optRequireUniqueMetaSolutions)
      ]
      where
        yesOrNo :: String -> (Bool, String)
    yesOrNo (Char
    'n':Char
    'o':Char
    '-':String
    s) = (Bool
    False, String
    s)
        yesOrNo String
    s               = (Bool
    True, String
    s)
        (String
    nameA, PragmaOptions -> WithDefault a
    optA) ==> :: (String, PragmaOptions -> WithDefault a)
    -> (String, PragmaOptions -> WithDefault b) -> ImpliedPragmaOption
    ==> (String
    nameB, PragmaOptions -> WithDefault b
    optB) = String
    -> Bool
    -> (PragmaOptions -> WithDefault a)
    -> String
    -> Bool
    -> (PragmaOptions -> WithDefault b)
    -> ImpliedPragmaOption
    forall (a :: Bool) (b :: Bool).
    String
    -> Bool
    -> (PragmaOptions -> WithDefault a)
    -> String
    -> Bool
    -> (PragmaOptions -> WithDefault b)
    -> ImpliedPragmaOption
    ImpliesPragmaOption String
    stemA Bool
    valA PragmaOptions -> WithDefault a
    optA String
    stemB Bool
    valB PragmaOptions -> WithDefault b
    optB
          where
            (Bool
    valA, String
    stemA) = String -> (Bool, String)
    yesOrNo String
    nameA
            (Bool
    valB, String
    stemB) = String -> (Bool, String)
    yesOrNo String
    nameB

    -- collapse defaults
    optShowImplicit              :: PragmaOptions -> Bool
    optShowGeneralized           :: PragmaOptions -> Bool
    optShowIrrelevant            :: PragmaOptions -> Bool
    optProp                      :: PragmaOptions -> Bool
    optLevelUniverse             :: PragmaOptions -> Bool
    optTwoLevel                  :: PragmaOptions -> Bool
    optAllowUnsolved             :: PragmaOptions -> Bool
    optAllowIncompleteMatch      :: PragmaOptions -> Bool
    optPositivityCheck           :: PragmaOptions -> Bool
    optTerminationCheck          :: PragmaOptions -> Bool
    optUniverseCheck             :: PragmaOptions -> Bool
    optOmegaInOmega              :: PragmaOptions -> Bool
    optCumulativity              :: PragmaOptions -> Bool
    optSizedTypes                :: PragmaOptions -> Bool
    optGuardedness               :: PragmaOptions -> Bool
    optInjectiveTypeConstructors :: PragmaOptions -> Bool
    optUniversePolymorphism      :: PragmaOptions -> Bool
    optIrrelevantProjections     :: PragmaOptions -> Bool
    optExperimentalIrrelevance   :: PragmaOptions -> Bool
    optWithoutK                  :: PragmaOptions -> Bool
    optCubicalCompatible         :: PragmaOptions -> Bool
    optCopatterns                :: PragmaOptions -> Bool
    optPatternMatching           :: PragmaOptions -> Bool
    optHiddenArgumentPuns        :: PragmaOptions -> Bool
    optEta                       :: PragmaOptions -> Bool
    optForcing                   :: PragmaOptions -> Bool
    optProjectionLike            :: PragmaOptions -> Bool
    -- | 'optErasure' is implied by 'optEraseRecordParameters'.
    --   'optErasure' is also implied by an explicitly given `--erased-matches`.
    optErasure                   :: PragmaOptions -> Bool
    optErasedMatches             :: PragmaOptions -> Bool
    optEraseRecordParameters     :: PragmaOptions -> Bool
    optRewriting                 :: PragmaOptions -> Bool
    optGuarded                   :: PragmaOptions -> Bool
    optFirstOrder                :: PragmaOptions -> Bool
    optRequireUniqueMetaSolutions :: PragmaOptions -> Bool
    optPostfixProjections        :: PragmaOptions -> Bool
    optKeepPatternVariables      :: PragmaOptions -> Bool
    optInferAbsurdClauses        :: PragmaOptions -> Bool
    optBacktrackingInstances     :: 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' is implied by 'optFlatSplit'.
    optCohesion                  :: PragmaOptions -> Bool
    optFlatSplit                 :: PragmaOptions -> Bool
    optPolarity                  :: PragmaOptions -> Bool
    -- | 'optImportSorts' requires 'optLoadPrimitives'.
    optImportSorts               :: PragmaOptions -> Bool
    optLoadPrimitives            :: PragmaOptions -> Bool
    optAllowExec                 :: PragmaOptions -> Bool
    optSaveMetas                 :: PragmaOptions -> Bool
    optShowIdentitySubstitutions :: PragmaOptions -> Bool
    optKeepCoveringClauses       :: PragmaOptions -> Bool
    optLargeIndices              :: PragmaOptions -> Bool
    optForcedArgumentRecursion   :: PragmaOptions -> Bool

    optShowImplicit :: PragmaOptions -> Bool
    optShowImplicit              = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optShowImplicit
    optShowGeneralized :: PragmaOptions -> Bool
    optShowGeneralized           = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optShowGeneralized
    optShowIrrelevant :: PragmaOptions -> Bool
    optShowIrrelevant            = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optShowIrrelevant
    optProp :: PragmaOptions -> Bool
    optProp                      = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optProp
    optLevelUniverse :: PragmaOptions -> Bool
    optLevelUniverse             = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optLevelUniverse
    optTwoLevel :: PragmaOptions -> Bool
    optTwoLevel                  = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optTwoLevel
    optAllowUnsolved :: PragmaOptions -> Bool
    optAllowUnsolved             = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optAllowUnsolved
    optAllowIncompleteMatch :: PragmaOptions -> Bool
    optAllowIncompleteMatch      = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optAllowIncompleteMatch
    optPositivityCheck :: PragmaOptions -> Bool
    optPositivityCheck           = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optPositivityCheck
    optTerminationCheck :: PragmaOptions -> Bool
    optTerminationCheck          = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optTerminationCheck
    optUniverseCheck :: PragmaOptions -> Bool
    optUniverseCheck             = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optUniverseCheck
    optOmegaInOmega :: PragmaOptions -> Bool
    optOmegaInOmega              = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optOmegaInOmega
    optCumulativity :: PragmaOptions -> Bool
    optCumulativity              = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optCumulativity
    optSizedTypes :: PragmaOptions -> Bool
    optSizedTypes                = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optSizedTypes
    optGuardedness :: PragmaOptions -> Bool
    optGuardedness               = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optGuardedness
    optInjectiveTypeConstructors :: PragmaOptions -> Bool
    optInjectiveTypeConstructors = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optInjectiveTypeConstructors
    optUniversePolymorphism :: PragmaOptions -> Bool
    optUniversePolymorphism      = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optUniversePolymorphism
    optIrrelevantProjections :: PragmaOptions -> Bool
    optIrrelevantProjections     = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optIrrelevantProjections
    optExperimentalIrrelevance :: PragmaOptions -> Bool
    optExperimentalIrrelevance   = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optExperimentalIrrelevance
    optWithoutK :: PragmaOptions -> Bool
    optWithoutK                  = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optWithoutK
    optCubicalCompatible :: PragmaOptions -> Bool
    optCubicalCompatible         = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optCubicalCompatible
    optCopatterns :: PragmaOptions -> Bool
    optCopatterns                = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optCopatterns
    optPatternMatching :: PragmaOptions -> Bool
    optPatternMatching           = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optPatternMatching
    optHiddenArgumentPuns :: PragmaOptions -> Bool
    optHiddenArgumentPuns        = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optHiddenArgumentPuns
    optEta :: PragmaOptions -> Bool
    optEta                       = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optEta
    optForcing :: PragmaOptions -> Bool
    optForcing                   = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optForcing
    optProjectionLike :: PragmaOptions -> Bool
    optProjectionLike            = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optProjectionLike
    -- --erase-record-parameters implies --erasure
    optErasure :: PragmaOptions -> Bool
    optErasure                   = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optErasure (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    || PragmaOptions -> Bool
    optEraseRecordParameters (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    || (Bool -> WithDefault' Bool 'True
    forall a (b :: Bool). a -> WithDefault' a b
    Value Bool
    True WithDefault' Bool 'True -> WithDefault' Bool 'True -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optErasedMatches
    optErasedMatches :: PragmaOptions -> Bool
    optErasedMatches             = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optErasedMatches (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    && PragmaOptions -> Bool
    optErasure
    optEraseRecordParameters :: PragmaOptions -> Bool
    optEraseRecordParameters     = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optEraseRecordParameters
    optRewriting :: PragmaOptions -> Bool
    optRewriting                 = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optRewriting
    optGuarded :: PragmaOptions -> Bool
    optGuarded                   = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optGuarded
    optFirstOrder :: PragmaOptions -> Bool
    optFirstOrder                = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optFirstOrder
    optRequireUniqueMetaSolutions :: PragmaOptions -> Bool
    optRequireUniqueMetaSolutions = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optRequireUniqueMetaSolutions (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    && Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optFirstOrder
    -- --lossy-unification implies --no-require-unique-meta-solutions
    optPostfixProjections :: PragmaOptions -> Bool
    optPostfixProjections        = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optPostfixProjections
    optKeepPatternVariables :: PragmaOptions -> Bool
    optKeepPatternVariables      = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optKeepPatternVariables
    optInferAbsurdClauses :: PragmaOptions -> Bool
    optInferAbsurdClauses        = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optInferAbsurdClauses
    optBacktrackingInstances :: PragmaOptions -> Bool
    optBacktrackingInstances     = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optBacktrackingInstances
    optQualifiedInstances :: PragmaOptions -> Bool
    optQualifiedInstances        = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optQualifiedInstances
    optSafe :: PragmaOptions -> Bool
    optSafe                      = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optSafe
    optDoubleCheck :: PragmaOptions -> Bool
    optDoubleCheck               = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optDoubleCheck
    optCompileNoMain :: PragmaOptions -> Bool
    optCompileNoMain             = Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optCompileMain
    optCaching :: PragmaOptions -> Bool
    optCaching                   = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optCaching
    optCountClusters :: PragmaOptions -> Bool
    optCountClusters             = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optCountClusters
    optAutoInline :: PragmaOptions -> Bool
    optAutoInline                = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optAutoInline
    optPrintPatternSynonyms :: PragmaOptions -> Bool
    optPrintPatternSynonyms      = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optPrintPatternSynonyms
    optFastReduce :: PragmaOptions -> Bool
    optFastReduce                = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optFastReduce
    optCallByName :: PragmaOptions -> Bool
    optCallByName                = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optCallByName
    -- --flat-split implies --cohesion
    optCohesion :: PragmaOptions -> Bool
    optCohesion                  = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optCohesion      (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    || PragmaOptions -> Bool
    optFlatSplit
    optFlatSplit :: PragmaOptions -> Bool
    optFlatSplit                 = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optFlatSplit
    optPolarity :: PragmaOptions -> Bool
    optPolarity                  = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optPolarity
    -- --no-load-primitives implies --no-import-sorts
    optImportSorts :: PragmaOptions -> Bool
    optImportSorts               = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optImportSorts   (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    && PragmaOptions -> Bool
    optLoadPrimitives
    optLoadPrimitives :: PragmaOptions -> Bool
    optLoadPrimitives            = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optLoadPrimitives
    optAllowExec :: PragmaOptions -> Bool
    optAllowExec                 = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optAllowExec
    optSaveMetas :: PragmaOptions -> Bool
    optSaveMetas                 = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optSaveMetas
    optShowIdentitySubstitutions :: PragmaOptions -> Bool
    optShowIdentitySubstitutions = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optShowIdentitySubstitutions
    optKeepCoveringClauses :: PragmaOptions -> Bool
    optKeepCoveringClauses       = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optKeepCoveringClauses
    optLargeIndices :: PragmaOptions -> Bool
    optLargeIndices              = WithDefault 'False -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault 'False -> Bool)
    -> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault 'False
    _optLargeIndices
    optForcedArgumentRecursion :: PragmaOptions -> Bool
    optForcedArgumentRecursion   = WithDefault' Bool 'True -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' Bool 'True -> Bool)
    -> (PragmaOptions -> WithDefault' Bool 'True)
    -> PragmaOptions
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' Bool 'True
    _optForcedArgumentRecursion

    -- Collapse defaults (non-Bool)

    optUseUnicode                :: PragmaOptions -> UnicodeOrAscii
    optUseUnicode :: PragmaOptions -> UnicodeOrAscii
    optUseUnicode                = WithDefault' UnicodeOrAscii 'True -> UnicodeOrAscii
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (WithDefault' UnicodeOrAscii 'True -> UnicodeOrAscii)
    -> (PragmaOptions -> WithDefault' UnicodeOrAscii 'True)
    -> PragmaOptions
    -> UnicodeOrAscii
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> WithDefault' UnicodeOrAscii 'True
    _optUseUnicode

    -- Extra trivial accessors (keep in alphabetical order)

    optConfluenceCheck     :: PragmaOptions -> _
    optCubical             :: PragmaOptions -> _
    optInstanceSearchDepth :: PragmaOptions -> _
    optInversionMaxDepth   :: PragmaOptions -> _
    optProfiling           :: PragmaOptions -> _
    optSyntacticEquality   :: PragmaOptions -> _
    optTerminationDepth    :: PragmaOptions -> _
    optVerbose             :: PragmaOptions -> _
    optWarningMode         :: PragmaOptions -> _

    optConfluenceCheck :: PragmaOptions -> Maybe ConfluenceCheck
    optConfluenceCheck     = PragmaOptions -> Maybe ConfluenceCheck
    _optConfluenceCheck
    optCubical :: PragmaOptions -> Maybe Cubical
    optCubical             = PragmaOptions -> Maybe Cubical
    _optCubical
    optInstanceSearchDepth :: PragmaOptions -> Int
    optInstanceSearchDepth = PragmaOptions -> Int
    _optInstanceSearchDepth
    optInversionMaxDepth :: PragmaOptions -> Int
    optInversionMaxDepth   = PragmaOptions -> Int
    _optInversionMaxDepth
    optProfiling :: PragmaOptions -> ProfileOptions
    optProfiling           = PragmaOptions -> ProfileOptions
    _optProfiling
    optSyntacticEquality :: PragmaOptions -> Maybe Int
    optSyntacticEquality   = PragmaOptions -> Maybe Int
    _optSyntacticEquality
    optTerminationDepth :: PragmaOptions -> CutOff
    optTerminationDepth    = PragmaOptions -> CutOff
    _optTerminationDepth
    optVerbose :: PragmaOptions -> Verbosity
    optVerbose             = PragmaOptions -> Verbosity
    _optVerbose
    optWarningMode :: PragmaOptions -> WarningMode
    optWarningMode         = PragmaOptions -> WarningMode
    _optWarningMode

    -- Lenses for PragmaOptions
    -- N.B.: We use PartialTypeSignatures here to not repeat default values (DRY!).

    lensOptShowImplicit :: Lens' PragmaOptions _
    lensOptShowImplicit :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowImplicit WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optShowImplicit PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optShowImplicit = i }

    lensOptShowIrrelevant :: Lens' PragmaOptions _
    lensOptShowIrrelevant :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowIrrelevant WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optShowIrrelevant PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optShowIrrelevant = i }

    lensOptUseUnicode :: Lens' PragmaOptions _
    lensOptUseUnicode :: (WithDefault' UnicodeOrAscii 'True
     -> f (WithDefault' UnicodeOrAscii 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptUseUnicode WithDefault' UnicodeOrAscii 'True
    -> f (WithDefault' UnicodeOrAscii 'True)
    f PragmaOptions
    o = WithDefault' UnicodeOrAscii 'True
    -> f (WithDefault' UnicodeOrAscii 'True)
    f (PragmaOptions -> WithDefault' UnicodeOrAscii 'True
    _optUseUnicode PragmaOptions
    o) f (WithDefault' UnicodeOrAscii 'True)
    -> (WithDefault' UnicodeOrAscii 'True -> PragmaOptions)
    -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' UnicodeOrAscii 'True
    i -> PragmaOptions
    o{ _optUseUnicode = i }

    lensOptVerbose :: Lens' PragmaOptions _
    lensOptVerbose :: (Verbosity -> f Verbosity) -> PragmaOptions -> f PragmaOptions
    lensOptVerbose Verbosity -> f Verbosity
    f PragmaOptions
    o = Verbosity -> f Verbosity
    f (PragmaOptions -> Verbosity
    _optVerbose PragmaOptions
    o) f Verbosity -> (Verbosity -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Verbosity
    i -> PragmaOptions
    o{ _optVerbose = i }

    lensOptProfiling :: Lens' PragmaOptions _
    lensOptProfiling :: (ProfileOptions -> f ProfileOptions)
    -> PragmaOptions -> f PragmaOptions
    lensOptProfiling ProfileOptions -> f ProfileOptions
    f PragmaOptions
    o = ProfileOptions -> f ProfileOptions
    f (PragmaOptions -> ProfileOptions
    _optProfiling PragmaOptions
    o) f ProfileOptions
    -> (ProfileOptions -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ ProfileOptions
    i -> PragmaOptions
    o{ _optProfiling = i }

    lensOptProp :: Lens' PragmaOptions _
    lensOptProp :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptProp WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optProp PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optProp = i }

    lensOptLevelUniverse :: Lens' PragmaOptions _
    lensOptLevelUniverse :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptLevelUniverse WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optLevelUniverse PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optLevelUniverse = i }

    lensOptTwoLevel :: Lens' PragmaOptions _
    lensOptTwoLevel :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptTwoLevel WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optTwoLevel PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optTwoLevel = i }

    lensOptAllowUnsolved :: Lens' PragmaOptions _
    lensOptAllowUnsolved :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowUnsolved WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optAllowUnsolved PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optAllowUnsolved = i }

    lensOptAllowIncompleteMatch :: Lens' PragmaOptions _
    lensOptAllowIncompleteMatch :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowIncompleteMatch WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optAllowIncompleteMatch PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optAllowIncompleteMatch = i }

    lensOptPositivityCheck :: Lens' PragmaOptions _
    lensOptPositivityCheck :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPositivityCheck WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optPositivityCheck PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optPositivityCheck = i }

    lensOptTerminationCheck :: Lens' PragmaOptions _
    lensOptTerminationCheck :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptTerminationCheck WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optTerminationCheck PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optTerminationCheck = i }

    lensOptTerminationDepth :: Lens' PragmaOptions _
    lensOptTerminationDepth :: (CutOff -> f CutOff) -> PragmaOptions -> f PragmaOptions
    lensOptTerminationDepth CutOff -> f CutOff
    f PragmaOptions
    o = CutOff -> f CutOff
    f (PragmaOptions -> CutOff
    _optTerminationDepth PragmaOptions
    o) f CutOff -> (CutOff -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ CutOff
    i -> PragmaOptions
    o{ _optTerminationDepth = i }

    lensOptUniverseCheck :: Lens' PragmaOptions _
    lensOptUniverseCheck :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptUniverseCheck WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optUniverseCheck PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optUniverseCheck = i }

    lensOptNoUniverseCheck :: Lens' PragmaOptions _
    lensOptNoUniverseCheck :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptNoUniverseCheck WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f ((Bool -> Bool)
    -> WithDefault' Bool 'True -> WithDefault' Bool 'True
    forall a (b :: Bool).
    Boolean a =>
    (a -> a) -> WithDefault' a b -> WithDefault' a b
    mapValue Bool -> Bool
    forall a. Boolean a => a -> a
    not (WithDefault' Bool 'True -> WithDefault' Bool 'True)
    -> WithDefault' Bool 'True -> WithDefault' Bool 'True
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> WithDefault' Bool 'True
    _optUniverseCheck PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optUniverseCheck = mapValue not i }

    lensOptOmegaInOmega :: Lens' PragmaOptions _
    lensOptOmegaInOmega :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptOmegaInOmega WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optOmegaInOmega PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optOmegaInOmega = i }

    lensOptCumulativity :: Lens' PragmaOptions _
    lensOptCumulativity :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCumulativity WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optCumulativity PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optCumulativity = i }

    lensOptSizedTypes :: Lens' PragmaOptions _
    lensOptSizedTypes :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptSizedTypes WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optSizedTypes PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optSizedTypes = i }

    lensOptGuardedness :: Lens' PragmaOptions _
    lensOptGuardedness :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptGuardedness WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optGuardedness PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optGuardedness = i }

    lensOptInjectiveTypeConstructors :: Lens' PragmaOptions _
    lensOptInjectiveTypeConstructors :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptInjectiveTypeConstructors WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optInjectiveTypeConstructors PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optInjectiveTypeConstructors = i }

    lensOptUniversePolymorphism :: Lens' PragmaOptions _
    lensOptUniversePolymorphism :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptUniversePolymorphism WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optUniversePolymorphism PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optUniversePolymorphism = i }

    lensOptIrrelevantProjections :: Lens' PragmaOptions _
    lensOptIrrelevantProjections :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptIrrelevantProjections WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optIrrelevantProjections PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optIrrelevantProjections = i }

    lensOptExperimentalIrrelevance :: Lens' PragmaOptions _
    lensOptExperimentalIrrelevance :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExperimentalIrrelevance WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optExperimentalIrrelevance PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optExperimentalIrrelevance = i }

    lensOptWithoutK :: Lens' PragmaOptions _
    lensOptWithoutK :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptWithoutK WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optWithoutK PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optWithoutK = i }

    lensOptCubicalCompatible :: Lens' PragmaOptions _
    lensOptCubicalCompatible :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCubicalCompatible WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optCubicalCompatible PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optCubicalCompatible = i }

    lensOptCopatterns :: Lens' PragmaOptions _
    lensOptCopatterns :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCopatterns WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optCopatterns PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optCopatterns = i }

    lensOptPatternMatching :: Lens' PragmaOptions _
    lensOptPatternMatching :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPatternMatching WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optPatternMatching PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optPatternMatching = i }

    lensOptExactSplit :: Lens' PragmaOptions _
    lensOptExactSplit :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExactSplit WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optExactSplit PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optExactSplit = i }

    lensOptHiddenArgumentPuns :: Lens' PragmaOptions _
    lensOptHiddenArgumentPuns :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptHiddenArgumentPuns WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optHiddenArgumentPuns PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optHiddenArgumentPuns = i }

    lensOptEta :: Lens' PragmaOptions _
    lensOptEta :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptEta WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optEta PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optEta = i }

    lensOptForcing :: Lens' PragmaOptions _
    lensOptForcing :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptForcing WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optForcing PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optForcing = i }

    lensOptProjectionLike :: Lens' PragmaOptions _
    lensOptProjectionLike :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptProjectionLike WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optProjectionLike PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optProjectionLike = i }

    lensOptErasure :: Lens' PragmaOptions _
    lensOptErasure :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptErasure WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optErasure PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optErasure = i }

    lensOptErasedMatches :: Lens' PragmaOptions _
    lensOptErasedMatches :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptErasedMatches WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optErasedMatches PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optErasedMatches = i }

    lensOptEraseRecordParameters :: Lens' PragmaOptions _
    lensOptEraseRecordParameters :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptEraseRecordParameters WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optEraseRecordParameters PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optEraseRecordParameters = i }

    lensOptRewriting :: Lens' PragmaOptions _
    lensOptRewriting :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptRewriting WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optRewriting PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optRewriting = i }

    lensOptCubical :: Lens' PragmaOptions _
    lensOptCubical :: (Maybe Cubical -> f (Maybe Cubical))
    -> PragmaOptions -> f PragmaOptions
    lensOptCubical Maybe Cubical -> f (Maybe Cubical)
    f PragmaOptions
    o = Maybe Cubical -> f (Maybe Cubical)
    f (PragmaOptions -> Maybe Cubical
    _optCubical PragmaOptions
    o) f (Maybe Cubical)
    -> (Maybe Cubical -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Maybe Cubical
    i -> PragmaOptions
    o{ _optCubical = i }

    lensOptGuarded :: Lens' PragmaOptions _
    lensOptGuarded :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptGuarded WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optGuarded PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optGuarded = i }

    lensOptFirstOrder :: Lens' PragmaOptions _
    lensOptFirstOrder :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptFirstOrder WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optFirstOrder PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optFirstOrder = i }

    lensOptRequireUniqueMetaSolutions :: Lens' PragmaOptions _
    lensOptRequireUniqueMetaSolutions :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptRequireUniqueMetaSolutions WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optRequireUniqueMetaSolutions PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optRequireUniqueMetaSolutions = i }

    lensOptPostfixProjections :: Lens' PragmaOptions _
    lensOptPostfixProjections :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPostfixProjections WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optPostfixProjections PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optPostfixProjections = i }

    lensOptKeepPatternVariables :: Lens' PragmaOptions _
    lensOptKeepPatternVariables :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptKeepPatternVariables WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optKeepPatternVariables PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optKeepPatternVariables = i }

    lensOptInferAbsurdClauses :: Lens' PragmaOptions _
    lensOptInferAbsurdClauses :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptInferAbsurdClauses WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optInferAbsurdClauses PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optInferAbsurdClauses = i }

    lensOptInstanceSearchDepth :: Lens' PragmaOptions _
    lensOptInstanceSearchDepth :: (Int -> f Int) -> PragmaOptions -> f PragmaOptions
    lensOptInstanceSearchDepth Int -> f Int
    f PragmaOptions
    o = Int -> f Int
    f (PragmaOptions -> Int
    _optInstanceSearchDepth PragmaOptions
    o) f Int -> (Int -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Int
    i -> PragmaOptions
    o{ _optInstanceSearchDepth = i }

    lensOptBacktrackingInstances :: Lens' PragmaOptions _
    lensOptBacktrackingInstances :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptBacktrackingInstances WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optBacktrackingInstances PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optBacktrackingInstances = i }

    lensOptQualifiedInstances :: Lens' PragmaOptions _
    lensOptQualifiedInstances :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptQualifiedInstances WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optQualifiedInstances PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optQualifiedInstances = i }

    lensOptInversionMaxDepth :: Lens' PragmaOptions _
    lensOptInversionMaxDepth :: (Int -> f Int) -> PragmaOptions -> f PragmaOptions
    lensOptInversionMaxDepth Int -> f Int
    f PragmaOptions
    o = Int -> f Int
    f (PragmaOptions -> Int
    _optInversionMaxDepth PragmaOptions
    o) f Int -> (Int -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Int
    i -> PragmaOptions
    o{ _optInversionMaxDepth = i }

    lensOptSafe :: Lens' PragmaOptions _
    lensOptSafe :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptSafe WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optSafe PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optSafe = i }

    lensOptDoubleCheck :: Lens' PragmaOptions _
    lensOptDoubleCheck :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptDoubleCheck WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optDoubleCheck PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optDoubleCheck = i }

    lensOptSyntacticEquality :: Lens' PragmaOptions _
    lensOptSyntacticEquality :: (Maybe Int -> f (Maybe Int)) -> PragmaOptions -> f PragmaOptions
    lensOptSyntacticEquality Maybe Int -> f (Maybe Int)
    f PragmaOptions
    o = Maybe Int -> f (Maybe Int)
    f (PragmaOptions -> Maybe Int
    _optSyntacticEquality PragmaOptions
    o) f (Maybe Int) -> (Maybe Int -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Maybe Int
    i -> PragmaOptions
    o{ _optSyntacticEquality = i }

    lensOptWarningMode :: Lens' PragmaOptions _
    lensOptWarningMode :: (WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions
    lensOptWarningMode WarningMode -> f WarningMode
    f PragmaOptions
    o = WarningMode -> f WarningMode
    f (PragmaOptions -> WarningMode
    _optWarningMode PragmaOptions
    o) f WarningMode -> (WarningMode -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WarningMode
    i -> PragmaOptions
    o{ _optWarningMode = i }

    lensOptCompileMain :: Lens' PragmaOptions _
    lensOptCompileMain :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCompileMain WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optCompileMain PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optCompileMain = i }

    lensOptCaching :: Lens' PragmaOptions _
    lensOptCaching :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCaching WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optCaching PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optCaching = i }

    lensOptCountClusters :: Lens' PragmaOptions _
    lensOptCountClusters :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCountClusters WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optCountClusters PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optCountClusters = i }

    lensOptAutoInline :: Lens' PragmaOptions _
    lensOptAutoInline :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAutoInline WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optAutoInline PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optAutoInline = i }

    lensOptPrintPatternSynonyms :: Lens' PragmaOptions _
    lensOptPrintPatternSynonyms :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPrintPatternSynonyms WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optPrintPatternSynonyms PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optPrintPatternSynonyms = i }

    lensOptFastReduce :: Lens' PragmaOptions _
    lensOptFastReduce :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptFastReduce WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optFastReduce PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optFastReduce = i }

    lensOptCallByName :: Lens' PragmaOptions _
    lensOptCallByName :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCallByName WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optCallByName PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optCallByName = i }

    lensOptConfluenceCheck :: Lens' PragmaOptions _
    lensOptConfluenceCheck :: (Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck))
    -> PragmaOptions -> f PragmaOptions
    lensOptConfluenceCheck Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)
    f PragmaOptions
    o = Maybe ConfluenceCheck -> f (Maybe ConfluenceCheck)
    f (PragmaOptions -> Maybe ConfluenceCheck
    _optConfluenceCheck PragmaOptions
    o) f (Maybe ConfluenceCheck)
    -> (Maybe ConfluenceCheck -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ Maybe ConfluenceCheck
    i -> PragmaOptions
    o{ _optConfluenceCheck = i }

    lensOptCohesion :: Lens' PragmaOptions _
    lensOptCohesion :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCohesion WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optCohesion PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optCohesion = i }

    lensOptFlatSplit :: Lens' PragmaOptions _
    lensOptFlatSplit :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptFlatSplit WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optFlatSplit PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optFlatSplit = i }

    lensOptPolarity :: Lens' PragmaOptions _
    lensOptPolarity :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptPolarity WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optPolarity PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optPolarity = i}

    lensOptImportSorts :: Lens' PragmaOptions _
    lensOptImportSorts :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptImportSorts WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optImportSorts PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optImportSorts = i }

    lensOptLoadPrimitives :: Lens' PragmaOptions _
    lensOptLoadPrimitives :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptLoadPrimitives WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optLoadPrimitives PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optLoadPrimitives = i }

    lensOptAllowExec :: Lens' PragmaOptions _
    lensOptAllowExec :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowExec WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optAllowExec PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optAllowExec = i }

    lensOptSaveMetas :: Lens' PragmaOptions _
    lensOptSaveMetas :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptSaveMetas WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optSaveMetas PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optSaveMetas = i }

    lensOptShowIdentitySubstitutions :: Lens' PragmaOptions _
    lensOptShowIdentitySubstitutions :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowIdentitySubstitutions WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optShowIdentitySubstitutions PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optShowIdentitySubstitutions = i }

    lensOptKeepCoveringClauses :: Lens' PragmaOptions _
    lensOptKeepCoveringClauses :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptKeepCoveringClauses WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optKeepCoveringClauses PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optKeepCoveringClauses = i }

    lensOptLargeIndices :: Lens' PragmaOptions _
    lensOptLargeIndices :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptLargeIndices WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optLargeIndices PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optLargeIndices = i }

    lensOptForcedArgumentRecursion :: Lens' PragmaOptions _
    lensOptForcedArgumentRecursion :: (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptForcedArgumentRecursion WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f PragmaOptions
    o = WithDefault' Bool 'True -> f (WithDefault' Bool 'True)
    f (PragmaOptions -> WithDefault' Bool 'True
    _optForcedArgumentRecursion PragmaOptions
    o) f (WithDefault' Bool 'True)
    -> (WithDefault' Bool 'True -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault' Bool 'True
    i -> PragmaOptions
    o{ _optForcedArgumentRecursion = i }

    lensOptExperimentalLazyInstances :: Lens' PragmaOptions _
    lensOptExperimentalLazyInstances :: (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExperimentalLazyInstances WithDefault 'False -> f (WithDefault 'False)
    f PragmaOptions
    o = WithDefault 'False -> f (WithDefault 'False)
    f (PragmaOptions -> WithDefault 'False
    _optExperimentalLazyInstances PragmaOptions
    o) f (WithDefault 'False)
    -> (WithDefault 'False -> PragmaOptions) -> f PragmaOptions
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ WithDefault 'False
    i -> PragmaOptions
    o{ _optExperimentalLazyInstances = i }

    -- | Map a function over the long options. Also removes the short options.
    --   Will be used to add the plugin name to the plugin options.
    mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
    mapFlag :: forall a. (String -> String) -> OptDescr a -> OptDescr a
    mapFlag String -> String
    f (Option String
    _ [String]
    long ArgDescr a
    arg String
    descr) = String -> [String] -> ArgDescr a -> String -> OptDescr a
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] ((String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    f [String]
    long) ArgDescr a
    arg String
    descr

    defaultInteractionOptions :: PragmaOptions
    defaultInteractionOptions :: PragmaOptions
    defaultInteractionOptions = PragmaOptions
    defaultPragmaOptions

    defaultOptions :: CommandLineOptions
    defaultOptions :: CommandLineOptions
    defaultOptions = Options
      { optProgramName :: String
    optProgramName      = String
    "agda"
      , optInputFile :: Maybe String
    optInputFile             = Maybe String
    forall a. Maybe a
    Nothing
      , optIncludePaths :: [String]
    optIncludePaths          = []
      , optAbsoluteIncludePaths :: [AbsolutePath]
    optAbsoluteIncludePaths  = []
      , optLibraries :: [LibName]
    optLibraries             = []
      , optOverrideLibrariesFile :: Maybe String
    optOverrideLibrariesFile = Maybe String
    forall a. Maybe a
    Nothing
      , optDefaultLibs :: Bool
    optDefaultLibs           = Bool
    True
      , optUseLibs :: Bool
    optUseLibs               = Bool
    True
      , optTraceImports :: Integer
    optTraceImports          = Integer
    1
      , optTrustedExecutables :: Map ExeName String
    optTrustedExecutables    = Map ExeName String
    forall k a. Map k a
    Map.empty
      , optPrintAgdaDataDir :: Bool
    optPrintAgdaDataDir      = Bool
    False
      , optPrintAgdaAppDir :: Bool
    optPrintAgdaAppDir       = Bool
    False
      , optPrintVersion :: Maybe PrintAgdaVersion
    optPrintVersion          = Maybe PrintAgdaVersion
    forall a. Maybe a
    Nothing
      , optPrintHelp :: Maybe Help
    optPrintHelp             = Maybe Help
    forall a. Maybe a
    Nothing
      , optBuildLibrary :: Bool
    optBuildLibrary          = Bool
    False
      , optSetup :: Bool
    optSetup                 = Bool
    False
      , optEmacsMode :: Set EmacsModeCommand
    optEmacsMode             = Set EmacsModeCommand
    forall a. Set a
    Set.empty
      , optInteractive :: Bool
    optInteractive           = Bool
    False
      , optGHCiInteraction :: Bool
    optGHCiInteraction       = Bool
    False
      , optJSONInteraction :: Bool
    optJSONInteraction       = Bool
    False
      , optExitOnError :: Bool
    optExitOnError           = Bool
    False
      , optCompileDir :: Maybe String
    optCompileDir            = Maybe String
    forall a. Maybe a
    Nothing
      , optGenerateVimFile :: Bool
    optGenerateVimFile       = Bool
    False
      , optIgnoreInterfaces :: Bool
    optIgnoreInterfaces      = Bool
    False
      , optIgnoreAllInterfaces :: Bool
    optIgnoreAllInterfaces   = Bool
    False
      , optPragmaOptions :: PragmaOptions
    optPragmaOptions         = PragmaOptions
    defaultPragmaOptions
      , optOnlyScopeChecking :: Bool
    optOnlyScopeChecking     = Bool
    False
      , optTransliterate :: Bool
    optTransliterate         = Bool
    False
      , optDiagnosticsColour :: DiagnosticsColours
    optDiagnosticsColour     = DiagnosticsColours
    AutoColour
      }

    defaultPragmaOptions :: PragmaOptions
    defaultPragmaOptions :: PragmaOptions
    defaultPragmaOptions = PragmaOptions
      { _optShowImplicit :: WithDefault 'False
    _optShowImplicit              = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optShowGeneralized :: WithDefault' Bool 'True
    _optShowGeneralized           = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optShowIrrelevant :: WithDefault 'False
    _optShowIrrelevant            = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
    _optUseUnicode                = WithDefault' UnicodeOrAscii 'True
    forall a (b :: Bool). WithDefault' a b
    Default -- UnicodeOk
      , _optVerbose :: Verbosity
    _optVerbose                   = Verbosity
    forall a. Maybe a
    Strict.Nothing
      , _optProfiling :: ProfileOptions
    _optProfiling                 = ProfileOptions
    noProfileOptions
      , _optProp :: WithDefault 'False
    _optProp                      = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optLevelUniverse :: WithDefault 'False
    _optLevelUniverse             = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optTwoLevel :: WithDefault 'False
    _optTwoLevel                  = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optAllowUnsolved :: WithDefault 'False
    _optAllowUnsolved             = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optAllowIncompleteMatch :: WithDefault 'False
    _optAllowIncompleteMatch      = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optPositivityCheck :: WithDefault' Bool 'True
    _optPositivityCheck           = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optTerminationCheck :: WithDefault' Bool 'True
    _optTerminationCheck          = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optTerminationDepth :: CutOff
    _optTerminationDepth          = CutOff
    defaultCutOff
      , _optUniverseCheck :: WithDefault' Bool 'True
    _optUniverseCheck             = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optOmegaInOmega :: WithDefault 'False
    _optOmegaInOmega              = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCumulativity :: WithDefault 'False
    _optCumulativity              = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optSizedTypes :: WithDefault 'False
    _optSizedTypes                = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optGuardedness :: WithDefault 'False
    _optGuardedness               = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optInjectiveTypeConstructors :: WithDefault 'False
    _optInjectiveTypeConstructors = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optUniversePolymorphism :: WithDefault' Bool 'True
    _optUniversePolymorphism      = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optIrrelevantProjections :: WithDefault 'False
    _optIrrelevantProjections     = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optExperimentalIrrelevance :: WithDefault 'False
    _optExperimentalIrrelevance   = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optWithoutK :: WithDefault 'False
    _optWithoutK                  = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCubicalCompatible :: WithDefault 'False
    _optCubicalCompatible         = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCopatterns :: WithDefault' Bool 'True
    _optCopatterns                = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optPatternMatching :: WithDefault' Bool 'True
    _optPatternMatching           = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optExactSplit :: WithDefault 'False
    _optExactSplit                = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optHiddenArgumentPuns :: WithDefault 'False
    _optHiddenArgumentPuns        = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optEta :: WithDefault' Bool 'True
    _optEta                       = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optForcing :: WithDefault' Bool 'True
    _optForcing                   = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optProjectionLike :: WithDefault' Bool 'True
    _optProjectionLike            = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optErasure :: WithDefault 'False
    _optErasure                   = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optErasedMatches :: WithDefault' Bool 'True
    _optErasedMatches             = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optEraseRecordParameters :: WithDefault 'False
    _optEraseRecordParameters     = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optRewriting :: WithDefault 'False
    _optRewriting                 = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCubical :: Maybe Cubical
    _optCubical                   = Maybe Cubical
    forall a. Maybe a
    Nothing
      , _optGuarded :: WithDefault 'False
    _optGuarded                   = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optFirstOrder :: WithDefault 'False
    _optFirstOrder                = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optRequireUniqueMetaSolutions :: WithDefault' Bool 'True
    _optRequireUniqueMetaSolutions = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optPostfixProjections :: WithDefault' Bool 'True
    _optPostfixProjections        = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optKeepPatternVariables :: WithDefault' Bool 'True
    _optKeepPatternVariables      = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optInferAbsurdClauses :: WithDefault' Bool 'True
    _optInferAbsurdClauses        = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optInstanceSearchDepth :: Int
    _optInstanceSearchDepth       = Int
    500
      , _optBacktrackingInstances :: WithDefault 'False
    _optBacktrackingInstances     = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optQualifiedInstances :: WithDefault' Bool 'True
    _optQualifiedInstances        = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optInversionMaxDepth :: Int
    _optInversionMaxDepth         = Int
    50
      , _optSafe :: WithDefault 'False
    _optSafe                      = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optDoubleCheck :: WithDefault 'False
    _optDoubleCheck               = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optSyntacticEquality :: Maybe Int
    _optSyntacticEquality         = Maybe Int
    forall a. Maybe a
    Strict.Nothing
      , _optWarningMode :: WarningMode
    _optWarningMode               = WarningMode
    defaultWarningMode
      , _optCompileMain :: WithDefault' Bool 'True
    _optCompileMain               = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCaching :: WithDefault' Bool 'True
    _optCaching                   = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCountClusters :: WithDefault 'False
    _optCountClusters             = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optAutoInline :: WithDefault 'False
    _optAutoInline                = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optPrintPatternSynonyms :: WithDefault' Bool 'True
    _optPrintPatternSynonyms      = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optFastReduce :: WithDefault' Bool 'True
    _optFastReduce                = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optCallByName :: WithDefault 'False
    _optCallByName                = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optConfluenceCheck :: Maybe ConfluenceCheck
    _optConfluenceCheck           = Maybe ConfluenceCheck
    forall a. Maybe a
    Nothing
      , _optCohesion :: WithDefault 'False
    _optCohesion                  = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optFlatSplit :: WithDefault 'False
    _optFlatSplit                 = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optPolarity :: WithDefault 'False
    _optPolarity                  = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optImportSorts :: WithDefault' Bool 'True
    _optImportSorts               = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optLoadPrimitives :: WithDefault' Bool 'True
    _optLoadPrimitives            = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optAllowExec :: WithDefault 'False
    _optAllowExec                 = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optSaveMetas :: WithDefault 'False
    _optSaveMetas                 = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optShowIdentitySubstitutions :: WithDefault 'False
    _optShowIdentitySubstitutions = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optKeepCoveringClauses :: WithDefault 'False
    _optKeepCoveringClauses       = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optForcedArgumentRecursion :: WithDefault' Bool 'True
    _optForcedArgumentRecursion   = WithDefault' Bool 'True
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optLargeIndices :: WithDefault 'False
    _optLargeIndices              = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      , _optExperimentalLazyInstances :: WithDefault 'False
    _optExperimentalLazyInstances = WithDefault 'False
    forall a (b :: Bool). WithDefault' a b
    Default
      }

    -- | The options parse monad 'OptM' collects warnings that are not discarded
    --   when a fatal error occurrs
    newtype OptM a = OptM { forall a. OptM a -> ExceptT String (Writer OptionWarnings) a
    unOptM :: ExceptT OptionError (Writer OptionWarnings) a }
      deriving ((forall a b. (a -> b) -> OptM a -> OptM b)
    -> (forall a b. a -> OptM b -> OptM a) -> Functor OptM
    forall a b. a -> OptM b -> OptM a
    forall a b. (a -> b) -> OptM a -> OptM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> OptM a -> OptM b
    fmap :: forall a b. (a -> b) -> OptM a -> OptM b
    $c<$ :: forall a b. a -> OptM b -> OptM a
    <$ :: forall a b. a -> OptM b -> OptM a
    Functor, Functor OptM
    Functor OptM =>
    (forall a. a -> OptM a)
    -> (forall a b. OptM (a -> b) -> OptM a -> OptM b)
    -> (forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c)
    -> (forall a b. OptM a -> OptM b -> OptM b)
    -> (forall a b. OptM a -> OptM b -> OptM a)
    -> Applicative OptM
    forall a. a -> OptM a
    forall a b. OptM a -> OptM b -> OptM a
    forall a b. OptM a -> OptM b -> OptM b
    forall a b. OptM (a -> b) -> OptM a -> OptM b
    forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> OptM a
    pure :: forall a. a -> OptM a
    $c<*> :: forall a b. OptM (a -> b) -> OptM a -> OptM b
    <*> :: forall a b. OptM (a -> b) -> OptM a -> OptM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c
    liftA2 :: forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c
    $c*> :: forall a b. OptM a -> OptM b -> OptM b
    *> :: forall a b. OptM a -> OptM b -> OptM b
    $c<* :: forall a b. OptM a -> OptM b -> OptM a
    <* :: forall a b. OptM a -> OptM b -> OptM a
    Applicative, Applicative OptM
    Applicative OptM =>
    (forall a b. OptM a -> (a -> OptM b) -> OptM b)
    -> (forall a b. OptM a -> OptM b -> OptM b)
    -> (forall a. a -> OptM a)
    -> Monad OptM
    forall a. a -> OptM a
    forall a b. OptM a -> OptM b -> OptM b
    forall a b. OptM a -> (a -> OptM b) -> OptM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. OptM a -> (a -> OptM b) -> OptM b
    >>= :: forall a b. OptM a -> (a -> OptM b) -> OptM b
    $c>> :: forall a b. OptM a -> OptM b -> OptM b
    >> :: forall a b. OptM a -> OptM b -> OptM b
    $creturn :: forall a. a -> OptM a
    return :: forall a. a -> OptM a
    Monad, MonadError OptionError, MonadWriter OptionWarnings)

    type OptionError = String
    type OptionWarnings = [OptionWarning]

    runOptM :: OptM opts -> (Either OptionError opts, OptionWarnings)
    runOptM :: forall opts. OptM opts -> (Either String opts, OptionWarnings)
    runOptM = Writer OptionWarnings (Either String opts)
    -> (Either String opts, OptionWarnings)
    forall w a. Writer w a -> (a, w)
    runWriter (Writer OptionWarnings (Either String opts)
     -> (Either String opts, OptionWarnings))
    -> (OptM opts -> Writer OptionWarnings (Either String opts))
    -> OptM opts
    -> (Either String opts, OptionWarnings)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ExceptT String (Writer OptionWarnings) opts
    -> Writer OptionWarnings (Either String opts)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT String (Writer OptionWarnings) opts
     -> Writer OptionWarnings (Either String opts))
    -> (OptM opts -> ExceptT String (Writer OptionWarnings) opts)
    -> OptM opts
    -> Writer OptionWarnings (Either String opts)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . OptM opts -> ExceptT String (Writer OptionWarnings) opts
    forall a. OptM a -> ExceptT String (Writer OptionWarnings) a
    unOptM

    {- | @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 Flag opts = opts -> OptM opts

    -- | Warnings when parsing options.

    data OptionWarning
      = OptionRenamed { OptionWarning -> String
    oldOptionName :: String, OptionWarning -> String
    newOptionName :: String }
          -- ^ Name of option changed in a newer version of Agda.
      | WarningProblem WarningModeError
          -- ^ A problem with setting or unsetting a warning.
      deriving (Int -> OptionWarning -> String -> String
    OptionWarnings -> String -> String
    OptionWarning -> String
    (Int -> OptionWarning -> String -> String)
    -> (OptionWarning -> String)
    -> (OptionWarnings -> String -> String)
    -> Show OptionWarning
    forall a.
    (Int -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Int -> OptionWarning -> String -> String
    showsPrec :: Int -> OptionWarning -> String -> String
    $cshow :: OptionWarning -> String
    show :: OptionWarning -> String
    $cshowList :: OptionWarnings -> String -> String
    showList :: OptionWarnings -> String -> String
    Show, (forall x. OptionWarning -> Rep OptionWarning x)
    -> (forall x. Rep OptionWarning x -> OptionWarning)
    -> Generic OptionWarning
    forall x. Rep OptionWarning x -> OptionWarning
    forall x. OptionWarning -> Rep OptionWarning x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. OptionWarning -> Rep OptionWarning x
    from :: forall x. OptionWarning -> Rep OptionWarning x
    $cto :: forall x. Rep OptionWarning x -> OptionWarning
    to :: forall x. Rep OptionWarning x -> OptionWarning
    Generic)

    instance NFData OptionWarning

    instance Pretty OptionWarning where
      pretty :: OptionWarning -> Doc
    pretty = \case
        OptionRenamed String
    old String
    new -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    hsep
          [ Doc
    "Option", String -> Doc
    forall {a}. String -> Doc a
    option String
    old, Doc
    "is deprecated, please use", String -> Doc
    forall {a}. String -> Doc a
    option String
    new, Doc
    "instead" ]
        WarningProblem WarningModeError
    err -> ExeName -> Doc
    forall a. Pretty a => a -> Doc
    pretty (WarningModeError -> ExeName
    prettyWarningModeError WarningModeError
    err) Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "See --help=warning."
        where
        option :: String -> Doc a
    option = String -> Doc a
    forall {a}. String -> Doc a
    text (String -> Doc a) -> (String -> String) -> String -> Doc a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String
    "--" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++)

    optionWarningName :: OptionWarning -> WarningName
    optionWarningName :: OptionWarning -> WarningName
    optionWarningName = \case
      OptionRenamed{} -> WarningName
    OptionRenamed_
      WarningProblem{} -> WarningName
    WarningProblem_

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

    checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions
    checkOpts :: forall (m :: * -> *).
    MonadError String m =>
    CommandLineOptions -> m CommandLineOptions
    checkOpts CommandLineOptions
    opts = do
      -- NOTE: This is a temporary hold-out until --vim can be converted into a backend or plugin,
      -- whose options compatibility currently is checked in `Agda.Compiler.Backend`.
      --
      -- Additionally, note that some options checking is performed in `Agda.Main`
      -- in which the top-level frontend and backend interactors are selected.
      --
      -- Those checks are not represented here, because:
      --   - They are used solely for selecting the initial executon mode; they
      --     don't need to be checked on a per-module etc basis.
      --   - I hope/expect that the presence of those specific flags will be eventually
      --     abstracted out (like the Backends' internal flags), so that they are invisible
      --     to the rest of the type-checking system.
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (CommandLineOptions -> Bool
    optGenerateVimFile CommandLineOptions
    opts Bool -> Bool -> Bool
    forall a. Boolean a => a -> a -> a
    && CommandLineOptions -> Bool
    optOnlyScopeChecking CommandLineOptions
    opts) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        String -> m ()
    forall a. String -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> m ()) -> String -> m ()
    forall a b. (a -> b) -> a -> b
    $ String
    "The --only-scope-checking flag cannot be combined with --vim."

      (PragmaOptions -> m PragmaOptions)
    -> CommandLineOptions -> m CommandLineOptions
    forall a. LensPragmaOptions a => Lens' a PragmaOptions
    Lens' CommandLineOptions PragmaOptions
    lensPragmaOptions PragmaOptions -> m PragmaOptions
    forall (m :: * -> *).
    MonadError String m =>
    PragmaOptions -> m PragmaOptions
    checkPragmaOptions CommandLineOptions
    opts

    -- | Check for pragma option consistency and make adjustments.

    checkPragmaOptions :: MonadError OptionError m => PragmaOptions -> m PragmaOptions
    checkPragmaOptions :: forall (m :: * -> *).
    MonadError String m =>
    PragmaOptions -> m PragmaOptions
    checkPragmaOptions PragmaOptions
    opts = do

      -- Check for errors in pragma options.

      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((PragmaOptions -> Bool
    optEraseRecordParameters (PragmaOptions -> Bool)
    -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall a. Boolean a => a -> a -> a
    `butNot` PragmaOptions -> Bool
    optErasure) PragmaOptions
    opts) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        String -> m ()
    forall a. String -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError
          String
    "The option --erase-record-parameters requires the use of --erasure"

    #ifndef COUNT_CLUSTERS
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (PragmaOptions -> Bool
    optCountClusters PragmaOptions
    opts) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        String -> m ()
    forall a. String -> m a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError
          String
    "Cluster counting has not been enabled in this build of Agda."
    #endif

      -- Perform corrections in pragma options.

      PragmaOptions -> m PragmaOptions
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PragmaOptions -> m PragmaOptions)
    -> PragmaOptions -> m PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    opts

        -- -WTerminationIssue iff --termination-check
        PragmaOptions -> (PragmaOptions -> PragmaOptions) -> PragmaOptions
    forall a b. a -> (a -> b) -> b
    & WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningToOption WarningName
    TerminationIssue_ PragmaOptions -> Bool
    optTerminationCheck

        -- -WNotStrictlyPositive iff --positivity-check
        (PragmaOptions -> PragmaOptions)
    -> (PragmaOptions -> PragmaOptions)
    -> PragmaOptions
    -> PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningToOption WarningName
    NotStrictlyPositive_ PragmaOptions -> Bool
    optPositivityCheck

        -- unsolvedWarnings iff --no-allow-unsolved-metas
        (PragmaOptions -> PragmaOptions)
    -> (PragmaOptions -> PragmaOptions)
    -> PragmaOptions
    -> PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningsToOption Set WarningName
    unsolvedWarnings (Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAllowUnsolved)

        -- incompleteMatchWarnings iff --no-allow-incomplete-matches
        (PragmaOptions -> PragmaOptions)
    -> (PragmaOptions -> PragmaOptions)
    -> PragmaOptions
    -> PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningsToOption Set WarningName
    incompleteMatchWarnings (Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optAllowIncompleteMatch)

    -- | Activate warning when and only when option is on.
    conformWarningToOption ::
         WarningName
           -- ^ Warning to toggle.
      -> (PragmaOptions -> Bool)
           -- ^ Which flag to conform to?
      -> PragmaOptions
           -- ^ Options to modify.
      -> PragmaOptions
           -- ^ Modified options.
    conformWarningToOption :: WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningToOption = Set WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningsToOption (Set WarningName
     -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions)
    -> (WarningName -> Set WarningName)
    -> WarningName
    -> (PragmaOptions -> Bool)
    -> PragmaOptions
    -> PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WarningName -> Set WarningName
    forall a. a -> Set a
    Set.singleton

    -- | Activate warnings when option is on and deactivate them when option is off.
    conformWarningsToOption ::
         Set WarningName
           -- ^ Warnings to toggle.
      -> (PragmaOptions -> Bool)
           -- ^ Which flag to conform to?
      -> PragmaOptions
           -- ^ Options to modify.
      -> PragmaOptions
           -- ^ Modified options.
    conformWarningsToOption :: Set WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningsToOption Set WarningName
    ws PragmaOptions -> Bool
    f PragmaOptions
    opts =
      Lens' PragmaOptions (Set WarningName)
    -> LensMap PragmaOptions (Set WarningName)
    forall o i. Lens' o i -> LensMap o i
    over ((WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WarningMode -> f WarningMode) -> PragmaOptions -> f PragmaOptions
    lensOptWarningMode ((WarningMode -> f WarningMode)
     -> PragmaOptions -> f PragmaOptions)
    -> ((Set WarningName -> f (Set WarningName))
        -> WarningMode -> f WarningMode)
    -> (Set WarningName -> f (Set WarningName))
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Set WarningName -> f (Set WarningName))
    -> WarningMode -> f WarningMode
    Lens' WarningMode (Set WarningName)
    warningSet) (if PragmaOptions -> Bool
    f PragmaOptions
    opts then (Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set WarningName
    ws) else (Set WarningName -> Set WarningName -> Set WarningName
    forall a. Ord a => Set a -> Set a -> Set a
    Set.\\ Set WarningName
    ws)) PragmaOptions
    opts

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

    unsafePragmaOptions :: PragmaOptions -> [String]
    unsafePragmaOptions :: PragmaOptions -> [String]
    unsafePragmaOptions PragmaOptions
    opts =
      [ String
    "--allow-unsolved-metas"            | PragmaOptions -> Bool
    optAllowUnsolved PragmaOptions
    opts                             ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--allow-incomplete-matches"        | PragmaOptions -> Bool
    optAllowIncompleteMatch PragmaOptions
    opts                      ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--no-positivity-check"             | Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optPositivityCheck PragmaOptions
    opts)                     ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--no-termination-check"            | Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optTerminationCheck PragmaOptions
    opts)                    ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--type-in-type"                    | Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optUniverseCheck PragmaOptions
    opts)                       ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--omega-in-omega"                  | PragmaOptions -> Bool
    optOmegaInOmega PragmaOptions
    opts                              ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--sized-types"                     | PragmaOptions -> Bool
    optSizedTypes PragmaOptions
    opts                                ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--injective-type-constructors"     | PragmaOptions -> Bool
    optInjectiveTypeConstructors PragmaOptions
    opts                 ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--irrelevant-projections"          | PragmaOptions -> Bool
    optIrrelevantProjections PragmaOptions
    opts                     ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--experimental-irrelevance"        | PragmaOptions -> Bool
    optExperimentalIrrelevance PragmaOptions
    opts                   ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--rewriting"                       | PragmaOptions -> Bool
    optRewriting PragmaOptions
    opts                                 ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--cubical-compatible and --with-K" | PragmaOptions -> Bool
    optCubicalCompatible PragmaOptions
    opts, Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optWithoutK PragmaOptions
    opts) ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--without-K and --flat-split"      | PragmaOptions -> Bool
    optWithoutK PragmaOptions
    opts, PragmaOptions -> Bool
    optFlatSplit PragmaOptions
    opts               ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--cumulativity"                    | PragmaOptions -> Bool
    optCumulativity PragmaOptions
    opts                              ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--allow-exec"                      | PragmaOptions -> Bool
    optAllowExec PragmaOptions
    opts                                 ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--no-load-primitives"              | Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions -> Bool
    optLoadPrimitives PragmaOptions
    opts                      ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--without-K and --large-indices"   | PragmaOptions -> Bool
    optWithoutK PragmaOptions
    opts, PragmaOptions -> Bool
    optLargeIndices PragmaOptions
    opts            ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    "--large-indices and --forced-argument-recursion"
      | PragmaOptions -> Bool
    optLargeIndices PragmaOptions
    opts, PragmaOptions -> Bool
    optForcedArgumentRecursion PragmaOptions
    opts ] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      []

    -- | This function returns 'True' if the file should be rechecked.

    recheckBecausePragmaOptionsChanged
      :: PragmaOptions
         -- ^ The options that were used to check the file.
      -> PragmaOptions
         -- ^ The options that are currently in effect.
      -> Bool
    recheckBecausePragmaOptionsChanged :: PragmaOptions -> PragmaOptions -> Bool
    recheckBecausePragmaOptionsChanged PragmaOptions
    used PragmaOptions
    current =
      PragmaOptions -> PragmaOptions
    blankOut PragmaOptions
    used PragmaOptions -> PragmaOptions -> Bool
    forall a. Eq a => a -> a -> Bool
    /= PragmaOptions -> PragmaOptions
    blankOut PragmaOptions
    current
      where
      -- "Blank out" irrelevant options.
      -- It does not matter what we replace them with, so we take the null value.
      blankOut :: PragmaOptions -> PragmaOptions
    blankOut PragmaOptions
    opts = PragmaOptions
    opts
        { _optShowImplicit              = empty
        , _optShowIrrelevant            = empty
        , _optVerbose                   = empty
        , _optProfiling                 = empty
        , _optPostfixProjections        = empty
        , _optCompileMain               = empty
        , _optCaching                   = empty
        , _optCountClusters             = empty
        , _optPrintPatternSynonyms      = empty
        , _optShowIdentitySubstitutions = empty
        , _optKeepPatternVariables      = empty
        }

    -- | Descriptions of infective and coinfective options.

    data InfectiveCoinfectiveOption = ICOption
      { InfectiveCoinfectiveOption -> PragmaOptions -> Bool
    icOptionActive :: PragmaOptions -> Bool
        -- ^ Is the option active?
      , InfectiveCoinfectiveOption -> String
    icOptionDescription :: String
        -- ^ A description of the option (typically a flag that activates
        -- the option).
      , InfectiveCoinfectiveOption -> InfectiveCoinfective
    icOptionKind :: InfectiveCoinfective
        -- ^ Is the option (roughly speaking) infective or coinfective?
      , InfectiveCoinfectiveOption
    -> PragmaOptions -> PragmaOptions -> Bool
    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).
      , InfectiveCoinfectiveOption -> TopLevelModuleName -> Doc
    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.
      }

    -- | A standard infective option: If the option is active in an
    -- imported module, then it must be active in the current module.

    infectiveOption
      :: (PragmaOptions -> Bool)
         -- ^ Is the option active?
      -> String
        -- ^ A description of the option.
      -> InfectiveCoinfectiveOption
    infectiveOption :: (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    opt String
    s = ICOption
      { icOptionActive :: PragmaOptions -> Bool
    icOptionActive      = PragmaOptions -> Bool
    opt
      , icOptionDescription :: String
    icOptionDescription = String
    s
      , icOptionKind :: InfectiveCoinfective
    icOptionKind        = InfectiveCoinfective
    Infective
      , icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
    icOptionOK          = \PragmaOptions
    current PragmaOptions
    imported ->
                               PragmaOptions -> Bool
    opt PragmaOptions
    imported Bool -> Bool -> Bool
    forall a. Ord a => a -> a -> Bool
    <= PragmaOptions -> Bool
    opt PragmaOptions
    current
      , icOptionWarning :: TopLevelModuleName -> Doc
    icOptionWarning     = \TopLevelModuleName
    m -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Importing module" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [TopLevelModuleName -> Doc
    forall a. Pretty a => a -> Doc
    pretty TopLevelModuleName
    m] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [Doc]
    pwords String
    "using the" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
          [String -> Doc
    forall {a}. String -> Doc a
    text String
    s] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ String -> [Doc]
    pwords String
    "flag from a module which does not."
      }

    -- | A standard coinfective option: If the option is active in the
    -- current module, then it must be active in all imported modules.

    coinfectiveOption
      :: (PragmaOptions -> Bool)
         -- ^ Is the option active?
      -> String
        -- ^ A description of the option.
      -> InfectiveCoinfectiveOption
    coinfectiveOption :: (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption PragmaOptions -> Bool
    opt String
    s = ICOption
      { icOptionActive :: PragmaOptions -> Bool
    icOptionActive      = PragmaOptions -> Bool
    opt
      , icOptionDescription :: String
    icOptionDescription = String
    s
      , icOptionKind :: InfectiveCoinfective
    icOptionKind        = InfectiveCoinfective
    Coinfective
      , icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
    icOptionOK          = \PragmaOptions
    current PragmaOptions
    imported ->
                               PragmaOptions -> Bool
    opt PragmaOptions
    current Bool -> Bool -> Bool
    forall a. Ord a => a -> a -> Bool
    <= PragmaOptions -> Bool
    opt PragmaOptions
    imported
      , icOptionWarning :: TopLevelModuleName -> Doc
    icOptionWarning     = \TopLevelModuleName
    m -> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    fsep ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $
          String -> [Doc]
    pwords String
    "Importing module" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [TopLevelModuleName -> Doc
    forall a. Pretty a => a -> Doc
    pretty TopLevelModuleName
    m] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
          String -> [Doc]
    pwords String
    "not using the" [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ [String -> Doc
    forall {a}. String -> Doc a
    text String
    s] [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++
          String -> [Doc]
    pwords String
    "flag from a module which does."
      }

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

    infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption]
    infectiveCoinfectiveOptions :: [InfectiveCoinfectiveOption]
    infectiveCoinfectiveOptions =
      [ (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption PragmaOptions -> Bool
    optSafe                 String
    "--safe"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption PragmaOptions -> Bool
    optWithoutK             String
    "--without-K"
      , InfectiveCoinfectiveOption
    cubicalCompatible
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption (Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optUniversePolymorphism)
                                                  String
    "--no-universe-polymorphism"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption (Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Bool
    optCumulativity) String
    "--no-cumulativity"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption PragmaOptions -> Bool
    optLevelUniverse        String
    "--level-universe"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption (Maybe Cubical -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Cubical -> Bool)
    -> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PragmaOptions -> Maybe Cubical
    optCubical)     String
    "--cubical/--erased-cubical"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optGuarded                String
    "--guarded"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optProp                   String
    "--prop"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optTwoLevel               String
    "--two-level"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optRewriting              String
    "--rewriting"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optSizedTypes             String
    "--sized-types"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optGuardedness            String
    "--guardedness"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optFlatSplit              String
    "--flat-split"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optPolarity               String
    "--polarity"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optCohesion               String
    "--cohesion"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optErasure                String
    "--erasure"
      , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    infectiveOption PragmaOptions -> Bool
    optErasedMatches          String
    "--erased-matches"
      ]
      where
      cubicalCompatible :: InfectiveCoinfectiveOption
    cubicalCompatible =
        ((PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
    coinfectiveOption PragmaOptions -> Bool
    optCubicalCompatible String
    "--cubical-compatible")
          { icOptionOK = \PragmaOptions
    current PragmaOptions
    imported ->
            -- One must use --cubical-compatible in the imported module if
            -- it is used in the current module, except if the current
            -- module also uses --with-K and not --safe, and the imported
            -- module uses --with-K.
            if PragmaOptions -> Bool
    optCubicalCompatible PragmaOptions
    current
            then PragmaOptions -> Bool
    optCubicalCompatible PragmaOptions
    imported
                   Bool -> Bool -> Bool
    forall a. Boolean a => a -> a -> a
    ||
                 Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optWithoutK PragmaOptions
    imported)
                   Bool -> Bool -> Bool
    forall a. Boolean a => a -> a -> a
    &&
                 Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optWithoutK PragmaOptions
    current)
                   Bool -> Bool -> Bool
    forall a. Boolean a => a -> a -> a
    &&
                 Bool -> Bool
    forall a. Boolean a => a -> a
    not (PragmaOptions -> Bool
    optSafe PragmaOptions
    current)
            else Bool
    True
          }

    inputFlag :: FilePath -> Flag CommandLineOptions
    inputFlag :: String -> Flag CommandLineOptions
    inputFlag String
    f CommandLineOptions
    o =
        case CommandLineOptions -> Maybe String
    optInputFile CommandLineOptions
    o of
            Maybe String
    Nothing  -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optInputFile = Just f }
            Just String
    _   -> String -> OptM CommandLineOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "only one input file allowed"

    printAgdaDataDirFlag :: Flag CommandLineOptions
    printAgdaDataDirFlag :: Flag CommandLineOptions
    printAgdaDataDirFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintAgdaDataDir = True }

    printAgdaAppDirFlag :: Flag CommandLineOptions
    printAgdaAppDirFlag :: Flag CommandLineOptions
    printAgdaAppDirFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintAgdaAppDir = True }

    setupFlag :: Flag CommandLineOptions
    setupFlag :: Flag CommandLineOptions
    setupFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optSetup = True }

    versionFlag :: Flag CommandLineOptions
    versionFlag :: Flag CommandLineOptions
    versionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintVersion = Just PrintAgdaVersion }

    numericVersionFlag :: Flag CommandLineOptions
    numericVersionFlag :: Flag CommandLineOptions
    numericVersionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintVersion = Just PrintAgdaNumericVersion }

    helpFlag :: Maybe String -> Flag CommandLineOptions
    helpFlag :: Maybe String -> Flag CommandLineOptions
    helpFlag Maybe String
    Nothing    CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintHelp = Just GeneralHelp }
    helpFlag (Just String
    str) CommandLineOptions
    o = case String -> Maybe HelpTopic
    string2HelpTopic String
    str of
      Just HelpTopic
    hpt -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optPrintHelp = Just (HelpFor hpt) }
      Maybe HelpTopic
    Nothing -> String -> OptM CommandLineOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM CommandLineOptions)
    -> String -> OptM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
        [ String
    "unknown help topic ", String
    str, String
    " (", String -> String
    printHelpTopics String
    "topic", String
    ")" ]

    -- | Helper to explain @--help@.
    printHelpTopics :: String -> String
    printHelpTopics :: String -> String
    printHelpTopics String
    mvar = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ String
    "available"
      , String -> String -> (String -> String) -> String
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull String
    mvar String
    "" {-else-} \ String
    topic -> String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [(String, HelpTopic)] -> String -> String
    forall a. Sized a => a -> String -> String
    String.pluralS [(String, HelpTopic)]
    allHelpTopics String
    topic
      , String
    ": "
      , String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ ((String, HelpTopic) -> String)
    -> [(String, HelpTopic)] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, HelpTopic) -> String
    forall a b. (a, b) -> a
    fst [(String, HelpTopic)]
    allHelpTopics
      ]

    emacsModeFlag :: String -> Flag CommandLineOptions
    emacsModeFlag :: String -> Flag CommandLineOptions
    emacsModeFlag String
    s CommandLineOptions
    o
      | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    EmacsMode.setupFlag   = EmacsModeCommand -> OptM CommandLineOptions
    add EmacsModeCommand
    EmacsModeSetup
      | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    EmacsMode.compileFlag = EmacsModeCommand -> OptM CommandLineOptions
    add EmacsModeCommand
    EmacsModeCompile
      | String
    s String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    EmacsMode.locateFlag  = EmacsModeCommand -> OptM CommandLineOptions
    add EmacsModeCommand
    EmacsModeLocate
      | Bool
    otherwise = String -> OptM CommandLineOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM CommandLineOptions)
    -> String -> OptM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
         [ String
    "unknown emacs-mode command "
         , String
    s
         , String
    " ("
         , String -> String
    printEmacsModeCommands String
    "commands"
         , String
    ")"
         ]
      where
        add :: EmacsModeCommand -> OptM CommandLineOptions
    add EmacsModeCommand
    m = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    o{ optEmacsMode = Set.insert m $ optEmacsMode o }

    printEmacsModeCommands :: String -> String
    printEmacsModeCommands :: String -> String
    printEmacsModeCommands String
    mvar = [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ String
    "available"
      , String -> String -> (String -> String) -> String
    forall a b. Null a => a -> b -> (a -> b) -> b
    ifNull String
    mvar String
    "" {-else-} \ String
    cmd -> String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    cmd
      , String
    ": "
      , String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    emacsModeCommands
      ]

    emacsModeCommands :: [String]
    emacsModeCommands :: [String]
    emacsModeCommands = [String
    EmacsMode.setupFlag, String
    EmacsMode.compileFlag, String
    EmacsMode.locateFlag]

    safeFlag :: Flag PragmaOptions
    safeFlag :: Flag PragmaOptions
    safeFlag PragmaOptions
    o = do
      Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optSafe        = Value True
                 , _optSizedTypes  = setDefault False (_optSizedTypes o)
                 }

    syntacticEqualityFlag :: Maybe String -> Flag PragmaOptions
    syntacticEqualityFlag :: Maybe String -> Flag PragmaOptions
    syntacticEqualityFlag Maybe String
    s PragmaOptions
    o =
      case Either String (Maybe Int)
    fuel of
        Left String
    err   -> String -> OptM PragmaOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    err
        Right Maybe Int
    fuel -> Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optSyntacticEquality = fuel }
      where
      fuel :: Either String (Maybe Int)
    fuel = case Maybe String
    s of
        Maybe String
    Nothing -> Maybe Int -> Either String (Maybe Int)
    forall a b. b -> Either a b
    Right Maybe Int
    forall a. Maybe a
    Strict.Nothing
        Just String
    s  -> case String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s of
          Just Int
    n | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    0 -> Maybe Int -> Either String (Maybe Int)
    forall a b. b -> Either a b
    Right (Int -> Maybe Int
    forall a. a -> Maybe a
    Strict.Just Int
    n)
          Maybe Int
    _               -> String -> Either String (Maybe Int)
    forall a b. a -> Either a b
    Left (String -> Either String (Maybe Int))
    -> String -> Either String (Maybe Int)
    forall a b. (a -> b) -> a -> b
    $ String
    "Not a natural number: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s

    ignoreInterfacesFlag :: Flag CommandLineOptions
    ignoreInterfacesFlag :: Flag CommandLineOptions
    ignoreInterfacesFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIgnoreInterfaces = True }

    ignoreAllInterfacesFlag :: Flag CommandLineOptions
    ignoreAllInterfacesFlag :: Flag CommandLineOptions
    ignoreAllInterfacesFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIgnoreAllInterfaces = True }

    traceImportsFlag :: Maybe String -> Flag CommandLineOptions
    traceImportsFlag :: Maybe String -> Flag CommandLineOptions
    traceImportsFlag Maybe String
    arg CommandLineOptions
    o = do
      mode <- case Maybe String
    arg of
                Maybe String
    Nothing -> Integer -> OptM Integer
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    2
                Just String
    str -> case ReadS Integer
    forall a. Read a => ReadS a
    reads String
    str :: [(Integer, String)] of
                              [(Integer
    n, String
    "")] -> Integer -> OptM Integer
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Integer
    n
                              [(Integer, String)]
    _ -> String -> OptM Integer
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM Integer) -> String -> OptM Integer
    forall a b. (a -> b) -> a -> b
    $ String
    "unknown printing option " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    str String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ". Please specify a number."
      return $ o { optTraceImports = mode }

    diagnosticsColour :: Maybe String -> Flag CommandLineOptions
    diagnosticsColour :: Maybe String -> Flag CommandLineOptions
    diagnosticsColour Maybe String
    arg CommandLineOptions
    o = case Maybe String
    arg of
      Just String
    "auto"   -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o { optDiagnosticsColour = AutoColour }
      Just String
    "always" -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o { optDiagnosticsColour = AlwaysColour }
      Just String
    "never"  -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o { optDiagnosticsColour = NeverColour }
      Just String
    str -> String -> OptM CommandLineOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM CommandLineOptions)
    -> String -> OptM CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ String
    "unknown colour option " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    str String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ". Please specify one of auto, always, or never."
      Maybe String
    Nothing -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure CommandLineOptions
    o { optDiagnosticsColour = AutoColour }

    -- | Side effect for setting '_optUseUnicode'.
    --
    unicodeOrAsciiEffect :: UnicodeOrAscii -> Flag PragmaOptions
    unicodeOrAsciiEffect :: UnicodeOrAscii -> Flag PragmaOptions
    unicodeOrAsciiEffect UnicodeOrAscii
    a PragmaOptions
    o = Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ IO PragmaOptions -> PragmaOptions
    forall a. IO a -> a
    UNSAFE.unsafePerformIO (IO PragmaOptions -> PragmaOptions)
    -> IO PragmaOptions -> PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ do
      UnicodeOrAscii -> IO ()
    unsafeSetUnicodeOrAscii UnicodeOrAscii
    a
      PragmaOptions -> IO PragmaOptions
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return PragmaOptions
    o

    ghciInteractionFlag :: Flag CommandLineOptions
    ghciInteractionFlag :: Flag CommandLineOptions
    ghciInteractionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optGHCiInteraction = True }

    jsonInteractionFlag :: Flag CommandLineOptions
    jsonInteractionFlag :: Flag CommandLineOptions
    jsonInteractionFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optJSONInteraction = True }

    interactionExitFlag :: Flag CommandLineOptions
    interactionExitFlag :: Flag CommandLineOptions
    interactionExitFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optExitOnError = True }

    vimFlag :: Flag CommandLineOptions
    vimFlag :: Flag CommandLineOptions
    vimFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optGenerateVimFile = True }

    onlyScopeCheckingFlag :: Flag CommandLineOptions
    onlyScopeCheckingFlag :: Flag CommandLineOptions
    onlyScopeCheckingFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optOnlyScopeChecking = True }

    transliterateFlag :: Flag CommandLineOptions
    transliterateFlag :: Flag CommandLineOptions
    transliterateFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optTransliterate = True }

    withKFlag :: Flag PragmaOptions
    withKFlag :: Flag PragmaOptions
    withKFlag =
      -- with-K is the opposite of --without-K, so collapse default when disabling --without-K
      (WithDefault 'False -> OptM (WithDefault 'False))
    -> Flag PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptWithoutK ((Bool -> OptM Bool)
    -> WithDefault 'False -> OptM (WithDefault 'False)
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault 'False) Bool
    lensCollapseDefault ((Bool -> OptM Bool)
     -> WithDefault 'False -> OptM (WithDefault 'False))
    -> (Bool -> OptM Bool)
    -> WithDefault 'False
    -> OptM (WithDefault 'False)
    forall a b. (a -> b) -> a -> b
    $ OptM Bool -> Bool -> OptM Bool
    forall a b. a -> b -> a
    const (OptM Bool -> Bool -> OptM Bool) -> OptM Bool -> Bool -> OptM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> OptM Bool
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False)
      Flag PragmaOptions -> Flag PragmaOptions -> Flag PragmaOptions
    forall (m :: * -> *) a b c.
    Monad m =>
    (a -> m b) -> (b -> m c) -> a -> m c
    >=>
      -- with-K only restores any unsetting of --erased-matches, so keep its default
      (WithDefault' Bool 'True -> OptM (WithDefault' Bool 'True))
    -> Flag PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptErasedMatches ((Bool -> OptM Bool)
    -> WithDefault' Bool 'True -> OptM (WithDefault' Bool 'True)
    forall a (b :: Bool).
    (Boolean a, Eq a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault' Bool 'True) Bool
    lensKeepDefault ((Bool -> OptM Bool)
     -> WithDefault' Bool 'True -> OptM (WithDefault' Bool 'True))
    -> (Bool -> OptM Bool)
    -> WithDefault' Bool 'True
    -> OptM (WithDefault' Bool 'True)
    forall a b. (a -> b) -> a -> b
    $ OptM Bool -> Bool -> OptM Bool
    forall a b. a -> b -> a
    const (OptM Bool -> Bool -> OptM Bool) -> OptM Bool -> Bool -> OptM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> OptM Bool
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    True)

    withoutKFlag :: Flag PragmaOptions
    withoutKFlag :: Flag PragmaOptions
    withoutKFlag PragmaOptions
    o = Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o
      { _optWithoutK                = Value True
      , _optFlatSplit               = setDefault False $ _optFlatSplit o
      , _optErasedMatches           = setDefault False $ _optErasedMatches o
      }

    cubicalCompatibleFlag :: Flag PragmaOptions
    cubicalCompatibleFlag :: Flag PragmaOptions
    cubicalCompatibleFlag PragmaOptions
    o =
      Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o
      { _optCubicalCompatible       = Value True
      , _optWithoutK                = setDefault True  $ _optWithoutK o
      , _optFlatSplit               = setDefault False $ _optFlatSplit o
      , _optErasedMatches           = setDefault False $ _optErasedMatches o
      }

    cubicalFlag
      :: Cubical  -- ^ Which variant of Cubical Agda?
      -> Flag PragmaOptions
    cubicalFlag :: Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    variant PragmaOptions
    o =
      Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o
      { _optCubical                 = Just variant
      , _optCubicalCompatible       = setDefault True  $ _optCubicalCompatible o
      , _optWithoutK                = setDefault True  $ _optWithoutK o
      , _optTwoLevel                = setDefault True  $ _optTwoLevel o
      , _optFlatSplit               = setDefault False $ _optFlatSplit o
      , _optErasedMatches           = setDefault False $ _optErasedMatches o
      }

    instanceDepthFlag :: String -> Flag PragmaOptions
    instanceDepthFlag :: String -> Flag PragmaOptions
    instanceDepthFlag String
    s PragmaOptions
    o = do
      d <- String -> String -> OptM Int
    integerArgument String
    "--instance-search-depth" String
    s
      return $ o { _optInstanceSearchDepth = d }

    inversionMaxDepthFlag :: String -> Flag PragmaOptions
    inversionMaxDepthFlag :: String -> Flag PragmaOptions
    inversionMaxDepthFlag String
    s PragmaOptions
    o = do
      d <- String -> String -> OptM Int
    integerArgument String
    "--inversion-max-depth" String
    s
      return $ o { _optInversionMaxDepth = d }

    interactiveFlag :: Flag CommandLineOptions
    interactiveFlag :: Flag CommandLineOptions
    interactiveFlag  CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optInteractive = True }

    compileDirFlag :: FilePath -> Flag CommandLineOptions
    compileDirFlag :: String -> Flag CommandLineOptions
    compileDirFlag String
    f CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optCompileDir = Just f }

    includeFlag :: FilePath -> Flag CommandLineOptions
    includeFlag :: String -> Flag CommandLineOptions
    includeFlag String
    d CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optIncludePaths = d : optIncludePaths o }

    libraryFlag :: String -> Flag CommandLineOptions
    libraryFlag :: String -> Flag CommandLineOptions
    libraryFlag String
    s CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optLibraries = optLibraries o ++ [parseLibName s] }

    overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
    overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
    overrideLibrariesFileFlag String
    s CommandLineOptions
    o =
      Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o
        { optOverrideLibrariesFile = Just s
        , optUseLibs = True
        }

    noDefaultLibsFlag :: Flag CommandLineOptions
    noDefaultLibsFlag :: Flag CommandLineOptions
    noDefaultLibsFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optDefaultLibs = False }

    noLibsFlag :: Flag CommandLineOptions
    noLibsFlag :: Flag CommandLineOptions
    noLibsFlag CommandLineOptions
    o = Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag CommandLineOptions -> Flag CommandLineOptions
    forall a b. (a -> b) -> a -> b
    $ CommandLineOptions
    o { optUseLibs = False }

    verboseFlag :: String -> Flag PragmaOptions
    verboseFlag :: String -> Flag PragmaOptions
    verboseFlag String
    s PragmaOptions
    o =
        do  (k,n) <- String -> OptM ([VerboseKeyItem], Int)
    parseVerbose String
    s
            return $
              o { _optVerbose =
                    Strict.Just $ Trie.insert k n $
                    case _optVerbose o of
                      Verbosity
    Strict.Nothing -> [VerboseKeyItem] -> Int -> Trie VerboseKeyItem Int
    forall k v. [k] -> v -> Trie k v
    Trie.singleton [] Int
    1
                      Strict.Just Trie VerboseKeyItem Int
    v  -> Trie VerboseKeyItem Int
    v
                }
      where
        parseVerbose :: String -> OptM ([VerboseKeyItem], VerboseLevel)
        parseVerbose :: String -> OptM ([VerboseKeyItem], Int)
    parseVerbose String
    s = case String -> [VerboseKeyItem]
    parseVerboseKey String
    s of
          []  -> OptM ([VerboseKeyItem], Int)
    forall {a}. OptM a
    usage
          VerboseKeyItem
    s0:[VerboseKeyItem]
    ss0 -> do
            let ([VerboseKeyItem]
    ss, VerboseKeyItem
    s) = VerboseKeyItem
    -> [VerboseKeyItem] -> ([VerboseKeyItem], VerboseKeyItem)
    forall a. a -> [a] -> ([a], a)
    initLast1 VerboseKeyItem
    s0 [VerboseKeyItem]
    ss0
            -- The last entry must be a number.
            n <- OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    forall {a}. OptM a
    usage Int -> OptM Int
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe (String -> Maybe Int) -> String -> Maybe Int
    forall a b. (a -> b) -> a -> b
    $ VerboseKeyItem -> [Item VerboseKeyItem]
    forall l. IsList l => l -> [Item l]
    toList VerboseKeyItem
    s
            return (ss, n)
        usage :: OptM a
    usage = String -> OptM a
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "argument to verbose should be on the form x.y.z:N or N"

    profileFlag :: String -> Flag PragmaOptions
    profileFlag :: String -> Flag PragmaOptions
    profileFlag String
    s PragmaOptions
    o =
      case String -> ProfileOptions -> Either String ProfileOptions
    addProfileOption String
    s (PragmaOptions -> ProfileOptions
    _optProfiling PragmaOptions
    o) of
        Left String
    err   -> String -> OptM PragmaOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    err
        Right ProfileOptions
    prof -> Flag PragmaOptions
    forall a. a -> OptM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure PragmaOptions
    o{ _optProfiling = prof }

    warningModeFlag :: String -> Flag PragmaOptions
    warningModeFlag :: String -> Flag PragmaOptions
    warningModeFlag String
    s PragmaOptions
    o = case String -> Either WarningModeError WarningModeUpdate
    warningModeUpdate String
    s of
      Right WarningModeUpdate
    upd -> Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optWarningMode = upd (_optWarningMode o) }
      Left WarningModeError
    err  -> PragmaOptions
    o PragmaOptions -> OptM () -> OptM PragmaOptions
    forall a b. a -> OptM b -> OptM a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ OptionWarning -> OptM ()
    forall ws w (m :: * -> *).
    (Monoid ws, Singleton w ws, MonadWriter ws m) =>
    w -> m ()
    tell1 (WarningModeError -> OptionWarning
    WarningProblem WarningModeError
    err)

    terminationDepthFlag :: String -> Flag PragmaOptions
    terminationDepthFlag :: String -> Flag PragmaOptions
    terminationDepthFlag String
    s PragmaOptions
    o =
        do k <- OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    forall {a}. OptM a
    usage Int -> OptM Int
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
           when (k < 1) $ usage -- or: turn termination checking off for 0
           return $ o { _optTerminationDepth = CutOff $ k-1 }
        where usage :: OptM a
    usage = String -> OptM a
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    "argument to termination-depth should be >= 1"

    confluenceCheckFlag :: ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag :: ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    f PragmaOptions
    o = Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optConfluenceCheck = Just f }

    noConfluenceCheckFlag :: Flag PragmaOptions
    noConfluenceCheckFlag :: Flag PragmaOptions
    noConfluenceCheckFlag PragmaOptions
    o = Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optConfluenceCheck = Nothing }

    exactSplitFlag :: Bool -> Flag PragmaOptions
    exactSplitFlag :: Bool -> Flag PragmaOptions
    exactSplitFlag Bool
    b PragmaOptions
    o = do
      Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Flag PragmaOptions -> Flag PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ Set WarningName
    -> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
    conformWarningsToOption Set WarningName
    exactSplitWarnings (Bool -> PragmaOptions -> Bool
    forall a b. a -> b -> a
    const Bool
    b)
             (PragmaOptions -> PragmaOptions) -> PragmaOptions -> PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ PragmaOptions
    o { _optExactSplit  = Value b }

    integerArgument :: String -> String -> OptM Int
    integerArgument :: String -> String -> OptM Int
    integerArgument String
    flag String
    s = OptM Int -> (Int -> OptM Int) -> Maybe Int -> OptM Int
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe OptM Int
    usage Int -> OptM Int
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Int -> OptM Int) -> Maybe Int -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe Int
    forall a. Read a => String -> Maybe a
    readMaybe String
    s
      where
      usage :: OptM Int
    usage = String -> OptM Int
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM Int) -> String -> OptM Int
    forall a b. (a -> b) -> a -> b
    $ String
    "option '" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    flag String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "' requires an integer argument"

    standardOptions :: [OptDescr (Flag CommandLineOptions)]
    standardOptions :: [OptDescr (Flag CommandLineOptions)]
    standardOptions =
        [ String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'V']  [String
    "version"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    versionFlag)
                        (String
    "print version information")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "numeric-version"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    numericVersionFlag)
                        (String
    "print version number")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    '?']  [String
    "help"]    ((Maybe String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (Maybe String -> a) -> String -> ArgDescr a
    OptArg Maybe String -> Flag CommandLineOptions
    helpFlag String
    "TOPIC")
                        (String
    "print help; " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    printHelpTopics String
    "TOPIC")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "emacs-mode"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    emacsModeFlag String
    "COMMAND") (String -> OptDescr (Flag CommandLineOptions))
    -> String -> OptDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
                        [ String
    "administer the Emacs Agda mode; "
                        , String -> String
    printEmacsModeCommands String
    "COMMANDs"
                        , String
    "; confer --help=emacs-mode"
                        ]

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "print-agda-dir"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    printAgdaDataDirFlag)
                        (String
    "print the Agda data directory")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "print-agda-app-dir"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    printAgdaAppDirFlag)
                        (String
    "print $AGDA_DIR")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "print-agda-data-dir"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    printAgdaDataDirFlag)
                        (String
    "print the Agda data directory")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "build-library"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg \ CommandLineOptions
    o -> Flag CommandLineOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return CommandLineOptions
    o{ optBuildLibrary = True })
                        String
    "build all modules included by the @.agda-lib@ file in the current directory"

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "setup"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    setupFlag)
                        (String
    "setup the Agda data directory")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'I']  [String
    "interactive"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    interactiveFlag)
                        String
    "start in interactive mode"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "interaction"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ghciInteractionFlag)
                        String
    "for use with the Emacs mode"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "interaction-json"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    jsonInteractionFlag)
                        String
    "for use with other editors such as Atom"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "interaction-exit-on-error"]
                        (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    interactionExitFlag)
                        String
    "exit if a type error is encountered"

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "compile-dir"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    compileDirFlag String
    "DIR")
                        (String
    "directory for compiler output (default: the project root)")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "trace-imports"] ((Maybe String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (Maybe String -> a) -> String -> ArgDescr a
    OptArg Maybe String -> Flag CommandLineOptions
    traceImportsFlag String
    "LEVEL")
                        (String
    "print information about accessed modules during type-checking (where LEVEL=0|1|2|3, default: 2)")

        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "vim"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    vimFlag)
                        String
    "generate Vim highlighting files"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "ignore-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ignoreInterfacesFlag)
                        String
    "ignore interface files (re-type check everything)"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'i']  [String
    "include-path"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    includeFlag String
    "DIR")
                        String
    "look for imports in DIR"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'l']  [String
    "library"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    libraryFlag String
    "LIB")
                        String
    "use library LIB"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "library-file"] ((String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag CommandLineOptions
    overrideLibrariesFileFlag String
    "FILE")
                        String
    "use FILE instead of the standard libraries file"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    noLibsFlag)
                        String
    "don't use any library files"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-default-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    noDefaultLibsFlag)
                        String
    "don't use default libraries"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "only-scope-checking"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    onlyScopeCheckingFlag)
                        String
    "only scope-check the top-level module, do not type-check it"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "transliterate"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    transliterateFlag)
                        String
    "transliterate unsupported code points when printing to stdout/stderr"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "colour", String
    "color"] ((Maybe String -> Flag CommandLineOptions)
    -> String -> ArgDescr (Flag CommandLineOptions)
    forall a. (Maybe String -> a) -> String -> ArgDescr a
    OptArg Maybe String -> Flag CommandLineOptions
    diagnosticsColour String
    "always|auto|never")
                        (String
    "whether or not to colour diagnostics output. The default is auto.")
        ] [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ (OptDescr (Flag PragmaOptions)
     -> OptDescr (Flag CommandLineOptions))
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Flag PragmaOptions -> Flag CommandLineOptions)
    -> OptDescr (Flag PragmaOptions)
    -> OptDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> OptDescr a -> OptDescr b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Flag PragmaOptions -> Flag CommandLineOptions
    forall a. LensPragmaOptions a => Lens' a PragmaOptions
    Lens' CommandLineOptions PragmaOptions
    lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
    pragmaOptions

    -- | Command line options of previous versions of Agda.
    --   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
    deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
    deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
    deadStandardOptions =
        [ String -> String -> OptDescr (Flag CommandLineOptions)
    forall a. String -> String -> OptDescr (Flag a)
    removedOption String
    "sharing"    String
    msgSharing
        , String -> String -> OptDescr (Flag CommandLineOptions)
    forall a. String -> String -> OptDescr (Flag a)
    removedOption String
    "no-sharing" String
    msgSharing
        , String -> String -> OptDescr (Flag CommandLineOptions)
    forall a. String -> String -> OptDescr (Flag a)
    removedOption String
    "local-interfaces" String
    "(in 2.8.0)"
        , String
    -> [String]
    -> ArgDescr (Flag CommandLineOptions)
    -> String
    -> OptDescr (Flag CommandLineOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "ignore-all-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
    forall a. a -> ArgDescr a
    NoArg Flag CommandLineOptions
    ignoreAllInterfacesFlag) -- not deprecated! Just hidden
                        String
    "ignore all interface files (re-type check everything, including builtin files)"
          -- https://github.com/agda/agda/issues/3522#issuecomment-461010898
          -- The option is "developer only", so it is hidden.
          -- However, it is documented in the user manual.
        ] [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a. [a] -> [a] -> [a]
    ++ (OptDescr (Flag PragmaOptions)
     -> OptDescr (Flag CommandLineOptions))
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag CommandLineOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Flag PragmaOptions -> Flag CommandLineOptions)
    -> OptDescr (Flag PragmaOptions)
    -> OptDescr (Flag CommandLineOptions)
    forall a b. (a -> b) -> OptDescr a -> OptDescr b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Flag PragmaOptions -> Flag CommandLineOptions
    forall a. LensPragmaOptions a => Lens' a PragmaOptions
    Lens' CommandLineOptions PragmaOptions
    lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions
      where
        msgSharing :: String
    msgSharing = String
    "(in favor of the Agda abstract machine)"

    -- | Construct a flag of type @WithDefault _@
    --
    pragmaFlag :: (IsBool a, KnownBool b)
      => String
           -- ^ Long option name.  Prepended with @no-@ for negative version.
      -> Lens' PragmaOptions (WithDefault' a b)
           -- ^ Field to switch.
      -> String
           -- ^ Explanation for positive option.
      -> String
           -- ^ Additional info for positive option (not repeated for negative option).
      -> Maybe String
           -- ^ Explanation for negative option.
      -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag :: forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag String
    long Lens' PragmaOptions (WithDefault' a b)
    field = String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag' String
    long (WithDefault' a b -> f (WithDefault' a b))
    -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions (WithDefault' a b)
    field (Flag PragmaOptions -> a -> Flag PragmaOptions
    forall a b. a -> b -> a
    const Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)

    -- | Construct a flag of type @WithDefault _@
    --
    pragmaFlag' :: (IsBool a, KnownBool b)
      => String
           -- ^ Long option name.  Prepended with @no-@ for negative version.
      -> Lens' PragmaOptions (WithDefault' a b)
           -- ^ Field to switch.
      -> (a -> Flag PragmaOptions)
           -- ^ Given the new value, perform additional effect (can override field setting).
      -> String
           -- ^ Explanation for positive option.
      -> String
           -- ^ Additional info for positive option (not repeated for negative option).
      -> Maybe String
           -- ^ Explanation for negative option.
      -> [OptDescr (Flag PragmaOptions)]
           -- ^ Pair of option descriptors (positive, negative)
    pragmaFlag' :: forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag' String
    long Lens' PragmaOptions (WithDefault' a b)
    field = String
    -> Lens' PragmaOptions a
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a.
    IsBool a =>
    String
    -> Lens' PragmaOptions a
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlagBool' String
    long ((WithDefault' a b -> f (WithDefault' a b))
    -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions (WithDefault' a b)
    field ((WithDefault' a b -> f (WithDefault' a b))
     -> PragmaOptions -> f PragmaOptions)
    -> ((a -> f a) -> WithDefault' a b -> f (WithDefault' a b))
    -> (a -> f a)
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> f a) -> WithDefault' a b -> f (WithDefault' a b)
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault' a b) a
    lensCollapseDefault)

    -- | Construct a flag of type 'IsBool'.
    --
    pragmaFlagBool :: (IsBool a)
      => String
           -- ^ Long option name.  Prepended with @no-@ for negative version.
      -> Lens' PragmaOptions a
           -- ^ Field to switch.
      -> String
           -- ^ Explanation for positive option.
      -> String
           -- ^ Additional info for positive option (not repeated for negative option).
      -> Maybe String
           -- ^ Explanation for negative option.
      -> [OptDescr (Flag PragmaOptions)]
    pragmaFlagBool :: forall a.
    IsBool a =>
    String
    -> Lens' PragmaOptions a
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlagBool String
    long Lens' PragmaOptions a
    field = String
    -> Lens' PragmaOptions a
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a.
    IsBool a =>
    String
    -> Lens' PragmaOptions a
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlagBool' String
    long (a -> f a) -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions a
    field (Flag PragmaOptions -> a -> Flag PragmaOptions
    forall a b. a -> b -> a
    const Flag PragmaOptions
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return)

    -- | Construct a flag of type 'IsBool' with extra effect.
    --
    pragmaFlagBool' :: IsBool a
      => String
           -- ^ Long option name.  Prepended with @no-@ for negative version.
      -> Lens' PragmaOptions a
           -- ^ Field to switch.
      -> (a -> Flag PragmaOptions)
           -- ^ Given the new value, perform additional effect (can override field setting).
      -> String
           -- ^ Explanation for positive option.
      -> String
           -- ^ Additional info for positive option (not repeated for negative option).
      -> Maybe String
           -- ^ Explanation for negative option.
      -> [OptDescr (Flag PragmaOptions)]
           -- ^ Pair of option descriptors (positive, negative)
    pragmaFlagBool' :: forall a.
    IsBool a =>
    String
    -> Lens' PragmaOptions a
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlagBool' String
    long Lens' PragmaOptions a
    field a -> Flag PragmaOptions
    effect String
    pos String
    info Maybe String
    neg =
      [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [Bool -> String -> String
    forall {b}. IsBool b => b -> String -> String
    no Bool
    b String
    long] (Bool -> ArgDescr (Flag PragmaOptions)
    flag Bool
    b) (Bool -> String -> String
    def Bool
    b (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ Bool -> String
    expl Bool
    b) | Bool
    b <- [Bool
    True,Bool
    False] ]
      where
      b0 :: a
    b0     = PragmaOptions
    defaultPragmaOptions PragmaOptions -> Lens' PragmaOptions a -> a
    forall o i. o -> Lens' o i -> i
    ^. (a -> f a) -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions a
    field
      no :: b -> String -> String
    no   b
    b = b -> (String -> String) -> String -> String
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyUnless b
    b (String
    "no-" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++)
      flag :: Bool -> ArgDescr (Flag PragmaOptions)
    flag Bool
    b = Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ a -> Flag PragmaOptions
    effect a
    a Flag PragmaOptions
    -> (PragmaOptions -> PragmaOptions) -> Flag PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Lens' PragmaOptions a -> LensSet PragmaOptions a
    forall o i. Lens' o i -> LensSet o i
    set (a -> f a) -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions a
    field a
    a
        where a :: a
    a = Bool -> a
    forall a. Boolean a => Bool -> a
    fromBool Bool
    b
      def :: Bool -> String -> String
    def  Bool
    b = Bool -> (String -> String) -> String -> String
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Bool -> a
    forall a. Boolean a => Bool -> a
    fromBool Bool
    b a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    b0) (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (default)")
      expl :: Bool -> String
    expl Bool
    b = if Bool
    b then [String] -> String
    unwords1 [String
    pos, String
    info] else String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe (String
    "do not " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    pos) Maybe String
    neg

    pragmaOptions :: [OptDescr (Flag PragmaOptions)]
    pragmaOptions :: [OptDescr (Flag PragmaOptions)]
    pragmaOptions = [[OptDescr (Flag PragmaOptions)]]
    -> [OptDescr (Flag PragmaOptions)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "show-implicit" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowImplicit
                        String
    "show implicit arguments when printing" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "show-irrelevant" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowIrrelevant
                        String
    "show irrelevant arguments when printing" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "show-identity-substitutions" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptShowIdentitySubstitutions
                        String
    "show all arguments of metavariables when printing terms" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> Lens' PragmaOptions (WithDefault' UnicodeOrAscii 'True)
    -> (UnicodeOrAscii -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> (a -> Flag PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag'     String
    "unicode" (WithDefault' UnicodeOrAscii 'True
     -> f (WithDefault' UnicodeOrAscii 'True))
    -> PragmaOptions -> f PragmaOptions
    Lens' PragmaOptions (WithDefault' UnicodeOrAscii 'True)
    lensOptUseUnicode UnicodeOrAscii -> Flag PragmaOptions
    unicodeOrAsciiEffect
                        String
    "use unicode characters when printing terms" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'v']  [String
    "verbose"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    verboseFlag String
    "N")
                        String
    "set verbosity level to N. Only has an effect if Agda was built with the \"debug\" flag."
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "profile"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    profileFlag String
    "TYPE")
                        (String
    "turn on profiling for TYPE (where TYPE=" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "|" [String]
    validProfileOptionStrings String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")")
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "allow-unsolved-metas" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowUnsolved
                        String
    "succeed and create interface file regardless of unsolved meta variables" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "allow-incomplete-matches" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowIncompleteMatch
                        String
    "succeed and create interface file regardless of incomplete pattern matches" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "positivity-check" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPositivityCheck
                        String
    "warn about not strictly positive data types" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "termination-check" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptTerminationCheck
                        String
    "warn about possibly nonterminating code" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "termination-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    terminationDepthFlag String
    "N")
                        String
    "allow termination checker to count decrease/increase upto N (default N=1)"
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "type-in-type" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptNoUniverseCheck
                        String
    "ignore universe levels"  String
    "(this makes Agda inconsistent)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "omega-in-omega" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptOmegaInOmega
                        String
    "enable typing rule Setω : Setω" String
    "(this makes Agda inconsistent)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "cumulativity" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCumulativity
                        String
    "enable subtyping of universes" String
    "(e.g. Set =< Set₁)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable subtyping of universes"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "prop" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptProp
                        String
    "enable the use of the Prop universe" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable the use of the Prop universe"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "level-universe" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptLevelUniverse
                        String
    "place type Level in a dedicated LevelUniv universe" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "two-level" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptTwoLevel
                        String
    "enable the use of SSet* universes" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "sized-types" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptSizedTypes
                        String
    "enable sized types" String
    "(inconsistent with --guardedness)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable sized types"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "cohesion" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCohesion
                        String
    "enable the cohesion modalities" String
    "(in particular @flat)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "flat-split" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptFlatSplit
                        String
    "allow splitting on `(@flat x : A)' arguments" String
    "(implies --cohesion)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "polarity" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptPolarity
                        String
    "enable the polarity modalities (@++, @mixed, etc.) and their integration in the positivity checker" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "guardedness" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptGuardedness
                        String
    "enable constructor-based guarded corecursion" String
    "(inconsistent with --sized-types)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable constructor-based guarded corecursion"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "injective-type-constructors" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptInjectiveTypeConstructors
                        String
    "enable injective type constructors" String
    "(makes Agda anti-classical and possibly inconsistent)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable injective type constructors"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "universe-polymorphism" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptUniversePolymorphism
                        String
    "enable universe polymorphism" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable universe polymorphism"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "irrelevant-projections" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptIrrelevantProjections
                        String
    "enable projection of irrelevant record fields and similar irrelevant definitions" String
    "(inconsistent)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable projection of irrelevant record fields and similar irrelevant definitions"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "experimental-irrelevance" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExperimentalIrrelevance
                        String
    "enable potentially unsound irrelevance features" String
    "(irrelevant levels, irrelevant data matching)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "with-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    withKFlag)
                        String
    "enable the K rule in pattern matching (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "cubical-compatible"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    cubicalCompatibleFlag)
                        String
    "turn on generation of auxiliary code required for --cubical, implies --without-K"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "without-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    withoutKFlag)
                        String
    "turn on checks to make code compatible with HoTT (e.g. disabling the K rule). Implies --no-flat-split."
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "copatterns" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCopatterns
                        String
    "enable definitions by copattern matching" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable definitions by copattern matching"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "pattern-matching" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPatternMatching
                        String
    "enable pattern matching" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable pattern matching completely"
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag PragmaOptions
    exactSplitFlag Bool
    True)
                        String
    "require all clauses in a definition to hold as definitional equalities (unless marked CATCHALL)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Bool -> Flag PragmaOptions
    exactSplitFlag Bool
    False)
                        String
    "do not require all clauses in a definition to hold as definitional equalities (default)"
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "hidden-argument-puns" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptHiddenArgumentPuns
                        String
    "interpret the patterns {x} and {{x}} as puns" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "eta-equality" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptEta
                        String
    "default records to eta-equality" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "default records to no-eta-equality"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "forcing" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptForcing
                        String
    "enable the forcing analysis for data constructors" String
    "(optimisation)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable the forcing analysis"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "projection-like" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptProjectionLike
                        String
    "enable the analysis whether function signatures liken those of projections" String
    "(optimisation)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable the projection-like analysis"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "erasure" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptErasure
                        String
    "enable erasure" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "erased-matches" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptErasedMatches
                        String
    "allow matching in erased positions for single-constructor types" String
    "(implies --erasure if supplied explicitly)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "erase-record-parameters" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptEraseRecordParameters
                        String
    "mark all parameters of record modules as erased" String
    "(implies --erasure)"
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "rewriting" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptRewriting
                        String
    "enable declaration and use of REWRITE rules" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable declaration and use of REWRITE rules"
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "local-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    LocalConfluenceCheck)
                        String
    "enable checking of local confluence of REWRITE rules"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ ConfluenceCheck -> Flag PragmaOptions
    confluenceCheckFlag ConfluenceCheck
    GlobalConfluenceCheck)
                        String
    "enable global confluence checking of REWRITE rules (more restrictive than --local-confluence-check)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    noConfluenceCheckFlag)
                        String
    "disable confluence checking of REWRITE rules (default)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    CFull)
                        String
    "enable cubical features (e.g. overloads lambdas for paths), implies --cubical-compatible"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "erased-cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Cubical -> Flag PragmaOptions
    cubicalFlag Cubical
    CErased)
                        String
    "enable cubical features (some only in erased settings), implies --cubical-compatible"
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "guarded" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptGuarded
                        String
    "enable @lock/@tick attributes" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable @lock/@tick attributes"
      , [OptDescr (Flag PragmaOptions)]
    lossyUnificationOption
      , [OptDescr (Flag PragmaOptions)]
    requireUniqueMetaSolutionsOptions
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "postfix-projections" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPostfixProjections
                        String
    "prefer postfix projection notation" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "prefer prefix projection notation"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "keep-pattern-variables" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptKeepPatternVariables
                        String
    "don't replace variables with dot patterns during case splitting" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "replace variables with dot patterns during case splitting"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "infer-absurd-clauses" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptInferAbsurdClauses
                        String
    "eliminate absurd clauses in case splitting and coverage checking" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "do not automatically eliminate absurd clauses in case splitting and coverage checking (can speed up type-checking)"
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "instance-search-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    instanceDepthFlag String
    "N")
                        String
    "set instance search depth to N (default: 500)"
        ]
      , [OptDescr (Flag PragmaOptions)]
    backtrackingInstancesOption
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "qualified-instances" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptQualifiedInstances
                        String
    "use instances with qualified names" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "inversion-max-depth"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    inversionMaxDepthFlag String
    "N")
                        String
    "set maximum depth for pattern match inversion to N (default: 50)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "safe"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg Flag PragmaOptions
    safeFlag)
                        String
    "disable postulates, unsafe OPTION pragmas and primEraseEquality, implies --no-sized-types"
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "double-check" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptDoubleCheck
                        String
    "enable double-checking of all terms using the internal typechecker" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable double-checking of terms"
      , [ String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "no-syntactic-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a. a -> ArgDescr a
    NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
    -> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
    forall a b. (a -> b) -> a -> b
    $ Maybe String -> Flag PragmaOptions
    syntacticEqualityFlag (String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "0"))
                        String
    "disable the syntactic equality shortcut in the conversion checker"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option []     [String
    "syntactic-equality"] ((Maybe String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (Maybe String -> a) -> String -> ArgDescr a
    OptArg Maybe String -> Flag PragmaOptions
    syntacticEqualityFlag String
    "FUEL")
                        String
    "give the syntactic equality shortcut FUEL units of fuel (default: unlimited)"
        , String
    -> [String]
    -> ArgDescr (Flag PragmaOptions)
    -> String
    -> OptDescr (Flag PragmaOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [Char
    'W']  [String
    "warning"] ((String -> Flag PragmaOptions)
    -> String -> ArgDescr (Flag PragmaOptions)
    forall a. (String -> a) -> String -> ArgDescr a
    ReqArg String -> Flag PragmaOptions
    warningModeFlag String
    "FLAG")
                        (String
    "set warning flags. See --help=warning.")
        ]
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "main" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCompileMain
                        String
    "treat the requested module as the main module of a program when compiling" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "caching" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptCaching
                        String
    "enable caching of typechecking" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable caching of typechecking"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "count-clusters" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCountClusters
                        String
    "count extended grapheme clusters when generating LaTeX"
                        (String
    "(note that this flag " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
    #ifdef COUNT_CLUSTERS
                          "is not enabled in all builds"
    #else
                          String
    "has not been enabled in this build"
    #endif
                          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " of Agda)")
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "auto-inline" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAutoInline
                        String
    "enable automatic compile-time inlining" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable automatic compile-time inlining, only definitions marked INLINE will be inlined"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "print-pattern-synonyms" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPrintPatternSynonyms
                        String
    "keep pattern synonyms when printing terms" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "expand pattern synonyms when printing terms"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "fast-reduce" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptFastReduce
                        String
    "enable reduction using the Agda Abstract Machine" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable reduction using the Agda Abstract Machine"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "call-by-name" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptCallByName
                        String
    "use call-by-name evaluation instead of call-by-need" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "use call-by-need evaluation"

      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "import-sorts" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptImportSorts
                        String
    "implicitly import Agda.Primitive using (Set; Prop) at the start of each top-level module" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable the implicit import of Agda.Primitive using (Set; Prop) at the start of each top-level module"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "load-primitives" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptLoadPrimitives
                        String
    "load primitives modules" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "disable loading of primitive modules completely (implies --no-import-sorts)"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "allow-exec" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptAllowExec
                        String
    "allow system calls to trusted executables with primExec" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "save-metas" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptSaveMetas
                        String
    "save meta-variables" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "keep-covering-clauses" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptKeepCoveringClauses
                        String
    "do not discard covering clauses" String
    "(required for some external backends)"
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "discard covering clauses"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "large-indices" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptLargeIndices
                        String
    "allow constructors with large indices" String
    ""
                        (Maybe String -> [OptDescr (Flag PragmaOptions)])
    -> Maybe String -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> a -> b
    $ String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "always check that constructor arguments live in universes compatible with that of the datatype"
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "forced-argument-recursion" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptForcedArgumentRecursion
                        String
    "allow recursion on forced constructor arguments" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      , String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag      String
    "experimental-lazy-instances" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptExperimentalLazyInstances
                        String
    "enable experimental, faster implementation of instance search" String
    ""
                        Maybe String
    forall a. Maybe a
    Nothing
      ]

    pragmaOptionDefault :: KnownBool b => (PragmaOptions -> WithDefault b) -> Bool -> String
    pragmaOptionDefault :: forall (b :: Bool).
    KnownBool b =>
    (PragmaOptions -> WithDefault b) -> Bool -> String
    pragmaOptionDefault PragmaOptions -> WithDefault b
    f Bool
    b =
      if Bool
    b Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == WithDefault b -> Bool
    forall a (b :: Bool).
    (Boolean a, KnownBool b) =>
    WithDefault' a b -> a
    collapseDefault (PragmaOptions -> WithDefault b
    f PragmaOptions
    defaultPragmaOptions) then String
    " (default)" else String
    ""

    lossyUnificationOption :: [OptDescr (Flag PragmaOptions)]
    lossyUnificationOption :: [OptDescr (Flag PragmaOptions)]
    lossyUnificationOption =
      String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag String
    "lossy-unification" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptFirstOrder
        String
    "enable heuristically unifying `f es = f es'` by unifying `es = es'`"
        String
    "even when it could lose solutions"
        Maybe String
    forall a. Maybe a
    Nothing

    requireUniqueMetaSolutionsOptions :: [OptDescr (Flag PragmaOptions)]
    requireUniqueMetaSolutionsOptions :: [OptDescr (Flag PragmaOptions)]
    requireUniqueMetaSolutionsOptions =
      String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag String
    "require-unique-meta-solutions" (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault' Bool 'True -> f (WithDefault' Bool 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptRequireUniqueMetaSolutions
        String
    "require unique solutions to meta variables"
        String
    "even when it could lose solutions"
        Maybe String
    forall a. Maybe a
    Nothing

    backtrackingInstancesOption :: [OptDescr (Flag PragmaOptions)]
    backtrackingInstancesOption :: [OptDescr (Flag PragmaOptions)]
    backtrackingInstancesOption =
      String
    -> (forall (f :: * -> *).
        Functor f =>
        (WithDefault 'False -> f (WithDefault 'False))
        -> PragmaOptions -> f PragmaOptions)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    forall a (b :: Bool).
    (IsBool a, KnownBool b) =>
    String
    -> Lens' PragmaOptions (WithDefault' a b)
    -> String
    -> String
    -> Maybe String
    -> [OptDescr (Flag PragmaOptions)]
    pragmaFlag String
    "backtracking-instance-search" (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'False -> f (WithDefault 'False))
    -> PragmaOptions -> f PragmaOptions
    lensOptBacktrackingInstances
        String
    "allow backtracking during instance search"
        String
    ""
        Maybe String
    forall a. Maybe a
    Nothing

    -- | Pragma options of previous versions of Agda.
    --   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
    deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
    deadPragmaOptions = [[OptDescr (Flag PragmaOptions)]]
    -> [OptDescr (Flag PragmaOptions)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat
      [ ((String, String) -> OptDescr (Flag PragmaOptions))
    -> [(String, String)] -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String -> String -> OptDescr (Flag PragmaOptions))
    -> (String, String) -> OptDescr (Flag PragmaOptions)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry String -> String -> OptDescr (Flag PragmaOptions)
    forall a. String -> String -> OptDescr (Flag a)
    removedOption)
        [ (String
    "guardedness-preserving-type-constructors"
          , String
    "")
        , (String
    "no-coverage-check"
          , String -> String
    inVersion String
    "2.5.1") -- see issue #1918
        , (String
    "no-sort-comparison"
          , String
    "")
        , (String
    "subtyping"
          , String -> String
    inVersion String
    "2.6.3") -- see issue #5427
        , (String
    "no-subtyping"
          , String -> String
    inVersion String
    "2.6.3") -- see issue #5427
        , (String
    "no-flat-split", String -> String
    inVersion String
    "2.6.3")  -- See issue #6263.
        ]
      , ((String, OptDescr (Flag PragmaOptions))
     -> OptDescr (Flag PragmaOptions))
    -> [(String, OptDescr (Flag PragmaOptions))]
    -> [OptDescr (Flag PragmaOptions)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String
     -> OptDescr (Flag PragmaOptions) -> OptDescr (Flag PragmaOptions))
    -> (String, OptDescr (Flag PragmaOptions))
    -> OptDescr (Flag PragmaOptions)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry String
    -> OptDescr (Flag PragmaOptions) -> OptDescr (Flag PragmaOptions)
    forall a. String -> OptDescr (Flag a) -> OptDescr (Flag a)
    renamedNoArgOption)
        [ ( String
    "experimental-lossy-unification"
          , OptDescr (Flag PragmaOptions)
    -> [OptDescr (Flag PragmaOptions)] -> OptDescr (Flag PragmaOptions)
    forall a. a -> [a] -> a
    headWithDefault OptDescr (Flag PragmaOptions)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [OptDescr (Flag PragmaOptions)]
    lossyUnificationOption
          )
        , ( String
    "overlapping-instances"
          , OptDescr (Flag PragmaOptions)
    -> [OptDescr (Flag PragmaOptions)] -> OptDescr (Flag PragmaOptions)
    forall a. a -> [a] -> a
    headWithDefault OptDescr (Flag PragmaOptions)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [OptDescr (Flag PragmaOptions)]
    backtrackingInstancesOption
          )
        ]
      ]
      where
        inVersion :: String -> String
    inVersion = (String
    "in version " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++)

    -- | Generate a dead options that just error out saying this option has been removed.
    removedOption ::
         String
           -- ^ The name of the removed option.
      -> String
           -- ^ Optional: additional remark, like in which version the option was removed.
      -> OptDescr (Flag a)
    removedOption :: forall a. String -> String -> OptDescr (Flag a)
    removedOption String
    name String
    remark = String
    -> [String] -> ArgDescr (Flag a) -> String -> OptDescr (Flag a)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    name] (Flag a -> ArgDescr (Flag a)
    forall a. a -> ArgDescr a
    NoArg (Flag a -> ArgDescr (Flag a)) -> Flag a -> ArgDescr (Flag a)
    forall a b. (a -> b) -> a -> b
    $ OptM a -> Flag a
    forall a b. a -> b -> a
    const (OptM a -> Flag a) -> OptM a -> Flag a
    forall a b. (a -> b) -> a -> b
    $ String -> OptM a
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    msg) String
    msg
      where
      msg :: String
    msg = [String] -> String
    unwords [String
    "Option", String
    "--" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    name, String
    "has been removed", String
    remark]

    -- | Generate a deprecated option that resolves to another option.
    renamedNoArgOption ::
         String
           -- ^ The deprecated long option name.
      -> OptDescr (Flag a)
           -- ^ The new option.
      -> OptDescr (Flag a)
           -- ^ The old option which additionally emits a 'RenamedOption' warning.
    renamedNoArgOption :: forall a. String -> OptDescr (Flag a) -> OptDescr (Flag a)
    renamedNoArgOption String
    old = \case
      Option String
    _ [String
    new] (NoArg Flag a
    flag) String
    description ->
        String
    -> [String] -> ArgDescr (Flag a) -> String -> OptDescr (Flag a)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    old] (Flag a -> ArgDescr (Flag a)
    forall a. a -> ArgDescr a
    NoArg Flag a
    flag') (String -> OptDescr (Flag a)) -> String -> OptDescr (Flag a)
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String
    description, String
    " (DEPRECATED, use --", String
    new, String
    ")"]
        where
        flag' :: Flag a
    flag' a
    o = OptionWarning -> OptM ()
    forall ws w (m :: * -> *).
    (Monoid ws, Singleton w ws, MonadWriter ws m) =>
    w -> m ()
    tell1 (String -> String -> OptionWarning
    OptionRenamed String
    old String
    new) OptM () -> OptM a -> OptM a
    forall a b. OptM a -> OptM b -> OptM b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Flag a
    flag a
    o
      OptDescr (Flag a)
    _ -> OptDescr (Flag a)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Used for printing usage info.
    --   Does not include the dead options.
    standardOptions_ :: [OptDescr ()]
    standardOptions_ :: [OptDescr ()]
    standardOptions_ = (OptDescr (Flag CommandLineOptions) -> OptDescr ())
    -> [OptDescr (Flag CommandLineOptions)] -> [OptDescr ()]
    forall a b. (a -> b) -> [a] -> [b]
    map OptDescr (Flag CommandLineOptions) -> OptDescr ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void [OptDescr (Flag CommandLineOptions)]
    standardOptions

    -- | Simple interface for Agda.Utils.GetOpt
    --   Could be moved to Agda.Utils.Options (does not exist yet)
    getOptSimple
      :: [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
    getOptSimple :: forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple [String]
    argv [OptDescr (Flag opts)]
    opts String -> Flag opts
    fileArg = \ opts
    defaults ->
      case ArgOrder (Flag opts)
    -> [OptDescr (Flag opts)]
    -> [String]
    -> ([Flag opts], [String], [String], [String])
    forall a.
    ArgOrder a
    -> [OptDescr a] -> [String] -> ([a], [String], [String], [String])
    getOpt' ((String -> Flag opts) -> ArgOrder (Flag opts)
    forall a. (String -> a) -> ArgOrder a
    ReturnInOrder String -> Flag opts
    fileArg) [OptDescr (Flag opts)]
    opts [String]
    argv of
        ([Flag opts]
    o, [String]
    _, []          , [] )  -> (OptM opts -> Flag opts -> OptM opts)
    -> OptM opts -> [Flag opts] -> OptM opts
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl OptM opts -> Flag opts -> OptM opts
    forall a b. OptM a -> (a -> OptM b) -> OptM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    (>>=) (Flag opts
    forall a. a -> OptM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return opts
    defaults) [Flag opts]
    o
        ([Flag opts]
    _, [String]
    _, [String]
    unrecognized, [String]
    errs) -> String -> OptM opts
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM opts) -> String -> OptM opts
    forall a b. (a -> b) -> a -> b
    $ String
    umsg String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    emsg

          where
          ucap :: String
    ucap = String
    "Unrecognized " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String -> String
    forall a. Sized a => a -> String -> String
    String.pluralS [String]
    unrecognized String
    "option" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
          ecap :: String
    ecap = [String] -> String -> String
    forall a. Sized a => a -> String -> String
    String.pluralS [String]
    errs String
    "Option error" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ":"
          umsg :: String
    umsg = if [String] -> Bool
    forall a. Null a => a -> Bool
    null [String]
    unrecognized then String
    "" else [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
           String
    ucap String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map String -> String
    suggest [String]
    unrecognized
          emsg :: String
    emsg = if [String] -> Bool
    forall a. Null a => a -> Bool
    null [String]
    errs then String
    "" else [String] -> String
    unlines ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
           String
    ecap String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    errs

          -- Suggest alternatives that are at most 3 typos away

          longopts :: [String]
          longopts :: [String]
    longopts = (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (String
    "--" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++) ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (OptDescr (Flag opts) -> [String])
    -> [OptDescr (Flag opts)] -> [String]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\ (Option String
    _ [String]
    long ArgDescr (Flag opts)
    _ String
    _) -> [String]
    long) [OptDescr (Flag opts)]
    opts

          dist :: String -> String -> Int
          dist :: String -> String -> Int
    dist String
    s String
    t = EditCosts -> String -> String -> Int
    restrictedDamerauLevenshteinDistance EditCosts
    defaultEditCosts String
    s String
    t

          close :: String -> String -> Maybe (Int, String)
          close :: String -> String -> Maybe (Int, String)
    close String
    s String
    t = let d :: Int
    d = String -> String -> Int
    dist String
    s String
    t in if Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    3 then (Int, String) -> Maybe (Int, String)
    forall a. a -> Maybe a
    Just (Int
    d, String
    t) else Maybe (Int, String)
    forall a. Maybe a
    Nothing

          closeopts :: String -> [(Int, String)]
          closeopts :: String -> [(Int, String)]
    closeopts String
    s = (String -> Maybe (Int, String)) -> [String] -> [(Int, String)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (String -> String -> Maybe (Int, String)
    close String
    s) [String]
    longopts

          alts :: String -> [List1 String]
          alts :: String -> [List1 String]
    alts String
    s = (NonEmpty (Int, String) -> List1 String)
    -> [NonEmpty (Int, String)] -> [List1 String]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Int, String) -> String) -> NonEmpty (Int, String) -> List1 String
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Int, String) -> String
    forall a b. (a, b) -> b
    snd) ([NonEmpty (Int, String)] -> [List1 String])
    -> [NonEmpty (Int, String)] -> [List1 String]
    forall a b. (a -> b) -> a -> b
    $ ((Int, String) -> Int)
    -> [(Int, String)] -> [NonEmpty (Int, String)]
    forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
    List1.groupOn (Int, String) -> Int
    forall a b. (a, b) -> a
    fst ([(Int, String)] -> [NonEmpty (Int, String)])
    -> [(Int, String)] -> [NonEmpty (Int, String)]
    forall a b. (a -> b) -> a -> b
    $ String -> [(Int, String)]
    closeopts String
    s

          suggest :: String -> String
          suggest :: String -> String
    suggest String
    s = case String -> [List1 String]
    alts String
    s of
            []     -> String
    s
            List1 String
    as : [List1 String]
    _ -> String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " (did you mean " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ List1 String -> String
    sugs List1 String
    as String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ?)"

          sugs :: List1 String -> String
          sugs :: List1 String -> String
    sugs (String
    a :| []) = String
    a
          sugs List1 String
    as  = String
    "any of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ List1 String -> String
    List1.unwords List1 String
    as

    -- | Parse options from an options pragma.
    parsePragmaOptions
      :: OptionsPragma
         -- ^ Pragma options.
      -> CommandLineOptions
         -- ^ Command-line options which should be updated.
      -> OptM PragmaOptions
    parsePragmaOptions :: OptionsPragma -> CommandLineOptions -> OptM PragmaOptions
    parsePragmaOptions OptionsPragma
    argv CommandLineOptions
    opts = do
      ps <- [String]
    -> [OptDescr (Flag PragmaOptions)]
    -> (String -> Flag PragmaOptions)
    -> Flag PragmaOptions
    forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple
              (OptionsPragma -> [String]
    pragmaStrings OptionsPragma
    argv)
              ([OptDescr (Flag PragmaOptions)]
    deadPragmaOptions [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag PragmaOptions)]
    -> [OptDescr (Flag PragmaOptions)]
    forall a. [a] -> [a] -> [a]
    ++ [OptDescr (Flag PragmaOptions)]
    pragmaOptions)
              (\String
    s PragmaOptions
    _ -> String -> OptM PragmaOptions
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
    forall a b. (a -> b) -> a -> b
    $ String
    "Bad option in pragma: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s)
              (CommandLineOptions -> PragmaOptions
    optPragmaOptions CommandLineOptions
    opts)
      checkPragmaOptions ps

    -- | Parse options for a plugin.
    parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
    parsePluginOptions :: forall opts. [String] -> [OptDescr (Flag opts)] -> Flag opts
    parsePluginOptions [String]
    argv [OptDescr (Flag opts)]
    opts =
      [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    forall opts.
    [String]
    -> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
    getOptSimple [String]
    argv [OptDescr (Flag opts)]
    opts
        (\String
    s opts
    _ -> String -> OptM opts
    forall a. String -> OptM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (String -> OptM opts) -> String -> OptM opts
    forall a b. (a -> b) -> a -> b
    $
                   String
    "Internal error: Flag " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " passed to a plugin")

    -- | The usage info message. The argument is the program name (probably
    --   agda).
    usage :: [OptDescr ()] -> String -> Help -> String
    usage :: [OptDescr ()] -> String -> Help -> String
    usage [OptDescr ()]
    options String
    progName Help
    GeneralHelp = String -> [OptDescr ()] -> String
    forall a. String -> [OptDescr a] -> String
    usageInfo (String -> String
    header String
    progName) [OptDescr ()]
    options
        where
            header :: String -> String
    header String
    progName = [String] -> String
    unlines [ String
    "Agda version " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    version, String
    ""
                                      , String
    "Usage: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    progName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " [OPTIONS...] [FILE]" ]

    usage [OptDescr ()]
    options String
    progName (HelpFor HelpTopic
    topic) = HelpTopic -> String
    helpTopicUsage HelpTopic
    topic

    -- | Removes RTS options from a list of options.

    stripRTS :: [String] -> [String]
    stripRTS :: [String] -> [String]
    stripRTS [] = []
    stripRTS (String
    "--RTS" : [String]
    argv) = [String]
    argv
    stripRTS (String
    arg : [String]
    argv)
      | String -> String -> Bool
    is String
    "+RTS" String
    arg = [String] -> [String]
    stripRTS ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    drop Int
    1 ([String] -> [String]) -> [String] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (String -> Bool) -> [String] -> [String]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Bool -> Bool
    forall a. Boolean a => a -> a
    not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String -> Bool
    is String
    "-RTS") [String]
    argv
      | Bool
    otherwise     = String
    arg String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String] -> [String]
    stripRTS [String]
    argv
      where
        is :: String -> String -> Bool
    is String
    x String
    arg = [String
    x] [String] -> [String] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> [String] -> [String]
    forall a. Int -> [a] -> [a]
    take Int
    1 (String -> [String]
    words String
    arg)