{-# LANGUAGE CPP       #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}

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

module Agda.Interaction.Options.Base
    ( CommandLineOptions(..)
    , PragmaOptions(..)
    , OptionWarning(..), optionWarningName
    , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
    , Verbosity, VerboseKey, VerboseLevel
    , WarningMode(..)
    , ConfluenceCheck(..)
    , PrintAgdaVersion(..)
    , UnicodeOrAscii(..)
    , DiagnosticsColours(..)
    , checkOpts
    , parsePragmaOptions
    , parsePluginOptions
    , parseVerboseKey
    , stripRTS
    , defaultOptions
    , defaultInteractionOptions
    , defaultCutOff
    , defaultPragmaOptions
    , standardOptions_
    , unsafePragmaOptions
    , recheckBecausePragmaOptionsChanged
    , InfectiveCoinfective(..)
    , InfectiveCoinfectiveOption(..)
    , infectiveCoinfectiveOptions
    , 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
    , lensOptWithoutK
    , lensOptCubicalCompatible
    , lensOptCopatterns
    , lensOptPatternMatching
    , lensOptExactSplit
    , lensOptHiddenArgumentPuns
    , lensOptEta
    , lensOptForcing
    , lensOptProjectionLike
    , lensOptErasure
    , lensOptErasedMatches
    , lensOptEraseRecordParameters
    , lensOptRewriting
    , lensOptCubical
    , lensOptGuarded
    , lensOptFirstOrder
    , lensOptPostfixProjections
    , lensOptKeepPatternVariables
    , lensOptInferAbsurdClauses
    , lensOptInstanceSearchDepth
    , lensOptOverlappingInstances
    , lensOptQualifiedInstances
    , lensOptInversionMaxDepth
    , lensOptSafe
    , lensOptDoubleCheck
    , lensOptSyntacticEquality
    , lensOptWarningMode
    , lensOptCompileMain
    , lensOptCaching
    , lensOptCountClusters
    , lensOptAutoInline
    , lensOptPrintPatternSynonyms
    , lensOptFastReduce
    , lensOptCallByName
    , lensOptConfluenceCheck
    , lensOptCohesion
    , lensOptFlatSplit
    , 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
    , optPostfixProjections
    , optKeepPatternVariables
    , optInferAbsurdClauses
    , optOverlappingInstances
    , optQualifiedInstances
    , optSafe
    , optDoubleCheck
    , optCompileNoMain
    , optCaching
    , optCountClusters
    , optAutoInline
    , optPrintPatternSynonyms
    , optFastReduce
    , optCallByName
    , optCohesion
    , optFlatSplit
    , 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 GHC.Generics (Generic)

import System.Console.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(..) )
import Agda.Interaction.Options.Help
  ( Help(HelpFor, GeneralHelp)
  , string2HelpTopic
  , allHelpTopics
  , helpTopicUsage
  )
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 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 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

-- OptDescr is a Functor --------------------------------------------------

type VerboseKey     = String
type VerboseKeyItem = String1
type VerboseLevel   = Int
-- | 'Strict.Nothing' is used if no verbosity options have been given,
-- thus making it possible to handle the default case relatively
-- quickly. Note that 'Strict.Nothing' corresponds to a trie with
-- verbosity level 1 for the empty path.
type Verbosity = Strict.Maybe (Trie VerboseKeyItem VerboseLevel)

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

data DiagnosticsColours
  = AlwaysColour
  | NeverColour
  | AutoColour
  deriving (Int -> DiagnosticsColours -> ShowS
[DiagnosticsColours] -> ShowS
DiagnosticsColours -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiagnosticsColours] -> ShowS
$cshowList :: [DiagnosticsColours] -> ShowS
show :: DiagnosticsColours -> String
$cshow :: DiagnosticsColours -> String
showsPrec :: Int -> DiagnosticsColours -> ShowS
$cshowsPrec :: Int -> DiagnosticsColours -> ShowS
Show, forall x. Rep DiagnosticsColours x -> DiagnosticsColours
forall x. DiagnosticsColours -> Rep DiagnosticsColours x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DiagnosticsColours x -> DiagnosticsColours
$cfrom :: forall x. DiagnosticsColours -> Rep DiagnosticsColours x
Generic)

instance NFData DiagnosticsColours

-- Don't forget to update
--   doc/user-manual/tools/command-line-options.rst
-- if you make changes to the command-line options!

data CommandLineOptions = Options
  { CommandLineOptions -> String
optProgramName           :: String
  , CommandLineOptions -> Maybe String
optInputFile             :: Maybe FilePath
  , CommandLineOptions -> [String]
optIncludePaths          :: [FilePath]
  , CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths  :: [AbsolutePath]
      -- ^ The list should not contain duplicates.
  , CommandLineOptions -> [String]
optLibraries             :: [LibName]
  , CommandLineOptions -> Maybe String
optOverrideLibrariesFile :: Maybe FilePath
      -- ^ Use this (if 'Just') instead of @~\/.agda\/libraries@.
  , CommandLineOptions -> Bool
optDefaultLibs           :: Bool
       -- ^ Use @~\/.agda\/defaults@.
  , CommandLineOptions -> Bool
optUseLibs               :: Bool
       -- ^ look for @.agda-lib@ files.
  , CommandLineOptions -> Integer
optTraceImports          :: Integer
       -- ^ Configure notifications about imported modules.
  , CommandLineOptions -> Map ExeName String
optTrustedExecutables    :: Map ExeName FilePath
       -- ^ Map names of trusted executables to absolute paths.
  , CommandLineOptions -> Bool
optPrintAgdaDataDir      :: Bool
  , CommandLineOptions -> Bool
optPrintAgdaAppDir       :: Bool
  , CommandLineOptions -> Maybe PrintAgdaVersion
optPrintVersion          :: Maybe PrintAgdaVersion
  , CommandLineOptions -> Maybe Help
optPrintHelp             :: Maybe Help
  , CommandLineOptions -> Bool
optInteractive           :: Bool
      -- ^ Agda REPL (@-I@).
  , CommandLineOptions -> Bool
optGHCiInteraction       :: Bool
  , CommandLineOptions -> Bool
optJSONInteraction       :: Bool
  , CommandLineOptions -> Bool
optExitOnError           :: !Bool
      -- ^ Exit if an interactive command fails.
  , CommandLineOptions -> Maybe String
optCompileDir            :: Maybe FilePath
      -- ^ In the absence of a path the project root is used.
  , CommandLineOptions -> Bool
optGenerateVimFile       :: Bool
  , CommandLineOptions -> Bool
optIgnoreInterfaces      :: Bool
  , CommandLineOptions -> Bool
optIgnoreAllInterfaces   :: Bool
  , CommandLineOptions -> Bool
optLocalInterfaces       :: Bool
  , CommandLineOptions -> PragmaOptions
optPragmaOptions         :: PragmaOptions
  , CommandLineOptions -> Bool
optOnlyScopeChecking     :: Bool
      -- ^ Should the top-level module only be scope-checked, and not type-checked?
  , CommandLineOptions -> Bool
optTransliterate         :: Bool
      -- ^ Should code points that are not supported by the locale be transliterated?
  , CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour     :: DiagnosticsColours
      -- ^ Configure colour output.
  }
  deriving (Int -> CommandLineOptions -> ShowS
[CommandLineOptions] -> ShowS
CommandLineOptions -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CommandLineOptions] -> ShowS
$cshowList :: [CommandLineOptions] -> ShowS
show :: CommandLineOptions -> String
$cshow :: CommandLineOptions -> String
showsPrec :: Int -> CommandLineOptions -> ShowS
$cshowsPrec :: Int -> CommandLineOptions -> ShowS
Show, forall x. Rep CommandLineOptions x -> CommandLineOptions
forall x. CommandLineOptions -> Rep CommandLineOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CommandLineOptions x -> CommandLineOptions
$cfrom :: forall x. CommandLineOptions -> Rep CommandLineOptions x
Generic)

