-- | Default values for the options.

module Agda.Interaction.Options.Default where

import Agda.Interaction.Options.ProfileOptions () -- Null instance
import Agda.Interaction.Options.Types
import Agda.Interaction.Options.Warnings ( defaultWarningMode )
import Agda.Termination.CutOff           ( defaultCutOff )
import Agda.Utils.Null
import Agda.Utils.WithDefault

import Agda.Utils.Impossible

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

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

-- Null instances

instance Null CommandLineOptions where
  empty :: CommandLineOptions
empty = CommandLineOptions
defaultOptions
  null :: CommandLineOptions -> Bool
null = CommandLineOptions -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Null PragmaOptions where
  empty :: PragmaOptions
empty = PragmaOptions
defaultPragmaOptions