{-# 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
, inputFlag
, standardOptions, deadStandardOptions
, getOptSimple
, 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
, 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
, 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
type VerboseKey = String
type VerboseKeyItem = String1
type VerboseLevel = Int
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
data CommandLineOptions = Options
{ CommandLineOptions -> String
optProgramName :: String
, CommandLineOptions -> Maybe String
optInputFile :: Maybe FilePath
, CommandLineOptions -> [String]
optIncludePaths :: [FilePath]
, CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths :: [AbsolutePath]
, CommandLineOptions -> [String]
optLibraries :: [LibName]
, CommandLineOptions -> Maybe String
optOverrideLibrariesFile :: Maybe FilePath
, CommandLineOptions -> Bool
optDefaultLibs :: Bool
, CommandLineOptions -> Bool
optUseLibs :: Bool
, CommandLineOptions -> Integer
optTraceImports :: Integer
, CommandLineOptions -> Map ExeName String
optTrustedExecutables :: Map ExeName FilePath
, CommandLineOptions -> Bool
optPrintAgdaDataDir :: Bool
, CommandLineOptions -> Bool
optPrintAgdaAppDir :: Bool
, CommandLineOptions -> Maybe PrintAgdaVersion
optPrintVersion :: Maybe PrintAgdaVersion
, CommandLineOptions -> Maybe Help
optPrintHelp :: Maybe Help
, CommandLineOptions -> Bool
optInteractive :: Bool
, CommandLineOptions -> Bool
optGHCiInteraction :: Bool
, CommandLineOptions -> Bool
optJSONInteraction :: Bool
, CommandLineOptions -> Bool
optExitOnError :: !Bool
, CommandLineOptions -> Maybe String
optCompileDir :: Maybe FilePath
, CommandLineOptions -> Bool
optGenerateVimFile :: Bool
, CommandLineOptions -> Bool
optIgnoreInterfaces :: Bool
, CommandLineOptions -> Bool
optIgnoreAllInterfaces :: Bool
, CommandLineOptions -> Bool
optLocalInterfaces :: Bool
, CommandLineOptions -> PragmaOptions
optPragmaOptions :: PragmaOptions
, CommandLineOptions -> Bool
optOnlyScopeChecking :: Bool
, CommandLineOptions -> Bool
optTransliterate :: Bool
, CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour :: DiagnosticsColours
}
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
data PragmaOptions = PragmaOptions
{ PragmaOptions -> WithDefault 'False
_optShowImplicit :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optShowGeneralized :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optShowIrrelevant :: WithDefault 'False
, PragmaOptions -> WithDefault' UnicodeOrAscii 'True
_optUseUnicode :: WithDefault' UnicodeOrAscii 'True
, 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
, 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
, PragmaOptions -> WithDefault 'False
_optExperimentalIrrelevance :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optWithoutK :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optCubicalCompatible :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optCopatterns :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optPatternMatching :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optExactSplit :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optHiddenArgumentPuns :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optEta :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optForcing :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optProjectionLike :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optErasure :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optErasedMatches :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optEraseRecordParameters :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optRewriting :: WithDefault 'False
, PragmaOptions -> Maybe Cubical
_optCubical :: Maybe Cubical
, PragmaOptions -> WithDefault 'False
_optGuarded :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optFirstOrder :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optPostfixProjections :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optKeepPatternVariables :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optInferAbsurdClauses :: WithDefault 'True
, PragmaOptions -> Int
_optInstanceSearchDepth :: Int
, PragmaOptions -> WithDefault 'False
_optOverlappingInstances :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optQualifiedInstances :: WithDefault 'True
, PragmaOptions -> Int
_optInversionMaxDepth :: Int
, PragmaOptions -> WithDefault 'False
_optSafe :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optDoubleCheck :: WithDefault 'False
, PragmaOptions -> Maybe Int
_optSyntacticEquality :: !(Strict.Maybe Int)
, PragmaOptions -> WarningMode
_optWarningMode :: WarningMode
, PragmaOptions -> WithDefault 'True
_optCompileMain :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optCaching :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optCountClusters :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optAutoInline :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optPrintPatternSynonyms :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optFastReduce :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optCallByName :: WithDefault 'False
, PragmaOptions -> Maybe ConfluenceCheck
_optConfluenceCheck :: Maybe ConfluenceCheck
, PragmaOptions -> WithDefault 'False
_optCohesion :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optFlatSplit :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optImportSorts :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
_optLoadPrimitives :: WithDefault 'True
, PragmaOptions -> WithDefault 'False
_optAllowExec :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optSaveMetas :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optShowIdentitySubstitutions :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optKeepCoveringClauses :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
_optLargeIndices :: WithDefault 'False
, PragmaOptions -> WithDefault 'True
_optForcedArgumentRecursion :: WithDefault 'True
}
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
data PrintAgdaVersion
= PrintAgdaVersion
| PrintAgdaNumericVersion
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
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 :: PragmaOptions -> Bool
optErasedMatches :: PragmaOptions -> Bool
optEraseRecordParameters :: PragmaOptions -> Bool
optRewriting :: PragmaOptions -> Bool
optGuarded :: PragmaOptions -> Bool
optFirstOrder :: PragmaOptions -> Bool
optPostfixProjections :: PragmaOptions -> Bool
optKeepPatternVariables :: PragmaOptions -> Bool
optInferAbsurdClauses :: PragmaOptions -> Bool
optOverlappingInstances :: PragmaOptions -> Bool
optQualifiedInstances :: PragmaOptions -> Bool
optSafe :: PragmaOptions -> Bool
optDoubleCheck :: PragmaOptions -> Bool
optCompileNoMain :: PragmaOptions -> Bool
optCaching :: PragmaOptions -> Bool
optCountClusters :: PragmaOptions -> Bool
optAutoInline :: PragmaOptions -> Bool
optPrintPatternSynonyms :: PragmaOptions -> Bool
optFastReduce :: PragmaOptions -> Bool
optCallByName :: PragmaOptions -> Bool
optCohesion :: PragmaOptions -> Bool
optFlatSplit :: PragmaOptions -> Bool
optImportSorts :: PragmaOptions -> Bool
optLoadPrimitives :: PragmaOptions -> Bool
optAllowExec :: PragmaOptions -> Bool
optSaveMetas :: PragmaOptions -> Bool
optShowIdentitySubstitutions :: PragmaOptions -> Bool
optKeepCoveringClauses :: PragmaOptions -> Bool
optLargeIndices :: PragmaOptions -> Bool
optForcedArgumentRecursion :: PragmaOptions -> Bool
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
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
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
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
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
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
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 }
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
, _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
}
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
type Flag opts = opts -> OptM opts
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_
checkOpts :: MonadError OptionError m => CommandLineOptions -> m CommandLineOptions
checkOpts :: forall (m :: * -> *).
MonadError String m =>
CommandLineOptions -> m CommandLineOptions
checkOpts CommandLineOptions
opts = do
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
checkPragmaOptions :: MonadError OptionError m => PragmaOptions -> m PragmaOptions
checkPragmaOptions :: forall (m :: * -> *).
MonadError String m =>
PragmaOptions -> m PragmaOptions
checkPragmaOptions PragmaOptions
opts = do
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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
opts
forall a b. a -> (a -> b) -> b
& WarningName
-> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
conformWarningToOption WarningName
TerminationIssue_ PragmaOptions -> Bool
optTerminationCheck
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WarningName
-> (PragmaOptions -> Bool) -> PragmaOptions -> PragmaOptions
conformWarningToOption WarningName
NotStrictlyPositive_ PragmaOptions -> Bool
optPositivityCheck
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)
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)
conformWarningToOption ::
WarningName
-> (PragmaOptions -> Bool)
-> PragmaOptions
-> PragmaOptions
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
conformWarningsToOption ::
Set WarningName
-> (PragmaOptions -> Bool)
-> PragmaOptions
-> PragmaOptions
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
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]
++
[]
recheckBecausePragmaOptionsChanged
:: PragmaOptions
-> PragmaOptions
-> 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
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
}
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
data InfectiveCoinfectiveOption = ICOption
{ InfectiveCoinfectiveOption -> PragmaOptions -> Bool
icOptionActive :: PragmaOptions -> Bool
, InfectiveCoinfectiveOption -> String
icOptionDescription :: String
, InfectiveCoinfectiveOption -> InfectiveCoinfective
icOptionKind :: InfectiveCoinfective
, InfectiveCoinfectiveOption
-> PragmaOptions -> PragmaOptions -> Bool
icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
, InfectiveCoinfectiveOption -> TopLevelModuleName -> Doc
icOptionWarning :: TopLevelModuleName -> Doc
}
infectiveOption
:: (PragmaOptions -> Bool)
-> String
-> 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."
}
coinfectiveOption
:: (PragmaOptions -> Bool)
-> String
-> 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."
}
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 ->
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 }
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 =
(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
>=>
(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
-> 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
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
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
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 }
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)
String
"ignore all interface files (re-type check everything, including builtin files)"
] 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)"
pragmaFlag :: (IsBool a, KnownBool b)
=> String
-> Lens' PragmaOptions (WithDefault' a b)
-> String
-> String
-> Maybe String
-> [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)
pragmaFlag' :: (IsBool a, KnownBool b)
=> String
-> Lens' PragmaOptions (WithDefault' a b)
-> (a -> Flag PragmaOptions)
-> String
-> String
-> Maybe String
-> [OptDescr (Flag PragmaOptions)]
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)
pragmaFlagBool :: (IsBool a)
=> String
-> Lens' PragmaOptions a
-> String
-> String
-> Maybe String
-> [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)
pragmaFlagBool' :: IsBool a
=> String
-> Lens' PragmaOptions a
-> (a -> Flag PragmaOptions)
-> String
-> String
-> Maybe String
-> [OptDescr (Flag PragmaOptions)]
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
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")
, (String
"no-sort-comparison"
, String
"")
, (String
"subtyping"
, ShowS
inVersion String
"2.6.3")
, (String
"no-subtyping"
, ShowS
inVersion String
"2.6.3")
, (String
"no-flat-split", ShowS
inVersion String
"2.6.3")
]
, 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]
++)
removedOption ::
String
-> String
-> 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]
renamedNoArgOption ::
String
-> OptDescr (Flag a)
-> OptDescr (Flag a)
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__
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
getOptSimple
:: [String]
-> [OptDescr (Flag opts)]
-> (String -> Flag opts)
-> Flag opts
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"
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
parsePragmaOptions
:: OptionsPragma
-> CommandLineOptions
-> 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
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")
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
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)