instance NFData CommandLineOptions

-- | Options which can be set in a pragma.

data PragmaOptions = PragmaOptions
  { PragmaOptions -> WithDefault 'False
_optShowImplicit              :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optShowGeneralized           :: WithDefault 'True
      -- ^ Show generalized parameters in Pi types
  , PragmaOptions -> WithDefault 'False
_optShowIrrelevant            :: WithDefault 'False
  , PragmaOptions -> WithDefault' UnicodeOrAscii 'True
_optUseUnicode                :: WithDefault' UnicodeOrAscii 'True -- Would like to write UnicodeOk instead of True here
  , PragmaOptions -> Verbosity
_optVerbose                   :: !Verbosity
  , PragmaOptions -> ProfileOptions
_optProfiling                 :: ProfileOptions
  , PragmaOptions -> WithDefault 'False
_optProp                      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optLevelUniverse             :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optTwoLevel                  :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optAllowUnsolved             :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optAllowIncompleteMatch      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optPositivityCheck           :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optTerminationCheck          :: WithDefault 'True
  , PragmaOptions -> CutOff
_optTerminationDepth          :: CutOff
      -- ^ Cut off structural order comparison at some depth in termination checker?
  , PragmaOptions -> WithDefault 'True
_optUniverseCheck             :: WithDefault 'True
  , PragmaOptions -> WithDefault 'False
_optOmegaInOmega              :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optCumulativity              :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optSizedTypes                :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optGuardedness               :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optInjectiveTypeConstructors :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optUniversePolymorphism      :: WithDefault 'True
  , PragmaOptions -> WithDefault 'False
_optIrrelevantProjections     :: WithDefault 'False
      -- off by default in > 2.5.4, see issue #2170
  , PragmaOptions -> WithDefault 'False
_optExperimentalIrrelevance   :: WithDefault 'False
      -- ^ irrelevant levels, irrelevant data matching
  , PragmaOptions -> WithDefault 'False
_optWithoutK                  :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optCubicalCompatible         :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optCopatterns                :: WithDefault 'True
      -- ^ Allow definitions by copattern matching?
  , PragmaOptions -> WithDefault 'True
_optPatternMatching           :: WithDefault 'True
      -- ^ Is pattern matching allowed in the current file?
  , PragmaOptions -> WithDefault 'False
_optExactSplit                :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optHiddenArgumentPuns        :: WithDefault 'False
      -- ^ Should patterns of the form @{x}@ or @⦃ x ⦄@ be interpreted as puns?
  , PragmaOptions -> WithDefault 'True
_optEta                       :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optForcing                   :: WithDefault 'True
      -- ^ Perform the forcing analysis on data constructors?
  , PragmaOptions -> WithDefault 'True
_optProjectionLike            :: WithDefault 'True
      -- ^ Perform the projection-likeness analysis on functions?
  , PragmaOptions -> WithDefault 'False
_optErasure                   :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optErasedMatches             :: WithDefault 'True
      -- ^ Allow matching in erased positions for single-constructor,
      -- non-indexed data/record types. (This kind of matching is always
      -- allowed for record types with η-equality.)
  , PragmaOptions -> WithDefault 'False
_optEraseRecordParameters     :: WithDefault 'False
      -- ^ Mark parameters of record modules as erased?
  , PragmaOptions -> WithDefault 'False
_optRewriting                 :: WithDefault 'False
      -- ^ Can rewrite rules be added and used?
  , PragmaOptions -> Maybe Cubical
_optCubical                   :: Maybe Cubical
  , PragmaOptions -> WithDefault 'False
_optGuarded                   :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optFirstOrder                :: WithDefault 'False
      -- ^ Should we speculatively unify function applications as if they were injective?
  , PragmaOptions -> WithDefault 'False
_optPostfixProjections        :: WithDefault 'False
      -- ^ Should system generated projections 'ProjSystem' be printed
      --   postfix (True) or prefix (False).
  , PragmaOptions -> WithDefault 'False
_optKeepPatternVariables      :: WithDefault 'False
      -- ^ Should case splitting replace variables with dot patterns
      --   (False) or keep them as variables (True).
  , PragmaOptions -> WithDefault 'True
_optInferAbsurdClauses        :: WithDefault 'True
      -- ^ Should case splitting and coverage checking try to discharge absurd clauses?
      --   Default: 'True', but 'False' might make coverage checking considerably faster in some cases.
  , PragmaOptions -> Int
_optInstanceSearchDepth       :: Int
  , PragmaOptions -> WithDefault 'False
_optOverlappingInstances      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'True
_optQualifiedInstances        :: WithDefault 'True
      -- ^ Should instance search consider instances with qualified names?
  , PragmaOptions -> Int
_optInversionMaxDepth         :: Int
  , PragmaOptions -> WithDefault 'False
_optSafe                      :: WithDefault 'False
  , PragmaOptions -> WithDefault 'False
_optDoubleCheck               :: WithDefault 'False
  , PragmaOptions -> Maybe Int
_optSyntacticEquality         :: !(Strict.Maybe Int)
    -- ^ Should the conversion checker use the syntactic equality
    -- shortcut? 'Nothing' means that it should. @'Just' n@, for a
    -- non-negative number @n@, means that syntactic equality checking
    -- gets @n@ units of fuel. If the fuel becomes zero, then
    -- syntactic equality checking is turned off. The fuel counter is
    -- decreased in the failure continuation of
    -- 'Agda.TypeChecking.SyntacticEquality.checkSyntacticEquality'.
  , PragmaOptions -> WarningMode
_optWarningMode               :: WarningMode
  , PragmaOptions -> WithDefault 'True
_optCompileMain               :: WithDefault 'True
    -- ^ Treat the module given at the command line or via interaction as main module in compilation?
  , PragmaOptions -> WithDefault 'True
_optCaching                   :: WithDefault 'True
  , PragmaOptions -> WithDefault 'False
_optCountClusters             :: WithDefault 'False
    -- ^ Count extended grapheme clusters rather than code points
    --   when generating LaTeX.
  , PragmaOptions -> WithDefault 'False
_optAutoInline                :: WithDefault 'False
    -- ^ Automatic compile-time inlining for simple definitions
    --   (unless marked @NOINLINE@).
  , PragmaOptions -> WithDefault 'True
_optPrintPatternSynonyms      :: WithDefault 'True
  , PragmaOptions -> WithDefault 'True
_optFastReduce                :: WithDefault 'True
      -- ^ Use the Agda abstract machine ('fastReduce')?
  , PragmaOptions -> WithDefault 'False
_optCallByName                :: WithDefault 'False
      -- ^ Use call-by-name instead of call-by-need.
  , PragmaOptions -> Maybe ConfluenceCheck
_optConfluenceCheck           :: Maybe ConfluenceCheck
      -- ^ Check confluence of rewrite rules?
  , PragmaOptions -> WithDefault 'False
_optCohesion                  :: WithDefault 'False
      -- ^ Are the cohesion modalities available?
  , PragmaOptions -> WithDefault 'False
_optFlatSplit                 :: WithDefault 'False
      -- ^ Can we split on a @(\@flat x : A)@ argument?
  , PragmaOptions -> WithDefault 'True
_optImportSorts               :: WithDefault 'True
      -- ^ Should every top-level module start with an implicit statement
      --   @open import Agda.Primitive using (Set; Prop)@?
  , PragmaOptions -> WithDefault 'True
_optLoadPrimitives            :: WithDefault 'True
      -- ^ Should we load the primitive modules at all?
      --   This is a stronger form of 'optImportSorts'.
  , PragmaOptions -> WithDefault 'False
_optAllowExec                 :: WithDefault 'False
      -- ^ Allow running external @executables@ from meta programs.
  , PragmaOptions -> WithDefault 'False
_optSaveMetas                 :: WithDefault 'False
      -- ^ Save meta-variables to interface files.
  , PragmaOptions -> WithDefault 'False
_optShowIdentitySubstitutions :: WithDefault 'False
      -- ^ Show identity substitutions when pretty-printing terms
      --   (i.e. always show all arguments of a metavariable).
  , PragmaOptions -> WithDefault 'False
_optKeepCoveringClauses       :: WithDefault 'False
      -- ^ Do not discard clauses constructed by the coverage checker
      --   (needed for some external backends).
  , PragmaOptions -> WithDefault 'False
_optLargeIndices              :: WithDefault 'False
      -- ^ Allow large indices, and large forced arguments in
      -- constructors.
  , PragmaOptions -> WithDefault 'True
_optForcedArgumentRecursion   :: WithDefault 'True
      -- ^ Allow recursion on forced constructor arguments.
  }
  deriving (Int -> PragmaOptions -> ShowS
[PragmaOptions] -> ShowS
PragmaOptions -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PragmaOptions] -> ShowS
$cshowList :: [PragmaOptions] -> ShowS
show :: PragmaOptions -> String
$cshow :: PragmaOptions -> String
showsPrec :: Int -> PragmaOptions -> ShowS
$cshowsPrec :: Int -> PragmaOptions -> ShowS
Show, PragmaOptions -> PragmaOptions -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PragmaOptions -> PragmaOptions -> Bool
$c/= :: PragmaOptions -> PragmaOptions -> Bool
== :: PragmaOptions -> PragmaOptions -> Bool
$c== :: PragmaOptions -> PragmaOptions -> Bool
Eq, forall x. Rep PragmaOptions x -> PragmaOptions
forall x. PragmaOptions -> Rep PragmaOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PragmaOptions x -> PragmaOptions
$cfrom :: forall x. PragmaOptions -> Rep PragmaOptions x
Generic)

