{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
module Agda.Interaction.Options
( CommandLineOptions(..)
, PragmaOptions(..)
, OptionsPragma
, Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
, Verbosity, VerboseKey, VerboseLevel
, HtmlHighlight(..)
, WarningMode(..)
, checkOpts
, parsePragmaOptions
, parsePluginOptions
, stripRTS
, defaultOptions
, defaultInteractionOptions
, defaultVerbosity
, defaultCutOff
, defaultPragmaOptions
, standardOptions_
, unsafePragmaOptions
, restartOptions
, infectiveOptions
, coinfectiveOptions
, safeFlag
, mapFlag
, usage
, defaultLibDir
, inputFlag
, standardOptions, deadStandardOptions
, getOptSimple
) where
import Control.Monad ( when )
import Control.Monad.Trans
import Data.IORef
import Data.Function
import Data.Maybe
import Data.List ( intercalate )
import qualified Data.Set as Set
import System.Console.GetOpt ( getOpt', usageInfo, ArgOrder(ReturnInOrder)
, OptDescr(..), ArgDescr(..)
)
import System.Directory ( doesFileExist, doesDirectoryExist )
import Text.EditDistance
import Agda.Termination.CutOff ( CutOff(..) )
import Agda.Interaction.Library
import Agda.Interaction.Options.Help
import Agda.Interaction.Options.IORefs
import Agda.Interaction.Options.Warnings
import Agda.Utils.Except
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.FileName ( absolute, AbsolutePath, filePath )
import Agda.Utils.Functor ( (<&>) )
import Agda.Utils.Lens ( Lens', over )
import Agda.Utils.List ( groupOn, wordsBy )
import Agda.Utils.Monad ( ifM, readM )
import Agda.Utils.Trie ( Trie )
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.WithDefault
import Agda.Version
import Paths_Agda ( getDataFileName )
type VerboseKey = String
type VerboseLevel = Int
type Verbosity = Trie VerboseKey VerboseLevel
data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
deriving (Int -> HtmlHighlight -> ShowS
[HtmlHighlight] -> ShowS
HtmlHighlight -> String
(Int -> HtmlHighlight -> ShowS)
-> (HtmlHighlight -> String)
-> ([HtmlHighlight] -> ShowS)
-> Show HtmlHighlight
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HtmlHighlight] -> ShowS
$cshowList :: [HtmlHighlight] -> ShowS
show :: HtmlHighlight -> String
$cshow :: HtmlHighlight -> String
showsPrec :: Int -> HtmlHighlight -> ShowS
$cshowsPrec :: Int -> HtmlHighlight -> ShowS
Show, HtmlHighlight -> HtmlHighlight -> Bool
(HtmlHighlight -> HtmlHighlight -> Bool)
-> (HtmlHighlight -> HtmlHighlight -> Bool) -> Eq HtmlHighlight
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HtmlHighlight -> HtmlHighlight -> Bool
$c/= :: HtmlHighlight -> HtmlHighlight -> Bool
== :: HtmlHighlight -> HtmlHighlight -> Bool
$c== :: HtmlHighlight -> HtmlHighlight -> Bool
Eq)
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 -> Bool
optShowVersion :: Bool
, CommandLineOptions -> Maybe Help
optShowHelp :: Maybe Help
, CommandLineOptions -> Bool
optInteractive :: Bool
, CommandLineOptions -> Bool
optGHCiInteraction :: Bool
, CommandLineOptions -> Bool
optJSONInteraction :: Bool
, CommandLineOptions -> Bool
optOptimSmashing :: Bool
, CommandLineOptions -> Maybe String
optCompileDir :: Maybe FilePath
, CommandLineOptions -> Bool
optGenerateVimFile :: Bool
, CommandLineOptions -> Bool
optGenerateLaTeX :: Bool
, CommandLineOptions -> Bool
optGenerateHTML :: Bool
, CommandLineOptions -> HtmlHighlight
optHTMLHighlight :: HtmlHighlight
, CommandLineOptions -> Maybe String
optDependencyGraph :: Maybe FilePath
, CommandLineOptions -> String
optLaTeXDir :: FilePath
, CommandLineOptions -> String
optHTMLDir :: FilePath
, CommandLineOptions -> Maybe String
optCSSFile :: Maybe FilePath
, CommandLineOptions -> Bool
optIgnoreInterfaces :: Bool
, CommandLineOptions -> Bool
optIgnoreAllInterfaces :: Bool
, CommandLineOptions -> Bool
optLocalInterfaces :: Bool
, CommandLineOptions -> PragmaOptions
optPragmaOptions :: PragmaOptions
, CommandLineOptions -> Bool
optOnlyScopeChecking :: Bool
, CommandLineOptions -> Maybe String
optWithCompiler :: Maybe FilePath
}
deriving Int -> CommandLineOptions -> ShowS
[CommandLineOptions] -> ShowS
CommandLineOptions -> String
(Int -> CommandLineOptions -> ShowS)
-> (CommandLineOptions -> String)
-> ([CommandLineOptions] -> ShowS)
-> Show CommandLineOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CommandLineOptions] -> ShowS
$cshowList :: [CommandLineOptions] -> ShowS
show :: CommandLineOptions -> String
$cshow :: CommandLineOptions -> String
showsPrec :: Int -> CommandLineOptions -> ShowS
$cshowsPrec :: Int -> CommandLineOptions -> ShowS
Show
data PragmaOptions = PragmaOptions
{ PragmaOptions -> Bool
optShowImplicit :: Bool
, PragmaOptions -> Bool
optShowIrrelevant :: Bool
, PragmaOptions -> Bool
optUseUnicode :: Bool
, PragmaOptions -> Verbosity
optVerbose :: Verbosity
, PragmaOptions -> Bool
optProp :: Bool
, PragmaOptions -> Bool
optAllowUnsolved :: Bool
, PragmaOptions -> Bool
optAllowIncompleteMatch :: Bool
, PragmaOptions -> Bool
optDisablePositivity :: Bool
, PragmaOptions -> Bool
optTerminationCheck :: Bool
, PragmaOptions -> CutOff
optTerminationDepth :: CutOff
, PragmaOptions -> Bool
optCompletenessCheck :: Bool
, PragmaOptions -> Bool
optUniverseCheck :: Bool
, PragmaOptions -> Bool
optOmegaInOmega :: Bool
, PragmaOptions -> WithDefault 'False
optSubtyping :: WithDefault 'False
, PragmaOptions -> Bool
optCumulativity :: Bool
, PragmaOptions -> WithDefault 'True
optSizedTypes :: WithDefault 'True
, PragmaOptions -> WithDefault 'True
optGuardedness :: WithDefault 'True
, PragmaOptions -> Bool
optInjectiveTypeConstructors :: Bool
, PragmaOptions -> Bool
optUniversePolymorphism :: Bool
, PragmaOptions -> Bool
optIrrelevantProjections :: Bool
, PragmaOptions -> Bool
optExperimentalIrrelevance :: Bool
, PragmaOptions -> WithDefault 'False
optWithoutK :: 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
optRewriting :: Bool
, PragmaOptions -> Bool
optCubical :: Bool
, PragmaOptions -> Bool
optPostfixProjections :: Bool
, PragmaOptions -> Bool
optKeepPatternVariables :: Bool
, PragmaOptions -> Int
optInstanceSearchDepth :: Int
, PragmaOptions -> Bool
optOverlappingInstances :: Bool
, PragmaOptions -> Int
optInversionMaxDepth :: Int
, PragmaOptions -> Bool
optSafe :: Bool
, PragmaOptions -> Bool
optDoubleCheck :: Bool
, PragmaOptions -> Bool
optSyntacticEquality :: Bool
, PragmaOptions -> Bool
optCompareSorts :: Bool
, 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
optConfluenceCheck :: Bool
, PragmaOptions -> Bool
optFlatSplit :: Bool
}
deriving (Int -> PragmaOptions -> ShowS
[PragmaOptions] -> ShowS
PragmaOptions -> String
(Int -> PragmaOptions -> ShowS)
-> (PragmaOptions -> String)
-> ([PragmaOptions] -> ShowS)
-> Show PragmaOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PragmaOptions] -> ShowS
$cshowList :: [PragmaOptions] -> ShowS
show :: PragmaOptions -> String
$cshow :: PragmaOptions -> String
showsPrec :: Int -> PragmaOptions -> ShowS
$cshowsPrec :: Int -> PragmaOptions -> ShowS
Show, PragmaOptions -> PragmaOptions -> Bool
(PragmaOptions -> PragmaOptions -> Bool)
-> (PragmaOptions -> PragmaOptions -> Bool) -> Eq PragmaOptions
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)
type OptionsPragma = [String]
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
mapFlag :: ShowS -> OptDescr a -> OptDescr a
mapFlag f :: ShowS
f (Option _ long :: [String]
long arg :: ArgDescr a
arg descr :: String
descr) = String -> [String] -> ArgDescr a -> String -> OptDescr a
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
f [String]
long) ArgDescr a
arg String
descr
defaultVerbosity :: Verbosity
defaultVerbosity :: Verbosity
defaultVerbosity = [String] -> Int -> Verbosity
forall k v. [k] -> v -> Trie k v
Trie.singleton [] 1
defaultInteractionOptions :: PragmaOptions
defaultInteractionOptions :: PragmaOptions
defaultInteractionOptions = PragmaOptions
defaultPragmaOptions
defaultOptions :: CommandLineOptions
defaultOptions :: CommandLineOptions
defaultOptions = Options :: String
-> Maybe String
-> [String]
-> [AbsolutePath]
-> [String]
-> Maybe String
-> Bool
-> Bool
-> Bool
-> Maybe Help
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe String
-> Bool
-> Bool
-> Bool
-> HtmlHighlight
-> Maybe String
-> String
-> String
-> Maybe String
-> Bool
-> Bool
-> Bool
-> PragmaOptions
-> Bool
-> Maybe String
-> CommandLineOptions
Options
{ optProgramName :: String
optProgramName = "agda"
, optInputFile :: Maybe String
optInputFile = Maybe String
forall a. Maybe a
Nothing
, optIncludePaths :: [String]
optIncludePaths = []
, optAbsoluteIncludePaths :: [AbsolutePath]
optAbsoluteIncludePaths = []
, optLibraries :: [String]
optLibraries = []
, optOverrideLibrariesFile :: Maybe String
optOverrideLibrariesFile = Maybe String
forall a. Maybe a
Nothing
, optDefaultLibs :: Bool
optDefaultLibs = Bool
True
, optUseLibs :: Bool
optUseLibs = Bool
True
, optShowVersion :: Bool
optShowVersion = Bool
False
, optShowHelp :: Maybe Help
optShowHelp = Maybe Help
forall a. Maybe a
Nothing
, optInteractive :: Bool
optInteractive = Bool
False
, optGHCiInteraction :: Bool
optGHCiInteraction = Bool
False
, optJSONInteraction :: Bool
optJSONInteraction = Bool
False
, optOptimSmashing :: Bool
optOptimSmashing = Bool
True
, optCompileDir :: Maybe String
optCompileDir = Maybe String
forall a. Maybe a
Nothing
, optGenerateVimFile :: Bool
optGenerateVimFile = Bool
False
, optGenerateLaTeX :: Bool
optGenerateLaTeX = Bool
False
, optGenerateHTML :: Bool
optGenerateHTML = Bool
False
, optHTMLHighlight :: HtmlHighlight
optHTMLHighlight = HtmlHighlight
HighlightAll
, optDependencyGraph :: Maybe String
optDependencyGraph = Maybe String
forall a. Maybe a
Nothing
, optLaTeXDir :: String
optLaTeXDir = String
defaultLaTeXDir
, optHTMLDir :: String
optHTMLDir = String
defaultHTMLDir
, optCSSFile :: Maybe String
optCSSFile = Maybe String
forall a. Maybe a
Nothing
, 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
, optWithCompiler :: Maybe String
optWithCompiler = Maybe String
forall a. Maybe a
Nothing
}
defaultPragmaOptions :: PragmaOptions
defaultPragmaOptions :: PragmaOptions
defaultPragmaOptions = PragmaOptions :: Bool
-> Bool
-> Bool
-> Verbosity
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> CutOff
-> Bool
-> Bool
-> Bool
-> WithDefault 'False
-> Bool
-> WithDefault 'True
-> WithDefault 'True
-> Bool
-> Bool
-> Bool
-> Bool
-> WithDefault 'False
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Bool
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> WarningMode
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> PragmaOptions
PragmaOptions
{ optShowImplicit :: Bool
optShowImplicit = Bool
False
, optShowIrrelevant :: Bool
optShowIrrelevant = Bool
False
, optUseUnicode :: Bool
optUseUnicode = Bool
True
, optVerbose :: Verbosity
optVerbose = Verbosity
defaultVerbosity
, optProp :: Bool
optProp = Bool
False
, 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
, optCompletenessCheck :: Bool
optCompletenessCheck = Bool
True
, optUniverseCheck :: Bool
optUniverseCheck = Bool
True
, optOmegaInOmega :: Bool
optOmegaInOmega = Bool
False
, optSubtyping :: WithDefault 'False
optSubtyping = WithDefault 'False
forall (b :: Bool). WithDefault b
Default
, optCumulativity :: Bool
optCumulativity = Bool
False
, optSizedTypes :: WithDefault 'True
optSizedTypes = WithDefault 'True
forall (b :: Bool). WithDefault b
Default
, optGuardedness :: WithDefault 'True
optGuardedness = WithDefault 'True
forall (b :: Bool). WithDefault b
Default
, optInjectiveTypeConstructors :: Bool
optInjectiveTypeConstructors = Bool
False
, optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
True
, optWithoutK :: WithDefault 'False
optWithoutK = WithDefault 'False
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
, optRewriting :: Bool
optRewriting = Bool
False
, optCubical :: Bool
optCubical = Bool
False
, optPostfixProjections :: Bool
optPostfixProjections = Bool
False
, optKeepPatternVariables :: Bool
optKeepPatternVariables = Bool
False
, optInstanceSearchDepth :: Int
optInstanceSearchDepth = 500
, optOverlappingInstances :: Bool
optOverlappingInstances = Bool
False
, optInversionMaxDepth :: Int
optInversionMaxDepth = 50
, optSafe :: Bool
optSafe = Bool
False
, optDoubleCheck :: Bool
optDoubleCheck = Bool
False
, optSyntacticEquality :: Bool
optSyntacticEquality = Bool
True
, optCompareSorts :: Bool
optCompareSorts = Bool
True
, optWarningMode :: WarningMode
optWarningMode = WarningMode
defaultWarningMode
, optCompileNoMain :: Bool
optCompileNoMain = Bool
False
, optCaching :: Bool
optCaching = Bool
True
, optCountClusters :: Bool
optCountClusters = Bool
False
, optAutoInline :: Bool
optAutoInline = Bool
True
, optPrintPatternSynonyms :: Bool
optPrintPatternSynonyms = Bool
True
, optFastReduce :: Bool
optFastReduce = Bool
True
, optConfluenceCheck :: Bool
optConfluenceCheck = Bool
False
, optFlatSplit :: Bool
optFlatSplit = Bool
True
}
defaultCutOff :: CutOff
defaultCutOff :: CutOff
defaultCutOff = Int -> CutOff
CutOff 0
defaultLaTeXDir :: String
defaultLaTeXDir :: String
defaultLaTeXDir = "latex"
defaultHTMLDir :: String
defaultHTMLDir :: String
defaultHTMLDir = "html"
type OptM = ExceptT String IO
runOptM :: OptM a -> IO (Either String a)
runOptM :: OptM a -> IO (Either String a)
runOptM = OptM a -> IO (Either String a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
type Flag opts = opts -> OptM opts
checkOpts :: Flag CommandLineOptions
checkOpts :: Flag CommandLineOptions
checkOpts opts :: CommandLineOptions
opts
| Bool
htmlRelated = String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
htmlRelatedMessage
| Bool -> Bool
not ([CommandLineOptions -> Bool] -> Int
matches [CommandLineOptions -> Bool
optGHCiInteraction, CommandLineOptions -> Bool
optJSONInteraction, Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool)
-> (CommandLineOptions -> Maybe String)
-> CommandLineOptions
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe String
optInputFile] Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1) =
String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "Choose at most one: input file, --interactive, or --interaction-json.\n"
| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ CommandLineOptions -> Bool
p CommandLineOptions
opts Bool -> Bool -> Bool
&& [CommandLineOptions -> Bool] -> Int
matches [CommandLineOptions -> Bool]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 | (p :: CommandLineOptions -> Bool
p, ps :: [CommandLineOptions -> Bool]
ps) <- [(CommandLineOptions -> Bool, [CommandLineOptions -> Bool])]
exclusive ] =
String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
exclusiveMessage
| Bool
otherwise = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return CommandLineOptions
opts
where
matches :: [CommandLineOptions -> Bool] -> Int
matches = [CommandLineOptions -> Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([CommandLineOptions -> Bool] -> Int)
-> ([CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool])
-> [CommandLineOptions -> Bool]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CommandLineOptions -> Bool) -> Bool)
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter ((CommandLineOptions -> Bool) -> CommandLineOptions -> Bool
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
opts)
optionChanged :: (CommandLineOptions -> a) -> Bool
optionChanged opt :: CommandLineOptions -> a
opt = (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (a -> a -> Bool)
-> (CommandLineOptions -> a)
-> CommandLineOptions
-> CommandLineOptions
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CommandLineOptions -> a
opt) CommandLineOptions
opts CommandLineOptions
defaultOptions
atMostOne :: [CommandLineOptions -> Bool]
atMostOne =
[ CommandLineOptions -> Bool
optGenerateHTML
, Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool)
-> (CommandLineOptions -> Maybe String)
-> CommandLineOptions
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOptions -> Maybe String
optDependencyGraph
] [CommandLineOptions -> Bool]
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. [a] -> [a] -> [a]
++
((CommandLineOptions -> Bool, [CommandLineOptions -> Bool])
-> CommandLineOptions -> Bool)
-> [(CommandLineOptions -> Bool, [CommandLineOptions -> Bool])]
-> [CommandLineOptions -> Bool]
forall a b. (a -> b) -> [a] -> [b]
map (CommandLineOptions -> Bool, [CommandLineOptions -> Bool])
-> CommandLineOptions -> Bool
forall a b. (a, b) -> a
fst [(CommandLineOptions -> Bool, [CommandLineOptions -> Bool])]
exclusive
exclusive :: [(CommandLineOptions -> Bool, [CommandLineOptions -> Bool])]
exclusive =
[ ( CommandLineOptions -> Bool
optOnlyScopeChecking
, CommandLineOptions -> Bool
optGenerateVimFile (CommandLineOptions -> Bool)
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. a -> [a] -> [a]
:
[CommandLineOptions -> Bool]
atMostOne
)
, ( CommandLineOptions -> Bool
optInteractive
, CommandLineOptions -> Bool
optGenerateLaTeX (CommandLineOptions -> Bool)
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. a -> [a] -> [a]
: [CommandLineOptions -> Bool]
atMostOne
)
, ( CommandLineOptions -> Bool
optGHCiInteraction
, CommandLineOptions -> Bool
optGenerateLaTeX (CommandLineOptions -> Bool)
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. a -> [a] -> [a]
: [CommandLineOptions -> Bool]
atMostOne
)
, ( CommandLineOptions -> Bool
optJSONInteraction
, CommandLineOptions -> Bool
optGenerateLaTeX (CommandLineOptions -> Bool)
-> [CommandLineOptions -> Bool] -> [CommandLineOptions -> Bool]
forall a. a -> [a] -> [a]
: [CommandLineOptions -> Bool]
atMostOne
)
]
exclusiveMessage :: String
exclusiveMessage = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ "The options --interactive, --interaction, --interaction-json and"
, "--only-scope-checking cannot be combined with each other or"
, "with --html or --dependency-graph. Furthermore"
, "--interactive and --interaction cannot be combined with"
, "--latex, and --only-scope-checking cannot be combined with"
, "--vim."
]
htmlRelated :: Bool
htmlRelated = Bool -> Bool
not (CommandLineOptions -> Bool
optGenerateHTML CommandLineOptions
opts) Bool -> Bool -> Bool
&&
( (CommandLineOptions -> String) -> Bool
forall a. Eq a => (CommandLineOptions -> a) -> Bool
optionChanged CommandLineOptions -> String
optHTMLDir
Bool -> Bool -> Bool
|| (CommandLineOptions -> HtmlHighlight) -> Bool
forall a. Eq a => (CommandLineOptions -> a) -> Bool
optionChanged CommandLineOptions -> HtmlHighlight
optHTMLHighlight
Bool -> Bool -> Bool
|| (CommandLineOptions -> Maybe String) -> Bool
forall a. Eq a => (CommandLineOptions -> a) -> Bool
optionChanged CommandLineOptions -> Maybe String
optCSSFile
)
htmlRelatedMessage :: String
htmlRelatedMessage = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ "The options --html-highlight, --css-dir and --html-dir"
, "only be used along with --html flag."
]
unsafePragmaOptions :: PragmaOptions -> [String]
unsafePragmaOptions :: PragmaOptions -> [String]
unsafePragmaOptions opts :: PragmaOptions
opts =
[ "--allow-unsolved-metas" | PragmaOptions -> Bool
optAllowUnsolved PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--allow-incomplete-matches" | PragmaOptions -> Bool
optAllowIncompleteMatch PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--no-positivity-check" | PragmaOptions -> Bool
optDisablePositivity PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--no-termination-check" | Bool -> Bool
not (PragmaOptions -> Bool
optTerminationCheck PragmaOptions
opts) ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--type-in-type" | Bool -> Bool
not (PragmaOptions -> Bool
optUniverseCheck PragmaOptions
opts) ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--omega-in-omega" | PragmaOptions -> Bool
optOmegaInOmega PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--sized-types and --guardedness" | WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'True
optSizedTypes PragmaOptions
opts)
, WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (PragmaOptions -> WithDefault 'True
optGuardedness PragmaOptions
opts) ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--injective-type-constructors" | PragmaOptions -> Bool
optInjectiveTypeConstructors PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--irrelevant-projections" | PragmaOptions -> Bool
optIrrelevantProjections PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--experimental-irrelevance" | PragmaOptions -> Bool
optExperimentalIrrelevance PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--rewriting" | PragmaOptions -> Bool
optRewriting PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--cubical and --with-K" | PragmaOptions -> Bool
optCubical PragmaOptions
opts
, Bool -> Bool
not (WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool) -> WithDefault 'False -> Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
opts) ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ "--cumulativity" | PragmaOptions -> Bool
optCumulativity PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[]
restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
restartOptions =
[ (CutOff -> RestartCodomain
C (CutOff -> RestartCodomain)
-> (PragmaOptions -> CutOff) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> CutOff
optTerminationDepth, "--termination-depth")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUseUnicode, "--no-unicode")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAllowUnsolved, "--allow-unsolved-metas")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAllowIncompleteMatch, "--allow-incomplete-matches")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optDisablePositivity, "--no-positivity-check")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optTerminationCheck, "--no-termination-check")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniverseCheck, "--type-in-type")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optOmegaInOmega, "--omega-in-omega")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSubtyping, "--subtyping")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCumulativity, "--cumulativity")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'True -> Bool)
-> (PragmaOptions -> WithDefault 'True) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'True
optSizedTypes, "--no-sized-types")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'True -> Bool)
-> (PragmaOptions -> WithDefault 'True) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'True
optGuardedness, "--no-guardedness")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optInjectiveTypeConstructors, "--injective-type-constructors")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optProp, "--prop")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniversePolymorphism, "--no-universe-polymorphism")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optIrrelevantProjections, "--irrelevant-projections")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optExperimentalIrrelevance, "--experimental-irrelevance")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optWithoutK, "--without-K")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optExactSplit, "--exact-split")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optEta, "--no-eta-equality")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optRewriting, "--rewriting")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCubical, "--cubical")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optOverlappingInstances, "--overlapping-instances")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optSafe, "--safe")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optDoubleCheck, "--double-check")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optSyntacticEquality, "--no-syntactic-equality")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCompareSorts, "--no-sort-comparison")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAutoInline, "--no-auto-inline")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optFastReduce, "--no-fast-reduce")
, (Int -> RestartCodomain
I (Int -> RestartCodomain)
-> (PragmaOptions -> Int) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Int
optInstanceSearchDepth, "--instance-search-depth")
, (Int -> RestartCodomain
I (Int -> RestartCodomain)
-> (PragmaOptions -> Int) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Int
optInversionMaxDepth, "--inversion-max-depth")
, (WarningMode -> RestartCodomain
W (WarningMode -> RestartCodomain)
-> (PragmaOptions -> WarningMode)
-> PragmaOptions
-> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WarningMode
optWarningMode, "--warning")
, (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optConfluenceCheck, "--confluence-check")
]
data RestartCodomain = C CutOff | B Bool | I Int | W WarningMode
deriving RestartCodomain -> RestartCodomain -> Bool
(RestartCodomain -> RestartCodomain -> Bool)
-> (RestartCodomain -> RestartCodomain -> Bool)
-> Eq RestartCodomain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RestartCodomain -> RestartCodomain -> Bool
$c/= :: RestartCodomain -> RestartCodomain -> Bool
== :: RestartCodomain -> RestartCodomain -> Bool
$c== :: RestartCodomain -> RestartCodomain -> Bool
Eq
infectiveOptions :: [(PragmaOptions -> Bool, String)]
infectiveOptions :: [(PragmaOptions -> Bool, String)]
infectiveOptions =
[ (PragmaOptions -> Bool
optCubical, "--cubical")
, (PragmaOptions -> Bool
optProp, "--prop")
]
coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
coinfectiveOptions =
[ (PragmaOptions -> Bool
optSafe, "--safe")
, (WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optWithoutK, "--without-K")
, (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniversePolymorphism, "--no-universe-polymorphism")
, (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'True -> Bool)
-> (PragmaOptions -> WithDefault 'True) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'True
optSizedTypes, "--no-sized-types")
, (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'True -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'True -> Bool)
-> (PragmaOptions -> WithDefault 'True) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'True
optGuardedness, "--no-guardedness")
, (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithDefault 'False -> Bool
forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault (WithDefault 'False -> Bool)
-> (PragmaOptions -> WithDefault 'False) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optSubtyping, "--no-subtyping")
, (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCumulativity, "--no-cumulativity")
]
inputFlag :: FilePath -> Flag CommandLineOptions
inputFlag :: String -> Flag CommandLineOptions
inputFlag f :: String
f o :: CommandLineOptions
o =
case CommandLineOptions -> Maybe String
optInputFile CommandLineOptions
o of
Nothing -> Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optInputFile :: Maybe String
optInputFile = String -> Maybe String
forall a. a -> Maybe a
Just String
f }
Just _ -> String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "only one input file allowed"
versionFlag :: Flag CommandLineOptions
versionFlag :: Flag CommandLineOptions
versionFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optShowVersion :: Bool
optShowVersion = Bool
True }
helpFlag :: Maybe String -> Flag CommandLineOptions
helpFlag :: Maybe String -> Flag CommandLineOptions
helpFlag Nothing o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optShowHelp :: Maybe Help
optShowHelp = Help -> Maybe Help
forall a. a -> Maybe a
Just Help
GeneralHelp }
helpFlag (Just str :: String
str) o :: CommandLineOptions
o = case String -> Maybe HelpTopic
string2HelpTopic String
str of
Just hpt :: HelpTopic
hpt -> Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optShowHelp :: Maybe Help
optShowHelp = Help -> Maybe Help
forall a. a -> Maybe a
Just (HelpTopic -> Help
HelpFor HelpTopic
hpt) }
Nothing -> String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO CommandLineOptions)
-> String -> ExceptT String IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$ "unknown help topic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (available: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (((String, HelpTopic) -> String)
-> [(String, HelpTopic)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, HelpTopic) -> String
forall a b. (a, b) -> a
fst [(String, HelpTopic)]
allHelpTopics) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
safeFlag :: Flag PragmaOptions
safeFlag :: Flag PragmaOptions
safeFlag o :: PragmaOptions
o = do
let guardedness :: WithDefault 'True
guardedness = PragmaOptions -> WithDefault 'True
optGuardedness PragmaOptions
o
let sizedTypes :: WithDefault 'True
sizedTypes = PragmaOptions -> WithDefault 'True
optSizedTypes PragmaOptions
o
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSafe :: Bool
optSafe = Bool
True
, optGuardedness :: WithDefault 'True
optGuardedness = Bool -> WithDefault 'True -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False WithDefault 'True
guardedness
, optSizedTypes :: WithDefault 'True
optSizedTypes = Bool -> WithDefault 'True -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
False WithDefault 'True
sizedTypes
}
flatSplitFlag :: Flag PragmaOptions
flatSplitFlag :: Flag PragmaOptions
flatSplitFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optFlatSplit :: Bool
optFlatSplit = Bool
True }
noFlatSplitFlag :: Flag PragmaOptions
noFlatSplitFlag :: Flag PragmaOptions
noFlatSplitFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optFlatSplit :: Bool
optFlatSplit = Bool
False }
doubleCheckFlag :: Flag PragmaOptions
doubleCheckFlag :: Flag PragmaOptions
doubleCheckFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optDoubleCheck :: Bool
optDoubleCheck = Bool
True }
noSyntacticEqualityFlag :: Flag PragmaOptions
noSyntacticEqualityFlag :: Flag PragmaOptions
noSyntacticEqualityFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSyntacticEquality :: Bool
optSyntacticEquality = Bool
False }
noSortComparisonFlag :: Flag PragmaOptions
noSortComparisonFlag :: Flag PragmaOptions
noSortComparisonFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCompareSorts :: Bool
optCompareSorts = Bool
False }
sharingFlag :: Bool -> Flag CommandLineOptions
sharingFlag :: Bool -> Flag CommandLineOptions
sharingFlag _ _ = String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO CommandLineOptions)
-> String -> ExceptT String IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$
"Feature --sharing has been removed (in favor of the Agda abstract machine)."
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag b :: Bool
b o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCaching :: Bool
optCaching = Bool
b }
propFlag :: Flag PragmaOptions
propFlag :: Flag PragmaOptions
propFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProp :: Bool
optProp = Bool
True }
noPropFlag :: Flag PragmaOptions
noPropFlag :: Flag PragmaOptions
noPropFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProp :: Bool
optProp = Bool
False }
experimentalIrrelevanceFlag :: Flag PragmaOptions
experimentalIrrelevanceFlag :: Flag PragmaOptions
experimentalIrrelevanceFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optExperimentalIrrelevance :: Bool
optExperimentalIrrelevance = Bool
True }
irrelevantProjectionsFlag :: Flag PragmaOptions
irrelevantProjectionsFlag :: Flag PragmaOptions
irrelevantProjectionsFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optIrrelevantProjections :: Bool
optIrrelevantProjections = Bool
True }
noIrrelevantProjectionsFlag :: Flag PragmaOptions
noIrrelevantProjectionsFlag :: Flag PragmaOptions
noIrrelevantProjectionsFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optIrrelevantProjections :: Bool
optIrrelevantProjections = Bool
False }
ignoreInterfacesFlag :: Flag CommandLineOptions
ignoreInterfacesFlag :: Flag CommandLineOptions
ignoreInterfacesFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optIgnoreInterfaces :: Bool
optIgnoreInterfaces = Bool
True }
ignoreAllInterfacesFlag :: Flag CommandLineOptions
ignoreAllInterfacesFlag :: Flag CommandLineOptions
ignoreAllInterfacesFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optIgnoreAllInterfaces :: Bool
optIgnoreAllInterfaces = Bool
True }
localInterfacesFlag :: Flag CommandLineOptions
localInterfacesFlag :: Flag CommandLineOptions
localInterfacesFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optLocalInterfaces :: Bool
optLocalInterfaces = Bool
True }
allowUnsolvedFlag :: Flag PragmaOptions
allowUnsolvedFlag :: Flag PragmaOptions
allowUnsolvedFlag o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set WarningName
unsolvedWarnings)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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 o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (Set WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set WarningName
incompleteMatchWarnings)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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 o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optShowImplicit :: Bool
optShowImplicit = Bool
True }
showIrrelevantFlag :: Flag PragmaOptions
showIrrelevantFlag :: Flag PragmaOptions
showIrrelevantFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optShowIrrelevant :: Bool
optShowIrrelevant = Bool
True }
asciiOnlyFlag :: Flag PragmaOptions
asciiOnlyFlag :: Flag PragmaOptions
asciiOnlyFlag o :: PragmaOptions
o = do
IO () -> ExceptT String IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT String IO ()) -> IO () -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$ IORef UnicodeOrAscii -> UnicodeOrAscii -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef UnicodeOrAscii
unicodeOrAscii UnicodeOrAscii
AsciiOnly
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUseUnicode :: Bool
optUseUnicode = Bool
False }
ghciInteractionFlag :: Flag CommandLineOptions
ghciInteractionFlag :: Flag CommandLineOptions
ghciInteractionFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optGHCiInteraction :: Bool
optGHCiInteraction = Bool
True }
jsonInteractionFlag :: Flag CommandLineOptions
jsonInteractionFlag :: Flag CommandLineOptions
jsonInteractionFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optJSONInteraction :: Bool
optJSONInteraction = Bool
True }
vimFlag :: Flag CommandLineOptions
vimFlag :: Flag CommandLineOptions
vimFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optGenerateVimFile :: Bool
optGenerateVimFile = Bool
True }
latexFlag :: Flag CommandLineOptions
latexFlag :: Flag CommandLineOptions
latexFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optGenerateLaTeX :: Bool
optGenerateLaTeX = Bool
True }
onlyScopeCheckingFlag :: Flag CommandLineOptions
onlyScopeCheckingFlag :: Flag CommandLineOptions
onlyScopeCheckingFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optOnlyScopeChecking :: Bool
optOnlyScopeChecking = Bool
True }
countClustersFlag :: Flag PragmaOptions
countClustersFlag :: Flag PragmaOptions
countClustersFlag o :: PragmaOptions
o =
#ifdef COUNT_CLUSTERS
return $ o { optCountClusters = True }
#else
String -> ExceptT String IO PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
"Cluster counting has not been enabled in this build of Agda."
#endif
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optAutoInline :: Bool
optAutoInline = Bool
False }
noPrintPatSynFlag :: Flag PragmaOptions
noPrintPatSynFlag :: Flag PragmaOptions
noPrintPatSynFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPrintPatternSynonyms :: Bool
optPrintPatternSynonyms = Bool
False }
noFastReduceFlag :: Flag PragmaOptions
noFastReduceFlag :: Flag PragmaOptions
noFastReduceFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optFastReduce :: Bool
optFastReduce = Bool
False }
latexDirFlag :: FilePath -> Flag CommandLineOptions
latexDirFlag :: String -> Flag CommandLineOptions
latexDirFlag d :: String
d o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optLaTeXDir :: String
optLaTeXDir = String
d }
noPositivityFlag :: Flag PragmaOptions
noPositivityFlag :: Flag PragmaOptions
noPositivityFlag o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
NotStrictlyPositive_)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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 o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
TerminationIssue_)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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)
}
dontCompletenessCheckFlag :: Flag PragmaOptions
dontCompletenessCheckFlag :: Flag PragmaOptions
dontCompletenessCheckFlag _ =
String -> ExceptT String IO PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "The --no-coverage-check option has been removed."
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniverseCheck :: Bool
optUniverseCheck = Bool
False }
omegaInOmegaFlag :: Flag PragmaOptions
omegaInOmegaFlag :: Flag PragmaOptions
omegaInOmegaFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOmegaInOmega :: Bool
optOmegaInOmega = Bool
True }
subtypingFlag :: Flag PragmaOptions
subtypingFlag :: Flag PragmaOptions
subtypingFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSubtyping :: WithDefault 'False
optSubtyping = Bool -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
noSubtypingFlag :: Flag PragmaOptions
noSubtypingFlag :: Flag PragmaOptions
noSubtypingFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSubtyping :: WithDefault 'False
optSubtyping = Bool -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
cumulativityFlag :: Flag PragmaOptions
cumulativityFlag :: Flag PragmaOptions
cumulativityFlag o :: PragmaOptions
o =
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCumulativity :: Bool
optCumulativity = Bool
True
, optSubtyping :: WithDefault 'False
optSubtyping = Bool -> WithDefault 'False -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True (WithDefault 'False -> WithDefault 'False)
-> WithDefault 'False -> WithDefault 'False
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> WithDefault 'False
optSubtyping PragmaOptions
o
}
noCumulativityFlag :: Flag PragmaOptions
noCumulativityFlag :: Flag PragmaOptions
noCumulativityFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCumulativity :: Bool
optCumulativity = Bool
False }
noEtaFlag :: Flag PragmaOptions
noEtaFlag :: Flag PragmaOptions
noEtaFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optEta :: Bool
optEta = Bool
False }
sizedTypes :: Flag PragmaOptions
sizedTypes :: Flag PragmaOptions
sizedTypes o :: PragmaOptions
o =
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSizedTypes :: WithDefault 'True
optSizedTypes = Bool -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b
Value Bool
True
}
noSizedTypes :: Flag PragmaOptions
noSizedTypes :: Flag PragmaOptions
noSizedTypes o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optSizedTypes :: WithDefault 'True
optSizedTypes = Bool -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
guardedness :: Flag PragmaOptions
guardedness :: Flag PragmaOptions
guardedness o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optGuardedness :: WithDefault 'True
optGuardedness = Bool -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
noGuardedness :: Flag PragmaOptions
noGuardedness :: Flag PragmaOptions
noGuardedness o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optGuardedness :: WithDefault 'True
optGuardedness = Bool -> WithDefault 'True
forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
injectiveTypeConstructorFlag :: Flag PragmaOptions
injectiveTypeConstructorFlag :: Flag PragmaOptions
injectiveTypeConstructorFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optInjectiveTypeConstructors :: Bool
optInjectiveTypeConstructors = Bool
True }
guardingTypeConstructorFlag :: Flag PragmaOptions
guardingTypeConstructorFlag :: Flag PragmaOptions
guardingTypeConstructorFlag _ = String -> ExceptT String IO PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO PragmaOptions)
-> String -> ExceptT String IO PragmaOptions
forall a b. (a -> b) -> a -> b
$
"Experimental feature --guardedness-preserving-type-constructors has been removed."
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
True }
noUniversePolymorphismFlag :: Flag PragmaOptions
noUniversePolymorphismFlag :: Flag PragmaOptions
noUniversePolymorphismFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optUniversePolymorphism :: Bool
optUniversePolymorphism = Bool
False }
noForcingFlag :: Flag PragmaOptions
noForcingFlag :: Flag PragmaOptions
noForcingFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optForcing :: Bool
optForcing = Bool
False }
noProjectionLikeFlag :: Flag PragmaOptions
noProjectionLikeFlag :: Flag PragmaOptions
noProjectionLikeFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optProjectionLike :: Bool
optProjectionLike = Bool
False }
withKFlag :: Flag PragmaOptions
withKFlag :: Flag PragmaOptions
withKFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optWithoutK :: WithDefault 'False
optWithoutK = Bool -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b
Value Bool
False }
withoutKFlag :: Flag PragmaOptions
withoutKFlag :: Flag PragmaOptions
withoutKFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optWithoutK :: WithDefault 'False
optWithoutK = Bool -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b
Value Bool
True }
copatternsFlag :: Flag PragmaOptions
copatternsFlag :: Flag PragmaOptions
copatternsFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCopatterns :: Bool
optCopatterns = Bool
True }
noCopatternsFlag :: Flag PragmaOptions
noCopatternsFlag :: Flag PragmaOptions
noCopatternsFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCopatterns :: Bool
optCopatterns = Bool
False }
noPatternMatchingFlag :: Flag PragmaOptions
noPatternMatchingFlag :: Flag PragmaOptions
noPatternMatchingFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPatternMatching :: Bool
optPatternMatching = Bool
False }
exactSplitFlag :: Flag PragmaOptions
exactSplitFlag :: Flag PragmaOptions
exactSplitFlag o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.insert WarningName
CoverageNoExactSplit_)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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 o :: PragmaOptions
o = do
let upd :: WarningMode -> WarningMode
upd = Lens' (Set WarningName) WarningMode
-> LensMap (Set WarningName) WarningMode
forall i o. Lens' i o -> LensMap i o
over Lens' (Set WarningName) WarningMode
warningSet (WarningName -> Set WarningName -> Set WarningName
forall a. Ord a => a -> Set a -> Set a
Set.delete WarningName
CoverageNoExactSplit_)
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
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 o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optRewriting :: Bool
optRewriting = Bool
True }
cubicalFlag :: Flag PragmaOptions
cubicalFlag :: Flag PragmaOptions
cubicalFlag o :: PragmaOptions
o = do
let withoutK :: WithDefault 'False
withoutK = PragmaOptions -> WithDefault 'False
optWithoutK PragmaOptions
o
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCubical :: Bool
optCubical = Bool
True
, optWithoutK :: WithDefault 'False
optWithoutK = Bool -> WithDefault 'False -> WithDefault 'False
forall (b :: Bool). Bool -> WithDefault b -> WithDefault b
setDefault Bool
True WithDefault 'False
withoutK
}
postfixProjectionsFlag :: Flag PragmaOptions
postfixProjectionsFlag :: Flag PragmaOptions
postfixProjectionsFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optPostfixProjections :: Bool
optPostfixProjections = Bool
True }
keepPatternVariablesFlag :: Flag PragmaOptions
keepPatternVariablesFlag :: Flag PragmaOptions
keepPatternVariablesFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optKeepPatternVariables :: Bool
optKeepPatternVariables = Bool
True }
instanceDepthFlag :: String -> Flag PragmaOptions
instanceDepthFlag :: String -> Flag PragmaOptions
instanceDepthFlag s :: String
s o :: PragmaOptions
o = do
Int
d <- String -> String -> OptM Int
integerArgument "--instance-search-depth" String
s
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optInstanceSearchDepth :: Int
optInstanceSearchDepth = Int
d }
overlappingInstancesFlag :: Flag PragmaOptions
overlappingInstancesFlag :: Flag PragmaOptions
overlappingInstancesFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOverlappingInstances :: Bool
optOverlappingInstances = Bool
True }
noOverlappingInstancesFlag :: Flag PragmaOptions
noOverlappingInstancesFlag :: Flag PragmaOptions
noOverlappingInstancesFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optOverlappingInstances :: Bool
optOverlappingInstances = Bool
False }
inversionMaxDepthFlag :: String -> Flag PragmaOptions
inversionMaxDepthFlag :: String -> Flag PragmaOptions
inversionMaxDepthFlag s :: String
s o :: PragmaOptions
o = do
Int
d <- String -> String -> OptM Int
integerArgument "--inversion-max-depth" String
s
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optInversionMaxDepth :: Int
optInversionMaxDepth = Int
d }
interactiveFlag :: Flag CommandLineOptions
interactiveFlag :: Flag CommandLineOptions
interactiveFlag o :: CommandLineOptions
o = do
PragmaOptions
prag <- Flag PragmaOptions
allowUnsolvedFlag (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
o)
Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optInteractive :: Bool
optInteractive = Bool
True
, optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
prag
}
compileFlagNoMain :: Flag PragmaOptions
compileFlagNoMain :: Flag PragmaOptions
compileFlagNoMain o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optCompileNoMain :: Bool
optCompileNoMain = Bool
True }
compileDirFlag :: FilePath -> Flag CommandLineOptions
compileDirFlag :: String -> Flag CommandLineOptions
compileDirFlag f :: String
f o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optCompileDir :: Maybe String
optCompileDir = String -> Maybe String
forall a. a -> Maybe a
Just String
f }
htmlFlag :: Flag CommandLineOptions
htmlFlag :: Flag CommandLineOptions
htmlFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optGenerateHTML :: Bool
optGenerateHTML = Bool
True }
htmlHighlightFlag :: String -> Flag CommandLineOptions
htmlHighlightFlag :: String -> Flag CommandLineOptions
htmlHighlightFlag "code" o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optHTMLHighlight :: HtmlHighlight
optHTMLHighlight = HtmlHighlight
HighlightCode }
htmlHighlightFlag "all" o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optHTMLHighlight :: HtmlHighlight
optHTMLHighlight = HtmlHighlight
HighlightAll }
htmlHighlightFlag "auto" o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optHTMLHighlight :: HtmlHighlight
optHTMLHighlight = HtmlHighlight
HighlightAuto }
htmlHighlightFlag opt :: String
opt o :: CommandLineOptions
o = String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO CommandLineOptions)
-> String -> ExceptT String IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$ "Invalid option <" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
opt
String -> ShowS
forall a. [a] -> [a] -> [a]
++ ">, expected <all>, <auto> or <code>"
dependencyGraphFlag :: FilePath -> Flag CommandLineOptions
dependencyGraphFlag :: String -> Flag CommandLineOptions
dependencyGraphFlag f :: String
f o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optDependencyGraph :: Maybe String
optDependencyGraph = String -> Maybe String
forall a. a -> Maybe a
Just String
f }
htmlDirFlag :: FilePath -> Flag CommandLineOptions
htmlDirFlag :: String -> Flag CommandLineOptions
htmlDirFlag d :: String
d o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optHTMLDir :: String
optHTMLDir = String
d }
cssFlag :: FilePath -> Flag CommandLineOptions
cssFlag :: String -> Flag CommandLineOptions
cssFlag f :: String
f o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optCSSFile :: Maybe String
optCSSFile = String -> Maybe String
forall a. a -> Maybe a
Just String
f }
includeFlag :: FilePath -> Flag CommandLineOptions
includeFlag :: String -> Flag CommandLineOptions
includeFlag d :: String
d o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optIncludePaths :: [String]
optIncludePaths = String
d String -> [String] -> [String]
forall a. a -> [a] -> [a]
: CommandLineOptions -> [String]
optIncludePaths CommandLineOptions
o }
libraryFlag :: String -> Flag CommandLineOptions
libraryFlag :: String -> Flag CommandLineOptions
libraryFlag s :: String
s o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optLibraries :: [String]
optLibraries = CommandLineOptions -> [String]
optLibraries CommandLineOptions
o [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
s] }
overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
overrideLibrariesFileFlag s :: String
s o :: CommandLineOptions
o = do
ExceptT String IO Bool
-> ExceptT String IO CommandLineOptions
-> ExceptT String IO CommandLineOptions
-> ExceptT String IO CommandLineOptions
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (IO Bool -> ExceptT String IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> ExceptT String IO Bool)
-> IO Bool -> ExceptT String IO Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
s)
(Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optOverrideLibrariesFile :: Maybe String
optOverrideLibrariesFile = String -> Maybe String
forall a. a -> Maybe a
Just String
s
, optUseLibs :: Bool
optUseLibs = Bool
True
})
(String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO CommandLineOptions)
-> String -> ExceptT String IO CommandLineOptions
forall a b. (a -> b) -> a -> b
$ "Libraries file not found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s)
noDefaultLibsFlag :: Flag CommandLineOptions
noDefaultLibsFlag :: Flag CommandLineOptions
noDefaultLibsFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optDefaultLibs :: Bool
optDefaultLibs = Bool
False }
noLibsFlag :: Flag CommandLineOptions
noLibsFlag :: Flag CommandLineOptions
noLibsFlag o :: CommandLineOptions
o = Flag CommandLineOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag CommandLineOptions -> Flag CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions
o { optUseLibs :: Bool
optUseLibs = Bool
False }
verboseFlag :: String -> Flag PragmaOptions
verboseFlag :: String -> Flag PragmaOptions
verboseFlag s :: String
s o :: PragmaOptions
o =
do (k :: [String]
k,n :: Int
n) <- String -> ExceptT String IO ([String], Int)
forall e b.
(MonadError e (ExceptT String IO), Error e, Read b) =>
String -> ExceptT String IO ([String], b)
parseVerbose String
s
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optVerbose :: Verbosity
optVerbose = [String] -> Int -> Verbosity -> Verbosity
forall k v. Ord k => [k] -> v -> Trie k v -> Trie k v
Trie.insert [String]
k Int
n (Verbosity -> Verbosity) -> Verbosity -> Verbosity
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Verbosity
optVerbose PragmaOptions
o }
where
parseVerbose :: String -> ExceptT String IO ([String], b)
parseVerbose s :: String
s = case (Char -> Bool) -> String -> [String]
forall a. (a -> Bool) -> [a] -> [[a]]
wordsBy (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (":." :: String)) String
s of
[] -> ExceptT String IO ([String], b)
forall a. ExceptT String IO a
usage
ss :: [String]
ss -> do
b
n <- String -> ExceptT String IO b
forall e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM ([String] -> String
forall a. [a] -> a
last [String]
ss) ExceptT String IO b
-> (e -> ExceptT String IO b) -> ExceptT String IO b
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \_ -> ExceptT String IO b
forall a. ExceptT String IO a
usage
([String], b) -> ExceptT String IO ([String], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> [String]
forall a. [a] -> [a]
init [String]
ss, b
n)
usage :: ExceptT String IO a
usage = String -> ExceptT String IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "argument to verbose should be on the form x.y.z:N or N"
warningModeFlag :: String -> Flag PragmaOptions
warningModeFlag :: String -> Flag PragmaOptions
warningModeFlag s :: String
s o :: PragmaOptions
o = case String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate String
s of
Just upd :: WarningMode -> WarningMode
upd -> Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optWarningMode :: WarningMode
optWarningMode = WarningMode -> WarningMode
upd (PragmaOptions -> WarningMode
optWarningMode PragmaOptions
o) }
Nothing -> String -> ExceptT String IO PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO PragmaOptions)
-> String -> ExceptT String IO PragmaOptions
forall a b. (a -> b) -> a -> b
$ "unknown warning flag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ". See --help=warning."
terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag s :: String
s o :: PragmaOptions
o =
do Int
k <- String -> OptM Int
forall e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM String
s OptM Int -> (String -> OptM Int) -> OptM Int
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \_ -> OptM Int
forall a. ExceptT String IO a
usage
Bool -> ExceptT String IO () -> ExceptT String IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 1) (ExceptT String IO () -> ExceptT String IO ())
-> ExceptT String IO () -> ExceptT String IO ()
forall a b. (a -> b) -> a -> b
$ ExceptT String IO ()
forall a. ExceptT String IO a
usage
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optTerminationDepth :: CutOff
optTerminationDepth = Int -> CutOff
CutOff (Int -> CutOff) -> Int -> CutOff
forall a b. (a -> b) -> a -> b
$ Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-1 }
where usage :: ExceptT String IO a
usage = String -> ExceptT String IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "argument to termination-depth should be >= 1"
confluenceCheckFlag :: Flag PragmaOptions
confluenceCheckFlag :: Flag PragmaOptions
confluenceCheckFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optConfluenceCheck :: Bool
optConfluenceCheck = Bool
True }
noConfluenceCheckFlag :: Flag PragmaOptions
noConfluenceCheckFlag :: Flag PragmaOptions
noConfluenceCheckFlag o :: PragmaOptions
o = Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return Flag PragmaOptions -> Flag PragmaOptions
forall a b. (a -> b) -> a -> b
$ PragmaOptions
o { optConfluenceCheck :: Bool
optConfluenceCheck = Bool
False }
withCompilerFlag :: FilePath -> Flag CommandLineOptions
withCompilerFlag :: String -> Flag CommandLineOptions
withCompilerFlag fp :: String
fp o :: CommandLineOptions
o = case CommandLineOptions -> Maybe String
optWithCompiler CommandLineOptions
o of
Nothing -> Flag CommandLineOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure CommandLineOptions
o { optWithCompiler :: Maybe String
optWithCompiler = String -> Maybe String
forall a. a -> Maybe a
Just String
fp }
Just{} -> String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "only one compiler path allowed"
integerArgument :: String -> String -> OptM Int
integerArgument :: String -> String -> OptM Int
integerArgument flag :: String
flag s :: String
s =
String -> OptM Int
forall e (m :: * -> *) a.
(Error e, MonadError e m, Read a) =>
String -> m a
readM String
s OptM Int -> (String -> OptM Int) -> OptM Int
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \_ ->
String -> OptM Int
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> OptM Int) -> String -> OptM Int
forall a b. (a -> b) -> a -> b
$ "option '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
flag String -> ShowS
forall a. [a] -> [a] -> [a]
++ "' requires an integer argument"
standardOptions :: [OptDescr (Flag CommandLineOptions)]
standardOptions :: [OptDescr (Flag CommandLineOptions)]
standardOptions =
[ String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['V'] ["version"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
versionFlag) "show version number"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['?'] ["help"] ((Maybe String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (Maybe String -> a) -> String -> ArgDescr a
OptArg Maybe String -> Flag CommandLineOptions
helpFlag "TOPIC")
("show help for TOPIC (available: "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (((String, HelpTopic) -> String)
-> [(String, HelpTopic)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, HelpTopic) -> String
forall a b. (a, b) -> a
fst [(String, HelpTopic)]
allHelpTopics)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")")
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['I'] ["interactive"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
interactiveFlag)
"start in interactive mode"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["interaction"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ghciInteractionFlag)
"for use with the Emacs mode"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["interaction-json"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
jsonInteractionFlag)
"for use with other editors such as Atom"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["compile-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
compileDirFlag "DIR")
("directory for compiler output (default: the project root)")
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["vim"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
vimFlag)
"generate Vim highlighting files"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["latex"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
latexFlag)
"generate LaTeX with highlighted source code"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["latex-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
latexDirFlag "DIR")
("directory in which LaTeX files are placed (default: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
defaultLaTeXDir String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")")
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["html"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
htmlFlag)
"generate HTML files with highlighted source code"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["html-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
htmlDirFlag "DIR")
("directory in which HTML files are placed (default: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
defaultHTMLDir String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")")
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["css"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
cssFlag "URL")
"the CSS file used by the HTML files (can be relative)"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["html-highlight"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
htmlHighlightFlag "[code,all,auto]")
("whether to highlight only the code parts (code) or " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"the file as a whole (all) or " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"decide by source file type (auto)")
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["dependency-graph"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
dependencyGraphFlag "FILE")
"generate a Dot file with a module dependency graph"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["ignore-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ignoreInterfacesFlag)
"ignore interface files (re-type check everything)"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["local-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
localInterfacesFlag)
"put interface files next to the Agda files they correspond to"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['i'] ["include-path"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
includeFlag "DIR")
"look for imports in DIR"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['l'] ["library"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
libraryFlag "LIB")
"use library LIB"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["library-file"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
overrideLibrariesFileFlag "FILE")
"use FILE instead of the standard libraries file"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
noLibsFlag)
"don't use any library files"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-default-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
noDefaultLibsFlag)
"don't use default libraries"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["only-scope-checking"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
onlyScopeCheckingFlag)
"only scope-check the top-level module, do not type-check it"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["with-compiler"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
withCompilerFlag "PATH")
"use the compiler available at PATH"
] [OptDescr (Flag CommandLineOptions)]
-> [OptDescr (Flag CommandLineOptions)]
-> [OptDescr (Flag CommandLineOptions)]
forall a. [a] -> [a] -> [a]
++ (OptDescr (Flag PragmaOptions)
-> OptDescr (Flag CommandLineOptions))
-> [OptDescr (Flag PragmaOptions)]
-> [OptDescr (Flag CommandLineOptions)]
forall a b. (a -> b) -> [a] -> [b]
map ((Flag PragmaOptions -> Flag CommandLineOptions)
-> OptDescr (Flag PragmaOptions)
-> OptDescr (Flag CommandLineOptions)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Flag PragmaOptions -> Flag CommandLineOptions
Lens' PragmaOptions CommandLineOptions
lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
pragmaOptions
lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions :: (PragmaOptions -> f PragmaOptions)
-> CommandLineOptions -> f CommandLineOptions
lensPragmaOptions f :: PragmaOptions -> f PragmaOptions
f st :: CommandLineOptions
st = PragmaOptions -> f PragmaOptions
f (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
st) f PragmaOptions
-> (PragmaOptions -> CommandLineOptions) -> f CommandLineOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ opts :: PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }
deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
deadStandardOptions =
[ String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["sharing"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions))
-> Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Bool -> Flag CommandLineOptions
sharingFlag Bool
True)
"DEPRECATED: does nothing"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-sharing"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions))
-> Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a b. (a -> b) -> a -> b
$ Bool -> Flag CommandLineOptions
sharingFlag Bool
False)
"DEPRECATED: does nothing"
, String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["ignore-all-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ignoreAllInterfacesFlag)
"ignore all interface files (re-type check everything, including builtin files)"
] [OptDescr (Flag CommandLineOptions)]
-> [OptDescr (Flag CommandLineOptions)]
-> [OptDescr (Flag CommandLineOptions)]
forall a. [a] -> [a] -> [a]
++ (OptDescr (Flag PragmaOptions)
-> OptDescr (Flag CommandLineOptions))
-> [OptDescr (Flag PragmaOptions)]
-> [OptDescr (Flag CommandLineOptions)]
forall a b. (a -> b) -> [a] -> [b]
map ((Flag PragmaOptions -> Flag CommandLineOptions)
-> OptDescr (Flag PragmaOptions)
-> OptDescr (Flag CommandLineOptions)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Flag PragmaOptions -> Flag CommandLineOptions
Lens' PragmaOptions CommandLineOptions
lensPragmaOptions) [OptDescr (Flag PragmaOptions)]
deadPragmaOptions
pragmaOptions :: [OptDescr (Flag PragmaOptions)]
pragmaOptions :: [OptDescr (Flag PragmaOptions)]
pragmaOptions =
[ String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["show-implicit"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showImplicitFlag)
"show implicit arguments when printing"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["show-irrelevant"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showIrrelevantFlag)
"show irrelevant arguments when printing"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-unicode"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
asciiOnlyFlag)
"don't use unicode characters when printing terms"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['v'] ["verbose"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
verboseFlag "N")
"set verbosity level to N"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["allow-unsolved-metas"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowUnsolvedFlag)
"succeed and create interface file regardless of unsolved meta variables"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["allow-incomplete-matches"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowIncompleteMatchFlag)
"succeed and create interface file regardless of incomplete pattern matches"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-positivity-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPositivityFlag)
"do not warn about not strictly positive data types"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-termination-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontTerminationCheckFlag)
"do not warn about possibly nonterminating code"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["termination-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
terminationDepthFlag "N")
"allow termination checker to count decrease/increase upto N (default N=1)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["type-in-type"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontUniverseCheckFlag)
"ignore universe levels (this makes Agda inconsistent)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["omega-in-omega"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
omegaInOmegaFlag)
"enable typing rule Setω : Setω (this makes Agda inconsistent)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
subtypingFlag)
"enable subtyping rules in general (e.g. for irrelevance and erasure)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSubtypingFlag)
"disable subtyping rules in general (e.g. for irrelevance and erasure) (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cumulativityFlag)
"enable subtyping of universes (e.g. Set =< Set₁) (implies --subtyping)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCumulativityFlag)
"disable subtyping of universes (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
propFlag)
"enable the use of the Prop universe"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPropFlag)
"disable the use of the Prop universe (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
sizedTypes)
"enable sized types (default, inconsistent with --guardedness, implies --subtyping)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSizedTypes)
"disable sized types"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
flatSplitFlag)
"allow split on (x :{flat} A) arguments (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noFlatSplitFlag)
"disable split on (x :{flat} A) arguments"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardedness)
"enable constructor-based guarded corecursion (default, inconsistent with --sized-types)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noGuardedness)
"disable constructor-based guarded corecursion"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["injective-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
injectiveTypeConstructorFlag)
"enable injective type constructors (makes Agda anti-classical and possibly inconsistent)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noUniversePolymorphismFlag)
"disable universe polymorphism"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
universePolymorphismFlag)
"enable universe polymorphism (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
irrelevantProjectionsFlag)
"enable projection of irrelevant record fields and similar irrelevant definitions (inconsistent)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noIrrelevantProjectionsFlag)
"disable projection of irrelevant record fields and similar irrelevant definitions (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["experimental-irrelevance"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
experimentalIrrelevanceFlag)
"enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["with-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
withKFlag)
"enable the K rule in pattern matching (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["without-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
withoutKFlag)
"disable the K rule in pattern matching"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
copatternsFlag)
"enable definitions by copattern matching (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCopatternsFlag)
"disable definitions by copattern matching"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-pattern-matching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPatternMatchingFlag)
"disable pattern matching completely"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
exactSplitFlag)
"require all clauses in a definition to hold as definitional equalities (unless marked CATCHALL)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noExactSplitFlag)
"do not require all clauses in a definition to hold as definitional equalities (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-eta-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noEtaFlag)
"default records to no-eta-equality"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-forcing"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noForcingFlag)
"disable the forcing analysis for data constructors (optimisation)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-projection-like"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noProjectionLikeFlag)
"disable the analysis whether function signatures liken those of projections (optimisation)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["rewriting"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
rewritingFlag)
"enable declaration and use of REWRITE rules"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
confluenceCheckFlag)
"enable confluence checking of REWRITE rules"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noConfluenceCheckFlag)
"disalbe confluence checking of REWRITE rules (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cubicalFlag)
"enable cubical features (e.g. overloads lambdas for paths), implies --without-K"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["postfix-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
postfixProjectionsFlag)
"make postfix projection notation the default"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["keep-pattern-variables"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
keepPatternVariablesFlag)
"don't replace variables with dot patterns during case splitting"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["instance-search-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
instanceDepthFlag "N")
"set instance search depth to N (default: 500)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
overlappingInstancesFlag)
"consider recursive instance arguments during pruning of instance candidates"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noOverlappingInstancesFlag)
"don't consider recursive instance arguments during pruning of instance candidates (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["inversion-max-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
inversionMaxDepthFlag "N")
"set maximum depth for pattern match inversion to N (default: 50)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["safe"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
safeFlag)
"disable postulates, unsafe OPTION pragmas and primEraseEquality, implies --no-sized-types and --no-guardedness "
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["double-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
doubleCheckFlag)
"enable double-checking of all terms using the internal typechecker"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-syntactic-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSyntacticEqualityFlag)
"disable the syntactic equality shortcut in the conversion checker"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-sort-comparison"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSortComparisonFlag)
"disable the comparison of sorts when checking conversion of types"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option ['W'] ["warning"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
warningModeFlag "FLAG")
("set warning flags. See --help=warning.")
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-main"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
compileFlagNoMain)
"do not treat the requested module as the main module of a program when compiling"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["caching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
-> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
cachingFlag Bool
True)
"enable caching of typechecking (default)"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-caching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions))
-> Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a b. (a -> b) -> a -> b
$ Bool -> Flag PragmaOptions
cachingFlag Bool
False)
"disable caching of typechecking"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["count-clusters"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
countClustersFlag)
("count extended grapheme clusters when " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"generating LaTeX (note that this flag " String -> ShowS
forall a. [a] -> [a] -> [a]
++
#ifdef COUNT_CLUSTERS
"is not enabled in all builds of Agda)"
#else
"has not been enabled in this build of Agda)"
#endif
)
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-auto-inline"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noAutoInlineFlag)
("disable automatic compile-time inlining " String -> ShowS
forall a. [a] -> [a] -> [a]
++
"(only definitions marked INLINE will be inlined)")
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-print-pattern-synonyms"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPrintPatSynFlag)
"expand pattern synonyms when printing terms"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-fast-reduce"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noFastReduceFlag)
"disable reduction using the Agda Abstract Machine"
]
deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
deadPragmaOptions :: [OptDescr (Flag PragmaOptions)]
deadPragmaOptions =
[ String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["guardedness-preserving-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardingTypeConstructorFlag)
"treat type constructors as inductive constructors when checking productivity"
, String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] ["no-coverage-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontCompletenessCheckFlag)
"the option has been removed"
]
standardOptions_ :: [OptDescr ()]
standardOptions_ :: [OptDescr ()]
standardOptions_ = (OptDescr (Flag CommandLineOptions) -> OptDescr ())
-> [OptDescr (Flag CommandLineOptions)] -> [OptDescr ()]
forall a b. (a -> b) -> [a] -> [b]
map ((Flag CommandLineOptions -> ())
-> OptDescr (Flag CommandLineOptions) -> OptDescr ()
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Flag CommandLineOptions -> ())
-> OptDescr (Flag CommandLineOptions) -> OptDescr ())
-> (Flag CommandLineOptions -> ())
-> OptDescr (Flag CommandLineOptions)
-> OptDescr ()
forall a b. (a -> b) -> a -> b
$ () -> Flag CommandLineOptions -> ()
forall a b. a -> b -> a
const ()) [OptDescr (Flag CommandLineOptions)]
standardOptions
getOptSimple
:: [String]
-> [OptDescr (Flag opts)]
-> (String -> Flag opts)
-> Flag opts
getOptSimple :: [String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple argv :: [String]
argv opts :: [OptDescr (Flag opts)]
opts fileArg :: String -> Flag opts
fileArg = \ defaults :: opts
defaults ->
case ArgOrder (Flag opts)
-> [OptDescr (Flag opts)]
-> [String]
-> ([Flag opts], [String], [String], [String])
forall a.
ArgOrder a
-> [OptDescr a] -> [String] -> ([a], [String], [String], [String])
getOpt' ((String -> Flag opts) -> ArgOrder (Flag opts)
forall a. (String -> a) -> ArgOrder a
ReturnInOrder String -> Flag opts
fileArg) [OptDescr (Flag opts)]
opts [String]
argv of
(o :: [Flag opts]
o, _, [] , [] ) -> (ExceptT String IO opts -> Flag opts -> ExceptT String IO opts)
-> ExceptT String IO opts -> [Flag opts] -> ExceptT String IO opts
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ExceptT String IO opts -> Flag opts -> ExceptT String IO opts
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(>>=) (Flag opts
forall (m :: * -> *) a. Monad m => a -> m a
return opts
defaults) [Flag opts]
o
(_, _, unrecognized :: [String]
unrecognized, errs :: [String]
errs) -> String -> ExceptT String IO opts
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO opts)
-> String -> ExceptT String IO opts
forall a b. (a -> b) -> a -> b
$ String
umsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
emsg
where
ucap :: String
ucap = "Unrecognized " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> ShowS
forall a. [a] -> ShowS
plural [String]
unrecognized "option" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":"
ecap :: String
ecap = [String] -> ShowS
forall a. [a] -> ShowS
plural [String]
errs "Option error" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":"
umsg :: String
umsg = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
unrecognized then "" else [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
String
ucap String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
suggest [String]
unrecognized
emsg :: String
emsg = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
errs then "" else [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
String
ecap String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
errs
plural :: [a] -> ShowS
plural [_] x :: String
x = String
x
plural _ x :: String
x = String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ "s"
longopts :: [String]
longopts :: [String]
longopts = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("--" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ (OptDescr (Flag opts) -> [String])
-> [OptDescr (Flag opts)] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Option _ long :: [String]
long _ _) -> [String]
long) [OptDescr (Flag opts)]
opts
dist :: String -> String -> Int
dist :: String -> String -> Int
dist s :: String
s t :: 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 s :: String
s t :: String
t = let d :: Int
d = String -> String -> Int
dist String
s String
t in if Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 3 then (Int, String) -> Maybe (Int, String)
forall a. a -> Maybe a
Just (Int
d, String
t) else Maybe (Int, String)
forall a. Maybe a
Nothing
closeopts :: String -> [(Int, String)]
closeopts :: String -> [(Int, String)]
closeopts s :: String
s = (String -> Maybe (Int, String)) -> [String] -> [(Int, String)]
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 s :: String
s = ([(Int, String)] -> [String]) -> [[(Int, String)]] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> String
forall a b. (a, b) -> b
snd) ([[(Int, String)]] -> [[String]])
-> [[(Int, String)]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ ((Int, String) -> Int) -> [(Int, String)] -> [[(Int, String)]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn (Int, String) -> Int
forall a b. (a, b) -> a
fst ([(Int, String)] -> [[(Int, String)]])
-> [(Int, String)] -> [[(Int, String)]]
forall a b. (a -> b) -> a -> b
$ String -> [(Int, String)]
closeopts String
s
suggest :: String -> String
suggest :: ShowS
suggest s :: String
s = case String -> [[String]]
alts String
s of
[] -> String
s
as :: [String]
as : _ -> String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (did you mean " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
sugs [String]
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ " ?)"
sugs :: [String] -> String
sugs :: [String] -> String
sugs [a :: String
a] = String
a
sugs as :: [String]
as = "any of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " " [String]
as
parsePragmaOptions
:: [String]
-> CommandLineOptions
-> OptM PragmaOptions
parsePragmaOptions :: [String] -> CommandLineOptions -> ExceptT String IO PragmaOptions
parsePragmaOptions argv :: [String]
argv opts :: CommandLineOptions
opts = do
PragmaOptions
ps <- [String]
-> [OptDescr (Flag PragmaOptions)]
-> (String -> Flag PragmaOptions)
-> Flag PragmaOptions
forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple [String]
argv ([OptDescr (Flag PragmaOptions)]
deadPragmaOptions [OptDescr (Flag PragmaOptions)]
-> [OptDescr (Flag PragmaOptions)]
-> [OptDescr (Flag PragmaOptions)]
forall a. [a] -> [a] -> [a]
++ [OptDescr (Flag PragmaOptions)]
pragmaOptions)
(\s :: String
s _ -> String -> ExceptT String IO PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO PragmaOptions)
-> String -> ExceptT String IO PragmaOptions
forall a b. (a -> b) -> a -> b
$ "Bad option in pragma: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s)
(CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts)
CommandLineOptions
_ <- Flag CommandLineOptions
checkOpts (CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
ps })
Flag PragmaOptions
forall (m :: * -> *) a. Monad m => a -> m a
return PragmaOptions
ps
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
parsePluginOptions argv :: [String]
argv opts :: [OptDescr (Flag opts)]
opts =
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
forall opts.
[String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple [String]
argv [OptDescr (Flag opts)]
opts
(\s :: String
s _ -> String -> ExceptT String IO opts
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String IO opts)
-> String -> ExceptT String IO opts
forall a b. (a -> b) -> a -> b
$
"Internal error: Flag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " passed to a plugin")
usage :: [OptDescr ()] -> String -> Help -> String
usage :: [OptDescr ()] -> String -> Help -> String
usage options :: [OptDescr ()]
options progName :: String
progName GeneralHelp = String -> [OptDescr ()] -> String
forall a. String -> [OptDescr a] -> String
usageInfo (ShowS
header String
progName) [OptDescr ()]
options
where
header :: ShowS
header progName :: String
progName = [String] -> String
unlines [ "Agda version " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
version, ""
, "Usage: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
progName String -> ShowS
forall a. [a] -> [a] -> [a]
++ " [OPTIONS...] [FILE]" ]
usage options :: [OptDescr ()]
options progName :: String
progName (HelpFor topic :: HelpTopic
topic) = HelpTopic -> String
helpTopicUsage HelpTopic
topic
stripRTS :: [String] -> [String]
stripRTS :: [String] -> [String]
stripRTS [] = []
stripRTS ("--RTS" : argv :: [String]
argv) = [String]
argv
stripRTS (arg :: String
arg : argv :: [String]
argv)
| String -> String -> Bool
is "+RTS" String
arg = [String] -> [String]
stripRTS ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop 1 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> Bool
is "-RTS") [String]
argv
| Bool
otherwise = String
arg String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
stripRTS [String]
argv
where
is :: String -> String -> Bool
is x :: String
x arg :: String
arg = [String
x] [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take 1 (String -> [String]
words String
arg)
defaultLibDir :: IO FilePath
defaultLibDir :: IO String
defaultLibDir = do
String
libdir <- (AbsolutePath -> String) -> IO AbsolutePath -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbsolutePath -> String
filePath (String -> IO AbsolutePath
absolute (String -> IO AbsolutePath) -> IO String -> IO AbsolutePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> IO String
getDataFileName "lib")
IO Bool -> IO String -> IO String -> IO String
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (String -> IO Bool
doesDirectoryExist String
libdir)
(String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
libdir)
(String -> IO String
forall a. HasCallStack => String -> a
error (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ "The lib directory " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
libdir String -> ShowS
forall a. [a] -> [a] -> [a]
++ " does not exist")