{-# LANGUAGE DataKinds #-}

{-# OPTIONS_GHC -Wunused-imports #-}

-- | A module defining the types exported by "Agda.Interaction.Options" for use in the rest of the codebase.
--
-- This is a boot module to avoid cyclic module dependencies.
-- Only put types and trivial instances here.

module Agda.Interaction.Options.Types where

import           Control.DeepSeq                   ( NFData )
import           Data.Functor                      ( (<&>) )
import           Data.Map                          ( Map )
import           GHC.Generics                      ( Generic )

import           Agda.Syntax.Common                ( Cubical )
import           Agda.Syntax.Concrete.Glyph        ( UnicodeOrAscii )
import           Agda.Interaction.Library          ( ExeName, LibName )
import           Agda.Interaction.Options.Help     ( Help )
import           Agda.Interaction.Options.Warnings ( WarningMode )
import           Agda.Termination.CutOff           ( CutOff )

import           Agda.Utils.FileName               ( AbsolutePath )
import           Agda.Utils.Lens                   ( Lens', (^.), over )
import           Agda.Utils.List1                  ( String1 )
import qualified Agda.Utils.Maybe.Strict           as Strict
import           Agda.Utils.ProfileOptions         ( ProfileOptions )
import           Agda.Utils.Trie                   ( Trie )
import           Agda.Utils.WithDefault            ( WithDefault, WithDefault' )

---------------------------------------------------------------------------
-- * Option records

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

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

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

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

---------------------------------------------------------------------------
-- * Auxiliary structures (by default in alphabetic order)

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

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

-- | Infective or coinfective?
data InfectiveCoinfective
  = Infective
  | Coinfective
  deriving (InfectiveCoinfective -> InfectiveCoinfective -> Bool
(InfectiveCoinfective -> InfectiveCoinfective -> Bool)
-> (InfectiveCoinfective -> InfectiveCoinfective -> Bool)
-> Eq InfectiveCoinfective
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
== :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
$c/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
/= :: InfectiveCoinfective -> InfectiveCoinfective -> Bool
Eq, Int -> InfectiveCoinfective -> ShowS
[InfectiveCoinfective] -> ShowS
InfectiveCoinfective -> String
(Int -> InfectiveCoinfective -> ShowS)
-> (InfectiveCoinfective -> String)
-> ([InfectiveCoinfective] -> ShowS)
-> Show InfectiveCoinfective
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InfectiveCoinfective -> ShowS
showsPrec :: Int -> InfectiveCoinfective -> ShowS
$cshow :: InfectiveCoinfective -> String
show :: InfectiveCoinfective -> String
$cshowList :: [InfectiveCoinfective] -> ShowS
showList :: [InfectiveCoinfective] -> ShowS
Show, (forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x)
-> (forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective)
-> Generic InfectiveCoinfective
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
$cfrom :: forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
from :: forall x. InfectiveCoinfective -> Rep InfectiveCoinfective x
$cto :: forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
to :: forall x. Rep InfectiveCoinfective x -> InfectiveCoinfective
Generic)

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

type VerboseKey     = String
type VerboseKeyItem = String1
type VerboseLevel   = Int

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

---------------------------------------------------------------------------
-- * Lenses

class LensPragmaOptions a where
  getPragmaOptions  :: a -> PragmaOptions
  setPragmaOptions  :: PragmaOptions -> a -> a
  mapPragmaOptions  :: (PragmaOptions -> PragmaOptions) -> a -> a
  lensPragmaOptions :: Lens' a PragmaOptions

  {-# MINIMAL lensPragmaOptions #-}
  getPragmaOptions = (a -> Lens' a PragmaOptions -> PragmaOptions
forall o i. o -> Lens' o i -> i
^. (PragmaOptions -> f PragmaOptions) -> a -> f a
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' a PragmaOptions
lensPragmaOptions)
  setPragmaOptions = (PragmaOptions -> PragmaOptions) -> a -> a
forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions ((PragmaOptions -> PragmaOptions) -> a -> a)
-> (PragmaOptions -> PragmaOptions -> PragmaOptions)
-> PragmaOptions
-> a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> PragmaOptions -> PragmaOptions
forall a b. a -> b -> a
const
  mapPragmaOptions = Lens' a PragmaOptions -> (PragmaOptions -> PragmaOptions) -> a -> a
forall o i. Lens' o i -> LensMap o i
over (PragmaOptions -> f PragmaOptions) -> a -> f a
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' a PragmaOptions
lensPragmaOptions

instance LensPragmaOptions CommandLineOptions where
  lensPragmaOptions :: Lens' CommandLineOptions PragmaOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) f PragmaOptions
-> (PragmaOptions -> CommandLineOptions) -> f CommandLineOptions
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions = opts }

---------------------------------------------------------------------------
-- NFData instances

instance NFData CommandLineOptions
instance NFData PragmaOptions

instance NFData ConfluenceCheck
instance NFData DiagnosticsColours
instance NFData InfectiveCoinfective
instance NFData PrintAgdaVersion