instance NFData PragmaOptions

data ConfluenceCheck
  = LocalConfluenceCheck
  | GlobalConfluenceCheck
  deriving (Int -> ConfluenceCheck -> ShowS
[ConfluenceCheck] -> ShowS
ConfluenceCheck -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConfluenceCheck] -> ShowS
$cshowList :: [ConfluenceCheck] -> ShowS
show :: ConfluenceCheck -> String
$cshow :: ConfluenceCheck -> String
showsPrec :: Int -> ConfluenceCheck -> ShowS
$cshowsPrec :: Int -> ConfluenceCheck -> ShowS
Show, ConfluenceCheck -> ConfluenceCheck -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConfluenceCheck -> ConfluenceCheck -> Bool
$c/= :: ConfluenceCheck -> ConfluenceCheck -> Bool
== :: ConfluenceCheck -> ConfluenceCheck -> Bool
$c== :: ConfluenceCheck -> ConfluenceCheck -> Bool
Eq, forall x. Rep ConfluenceCheck x -> ConfluenceCheck
forall x. ConfluenceCheck -> Rep ConfluenceCheck x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ConfluenceCheck x -> ConfluenceCheck
$cfrom :: forall x. ConfluenceCheck -> Rep ConfluenceCheck x
Generic)

instance NFData ConfluenceCheck

-- | Options @--version@ and @--numeric-version@ (last wins).
data PrintAgdaVersion
  = PrintAgdaVersion
      -- ^ Print Agda version information and exit.
  | PrintAgdaNumericVersion
      -- ^ Print Agda version number and exit.
  deriving (Int -> PrintAgdaVersion -> ShowS
[PrintAgdaVersion] -> ShowS
PrintAgdaVersion -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PrintAgdaVersion] -> ShowS
$cshowList :: [PrintAgdaVersion] -> ShowS
show :: PrintAgdaVersion -> String
$cshow :: PrintAgdaVersion -> String
showsPrec :: Int -> PrintAgdaVersion -> ShowS
$cshowsPrec :: Int -> PrintAgdaVersion -> ShowS
Show, forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion
forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PrintAgdaVersion x -> PrintAgdaVersion
$cfrom :: forall x. PrintAgdaVersion -> Rep PrintAgdaVersion x
Generic)

instance NFData PrintAgdaVersion

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

-- Collapse defaults (non-Bool)

