{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
module Agda.Interaction.Options.Base
( CommandLineOptions(..)
, PragmaOptions(..)
, OptionsPragma
, Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
, Verbosity, VerboseKey, VerboseLevel
, WarningMode(..)
, ConfluenceCheck(..)
, UnicodeOrAscii(..)
, checkOpts
, parsePragmaOptions
, parsePluginOptions
, parseVerboseKey
, stripRTS
, defaultOptions
, defaultInteractionOptions
, defaultCutOff
, defaultPragmaOptions
, standardOptions_
, unsafePragmaOptions
, recheckBecausePragmaOptionsChanged
, InfectiveCoinfective(..)
, InfectiveCoinfectiveOption(..)
, infectiveCoinfectiveOptions
, safeFlag
, mapFlag
, usage
, inputFlag
, standardOptions, deadStandardOptions
, getOptSimple
) where
import Control.DeepSeq
import Control.Monad ( when, void )
import Control.Monad.Except ( Except, MonadError(throwError), runExcept )
import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO)
import Data.Maybe
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.List ( intercalate )
import qualified Data.Set as Set
import GHC.Generics (Generic)
import System.Console.GetOpt ( getOpt', usageInfo, ArgOrder(ReturnInOrder)
, OptDescr(..), ArgDescr(..)
)
import Text.EditDistance
import Text.Read ( readMaybe )
import Agda.Termination.CutOff ( CutOff(..), defaultCutOff )
import Agda.Interaction.Library ( ExeName, LibName )
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.TopLevelModuleName (TopLevelModuleName)
import Agda.Utils.FileName ( AbsolutePath )
import Agda.Utils.Functor ( (<&>) )
import Agda.Utils.Lens ( Lens', over )
import Agda.Utils.List ( groupOn, initLast1 )
import Agda.Utils.List1 ( String1, toList )
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null (empty)
import Agda.Utils.Pretty
import Agda.Utils.ProfileOptions
import Agda.Utils.Trie ( Trie )
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.WithDefault
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 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 -> Map ExeName String
optTrustedExecutables :: Map ExeName FilePath
, CommandLineOptions -> Bool
optPrintAgdaDir :: Bool
, CommandLineOptions -> Bool
optPrintVersion :: Bool
, 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
}
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 -> Bool
optShowImplicit :: Bool
, PragmaOptions -> Bool
optShowIrrelevant :: Bool
, PragmaOptions -> UnicodeOrAscii
optUseUnicode :: UnicodeOrAscii
, PragmaOptions -> Verbosity
optVerbose :: !Verbosity
, PragmaOptions -> ProfileOptions
optProfiling :: ProfileOptions
, PragmaOptions -> Bool
optProp :: Bool
, PragmaOptions -> WithDefault 'False
optTwoLevel :: WithDefault 'False
, PragmaOptions -> Bool
optAllowUnsolved :: Bool
, PragmaOptions -> Bool
optAllowIncompleteMatch :: Bool
, PragmaOptions -> Bool
optDisablePositivity :: Bool
, PragmaOptions -> Bool
optTerminationCheck :: Bool
, PragmaOptions -> CutOff
optTerminationDepth :: CutOff
, PragmaOptions -> Bool
optUniverseCheck :: Bool
, PragmaOptions -> Bool
optOmegaInOmega :: Bool
, PragmaOptions -> Bool
optCumulativity :: Bool
, PragmaOptions -> WithDefault 'False
optSizedTypes :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
optGuardedness :: WithDefault 'False
, PragmaOptions -> Bool
optInjectiveTypeConstructors :: Bool
, PragmaOptions -> Bool
optUniversePolymorphism :: Bool
, PragmaOptions -> Bool
optIrrelevantProjections :: Bool
, PragmaOptions -> Bool
optExperimentalIrrelevance :: Bool
, PragmaOptions -> WithDefault 'False
optWithoutK :: WithDefault 'False
, PragmaOptions -> WithDefault 'False
optCubicalCompatible :: WithDefault 'False
, PragmaOptions -> Bool
optCopatterns :: Bool
, PragmaOptions -> Bool
optPatternMatching :: Bool
, PragmaOptions -> Bool
optExactSplit :: Bool
, PragmaOptions -> Bool
optEta :: Bool
, PragmaOptions -> Bool
optForcing :: Bool
, PragmaOptions -> Bool
optProjectionLike :: Bool
, PragmaOptions -> Bool
optEraseRecordParameters :: Bool
, PragmaOptions -> Bool
optRewriting :: Bool
, PragmaOptions -> Maybe Cubical
optCubical :: Maybe Cubical
, PragmaOptions -> Bool
optGuarded :: Bool
, PragmaOptions -> Bool
optFirstOrder :: Bool
, PragmaOptions -> Bool
optPostfixProjections :: Bool
, PragmaOptions -> Bool
optKeepPatternVariables :: Bool
, PragmaOptions -> Int
optInstanceSearchDepth :: Int
, PragmaOptions -> Bool
optOverlappingInstances :: Bool
, PragmaOptions -> Bool
optQualifiedInstances :: Bool
, PragmaOptions -> Int
optInversionMaxDepth :: Int
, PragmaOptions -> Bool
optSafe :: Bool
, PragmaOptions -> Bool
optDoubleCheck :: Bool
, PragmaOptions -> Maybe Int
optSyntacticEquality :: !(Strict.Maybe Int)
, PragmaOptions -> WarningMode
optWarningMode :: WarningMode
, PragmaOptions -> Bool
optCompileNoMain :: Bool
, PragmaOptions -> Bool
optCaching :: Bool
, PragmaOptions -> Bool
optCountClusters :: Bool
, PragmaOptions -> Bool
optAutoInline :: Bool
, PragmaOptions -> Bool
optPrintPatternSynonyms :: Bool
, PragmaOptions -> Bool
optFastReduce :: Bool
, PragmaOptions -> Bool
optCallByName :: Bool
, PragmaOptions -> Maybe ConfluenceCheck
optConfluenceCheck :: Maybe ConfluenceCheck
, PragmaOptions -> Bool
optCohesion :: Bool
, PragmaOptions -> WithDefault 'False
optFlatSplit :: WithDefault 'False
, PragmaOptions -> Bool
optImportSorts :: Bool
, PragmaOptions -> Bool
optLoadPrimitives :: Bool
, PragmaOptions -> Bool
optAllowExec :: Bool
, PragmaOptions -> WithDefault 'False
optSaveMetas :: WithDefault 'False
, PragmaOptions -> Bool
optShowIdentitySubstitutions :: Bool
, PragmaOptions -> Bool
optKeepCoveringClauses :: Bool
}
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
type OptionsPragma = [String]
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
, optTrustedExecutables :: Map ExeName String
optTrustedExecutables = forall k a. Map k a
Map.empty
, optPrintAgdaDir :: Bool
optPrintAgdaDir = Bool
False
, optPrintVersion :: Bool
optPrintVersion = Bool
False
, 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
}
defaultPragmaOptions :: PragmaOptions
defaultPragmaOptions :: PragmaOptions
defaultPragmaOptions = PragmaOptions
{ optShowImplicit :: Bool
optShowImplicit = Bool
False
, optShowIrrelevant :: Bool
optShowIrrelevant = Bool
False
, optUseUnicode :: UnicodeOrAscii
optUseUnicode = UnicodeOrAscii
UnicodeOk
, optVerbose :: Verbosity
optVerbose = forall a. Maybe a
Strict.Nothing
, optProfiling :: ProfileOptions
optProfiling = ProfileOptions
noProfileOptions
, optProp :: Bool
optProp = Bool
False
, optTwoLevel :: WithDefault 'False
optTwoLevel = forall (b :: Bool). WithDefault b
Default
, optExperimentalIrrelevance :: Bool
optExperimentalIrrelevance = Bool
False
, optIrrelevantProjections :: Bool
optIrrelevantProjections = Bool
False
, optAllowUnsolved :: Bool
optAllowUnsolved = Bool
False
, optAllowIncompleteMatch :: Bool
optAllowIncompleteMatch = Bool
False
, optDisablePositivity :: Bool
optDisablePositivity = Bool
False
, optTerminationCheck :: Bool
optTerminationCheck = Bool
True
, optTerminationDepth :: CutOff
optTerminationDepth = CutOff
defaultCutOff
, optUniverseCheck :: Bool
optUniverseCheck = Bool
True
, optOmegaInOmega :: Bool
optOmegaInOmega = Bool
False
, optCumulativity :: Bool
optCumulativity = Bool
False
, optSizedTypes :: WithDefault 'False
optSizedTypes = forall (b :: Bool). WithDefault b
Default
, optGuardedness :: WithDefault 'False
optGuardedness = forall (b :: Bool). WithDefault b
Default
, optInjectiveTypeConstructors :: Bool
optInjectiveTypeConstructors = Bool
False
, optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
True
, optWithoutK :: WithDefault 'False
optWithoutK = forall (b :: Bool). WithDefault b
Default
, optCubicalCompatible :: WithDefault 'False
optCubicalCompatible = forall (b :: Bool). WithDefault b
Default
, optCopatterns :: Bool
optCopatterns = Bool
True
, optPatternMatching :: Bool
optPatternMatching = Bool
True
, optExactSplit :: Bool
optExactSplit = Bool
False
, optEta :: Bool
optEta = Bool
True
, optForcing :: Bool
optForcing = Bool
True
, optProjectionLike :: Bool
optProjectionLike = Bool
True
, optEraseRecordParameters :: Bool
optEraseRecordParameters = Bool
False
, optRewriting :: Bool
optRewriting = Bool
False
, optCubical :: Maybe Cubical
optCubical = forall a. Maybe a
Nothing
, optGuarded :: Bool
optGuarded = Bool
False
, optFirstOrder :: Bool
optFirstOrder = Bool
False
, optPostfixProjections :: Bool
optPostfixProjections = Bool
False
, optKeepPatternVariables :: Bool
optKeepPatternVariables = Bool
False
, optInstanceSearchDepth :: Int
optInstanceSearchDepth = Int
500
, optOverlappingInstances :: Bool
optOverlappingInstances = Bool
False
, optQualifiedInstances :: Bool
optQualifiedInstances = Bool
True
, optInversionMaxDepth :: Int
optInversionMaxDepth = Int
50
, optSafe :: Bool
optSafe = Bool
False
, optDoubleCheck :: Bool
optDoubleCheck = Bool
False
, optSyntacticEquality :: Maybe Int
optSyntacticEquality = forall a. Maybe a
Strict.Nothing
, optWarningMode :: WarningMode
optWarningMode = WarningMode
defaultWarningMode
, optCompileNoMain :: Bool
optCompileNoMain = Bool
False
, optCaching :: Bool
optCaching = Bool
True
, optCountClusters :: Bool
optCountClusters = Bool
False
, optAutoInline :: Bool
optAutoInline = Bool
False
, optPrintPatternSynonyms :: Bool
optPrintPatternSynonyms = Bool
True
, optFastReduce :: Bool
optFastReduce = Bool
True
, optCallByName :: Bool
optCallByName = Bool
False
, optConfluenceCheck :: Maybe ConfluenceCheck
optConfluenceCheck = forall a. Maybe a
Nothing
, optCohesion :: Bool
optCohesion = Bool
False
, optFlatSplit :: WithDefault 'False
optFlatSplit = forall (b :: Bool). WithDefault b
Default
, optImportSorts :: Bool
optImportSorts = Bool
True
, optAllowExec :: Bool
optAllowExec = Bool
False
, optSaveMetas :: WithDefault 'False
optSaveMetas = forall (b :: Bool). WithDefault b
Default
, optShowIdentitySubstitutions :: Bool
optShowIdentitySubstitutions = Bool
False
, optLoadPrimitives :: Bool
optLoadPrimitives = Bool
True
, optKeepCoveringClauses :: Bool
optKeepCoveringClauses = Bool
False
}
type OptM = Except String
runOptM :: Monad m => OptM opts -> m (Either String opts)
runOptM :: forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either String opts)
runOptM = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a. Except e a -> Either e a
runExcept
type Flag opts = opts -> OptM opts
checkOpts :: Flag CommandLineOptions
checkOpts :: Flag CommandLineOptions
checkOpts CommandLineOptions
opts = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
optGenerateVimFile CommandLineOptions
opts Bool -> Bool -> Bool
&& 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."
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
opts
unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
unsafePragmaOptions CommandLineOptions
clo 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" | PragmaOptions -> Bool
optDisablePositivity PragmaOptions
opts ] forall a. [a] -> [a] -> [a]
++
[ String
"--no-termination-check" | Bool -> Bool
not (PragmaOptions -> Bool
optTerminationCheck PragmaOptions
opts) ] forall a. [a] -> [a] -> [a]
++
[ String
"--type-in-type" | Bool -> Bool
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" | forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
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" | forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optCubicalCompatible PragmaOptions
opts)
, Bool -> Bool
not (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
opts) ] forall a. [a] -> [a] -> [a]
++
[ String
"--without-K and --flat-split" | forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
opts)
, forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
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" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optLoadPrimitives 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 :: Bool
optShowImplicit = Bool
False
, optShowIrrelevant :: Bool
optShowIrrelevant = Bool
False
, optVerbose :: Verbosity
optVerbose = forall a. Null a => a
empty
, optProfiling :: ProfileOptions
optProfiling = ProfileOptions
noProfileOptions
, optPostfixProjections :: Bool
optPostfixProjections = Bool
False
, optCompileNoMain :: Bool
optCompileNoMain = Bool
False
, optCaching :: Bool
optCaching = Bool
False
, optCountClusters :: Bool
optCountClusters = Bool
False
, optPrintPatternSynonyms :: Bool
optPrintPatternSynonyms = Bool
False
, optShowIdentitySubstitutions :: Bool
optShowIdentitySubstitutions = Bool
False
}
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]
++
[String -> Doc
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]
++ [String -> Doc
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 (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optWithoutK) String
"--without-K"
, InfectiveCoinfectiveOption
cubicalCompatible
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
coinfectiveOption (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniversePolymorphism)
String
"--no-universe-polymorphism"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
coinfectiveOption (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCumulativity) String
"--no-cumulativity"
, (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 (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optTwoLevel) String
"--two-level"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
infectiveOption PragmaOptions -> Bool
optRewriting String
"--rewriting"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
infectiveOption (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSizedTypes) String
"--sized-types"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
infectiveOption (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optGuardedness) String
"--guardedness"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
infectiveOption (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optFlatSplit) String
"--flat-split"
, (PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
infectiveOption PragmaOptions -> Bool
optCohesion String
"--cohesion"
]
where
cubicalCompatible :: InfectiveCoinfectiveOption
cubicalCompatible =
((PragmaOptions -> Bool) -> String -> InfectiveCoinfectiveOption
coinfectiveOption
(forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optCubicalCompatible)
String
"--cubical-compatible")
{ icOptionOK :: PragmaOptions -> PragmaOptions -> Bool
icOptionOK = \PragmaOptions
current PragmaOptions
imported ->
if forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optCubicalCompatible PragmaOptions
current)
then forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optCubicalCompatible PragmaOptions
imported)
Bool -> Bool -> Bool
||
Bool -> Bool
not (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
imported))
Bool -> Bool -> Bool
&&
Bool -> Bool
not (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
current))
Bool -> Bool -> Bool
&&
Bool -> Bool
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"
printAgdaDirFlag :: Flag CommandLineOptions
printAgdaDirFlag :: Flag CommandLineOptions
printAgdaDirFlag CommandLineOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optPrintAgdaDir :: Bool
optPrintAgdaDir = 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 :: Bool
optPrintVersion = Bool
True }
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
let sizedTypes :: WithDefault 'False
sizedTypes = PragmaOptions -> WithDefault 'False
optSizedTypes PragmaOptions
o
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSafe :: Bool
optSafe = Bool
True
, optSizedTypes :: WithDefault 'False
optSizedTypes = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False WithDefault 'False
sizedTypes
}
cohesionFlag :: Flag PragmaOptions
cohesionFlag :: Flag PragmaOptions
cohesionFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCohesion :: Bool
optCohesion = Bool
True }
flatSplitFlag :: Flag PragmaOptions
flatSplitFlag :: Flag PragmaOptions
flatSplitFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o
{ optFlatSplit :: WithDefault 'False
optFlatSplit = forall (b :: Bool). Bool -> WithDefault b
Value Bool
True
, optCohesion :: Bool
optCohesion = Bool
True
}
doubleCheckFlag :: Bool -> Flag PragmaOptions
doubleCheckFlag :: Bool -> Flag PragmaOptions
doubleCheckFlag Bool
b PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optDoubleCheck :: Bool
optDoubleCheck = Bool
b }
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
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag Bool
b PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCaching :: Bool
optCaching = Bool
b }
propFlag :: Flag PragmaOptions
propFlag :: Flag PragmaOptions
propFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProp :: Bool
optProp = Bool
True }
noPropFlag :: Flag PragmaOptions
noPropFlag :: Flag PragmaOptions
noPropFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProp :: Bool
optProp = Bool
False }
twoLevelFlag :: Flag PragmaOptions
twoLevelFlag :: Flag PragmaOptions
twoLevelFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optTwoLevel :: WithDefault 'False
optTwoLevel = forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
experimentalIrrelevanceFlag :: Flag PragmaOptions
experimentalIrrelevanceFlag :: Flag PragmaOptions
experimentalIrrelevanceFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optExperimentalIrrelevance :: Bool
optExperimentalIrrelevance = Bool
True }
irrelevantProjectionsFlag :: Flag PragmaOptions
irrelevantProjectionsFlag :: Flag PragmaOptions
irrelevantProjectionsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optIrrelevantProjections :: Bool
optIrrelevantProjections = Bool
True }
noIrrelevantProjectionsFlag :: Flag PragmaOptions
noIrrelevantProjectionsFlag :: Flag PragmaOptions
noIrrelevantProjectionsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optIrrelevantProjections :: Bool
optIrrelevantProjections = Bool
False }
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 }
noLoadPrimitivesFlag :: Flag PragmaOptions
noLoadPrimitivesFlag :: Flag PragmaOptions
noLoadPrimitivesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o
{ optLoadPrimitives :: Bool
optLoadPrimitives = Bool
False
, optImportSorts :: Bool
optImportSorts = Bool
False
}
allowUnsolvedFlag :: Flag PragmaOptions
allowUnsolvedFlag :: Flag PragmaOptions
allowUnsolvedFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set WarningName
unsolvedWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAllowUnsolved :: Bool
optAllowUnsolved = Bool
True
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
allowIncompleteMatchFlag :: Flag PragmaOptions
allowIncompleteMatchFlag :: Flag PragmaOptions
allowIncompleteMatchFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set WarningName
incompleteMatchWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAllowIncompleteMatch :: Bool
optAllowIncompleteMatch = Bool
True
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
showImplicitFlag :: Flag PragmaOptions
showImplicitFlag :: Flag PragmaOptions
showImplicitFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optShowImplicit :: Bool
optShowImplicit = Bool
True }
showIrrelevantFlag :: Flag PragmaOptions
showIrrelevantFlag :: Flag PragmaOptions
showIrrelevantFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optShowIrrelevant :: Bool
optShowIrrelevant = Bool
True }
showIdentitySubstitutionsFlag :: Flag PragmaOptions
showIdentitySubstitutionsFlag :: Flag PragmaOptions
showIdentitySubstitutionsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optShowIdentitySubstitutions :: Bool
optShowIdentitySubstitutions = Bool
True }
asciiOnlyFlag :: Flag PragmaOptions
asciiOnlyFlag :: Flag PragmaOptions
asciiOnlyFlag 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
AsciiOnly
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUseUnicode :: UnicodeOrAscii
optUseUnicode = UnicodeOrAscii
AsciiOnly }
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 }
countClustersFlag :: Flag PragmaOptions
countClustersFlag :: Flag PragmaOptions
countClustersFlag PragmaOptions
o =
#ifdef COUNT_CLUSTERS
return $ o { optCountClusters = True }
#else
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
String
"Cluster counting has not been enabled in this build of Agda."
#endif
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAutoInline :: Bool
optAutoInline = Bool
False }
autoInlineFlag :: Flag PragmaOptions
autoInlineFlag :: Flag PragmaOptions
autoInlineFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAutoInline :: Bool
optAutoInline = Bool
True }
noPrintPatSynFlag :: Flag PragmaOptions
noPrintPatSynFlag :: Flag PragmaOptions
noPrintPatSynFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPrintPatternSynonyms :: Bool
optPrintPatternSynonyms = Bool
False }
noFastReduceFlag :: Flag PragmaOptions
noFastReduceFlag :: Flag PragmaOptions
noFastReduceFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optFastReduce :: Bool
optFastReduce = Bool
False }
callByNameFlag :: Flag PragmaOptions
callByNameFlag :: Flag PragmaOptions
callByNameFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCallByName :: Bool
optCallByName = Bool
True }
noPositivityFlag :: Flag PragmaOptions
noPositivityFlag :: Flag PragmaOptions
noPositivityFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
NotStrictlyPositive_)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optDisablePositivity :: Bool
optDisablePositivity = Bool
True
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
dontTerminationCheckFlag :: Flag PragmaOptions
dontTerminationCheckFlag :: Flag PragmaOptions
dontTerminationCheckFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
TerminationIssue_)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optTerminationCheck :: Bool
optTerminationCheck = Bool
False
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniverseCheck :: Bool
optUniverseCheck = Bool
False }
omegaInOmegaFlag :: Flag PragmaOptions
omegaInOmegaFlag :: Flag PragmaOptions
omegaInOmegaFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOmegaInOmega :: Bool
optOmegaInOmega = Bool
True }
cumulativityFlag :: Flag PragmaOptions
cumulativityFlag :: Flag PragmaOptions
cumulativityFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCumulativity :: Bool
optCumulativity = Bool
True }
noCumulativityFlag :: Flag PragmaOptions
noCumulativityFlag :: Flag PragmaOptions
noCumulativityFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCumulativity :: Bool
optCumulativity = Bool
False }
noEtaFlag :: Flag PragmaOptions
noEtaFlag :: Flag PragmaOptions
noEtaFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optEta :: Bool
optEta = Bool
False }
sizedTypes :: Flag PragmaOptions
sizedTypes :: Flag PragmaOptions
sizedTypes PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSizedTypes :: WithDefault 'False
optSizedTypes = forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
noSizedTypes :: Flag PragmaOptions
noSizedTypes :: Flag PragmaOptions
noSizedTypes PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSizedTypes :: WithDefault 'False
optSizedTypes = forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
guardedness :: Flag PragmaOptions
guardedness :: Flag PragmaOptions
guardedness PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optGuardedness :: WithDefault 'False
optGuardedness = forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
noGuardedness :: Flag PragmaOptions
noGuardedness :: Flag PragmaOptions
noGuardedness PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optGuardedness :: WithDefault 'False
optGuardedness = forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
injectiveTypeConstructorFlag :: Flag PragmaOptions
injectiveTypeConstructorFlag :: Flag PragmaOptions
injectiveTypeConstructorFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optInjectiveTypeConstructors :: Bool
optInjectiveTypeConstructors = Bool
True }
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
True }
noUniversePolymorphismFlag :: Flag PragmaOptions
noUniversePolymorphismFlag :: Flag PragmaOptions
noUniversePolymorphismFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
False }
noForcingFlag :: Flag PragmaOptions
noForcingFlag :: Flag PragmaOptions
noForcingFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optForcing :: Bool
optForcing = Bool
False }
noProjectionLikeFlag :: Flag PragmaOptions
noProjectionLikeFlag :: Flag PragmaOptions
noProjectionLikeFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProjectionLike :: Bool
optProjectionLike = Bool
False }
withKFlag :: Flag PragmaOptions
withKFlag :: Flag PragmaOptions
withKFlag 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 (b :: Bool). Bool -> WithDefault b
Value Bool
False }
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 (b :: Bool). Bool -> WithDefault b
Value Bool
True
, optFlatSplit :: WithDefault 'False
optFlatSplit = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False (PragmaOptions -> WithDefault 'False
optFlatSplit PragmaOptions
o)
}
copatternsFlag :: Flag PragmaOptions
copatternsFlag :: Flag PragmaOptions
copatternsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCopatterns :: Bool
optCopatterns = Bool
True }
noCopatternsFlag :: Flag PragmaOptions
noCopatternsFlag :: Flag PragmaOptions
noCopatternsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCopatterns :: Bool
optCopatterns = Bool
False }
noPatternMatchingFlag :: Flag PragmaOptions
noPatternMatchingFlag :: Flag PragmaOptions
noPatternMatchingFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPatternMatching :: Bool
optPatternMatching = Bool
False }
exactSplitFlag :: Flag PragmaOptions
exactSplitFlag :: Flag PragmaOptions
exactSplitFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => a -> Set a -> Set a
Set.insert WarningName
CoverageNoExactSplit_)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optExactSplit :: Bool
optExactSplit = Bool
True
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
noExactSplitFlag :: Flag PragmaOptions
noExactSplitFlag :: Flag PragmaOptions
noExactSplitFlag PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
CoverageNoExactSplit_)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optExactSplit :: Bool
optExactSplit = Bool
False
, optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o)
}
rewritingFlag :: Flag PragmaOptions
rewritingFlag :: Flag PragmaOptions
rewritingFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optRewriting :: Bool
optRewriting = Bool
True }
firstOrderFlag :: Flag PragmaOptions
firstOrderFlag :: Flag PragmaOptions
firstOrderFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optFirstOrder :: Bool
optFirstOrder = Bool
True }
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 (b :: Bool). Bool -> WithDefault b
Value Bool
True
, optWithoutK :: WithDefault 'False
optWithoutK = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
o
, optFlatSplit :: WithDefault 'False
optFlatSplit = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False (PragmaOptions -> WithDefault 'False
optFlatSplit 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 (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optCubicalCompatible PragmaOptions
o
, optWithoutK :: WithDefault 'False
optWithoutK = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
o
, optTwoLevel :: WithDefault 'False
optTwoLevel = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optTwoLevel PragmaOptions
o
, optFlatSplit :: WithDefault 'False
optFlatSplit = forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False (PragmaOptions -> WithDefault 'False
optFlatSplit PragmaOptions
o)
}
guardedFlag :: Flag PragmaOptions
guardedFlag :: Flag PragmaOptions
guardedFlag PragmaOptions
o = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optGuarded :: Bool
optGuarded = Bool
True }
postfixProjectionsFlag :: Flag PragmaOptions
postfixProjectionsFlag :: Flag PragmaOptions
postfixProjectionsFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPostfixProjections :: Bool
optPostfixProjections = Bool
True }
keepPatternVariablesFlag :: Flag PragmaOptions
keepPatternVariablesFlag :: Flag PragmaOptions
keepPatternVariablesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optKeepPatternVariables :: Bool
optKeepPatternVariables = Bool
True }
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 }
overlappingInstancesFlag :: Flag PragmaOptions
overlappingInstancesFlag :: Flag PragmaOptions
overlappingInstancesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOverlappingInstances :: Bool
optOverlappingInstances = Bool
True }
noOverlappingInstancesFlag :: Flag PragmaOptions
noOverlappingInstancesFlag :: Flag PragmaOptions
noOverlappingInstancesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOverlappingInstances :: Bool
optOverlappingInstances = Bool
False }
qualifiedInstancesFlag :: Flag PragmaOptions
qualifiedInstancesFlag :: Flag PragmaOptions
qualifiedInstancesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optQualifiedInstances :: Bool
optQualifiedInstances = Bool
True }
noQualifiedInstancesFlag :: Flag PragmaOptions
noQualifiedInstancesFlag :: Flag PragmaOptions
noQualifiedInstancesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optQualifiedInstances :: Bool
optQualifiedInstances = Bool
False }
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 }
compileFlagNoMain :: Flag PragmaOptions
compileFlagNoMain :: Flag PragmaOptions
compileFlagNoMain PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCompileNoMain :: Bool
optCompileNoMain = 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}. ExceptT String Identity 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}. ExceptT String Identity 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 :: ExceptT String Identity 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 (WarningMode -> WarningMode)
warningModeUpdate String
s of
Right WarningMode -> WarningMode
upd -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
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}. ExceptT String Identity 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}. ExceptT String Identity 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 :: ExceptT String Identity 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 }
noImportSorts :: Flag PragmaOptions
noImportSorts :: Flag PragmaOptions
noImportSorts PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optImportSorts :: Bool
optImportSorts = Bool
False }
allowExec :: Flag PragmaOptions
allowExec :: Flag PragmaOptions
allowExec PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAllowExec :: Bool
optAllowExec = Bool
True }
saveMetas :: Bool -> Flag PragmaOptions
saveMetas :: Bool -> Flag PragmaOptions
saveMetas Bool
save PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSaveMetas :: WithDefault 'False
optSaveMetas = forall (b :: Bool). Bool -> WithDefault b
Value Bool
save }
eraseRecordParametersFlag :: Flag PragmaOptions
eraseRecordParametersFlag :: Flag PragmaOptions
eraseRecordParametersFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optEraseRecordParameters :: Bool
optEraseRecordParameters = Bool
True }
noEraseRecordParametersFlag :: Flag PragmaOptions
noEraseRecordParametersFlag :: Flag PragmaOptions
noEraseRecordParametersFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optEraseRecordParameters :: Bool
optEraseRecordParameters = Bool
False }
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"
keepCoveringClausesFlag :: Flag PragmaOptions
keepCoveringClausesFlag :: Flag PragmaOptions
keepCoveringClausesFlag PragmaOptions
o = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optKeepCoveringClauses :: Bool
optKeepCoveringClauses = Bool
True }
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 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
printAgdaDirFlag)
(String
"print $AGDA_DIR and 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
"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. [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' PragmaOptions CommandLineOptions
lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
pragmaOptions
lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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' PragmaOptions CommandLineOptions
lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
deadPragmaOptions
where
msgSharing :: String
msgSharing = String
"(in favor of the Agda abstract machine)"
pragmaOptions :: [OptDescr (Flag PragmaOptions)]
pragmaOptions :: [OptDescr (Flag PragmaOptions)]
pragmaOptions =
[ forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"show-implicit"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showImplicitFlag)
String
"show implicit arguments when printing"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"show-irrelevant"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showIrrelevantFlag)
String
"show irrelevant arguments when printing"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"show-identity-substitutions"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showIdentitySubstitutionsFlag)
String
"show all arguments of metavariables when printing terms"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-unicode"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
asciiOnlyFlag)
String
"don't use unicode characters when printing terms"
, 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"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"allow-unsolved-metas"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowUnsolvedFlag)
String
"succeed and create interface file regardless of unsolved meta variables"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"allow-incomplete-matches"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowIncompleteMatchFlag)
String
"succeed and create interface file regardless of incomplete pattern matches"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-positivity-check"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPositivityFlag)
String
"do not warn about not strictly positive data types"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-termination-check"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontTerminationCheckFlag)
String
"do not warn about possibly nonterminating code"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"type-in-type"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontUniverseCheckFlag)
String
"ignore universe levels (this makes Agda inconsistent)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"omega-in-omega"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
omegaInOmegaFlag)
String
"enable typing rule Setω : Setω (this makes Agda inconsistent)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"cumulativity"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cumulativityFlag)
String
"enable subtyping of universes (e.g. Set =< Set₁)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-cumulativity"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCumulativityFlag)
String
"disable subtyping of universes (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"prop"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
propFlag)
String
"enable the use of the Prop universe"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-prop"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPropFlag)
String
"disable the use of the Prop universe (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"two-level"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
twoLevelFlag)
String
"enable the use of SSet* universes"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"sized-types"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
sizedTypes)
String
"enable sized types (inconsistent with --guardedness)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-sized-types"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSizedTypes)
String
"disable sized types (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"cohesion"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cohesionFlag)
String
"enable the cohesion modalities (in particular @flat)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"flat-split"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
flatSplitFlag)
String
"allow split on (@flat x : A) arguments (implies --cohesion)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"guardedness"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardedness)
String
"enable constructor-based guarded corecursion (inconsistent with --sized-types)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-guardedness"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noGuardedness)
String
"disable constructor-based guarded corecursion (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"injective-type-constructors"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
injectiveTypeConstructorFlag)
String
"enable injective type constructors (makes Agda anti-classical and possibly inconsistent)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-universe-polymorphism"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noUniversePolymorphismFlag)
String
"disable universe polymorphism"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"universe-polymorphism"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
universePolymorphismFlag)
String
"enable universe polymorphism (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"irrelevant-projections"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
irrelevantProjectionsFlag)
String
"enable projection of irrelevant record fields and similar irrelevant definitions (inconsistent)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-irrelevant-projections"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noIrrelevantProjectionsFlag)
String
"disable projection of irrelevant record fields and similar irrelevant definitions (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"experimental-irrelevance"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
experimentalIrrelevanceFlag)
String
"enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"copatterns"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
copatternsFlag)
String
"enable definitions by copattern matching (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-copatterns"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCopatternsFlag)
String
"disable definitions by copattern matching"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-pattern-matching"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPatternMatchingFlag)
String
"disable pattern matching completely"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"exact-split"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
exactSplitFlag)
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 Flag PragmaOptions
noExactSplitFlag)
String
"do not require all clauses in a definition to hold as definitional equalities (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-eta-equality"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noEtaFlag)
String
"default records to no-eta-equality"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-forcing"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noForcingFlag)
String
"disable the forcing analysis for data constructors (optimisation)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-projection-like"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noProjectionLikeFlag)
String
"disable the analysis whether function signatures liken those of projections (optimisation)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"erase-record-parameters"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
eraseRecordParametersFlag)
String
"mark all parameters of record modules as erased"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-erase-record-parameters"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noEraseRecordParametersFlag)
String
"do mark all parameters of record modules as erased (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"rewriting"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
rewritingFlag)
String
"enable 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"guarded"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardedFlag)
String
"enable @lock/@tick attributes"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"lossy-unification"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
firstOrderFlag)
String
"enable heuristically unifying `f es = f es'` by unifying `es = es'`, even when it could lose solutions."
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"postfix-projections"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
postfixProjectionsFlag)
String
"make postfix projection notation the default"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"keep-pattern-variables"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
keepPatternVariablesFlag)
String
"don't replace variables with dot patterns during case splitting"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"overlapping-instances"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
overlappingInstancesFlag)
String
"consider recursive instance arguments during pruning of instance candidates"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-overlapping-instances"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noOverlappingInstancesFlag)
String
"don't consider recursive instance arguments during pruning of instance candidates (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"qualified-instances"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
qualifiedInstancesFlag)
String
"use instances with qualified names (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-qualified-instances"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noQualifiedInstancesFlag)
String
"don't use instances with qualified names"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"double-check"] (forall a. a -> ArgDescr a
NoArg (Bool -> Flag PragmaOptions
doubleCheckFlag Bool
True))
String
"enable double-checking of all terms using the internal typechecker"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-double-check"] (forall a. a -> ArgDescr a
NoArg (Bool -> Flag PragmaOptions
doubleCheckFlag Bool
False))
String
"disable double-checking of terms (default)"
, 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. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-main"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
compileFlagNoMain)
String
"do not treat the requested module as the main module of a program when compiling"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"caching"] (forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
cachingFlag Bool
True)
String
"enable caching of typechecking (default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-caching"] (forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
cachingFlag Bool
False)
String
"disable caching of typechecking"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"count-clusters"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
countClustersFlag)
(String
"count extended grapheme clusters when " forall a. [a] -> [a] -> [a]
++
String
"generating LaTeX (note that this flag " forall a. [a] -> [a] -> [a]
++
#ifdef COUNT_CLUSTERS
"is not enabled in all builds of Agda)"
#else
String
"has not been enabled in this build of Agda)"
#endif
)
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"auto-inline"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
autoInlineFlag)
String
"enable automatic compile-time inlining"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-auto-inline"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noAutoInlineFlag)
(String
"disable automatic compile-time inlining (default), " forall a. [a] -> [a] -> [a]
++
String
"only definitions marked INLINE will be inlined")
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-print-pattern-synonyms"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPrintPatSynFlag)
String
"expand pattern synonyms when printing terms"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-fast-reduce"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noFastReduceFlag)
String
"disable reduction using the Agda Abstract Machine"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"call-by-name"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
callByNameFlag)
String
"use call-by-name evaluation instead of call-by-need"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-import-sorts"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noImportSorts)
String
"disable the implicit import of Agda.Primitive using (Set; Prop) at the start of each top-level module"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-load-primitives"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noLoadPrimitivesFlag)
String
"disable loading of primitive modules at all (implies --no-import-sorts)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"allow-exec"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowExec)
String
"allow system calls to trusted executables with primExec"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"save-metas"] (forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
saveMetas Bool
True)
String
"save meta-variables"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"no-save-metas"] (forall a. a -> ArgDescr a
NoArg forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
saveMetas Bool
False)
String
"do not save meta-variables (the default)"
, forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"keep-covering-clauses"] (forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
keepCoveringClausesFlag)
String
"do not discard covering clauses (required for some external backends)"
]
deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
deadPragmaOptions = 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) forall a b. (a -> b) -> a -> b
$
[ (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")
]
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]
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 (t :: * -> *) a. Foldable t => t 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 (t :: * -> *) a. Foldable t => t 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 -> [[String]]
alts :: String -> [[String]]
alts String
s = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [[a]]
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 -> [[String]]
alts String
s of
[] -> String
s
[String]
as : [[String]]
_ -> String
s forall a. [a] -> [a] -> [a]
++ String
" (did you mean " forall a. [a] -> [a] -> [a]
++ [String] -> String
sugs [String]
as forall a. [a] -> [a] -> [a]
++ String
" ?)"
sugs :: [String] -> String
sugs :: [String] -> String
sugs [String
a] = String
a
sugs [String]
as = String
"any of " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
as
parsePragmaOptions
:: [String]
-> CommandLineOptions
-> OptM PragmaOptions
parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
parsePragmaOptions [String]
argv CommandLineOptions
opts = do
PragmaOptions
ps <- forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple [String]
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)
CommandLineOptions
_ <- Flag CommandLineOptions
checkOpts (CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
ps })
forall (m :: * -> *) a. Monad m => a -> m a
return 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 (Bool -> Bool
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)