optUseUnicode                :: PragmaOptions -> UnicodeOrAscii
optUseUnicode :: PragmaOptions -> UnicodeOrAscii
optUseUnicode                = forall a (b :: Bool).
(Boolean a, KnownBool b) =>
WithDefault' a b -> a
collapseDefault 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 :: Lens' PragmaOptions (WithDefault 'False)
lensOptShowImplicit WithDefault 'False -> f (WithDefault 'False)
f PragmaOptions
o = WithDefault 'False -> f (WithDefault 'False)
f (PragmaOptions -> WithDefault 'False
_optShowImplicit PragmaOptions
o) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ WithDefault 'False
i -> PragmaOptions
o{ _optShowImplicit :: WithDefault 'False
_optShowImplicit = WithDefault 'False
i }

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lensOptForcedArgumentRecursion :: Lens' PragmaOptions _
lensOptForcedArgumentRecursion :: Lens' PragmaOptions (WithDefault 'True)
lensOptForcedArgumentRecursion WithDefault 'True -> f (WithDefault 'True)
f PragmaOptions
o = WithDefault 'True -> f (WithDefault 'True)
f (PragmaOptions -> WithDefault 'True
_optForcedArgumentRecursion PragmaOptions
o) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ WithDefault 'True
i -> PragmaOptions
o{ _optForcedArgumentRecursion :: WithDefault 'True
_optForcedArgumentRecursion = WithDefault 'True
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. ShowS -> OptDescr a -> OptDescr a
mapFlag ShowS
f (Option String
_ [String]
long ArgDescr a
arg String
descr) = forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] (forall a b. (a -> b) -> [a] -> [b]
map ShowS
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             = forall a. Maybe a
Nothing
  , optIncludePaths :: [String]
optIncludePaths          = []
  , optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths  = []
  , optLibraries :: [String]
optLibraries             = []
  , optOverrideLibrariesFile :: Maybe String
optOverrideLibrariesFile = 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    = forall k a. Map k a
Map.empty
  , optPrintAgdaDataDir :: Bool
optPrintAgdaDataDir      = Bool
False
  , optPrintAgdaAppDir :: Bool
optPrintAgdaAppDir       = Bool
False
  , optPrintVersion :: Maybe PrintAgdaVersion
optPrintVersion          = forall a. Maybe a
Nothing
  , optPrintHelp :: Maybe Help
optPrintHelp             = forall a. Maybe a
Nothing
  , optInteractive :: Bool
optInteractive           = Bool
False
  , optGHCiInteraction :: Bool
optGHCiInteraction       = Bool
False
  , optJSONInteraction :: Bool
optJSONInteraction       = Bool
False
  , optExitOnError :: Bool
optExitOnError           = Bool
False
  , optCompileDir :: Maybe String
optCompileDir            = forall a. Maybe a
Nothing
  , optGenerateVimFile :: Bool
optGenerateVimFile       = Bool
False
  , optIgnoreInterfaces :: Bool
optIgnoreInterfaces      = Bool
False
  , optIgnoreAllInterfaces :: Bool
optIgnoreAllInterfaces   = Bool
False
  , optLocalInterfaces :: Bool
optLocalInterfaces       = 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              = forall a (b :: Bool). WithDefault' a b
Default
  , _optShowGeneralized :: WithDefault 'True
_optShowGeneralized           = forall a (b :: Bool). WithDefault' a b
Default
  , _optShowIrrelevant :: WithDefault 'False
_optShowIrrelevant            = forall a (b :: Bool). WithDefault' a b
Default
  , _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
_optUseUnicode                = forall a (b :: Bool). WithDefault' a b
Default -- UnicodeOk
  , _optVerbose :: Verbosity
_optVerbose                   = forall a. Maybe a
Strict.Nothing
  , _optProfiling :: ProfileOptions
_optProfiling                 = ProfileOptions
noProfileOptions
  , _optProp :: WithDefault 'False
_optProp                      = forall a (b :: Bool). WithDefault' a b
Default
  , _optLevelUniverse :: WithDefault 'False
_optLevelUniverse             = forall a (b :: Bool). WithDefault' a b
Default
  , _optTwoLevel :: WithDefault 'False
_optTwoLevel                  = forall a (b :: Bool). WithDefault' a b
Default
  , _optAllowUnsolved :: WithDefault 'False
_optAllowUnsolved             = forall a (b :: Bool). WithDefault' a b
Default
  , _optAllowIncompleteMatch :: WithDefault 'False
_optAllowIncompleteMatch      = forall a (b :: Bool). WithDefault' a b
Default
  , _optPositivityCheck :: WithDefault 'True
_optPositivityCheck           = forall a (b :: Bool). WithDefault' a b
Default
  , _optTerminationCheck :: WithDefault 'True
_optTerminationCheck          = forall a (b :: Bool). WithDefault' a b
Default
  , _optTerminationDepth :: CutOff
_optTerminationDepth          = CutOff
defaultCutOff
  , _optUniverseCheck :: WithDefault 'True
_optUniverseCheck             = forall a (b :: Bool). WithDefault' a b
Default
  , _optOmegaInOmega :: WithDefault 'False
_optOmegaInOmega              = forall a (b :: Bool). WithDefault' a b
Default
  , _optCumulativity :: WithDefault 'False
_optCumulativity              = forall a (b :: Bool). WithDefault' a b
Default
  , _optSizedTypes :: WithDefault 'False
_optSizedTypes                = forall a (b :: Bool). WithDefault' a b
Default
  , _optGuardedness :: WithDefault 'False
_optGuardedness               = forall a (b :: Bool). WithDefault' a b
Default
  , _optInjectiveTypeConstructors :: WithDefault 'False
_optInjectiveTypeConstructors = forall a (b :: Bool). WithDefault' a b
Default
  , _optUniversePolymorphism :: WithDefault 'True
_optUniversePolymorphism      = forall a (b :: Bool). WithDefault' a b
Default
  , _optIrrelevantProjections :: WithDefault 'False
_optIrrelevantProjections     = forall a (b :: Bool). WithDefault' a b
Default
  , _optExperimentalIrrelevance :: WithDefault 'False
_optExperimentalIrrelevance   = forall a (b :: Bool). WithDefault' a b
Default
  , _optWithoutK :: WithDefault 'False
_optWithoutK                  = forall a (b :: Bool). WithDefault' a b
Default
  , _optCubicalCompatible :: WithDefault 'False
_optCubicalCompatible         = forall a (b :: Bool). WithDefault' a b
Default
  , _optCopatterns :: WithDefault 'True
_optCopatterns                = forall a (b :: Bool). WithDefault' a b
Default
  , _optPatternMatching :: WithDefault 'True
_optPatternMatching           = forall a (b :: Bool). WithDefault' a b
Default
  , _optExactSplit :: WithDefault 'False
_optExactSplit                = forall a (b :: Bool). WithDefault' a b
Default
  , _optHiddenArgumentPuns :: WithDefault 'False
_optHiddenArgumentPuns        = forall a (b :: Bool). WithDefault' a b
Default
  , _optEta :: WithDefault 'True
_optEta                       = forall a (b :: Bool). WithDefault' a b
Default
  , _optForcing :: WithDefault 'True
_optForcing                   = forall a (b :: Bool). WithDefault' a b
Default
  , _optProjectionLike :: WithDefault 'True
_optProjectionLike            = forall a (b :: Bool). WithDefault' a b
Default
  , _optErasure :: WithDefault 'False
_optErasure                   = forall a (b :: Bool). WithDefault' a b
Default
  , _optErasedMatches :: WithDefault 'True
_optErasedMatches             = forall a (b :: Bool). WithDefault' a b
Default
  , _optEraseRecordParameters :: WithDefault 'False
_optEraseRecordParameters     = forall a (b :: Bool). WithDefault' a b
Default
  , _optRewriting :: WithDefault 'False
_optRewriting                 = forall a (b :: Bool). WithDefault' a b
Default
  , _optCubical :: Maybe Cubical
_optCubical                   = forall a. Maybe a
Nothing
  , _optGuarded :: WithDefault 'False
_optGuarded                   = forall a (b :: Bool). WithDefault' a b
Default
  , _optFirstOrder :: WithDefault 'False
_optFirstOrder                = forall a (b :: Bool). WithDefault' a b
Default
  , _optPostfixProjections :: WithDefault 'False
_optPostfixProjections        = forall a (b :: Bool). WithDefault' a b
Default
  , _optKeepPatternVariables :: WithDefault 'False
_optKeepPatternVariables      = forall a (b :: Bool). WithDefault' a b
Default
  , _optInferAbsurdClauses :: WithDefault 'True
_optInferAbsurdClauses        = forall a (b :: Bool). WithDefault' a b
Default
  , _optInstanceSearchDepth :: Int
_optInstanceSearchDepth       = Int
500
  , _optOverlappingInstances :: WithDefault 'False
_optOverlappingInstances      = forall a (b :: Bool). WithDefault' a b
Default
  , _optQualifiedInstances :: WithDefault 'True
_optQualifiedInstances        = forall a (b :: Bool). WithDefault' a b
Default
  , _optInversionMaxDepth :: Int
_optInversionMaxDepth         = Int
50
  , _optSafe :: WithDefault 'False
_optSafe                      = forall a (b :: Bool). WithDefault' a b
Default
  , _optDoubleCheck :: WithDefault 'False
_optDoubleCheck               = forall a (b :: Bool). WithDefault' a b
Default
  , _optSyntacticEquality :: Maybe Int
_optSyntacticEquality         = forall a. Maybe a
Strict.Nothing
  , _optWarningMode :: WarningMode
_optWarningMode               = WarningMode
defaultWarningMode
  , _optCompileMain :: WithDefault 'True
_optCompileMain               = forall a (b :: Bool). WithDefault' a b
Default
  , _optCaching :: WithDefault 'True
_optCaching                   = forall a (b :: Bool). WithDefault' a b
Default
  , _optCountClusters :: WithDefault 'False
_optCountClusters             = forall a (b :: Bool). WithDefault' a b
Default
  , _optAutoInline :: WithDefault 'False
_optAutoInline                = forall a (b :: Bool). WithDefault' a b
Default
  , _optPrintPatternSynonyms :: WithDefault 'True
_optPrintPatternSynonyms      = forall a (b :: Bool). WithDefault' a b
Default
  , _optFastReduce :: WithDefault 'True
_optFastReduce                = forall a (b :: Bool). WithDefault' a b
Default
  , _optCallByName :: WithDefault 'False
_optCallByName                = forall a (b :: Bool). WithDefault' a b
Default
  , _optConfluenceCheck :: Maybe ConfluenceCheck
_optConfluenceCheck           = forall a. Maybe a
Nothing
  , _optCohesion :: WithDefault 'False
_optCohesion                  = forall a (b :: Bool). WithDefault' a b
Default
  , _optFlatSplit :: WithDefault 'False
_optFlatSplit                 = forall a (b :: Bool). WithDefault' a b
Default
  , _optImportSorts :: WithDefault 'True
_optImportSorts               = forall a (b :: Bool). WithDefault' a b
Default
  , _optLoadPrimitives :: WithDefault 'True
_optLoadPrimitives            = forall a (b :: Bool). WithDefault' a b
Default
  , _optAllowExec :: WithDefault 'False
_optAllowExec                 = forall a (b :: Bool). WithDefault' a b
Default
  , _optSaveMetas :: WithDefault 'False
_optSaveMetas                 = forall a (b :: Bool). WithDefault' a b
Default
  , _optShowIdentitySubstitutions :: WithDefault 'False
_optShowIdentitySubstitutions = forall a (b :: Bool). WithDefault' a b
Default
  , _optKeepCoveringClauses :: WithDefault 'False
_optKeepCoveringClauses       = forall a (b :: Bool). WithDefault' a b
Default
  , _optForcedArgumentRecursion :: WithDefault 'True
_optForcedArgumentRecursion   = forall a (b :: Bool). WithDefault' a b
Default
  , _optLargeIndices :: WithDefault 'False
_optLargeIndices              = 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 -> 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
<$ :: forall a b. a -> OptM b -> OptM a
$c<$ :: forall a b. a -> OptM b -> OptM a
fmap :: forall a b. (a -> b) -> OptM a -> OptM b
$cfmap :: forall a b. (a -> b) -> OptM a -> OptM b
Functor, Functor 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
<* :: forall a b. OptM a -> OptM b -> OptM a
$c<* :: forall a b. OptM a -> OptM b -> OptM a
*> :: forall a b. OptM a -> OptM b -> OptM b
$c*> :: forall a b. OptM a -> OptM b -> OptM b
liftA2 :: forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c
$cliftA2 :: forall a b c. (a -> b -> c) -> OptM a -> OptM b -> OptM c
<*> :: forall a b. OptM (a -> b) -> OptM a -> OptM b
$c<*> :: forall a b. OptM (a -> b) -> OptM a -> OptM b
pure :: forall a. a -> OptM a
$cpure :: forall a. a -> OptM a
Applicative, Applicative 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
return :: forall a. a -> OptM a
$creturn :: forall a. a -> OptM a
>> :: forall a b. OptM a -> OptM b -> OptM b
$c>> :: forall a b. OptM a -> OptM b -> OptM b
>>= :: forall a b. OptM a -> (a -> OptM b) -> OptM b
$c>>= :: forall a b. OptM a -> (a -> OptM b) -> OptM b
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 = forall w a. Writer w a -> (a, w)
runWriter forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 }
  deriving (Int -> OptionWarning -> ShowS
OptionWarnings -> ShowS
OptionWarning -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: OptionWarnings -> ShowS
$cshowList :: OptionWarnings -> ShowS
show :: OptionWarning -> String
$cshow :: OptionWarning -> String
showsPrec :: Int -> OptionWarning -> ShowS
$cshowsPrec :: Int -> OptionWarning -> ShowS
Show, 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
$cto :: forall x. Rep OptionWarning x -> OptionWarning
$cfrom :: forall x. OptionWarning -> Rep OptionWarning x
Generic)

instance NFData OptionWarning

instance Pretty OptionWarning where
  pretty :: OptionWarning -> Doc
pretty = \case
    OptionRenamed String
old String
new -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep
      [ Doc
"Option", forall {a}. String -> Doc a
name String
old, Doc
"is deprecated, please use", forall {a}. String -> Doc a
name String
new, Doc
"instead" ]
    where
    name :: String -> Doc a
name = forall {a}. String -> Doc a
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"--" forall a. [a] -> [a] -> [a]
++)

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

-- | 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.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optGenerateVimFile CommandLineOptions
opts forall a. Boolean a => a -> a -> a
&& CommandLineOptions -> Bool
optOnlyScopeChecking CommandLineOptions
opts) forall a b. (a -> b) -> a -> b
$
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"The --only-scope-checking flag cannot be combined with --vim."

  Lens' CommandLineOptions PragmaOptions
lensPragmaOptions 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.

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((PragmaOptions -> Bool
optEraseRecordParameters forall a. Boolean a => a -> a -> a
`butNot` PragmaOptions -> Bool
optErasure) PragmaOptions
opts) forall a b. (a -> b) -> a -> b
$
    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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PragmaOptions -> Bool
optCountClusters PragmaOptions
opts) forall a b. (a -> b) -> a -> b
$
    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.

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

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

    -- -WNotStrictlyPositive iff --positivity-check
    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
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set WarningName
-> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
conformWarningsToOption Set WarningName
unsolvedWarnings (forall a. Boolean a => a -> a
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAllowUnsolved)

    -- incompleteMatchWarnings iff --no-allow-incomplete-matches
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set WarningName
-> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
conformWarningsToOption Set WarningName
incompleteMatchWarnings (forall a. Boolean a => a -> a
not 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
  forall o i. Lens' o i -> LensMap o i
over (Lens' PragmaOptions WarningMode
lensOptWarningMode forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' WarningMode (Set WarningName)
warningSet) (if PragmaOptions -> Bool
f PragmaOptions
opts then (forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set WarningName
ws) else (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                             ] forall a. [a] -> [a] -> [a]
++
  [ String
"--allow-incomplete-matches"        | PragmaOptions -> Bool
optAllowIncompleteMatch PragmaOptions
opts                      ] forall a. [a] -> [a] -> [a]
++
  [ String
"--no-positivity-check"             | forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optPositivityCheck PragmaOptions
opts)                     ] forall a. [a] -> [a] -> [a]
++
  [ String
"--no-termination-check"            | forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optTerminationCheck PragmaOptions
opts)                    ] forall a. [a] -> [a] -> [a]
++
  [ String
"--type-in-type"                    | forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optUniverseCheck PragmaOptions
opts)                       ] forall a. [a] -> [a] -> [a]
++
  [ String
"--omega-in-omega"                  | PragmaOptions -> Bool
optOmegaInOmega PragmaOptions
opts                              ] forall a. [a] -> [a] -> [a]
++
  [ String
"--sized-types"                     | PragmaOptions -> Bool
optSizedTypes PragmaOptions
opts                                ] forall a. [a] -> [a] -> [a]
++
  [ String
"--injective-type-constructors"     | PragmaOptions -> Bool
optInjectiveTypeConstructors PragmaOptions
opts                 ] forall a. [a] -> [a] -> [a]
++
  [ String
"--irrelevant-projections"          | PragmaOptions -> Bool
optIrrelevantProjections PragmaOptions
opts                     ] forall a. [a] -> [a] -> [a]
++
  [ String
"--experimental-irrelevance"        | PragmaOptions -> Bool
optExperimentalIrrelevance PragmaOptions
opts                   ] forall a. [a] -> [a] -> [a]
++
  [ String
"--rewriting"                       | PragmaOptions -> Bool
optRewriting PragmaOptions
opts                                 ] forall a. [a] -> [a] -> [a]
++
  [ String
"--cubical-compatible and --with-K" | PragmaOptions -> Bool
optCubicalCompatible PragmaOptions
opts, forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optWithoutK PragmaOptions
opts) ] forall a. [a] -> [a] -> [a]
++
  [ String
"--without-K and --flat-split"      | PragmaOptions -> Bool
optWithoutK PragmaOptions
opts, PragmaOptions -> Bool
optFlatSplit PragmaOptions
opts               ] forall a. [a] -> [a] -> [a]
++
  [ String
"--cumulativity"                    | PragmaOptions -> Bool
optCumulativity PragmaOptions
opts                              ] forall a. [a] -> [a] -> [a]
++
  [ String
"--allow-exec"                      | PragmaOptions -> Bool
optAllowExec PragmaOptions
opts                                 ] forall a. [a] -> [a] -> [a]
++
  [ String
"--no-load-primitives"              | forall a. Boolean a => a -> a
not forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optLoadPrimitives PragmaOptions
opts                      ] forall a. [a] -> [a] -> [a]
++
  [ String
"--without-K and --large-indices"   | PragmaOptions -> Bool
optWithoutK PragmaOptions
opts, PragmaOptions -> Bool
optLargeIndices PragmaOptions
opts            ] forall a. [a] -> [a] -> [a]
++
  [ String
"--large-indices and --forced-argument-recursion"
  | PragmaOptions -> Bool
optLargeIndices PragmaOptions
opts, PragmaOptions -> Bool
optForcedArgumentRecursion PragmaOptions
opts ] 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 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 :: WithDefault 'False
_optShowImplicit              = forall a. Null a => a
empty
    , _optShowIrrelevant :: WithDefault 'False
_optShowIrrelevant            = forall a. Null a => a
empty
    , _optVerbose :: Verbosity
_optVerbose                   = forall a. Null a => a
empty
    , _optProfiling :: ProfileOptions
_optProfiling                 = forall a. Null a => a
empty
    , _optPostfixProjections :: WithDefault 'False
_optPostfixProjections        = forall a. Null a => a
empty
    , _optCompileMain :: WithDefault 'True
_optCompileMain               = forall a. Null a => a
empty
    , _optCaching :: WithDefault 'True
_optCaching                   = forall a. Null a => a
empty
    , _optCountClusters :: WithDefault 'False
_optCountClusters             = forall a. Null a => a
empty
    , _optPrintPatternSynonyms :: WithDefault 'True
_optPrintPatternSynonyms      = forall a. Null a => a
empty
    , _optShowIdentitySubstitutions :: WithDefault 'False
_optShowIdentitySubstitutions = forall a. Null a => a
empty
    }

-- | Infective or coinfective?

data InfectiveCoinfective
  = Infective
  | Coinfective
    deriving (InfectiveCoinfective -> InfectiveCoinfective -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
$c/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
$c== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
Eq, Int -> InfectiveCoinfective -> ShowS
[InfectiveCoinfective] -> ShowS
InfectiveCoinfective -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [InfectiveCoinfective] -> ShowS
$cshowList :: [InfectiveCoinfective] -> ShowS
show :: InfectiveCoinfective -> String
$cshow :: InfectiveCoinfective -> String
showsPrec :: Int -> InfectiveCoinfective -> ShowS
$cshowsPrec :: Int -> InfectiveCoinfective -> ShowS
Show, forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
$cfrom :: forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
Generic)

instance NFData InfectiveCoinfective

-- | 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 forall a. Ord a => a -> a -> Bool
<= PragmaOptions -> Bool
opt PragmaOptions
current
  , icOptionWarning :: TopLevelModuleName -> Doc
icOptionWarning     = \TopLevelModuleName
m -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$
      String -> [Doc]
pwords String
"Importing module" forall a. [a] -> [a] -> [a]
++ [forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
m] forall a. [a] -> [a] -> [a]
++ String -> [Doc]
pwords String
"using the" forall a. [a] -> [a] -> [a]
++
      [forall {a}. String -> Doc a
text String
s] 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 forall a. Ord a => a -> a -> Bool
<= PragmaOptions -> Bool
opt PragmaOptions
imported
  , icOptionWarning :: TopLevelModuleName -> Doc
icOptionWarning     = \TopLevelModuleName
m -> forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep forall a b. (a -> b) -> a -> b
$
      String -> [Doc]
pwords String
"Importing module" forall a. [a] -> [a] -> [a]
++ [forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
m] forall a. [a] -> [a] -> [a]
++
      String -> [Doc]
pwords String
"not using the" forall a. [a] -> [a] -> [a]
++ [forall {a}. String -> Doc a
text String
s] 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 (forall a. Boolean a => a -> a
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniversePolymorphism)
                                              String
"--no-universe-polymorphism"
  , (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
coinfectiveOption (forall a. Boolean a => a -> a
not 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 (forall a. Maybe a -> Bool
isJust 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
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 -> PragmaOptions -> Bool
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
               forall a. Boolean a => a -> a -> a
||
             forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optWithoutK PragmaOptions
imported)
               forall a. Boolean a => a -> a -> a
&&
             forall a. Boolean a => a -> a
not (PragmaOptions -> Bool
optWithoutK PragmaOptions
current)
               forall a. Boolean a => a -> a -> a
&&
             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  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optInputFile :: Maybe String
optInputFile = forall a. a -> Maybe a
Just String
f }
        Just String
_   -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optPrintAgdaDataDir :: Bool
optPrintAgdaDataDir = Bool
True }

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

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

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

helpFlag :: Maybe String -> Flag CommandLineOptions
helpFlag :: Maybe String -> Flag CommandLineOptions
helpFlag Maybe String
Nothing    CommandLineOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optPrintHelp :: Maybe Help
optPrintHelp = forall a. a -> Maybe a
Just Help
GeneralHelp }
helpFlag (Just String
str) CommandLineOptions
o = case String -> Maybe HelpTopic
string2HelpTopic String
str of
  Just HelpTopic
hpt -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optPrintHelp :: Maybe Help
optPrintHelp = forall a. a -> Maybe a
Just (HelpTopic -> Help
HelpFor HelpTopic
hpt) }
  Maybe HelpTopic
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"unknown help topic " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
" (available: " forall a. [a] -> [a] -> [a]
++
                           forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, HelpTopic)]
allHelpTopics) forall a. [a] -> [a] -> [a]
++ String
")"

safeFlag :: Flag PragmaOptions
safeFlag :: Flag PragmaOptions
safeFlag PragmaOptions
o = do
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optSafe :: WithDefault 'False
_optSafe        = forall a (b :: Bool). a -> WithDefault' a b
Value Bool
True
             , _optSizedTypes :: WithDefault 'False
_optSizedTypes  = forall a (b :: Bool).
Boolean a =>
a -> WithDefault' a b -> WithDefault' a b
setDefault Bool
False (PragmaOptions -> WithDefault 'False
_optSizedTypes PragmaOptions
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   -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
err
    Right Maybe Int
fuel -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optSyntacticEquality :: Maybe Int
_optSyntacticEquality = Maybe Int
fuel }
  where
  fuel :: Either String (Maybe Int)
fuel = case Maybe String
s of
    Maybe String
Nothing -> forall a b. b -> Either a b
Right forall a. Maybe a
Strict.Nothing
    Just String
s  -> case forall a. Read a => String -> Maybe a
readMaybe String
s of
      Just Int
n | Int
n forall a. Ord a => a -> a -> Bool
>= Int
0 -> forall a b. b -> Either a b
Right (forall a. a -> Maybe a
Strict.Just Int
n)
      Maybe Int
_               -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Not a natural number: " forall a. [a] -> [a] -> [a]
++ String
s

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

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

localInterfacesFlag :: Flag CommandLineOptions
localInterfacesFlag :: Flag CommandLineOptions
localInterfacesFlag CommandLineOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optLocalInterfaces :: Bool
optLocalInterfaces = Bool
True }

traceImportsFlag :: Maybe String -> Flag CommandLineOptions
traceImportsFlag :: Maybe String -> Flag CommandLineOptions
traceImportsFlag Maybe String
arg CommandLineOptions
o = do
  Integer
mode <- case Maybe String
arg of
            Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Integer
2
            Just String
str -> case forall a. Read a => ReadS a
reads String
str :: [(Integer, String)] of
                          [(Integer
n, String
"")] -> forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
                          [(Integer, String)]
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"unknown printing option " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
". Please specify a number."
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optTraceImports :: Integer
optTraceImports = Integer
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"   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o { optDiagnosticsColour :: DiagnosticsColours
optDiagnosticsColour = DiagnosticsColours
AutoColour }
  Just String
"always" -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o { optDiagnosticsColour :: DiagnosticsColours
optDiagnosticsColour = DiagnosticsColours
AlwaysColour }
  Just String
"never"  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o { optDiagnosticsColour :: DiagnosticsColours
optDiagnosticsColour = DiagnosticsColours
NeverColour }
  Just String
str -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"unknown colour option " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
". Please specify one of auto, always, or never."
  Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o { optDiagnosticsColour :: DiagnosticsColours
optDiagnosticsColour = DiagnosticsColours
AutoColour }

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

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

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

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

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

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

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

withKFlag :: Flag PragmaOptions
withKFlag :: Flag PragmaOptions
withKFlag =
  -- with-K is the opposite of --without-K, so collapse default when disabling --without-K
  (Lens' PragmaOptions (WithDefault 'False)
lensOptWithoutK forall a b. (a -> b) -> a -> b
$ forall a (b :: Bool).
(Boolean a, KnownBool b) =>
Lens' (WithDefault' a b) a
lensCollapseDefault forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)
  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
  (Lens' PragmaOptions (WithDefault 'True)
lensOptErasedMatches forall a b. (a -> b) -> a -> b
$ forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
lensKeepDefault forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)


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

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

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

instanceDepthFlag :: String -> Flag PragmaOptions
instanceDepthFlag :: String -> Flag PragmaOptions
instanceDepthFlag String
s PragmaOptions
o = do
  Int
d <- String -> String -> OptM Int
integerArgument String
"--instance-search-depth" String
s
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optInstanceSearchDepth :: Int
_optInstanceSearchDepth = Int
d }

inversionMaxDepthFlag :: String -> Flag PragmaOptions
inversionMaxDepthFlag :: String -> Flag PragmaOptions
inversionMaxDepthFlag String
s PragmaOptions
o = do
  Int
d <- String -> String -> OptM Int
integerArgument String
"--inversion-max-depth" String
s
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optInversionMaxDepth :: Int
_optInversionMaxDepth = Int
d }

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

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

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

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

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

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

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

verboseFlag :: String -> Flag PragmaOptions
verboseFlag :: String -> Flag PragmaOptions
verboseFlag String
s PragmaOptions
o =
    do  ([VerboseKeyItem]
k,Int
n) <- String -> OptM ([VerboseKeyItem], Int)
parseVerbose String
s
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          PragmaOptions
o { _optVerbose :: Verbosity
_optVerbose =
                forall a. a -> Maybe a
Strict.Just forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => [k] -> v -> Trie k v -> Trie k v
Trie.insert [VerboseKeyItem]
k Int
n forall a b. (a -> b) -> a -> b
$
                case PragmaOptions -> Verbosity
_optVerbose PragmaOptions
o of
                  Verbosity
Strict.Nothing -> 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
      []  -> forall {a}. OptM a
usage
      VerboseKeyItem
s0:[VerboseKeyItem]
ss0 -> do
        let ([VerboseKeyItem]
ss, VerboseKeyItem
s) = forall a. a -> [a] -> ([a], a)
initLast1 VerboseKeyItem
s0 [VerboseKeyItem]
ss0
        -- The last entry must be a number.
        Int
n <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {a}. OptM a
usage forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Read a => String -> Maybe a
readMaybe forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
toList VerboseKeyItem
s
        forall (m :: * -> *) a. Monad m => a -> m a
return ([VerboseKeyItem]
ss, Int
n)
    usage :: OptM a
usage = 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   -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
err
    Right ProfileOptions
prof -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PragmaOptions
o{ _optProfiling :: ProfileOptions
_optProfiling = ProfileOptions
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optWarningMode :: WarningMode
_optWarningMode = WarningModeUpdate
upd (PragmaOptions -> WarningMode
_optWarningMode PragmaOptions
o) }
  Left WarningModeError
err  -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ WarningModeError -> String
prettyWarningModeError WarningModeError
err forall a. [a] -> [a] -> [a]
++ String
" See --help=warning."

terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag String
s PragmaOptions
o =
    do Int
k <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {a}. OptM a
usage forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Read a => String -> Maybe a
readMaybe String
s
       forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
k forall a. Ord a => a -> a -> Bool
< Int
1) forall a b. (a -> b) -> a -> b
$ forall {a}. OptM a
usage -- or: turn termination checking off for 0
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optTerminationDepth :: CutOff
_optTerminationDepth = Int -> CutOff
CutOff forall a b. (a -> b) -> a -> b
$ Int
kforall a. Num a => a -> a -> a
-Int
1 }
    where usage :: OptM a
usage = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { _optConfluenceCheck :: Maybe ConfluenceCheck
_optConfluenceCheck = forall a. a -> Maybe a
Just ConfluenceCheck
f }

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

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


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

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

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

    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'?']  [String
"help"]    (forall a. (Maybe String -> a) -> String -> ArgDescr a
OptArg Maybe String -> Flag CommandLineOptions
helpFlag String
"TOPIC") forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                    [ String
"print help and exit; available "
                    , forall a c. Sized a => a -> c -> c -> c
singPlural [(String, HelpTopic)]
allHelpTopics String
"TOPIC" String
"TOPICs"
                    , String
": "
                    , forall a. [a] -> [[a]] -> [a]
intercalate String
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, HelpTopic)]
allHelpTopics
                    ]

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

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

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


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

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

    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"trace-imports"] (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)")

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

-- | Defined locally here since module ''Agda.Interaction.Options.Lenses''
--   has cyclic dependency.
lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions
lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }

-- | 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 =
    [ forall a. String -> String -> OptDescr (Flag a)
removedOption String
"sharing"    String
msgSharing
    , forall a. String -> String -> OptDescr (Flag a)
removedOption String
"no-sharing" String
msgSharing
    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"ignore-all-interfaces"] (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.
    ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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 = 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 (forall a b. a -> b -> a
const 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 = forall a.
IsBool a =>
String
-> Lens' PragmaOptions a
-> (a -> Flag PragmaOptions)
-> String
-> String
-> Maybe String
-> [OptDescr (Flag PragmaOptions)]
pragmaFlagBool' String
long (Lens' PragmaOptions (WithDefault' a b)
field forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (b :: Bool).
(Boolean a, KnownBool b) =>
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 = 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 (forall a b. a -> b -> a
const 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 =
  [ forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [forall {b}. IsBool b => b -> ShowS
no Bool
b String
long] (Bool -> ArgDescr (Flag PragmaOptions)
flag Bool
b) (Bool -> ShowS
def Bool
b forall a b. (a -> b) -> a -> b
$ Bool -> String
expl Bool
b) | Bool
b <- [Bool
True,Bool
False] ]
  where
  b0 :: a
b0     = PragmaOptions
defaultPragmaOptions forall o i. o -> Lens' o i -> i
^. Lens' PragmaOptions a
field
  no :: b -> ShowS
no   b
b = forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless b
b (String
"no-" forall a. [a] -> [a] -> [a]
++)
  flag :: Bool -> ArgDescr (Flag PragmaOptions)
flag Bool
b = forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ a -> Flag PragmaOptions
effect a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o i. Lens' o i -> LensSet o i
set Lens' PragmaOptions a
field a
a
    where a :: a
a = forall a. Boolean a => Bool -> a
fromBool Bool
b
  def :: Bool -> ShowS
def  Bool
b = forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (forall a. Boolean a => Bool -> a
fromBool Bool
b forall a. Eq a => a -> a -> Bool
== a
b0) (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 forall a. a -> Maybe a -> a
fromMaybe (String
"do not " forall a. [a] -> [a] -> [a]
++ String
pos) Maybe String
neg


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

  , 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" Lens' PragmaOptions (WithDefault 'True)
lensOptImportSorts
                    String
"implicitly import Agda.Primitive using (Set; Prop) at the start of each top-level module" String
""
                    forall a b. (a -> b) -> a -> b
$ 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"
  , 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" Lens' PragmaOptions (WithDefault 'True)
lensOptLoadPrimitives
                    String
"load primitives modules" String
""
                    forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
"disable loading of primitive modules completely (implies --no-import-sorts)"
  , 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" Lens' PragmaOptions (WithDefault 'False)
lensOptAllowExec
                    String
"allow system calls to trusted executables with primExec" String
""
                    forall a. Maybe a
Nothing
  , 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" Lens' PragmaOptions (WithDefault 'False)
lensOptSaveMetas
                    String
"save meta-variables" String
""
                    forall a. Maybe a
Nothing
  , 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" Lens' PragmaOptions (WithDefault 'False)
lensOptKeepCoveringClauses
                    String
"do not discard covering clauses" String
"(required for some external backends)"
                    forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
"discard covering clauses"
  , 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" Lens' PragmaOptions (WithDefault 'False)
lensOptLargeIndices
                    String
"allow constructors with large indices" String
""
                    forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
"always check that constructor arguments live in universes compatible with that of the datatype"
  , 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" Lens' PragmaOptions (WithDefault 'True)
lensOptForcedArgumentRecursion
                    String
"allow recursion on forced constructor arguments" 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 forall a. Eq a => a -> a -> 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 =
  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" Lens' PragmaOptions (WithDefault 'False)
lensOptFirstOrder
    String
"enable heuristically unifying `f es = f es'` by unifying `es = es'`"
    String
"even when it could lose solutions"
    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 = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. String -> String -> OptDescr (Flag a)
removedOption)
    [ (String
"guardedness-preserving-type-constructors"
      , String
"")
    , (String
"no-coverage-check"
      , ShowS
inVersion String
"2.5.1") -- see issue #1918
    , (String
"no-sort-comparison"
      , String
"")
    , (String
"subtyping"
      , ShowS
inVersion String
"2.6.3") -- see issue #5427
    , (String
"no-subtyping"
      , ShowS
inVersion String
"2.6.3") -- see issue #5427
    , (String
"no-flat-split", ShowS
inVersion String
"2.6.3")  -- See issue #6263.
    ]
  , forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. String -> OptDescr (Flag a) -> OptDescr (Flag a)
renamedNoArgOption)
    [ ( String
"experimental-lossy-unification"
      , forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [OptDescr (Flag PragmaOptions)]
lossyUnificationOption
      )
    ]
  ]
  where
    inVersion :: ShowS
inVersion = (String
"in version " 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 = forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
name] (forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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
"--" 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 ->
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
old] (forall a. a -> ArgDescr a
NoArg Flag a
flag') forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
description, String
" (DEPRECATED, use --", String
new, String
")"]
    where
    flag' :: Flag a
flag' a
o = forall ws w (m :: * -> *).
(Monoid ws, Singleton w ws, MonadWriter ws m) =>
w -> m ()
tell1 (String -> String -> OptionWarning
OptionRenamed String
old String
new) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Flag a
flag a
o
  OptDescr (Flag a)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | Simple interface for System.Console.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 forall a.
ArgOrder a
-> [OptDescr a] -> [String] -> ([a], [String], [String], [String])
getOpt' (forall a. (String -> a) -> ArgOrder a
ReturnInOrder String -> Flag opts
fileArg) [OptDescr (Flag opts)]
opts [String]
argv of
    ([Flag opts]
o, [String]
_, []          , [] )  -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(>>=) (forall (m :: * -> *) a. Monad m => a -> m a
return opts
defaults) [Flag opts]
o
    ([Flag opts]
_, [String]
_, [String]
unrecognized, [String]
errs) -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
umsg forall a. [a] -> [a] -> [a]
++ String
emsg

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

      -- Suggest alternatives that are at most 3 typos away

      longopts :: [String]
      longopts :: [String]
longopts = forall a b. (a -> b) -> [a] -> [b]
map (String
"--" forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$ 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 forall a. Ord a => a -> a -> Bool
<= Int
3 then forall a. a -> Maybe a
Just (Int
d, String
t) else forall a. Maybe a
Nothing

      closeopts :: String -> [(Int, String)]
      closeopts :: String -> [(Int, String)]
closeopts String
s = 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 = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ String -> [(Int, String)]
closeopts String
s

      suggest :: String -> String
      suggest :: ShowS
suggest String
s = case String -> [List1 String]
alts String
s of
        []     -> String
s
        List1 String
as : [List1 String]
_ -> String
s forall a. [a] -> [a] -> [a]
++ String
" (did you mean " forall a. [a] -> [a] -> [a]
++ List1 String -> String
sugs List1 String
as 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 " 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
  PragmaOptions
ps <- forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple
          (OptionsPragma -> [String]
pragmaStrings OptionsPragma
argv)
          ([OptDescr (Flag PragmaOptions)]
deadPragmaOptions forall a. [a] -> [a] -> [a]
++ [OptDescr (Flag PragmaOptions)]
pragmaOptions)
          (\String
s PragmaOptions
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Bad option in pragma: " forall a. [a] -> [a] -> [a]
++ String
s)
          (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts)
  forall (m :: * -> *).
MonadError String m =>
PragmaOptions -> m PragmaOptions
checkPragmaOptions PragmaOptions
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 =
  forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple [String]
argv [OptDescr (Flag opts)]
opts
    (\String
s opts
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$
               String
"Internal error: Flag " forall a. [a] -> [a] -> [a]
++ String
s 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 = forall a. String -> [OptDescr a] -> String
usageInfo (ShowS
header String
progName) [OptDescr ()]
options
    where
        header :: ShowS
header String
progName = [String] -> String
unlines [ String
"Agda version " forall a. [a] -> [a] -> [a]
++ String
version, String
""
                                  , String
"Usage: " forall a. [a] -> [a] -> [a]
++ String
progName 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 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
1 forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Boolean a => a -> a
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
is String
"-RTS") [String]
argv
  | Bool
otherwise     = String
arg forall a. a -> [a] -> [a]
: [String] -> [String]
stripRTS [String]
argv
  where
    is :: String -> String -> Bool
is String
x String
arg = [String
x] forall a. Eq a => a -> a -> Bool
== forall a. Int -> [a] -> [a]
take Int
1 (String -> [String]
words String
arg)