{-# 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
    -- Reused by PandocAgda
    , 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
-- Paths_Agda.hs is in $(BUILD_DIR)/build/autogen/.
import Paths_Agda ( getDataFileName )

-- OptDescr is a Functor --------------------------------------------------

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)

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

data CommandLineOptions = Options
  { CommandLineOptions -> String
optProgramName      :: String
  , CommandLineOptions -> Maybe String
optInputFile        :: Maybe FilePath
  , CommandLineOptions -> [String]
optIncludePaths     :: [FilePath]
  , CommandLineOptions -> [AbsolutePath]
optAbsoluteIncludePaths :: [AbsolutePath]
  , CommandLineOptions -> [String]
optLibraries        :: [LibName]
  , CommandLineOptions -> Maybe String
optOverrideLibrariesFile :: Maybe FilePath
  -- ^ Use this (if Just) instead of .agda/libraries
  , CommandLineOptions -> Bool
optDefaultLibs      :: Bool
  -- ^ Use ~/.agda/defaults
  , CommandLineOptions -> Bool
optUseLibs          :: Bool
  -- ^ look for .agda-lib files
  , CommandLineOptions -> 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
  -- ^ In the absence of a path the project root is used.
  , 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
    -- ^ Should the top-level module only be scope-checked, and not
    --   type-checked?
  , CommandLineOptions -> Maybe String
optWithCompiler     :: Maybe FilePath
    -- ^ Use the compiler at PATH instead of ghc / js / etc.
  }
  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

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

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
    -- ^ Cut off structural order comparison at some depth in termination checker?
  , 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  -- ^ irrelevant levels, irrelevant data matching
  , PragmaOptions -> WithDefault 'False
optWithoutK                  :: WithDefault 'False
  , PragmaOptions -> Bool
optCopatterns                :: Bool  -- ^ Allow definitions by copattern matching?
  , PragmaOptions -> Bool
optPatternMatching           :: Bool  -- ^ Is pattern matching allowed in the current file?
  , PragmaOptions -> Bool
optExactSplit                :: Bool
  , PragmaOptions -> Bool
optEta                       :: Bool
  , PragmaOptions -> Bool
optForcing                   :: Bool  -- ^ Perform the forcing analysis on data constructors?
  , PragmaOptions -> Bool
optProjectionLike            :: Bool  -- ^ Perform the projection-likeness analysis on functions?
  , PragmaOptions -> Bool
optRewriting                 :: Bool  -- ^ Can rewrite rules be added and used?
  , PragmaOptions -> Bool
optCubical                   :: Bool
  , PragmaOptions -> Bool
optPostfixProjections        :: Bool
      -- ^ Should system generated projections 'ProjSystem' be printed
      --   postfix (True) or prefix (False).
  , PragmaOptions -> Bool
optKeepPatternVariables      :: Bool
      -- ^ Should case splitting replace variables with dot patterns
      --   (False) or keep them as variables (True).
  , PragmaOptions -> Int
optInstanceSearchDepth       :: Int
  , PragmaOptions -> Bool
optOverlappingInstances      :: Bool
  , PragmaOptions -> Int
optInversionMaxDepth         :: Int
  , PragmaOptions -> Bool
optSafe                      :: Bool
  , PragmaOptions -> Bool
optDoubleCheck               :: Bool
  , PragmaOptions -> Bool
optSyntacticEquality         :: Bool  -- ^ Should conversion checker use syntactic equality shortcut?
  , PragmaOptions -> Bool
optCompareSorts              :: Bool  -- ^ Should conversion checker compare sorts of types?
  , PragmaOptions -> WarningMode
optWarningMode               :: WarningMode
  , PragmaOptions -> Bool
optCompileNoMain             :: Bool
  , PragmaOptions -> Bool
optCaching                   :: Bool
  , PragmaOptions -> Bool
optCountClusters             :: Bool
    -- ^ Count extended grapheme clusters rather than code points when
    -- generating LaTeX.
  , PragmaOptions -> Bool
optAutoInline                :: Bool
    -- ^ Automatic compile-time inlining for simple definitions (unless marked
    --   NOINLINE).
  , PragmaOptions -> Bool
optPrintPatternSynonyms      :: Bool
  , PragmaOptions -> Bool
optFastReduce                :: Bool
    -- ^ Use the Agda abstract machine (fastReduce)?
  , PragmaOptions -> Bool
optConfluenceCheck           :: Bool
    -- ^ Check confluence of rewrite rules?
  , PragmaOptions -> Bool
optFlatSplit                 :: Bool
     -- ^ Can we split on a (x :{flat} A) argument?
  }
  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)

-- | The options from an @OPTIONS@ pragma.
--
-- In the future it might be nice to switch to a more structured
-- representation. Note that, currently, there is not a one-to-one
-- correspondence between list elements and options.
type OptionsPragma = [String]

-- | Map a function over the long options. Also removes the short options.
--   Will be used to add the plugin name to the plugin options.
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
mapFlag :: ShowS -> OptDescr a -> OptDescr a
mapFlag ShowS
f (Option String
_ [String]
long ArgDescr a
arg 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 [] Int
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      = String
"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 -- off by default in > 2.5.4, see issue #2170
  , 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       = Int
500
  , optOverlappingInstances :: Bool
optOverlappingInstances      = Bool
False
  , optInversionMaxDepth :: Int
optInversionMaxDepth         = Int
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
  }

-- | The default termination depth.

defaultCutOff :: CutOff
defaultCutOff :: CutOff
defaultCutOff = Int -> CutOff
CutOff Int
0 -- minimum value

-- | The default output directory for LaTeX.

defaultLaTeXDir :: String
defaultLaTeXDir :: String
defaultLaTeXDir = String
"latex"

-- | The default output directory for HTML.

defaultHTMLDir :: String
defaultHTMLDir :: String
defaultHTMLDir = String
"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

{- | @f :: Flag opts@  is an action on the option record that results from
     parsing an option.  @f opts@ produces either an error message or an
     updated options record
-}
type Flag opts = opts -> OptM opts

-- | Checks that the given options are consistent.

checkOpts :: Flag CommandLineOptions
checkOpts :: Flag CommandLineOptions
checkOpts 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
<= Int
1) =
      String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"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
> Int
1 | (CommandLineOptions -> Bool
p, [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 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
$
    [ String
"The options --interactive, --interaction, --interaction-json and"
    , String
"--only-scope-checking cannot be combined with each other or"
    , String
"with --html or --dependency-graph. Furthermore"
    , String
"--interactive and --interaction cannot be combined with"
    , String
"--latex, and --only-scope-checking cannot be combined with"
    , String
"--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
$
    [ String
"The options --html-highlight, --css-dir and --html-dir"
    , String
"only be used along with --html flag."
    ]

-- | Check for unsafe pragmas. Gives a list of used unsafe flags.

unsafePragmaOptions :: PragmaOptions -> [String]
unsafePragmaOptions :: PragmaOptions -> [String]
unsafePragmaOptions PragmaOptions
opts =
  [ String
"--allow-unsolved-metas"                     | PragmaOptions -> Bool
optAllowUnsolved PragmaOptions
opts             ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--allow-incomplete-matches"                 | PragmaOptions -> Bool
optAllowIncompleteMatch PragmaOptions
opts      ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--no-positivity-check"                      | PragmaOptions -> Bool
optDisablePositivity PragmaOptions
opts         ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--no-termination-check"                     | Bool -> Bool
not (PragmaOptions -> Bool
optTerminationCheck PragmaOptions
opts)    ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--type-in-type"                             | Bool -> Bool
not (PragmaOptions -> Bool
optUniverseCheck PragmaOptions
opts)       ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--omega-in-omega"                           | PragmaOptions -> Bool
optOmegaInOmega PragmaOptions
opts              ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
-- [ "--sized-types"                              | optSizedTypes opts                ] ++
  [ String
"--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]
++
  [ String
"--injective-type-constructors"              | PragmaOptions -> Bool
optInjectiveTypeConstructors PragmaOptions
opts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--irrelevant-projections"                   | PragmaOptions -> Bool
optIrrelevantProjections PragmaOptions
opts     ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--experimental-irrelevance"                 | PragmaOptions -> Bool
optExperimentalIrrelevance PragmaOptions
opts   ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--rewriting"                                | PragmaOptions -> Bool
optRewriting PragmaOptions
opts                 ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String
"--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]
++
  [ String
"--cumulativity"                             | PragmaOptions -> Bool
optCumulativity PragmaOptions
opts              ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  []

-- | If any these options have changed, then the file will be
--   rechecked. Boolean options are negated to mention non-default
--   options, where possible.

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, String
"--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, String
"--no-unicode")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAllowUnsolved, String
"--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, String
"--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, String
"--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,  String
"--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, String
"--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, String
"--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, String
"--subtyping")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCumulativity, String
"--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, String
"--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, String
"--no-guardedness")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optInjectiveTypeConstructors, String
"--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, String
"--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, String
"--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, String
"--irrelevant-projections")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optExperimentalIrrelevance, String
"--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, String
"--without-K")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optExactSplit, String
"--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, String
"--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, String
"--rewriting")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCubical, String
"--cubical")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optOverlappingInstances, String
"--overlapping-instances")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optSafe, String
"--safe")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optDoubleCheck, String
"--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, String
"--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, String
"--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, String
"--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, String
"--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, String
"--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, String
"--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, String
"--warning")
  , (Bool -> RestartCodomain
B (Bool -> RestartCodomain)
-> (PragmaOptions -> Bool) -> PragmaOptions -> RestartCodomain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optConfluenceCheck, String
"--confluence-check")
  ]

-- to make all restart options have the same type
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

-- | An infective option is an option that if used in one module, must
--   be used in all modules that depend on this module.

infectiveOptions :: [(PragmaOptions -> Bool, String)]
infectiveOptions :: [(PragmaOptions -> Bool, String)]
infectiveOptions =
  [ (PragmaOptions -> Bool
optCubical, String
"--cubical")
  , (PragmaOptions -> Bool
optProp, String
"--prop")
  ]

-- | A coinfective option is an option that if used in one module, must
--   be used in all modules that this module depends on.

coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
coinfectiveOptions =
  [ (PragmaOptions -> Bool
optSafe, String
"--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, String
"--without-K")
  , (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optUniversePolymorphism, String
"--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, String
"--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, String
"--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, String
"--no-subtyping")
  , (Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optCumulativity, String
"--no-cumulativity")
  ]

inputFlag :: FilePath -> Flag CommandLineOptions
inputFlag :: String -> Flag CommandLineOptions
inputFlag String
f CommandLineOptions
o =
    case CommandLineOptions -> Maybe String
optInputFile CommandLineOptions
o of
        Maybe String
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
_   -> String -> ExceptT String IO CommandLineOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"only one input file allowed"

versionFlag :: Flag CommandLineOptions
versionFlag :: Flag CommandLineOptions
versionFlag 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 Maybe String
Nothing    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 String
str) CommandLineOptions
o = case String -> Maybe HelpTopic
string2HelpTopic String
str of
  Just 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) }
  Maybe HelpTopic
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
$ String
"unknown help topic " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (available: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                           String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((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
")"

safeFlag :: Flag PragmaOptions
safeFlag :: Flag PragmaOptions
safeFlag 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 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 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 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 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 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 Bool
_ CommandLineOptions
_ = 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
$
  String
"Feature --sharing has been removed (in favor of the Agda abstract machine)."

cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag Bool
b 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 PragmaOptions
o =
#ifdef COUNT_CLUSTERS
  return $ o { optCountClusters = True }
#else
  String -> OptM PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
    String
"Cluster counting has not been enabled in this build of Agda."
#endif

noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag PragmaOptions
o = 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 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 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 String
d 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 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 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)
             }

-- The option was removed. See Issue 1918.
dontCompletenessCheckFlag :: Flag PragmaOptions
dontCompletenessCheckFlag :: Flag PragmaOptions
dontCompletenessCheckFlag PragmaOptions
_ =
  String -> OptM PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"The --no-coverage-check option has been removed."

dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag 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 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 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 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 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 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 }

--UNUSED Liang-Ting Chen 2019-07-16
--etaFlag :: Flag PragmaOptions
--etaFlag o = return $ o { optEta = True }

noEtaFlag :: Flag PragmaOptions
noEtaFlag :: Flag PragmaOptions
noEtaFlag 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 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
             --, optSubtyping  = setDefault True $ optSubtyping o
             }

noSizedTypes :: Flag PragmaOptions
noSizedTypes :: Flag PragmaOptions
noSizedTypes 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 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 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 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 PragmaOptions
_ = String -> OptM PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
forall a b. (a -> b) -> a -> b
$
  String
"Experimental feature --guardedness-preserving-type-constructors has been removed."

universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag 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  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 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 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 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 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 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 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 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 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 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 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 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 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 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 String
s PragmaOptions
o = do
  Int
d <- String -> String -> OptM Int
integerArgument String
"--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 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 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 String
s PragmaOptions
o = do
  Int
d <- String -> String -> OptM Int
integerArgument String
"--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  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 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 String
f 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 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 String
"code" 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 String
"all"  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 String
"auto" 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 String
opt    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
$ String
"Invalid option <" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
opt
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">, expected <all>, <auto> or <code>"

dependencyGraphFlag :: FilePath -> Flag CommandLineOptions
dependencyGraphFlag :: String -> Flag CommandLineOptions
dependencyGraphFlag String
f 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 String
d 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 String
f 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 String
d 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 String
s 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 String
s 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)
    {-then-} (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
                         })
    {-else-} (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
$ String
"Libraries file not found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s)

noDefaultLibsFlag :: Flag CommandLineOptions
noDefaultLibsFlag :: Flag CommandLineOptions
noDefaultLibsFlag 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 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 String
s PragmaOptions
o =
    do  ([String]
k,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 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)) String
s of
      []  -> ExceptT String IO ([String], b)
forall a. ExceptT String IO a
usage
      [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` \e
_ -> 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 String
"argument to verbose should be on the form x.y.z:N or N"

warningModeFlag :: String -> Flag PragmaOptions
warningModeFlag :: String -> Flag PragmaOptions
warningModeFlag String
s PragmaOptions
o = case String -> Maybe (WarningMode -> WarningMode)
warningModeUpdate String
s of
  Just 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) }
  Maybe (WarningMode -> WarningMode)
Nothing  -> String -> OptM PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
forall a b. (a -> b) -> a -> b
$ String
"unknown warning flag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". See --help=warning."

terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag String
s PragmaOptions
o =
    do Int
k <- 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 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
< Int
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 -- or: turn termination checking off for 0
       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
-Int
1 }
    where usage :: ExceptT String IO a
usage = String -> ExceptT String IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"argument to termination-depth should be >= 1"

confluenceCheckFlag :: Flag PragmaOptions
confluenceCheckFlag :: Flag PragmaOptions
confluenceCheckFlag 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 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 String
fp CommandLineOptions
o = case CommandLineOptions -> Maybe String
optWithCompiler CommandLineOptions
o of
 Maybe String
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 String
"only one compiler path allowed"


integerArgument :: String -> String -> OptM Int
integerArgument :: String -> String -> OptM Int
integerArgument String
flag 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
_ ->
        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
$ String
"option '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
flag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"' 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 [Char
'V']  [String
"version"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
versionFlag)       String
"show version number"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'?']  [String
"help"]    ((Maybe String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (Maybe String -> a) -> String -> ArgDescr a
OptArg Maybe String -> Flag CommandLineOptions
helpFlag String
"TOPIC")
                      (String
"show help for TOPIC (available: "
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((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
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'I']  [String
"interactive"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
interactiveFlag)
                    String
"start in interactive mode"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"interaction"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ghciInteractionFlag)
                    String
"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 []     [String
"interaction-json"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
jsonInteractionFlag)
                    String
"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 []     [String
"compile-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
compileDirFlag String
"DIR")
                    (String
"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 []     [String
"vim"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
vimFlag)
                    String
"generate Vim highlighting files"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"latex"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
latexFlag)
                    String
"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 []     [String
"latex-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
latexDirFlag String
"DIR")
                    (String
"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
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"html"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
htmlFlag)
                    String
"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 []     [String
"html-dir"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
htmlDirFlag String
"DIR")
                    (String
"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
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"css"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
cssFlag String
"URL")
                    String
"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 []     [String
"html-highlight"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
htmlHighlightFlag String
"[code,all,auto]")
                    (String
"whether to highlight only the code parts (code) or " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    String
"the file as a whole (all) or " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    String
"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 []     [String
"dependency-graph"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
dependencyGraphFlag String
"FILE")
                    String
"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 []     [String
"ignore-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ignoreInterfacesFlag)
                    String
"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 []     [String
"local-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
localInterfacesFlag)
                    String
"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 [Char
'i']  [String
"include-path"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
includeFlag String
"DIR")
                    String
"look for imports in DIR"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'l']  [String
"library"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
libraryFlag String
"LIB")
                    String
"use library LIB"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"library-file"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
overrideLibrariesFileFlag String
"FILE")
                    String
"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 []     [String
"no-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
noLibsFlag)
                    String
"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 []     [String
"no-default-libraries"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
noDefaultLibsFlag)
                    String
"don't use default libraries"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"only-scope-checking"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
onlyScopeCheckingFlag)
                    String
"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 []     [String
"with-compiler"] ((String -> Flag CommandLineOptions)
-> String -> ArgDescr (Flag CommandLineOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag CommandLineOptions
withCompilerFlag String
"PATH")
                    String
"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

-- | Defined locally here since module ''Agda.Interaction.Options.Lenses''
--   has cyclic dependency.
lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions :: (PragmaOptions -> f PragmaOptions)
-> CommandLineOptions -> f CommandLineOptions
lensPragmaOptions PragmaOptions -> f PragmaOptions
f 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
<&> \ PragmaOptions
opts -> CommandLineOptions
st { optPragmaOptions :: PragmaOptions
optPragmaOptions = PragmaOptions
opts }

-- | Command line options of previous versions of Agda.
--   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
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 []     [String
"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)
                    String
"DEPRECATED: does nothing"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"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)
                    String
"DEPRECATED: does nothing"
    , String
-> [String]
-> ArgDescr (Flag CommandLineOptions)
-> String
-> OptDescr (Flag CommandLineOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"ignore-all-interfaces"] (Flag CommandLineOptions -> ArgDescr (Flag CommandLineOptions)
forall a. a -> ArgDescr a
NoArg Flag CommandLineOptions
ignoreAllInterfacesFlag) -- not deprecated! Just hidden
                    String
"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 []     [String
"show-implicit"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showImplicitFlag)
                    String
"show implicit arguments when printing"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"show-irrelevant"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
showIrrelevantFlag)
                    String
"show irrelevant arguments when printing"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"no-unicode"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
asciiOnlyFlag)
                    String
"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 [Char
'v']  [String
"verbose"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
verboseFlag String
"N")
                    String
"set verbosity level to N"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"allow-unsolved-metas"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowUnsolvedFlag)
                    String
"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 []     [String
"allow-incomplete-matches"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
allowIncompleteMatchFlag)
                    String
"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 []     [String
"no-positivity-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPositivityFlag)
                    String
"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 []     [String
"no-termination-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontTerminationCheckFlag)
                    String
"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 []     [String
"termination-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
terminationDepthFlag String
"N")
                    String
"allow termination checker to count decrease/increase upto N (default N=1)"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"type-in-type"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontUniverseCheckFlag)
                    String
"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 []     [String
"omega-in-omega"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
omegaInOmegaFlag)
                    String
"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 []     [String
"subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
subtypingFlag)
                    String
"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 []     [String
"no-subtyping"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSubtypingFlag)
                    String
"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 []     [String
"cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cumulativityFlag)
                    String
"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 []     [String
"no-cumulativity"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCumulativityFlag)
                    String
"disable subtyping of universes (default)"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
propFlag)
                    String
"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 []     [String
"no-prop"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPropFlag)
                    String
"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 []     [String
"sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
sizedTypes)
                    String
"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 []     [String
"no-sized-types"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSizedTypes)
                    String
"disable sized types"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
flatSplitFlag)
                    String
"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 []     [String
"no-flat-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noFlatSplitFlag)
                    String
"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 []     [String
"guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardedness)
                    String
"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 []     [String
"no-guardedness"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noGuardedness)
                    String
"disable constructor-based guarded corecursion"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"injective-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
injectiveTypeConstructorFlag)
                    String
"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 []     [String
"no-universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noUniversePolymorphismFlag)
                    String
"disable universe polymorphism"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"universe-polymorphism"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
universePolymorphismFlag)
                    String
"enable universe polymorphism (default)"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
irrelevantProjectionsFlag)
                    String
"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 []     [String
"no-irrelevant-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noIrrelevantProjectionsFlag)
                    String
"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 []     [String
"experimental-irrelevance"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
experimentalIrrelevanceFlag)
                    String
"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 []     [String
"with-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
withKFlag)
                    String
"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 []     [String
"without-K"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
withoutKFlag)
                    String
"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 []     [String
"copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
copatternsFlag)
                    String
"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 []     [String
"no-copatterns"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noCopatternsFlag)
                    String
"disable definitions by copattern matching"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"no-pattern-matching"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPatternMatchingFlag)
                    String
"disable pattern matching completely"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
exactSplitFlag)
                    String
"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 []     [String
"no-exact-split"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noExactSplitFlag)
                    String
"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 []     [String
"no-eta-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noEtaFlag)
                    String
"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 []     [String
"no-forcing"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noForcingFlag)
                    String
"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 []     [String
"no-projection-like"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noProjectionLikeFlag)
                    String
"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 []     [String
"rewriting"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
rewritingFlag)
                    String
"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 []     [String
"confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
confluenceCheckFlag)
                    String
"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 []     [String
"no-confluence-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noConfluenceCheckFlag)
                    String
"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 []     [String
"cubical"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
cubicalFlag)
                    String
"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 []     [String
"postfix-projections"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
postfixProjectionsFlag)
                    String
"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 []     [String
"keep-pattern-variables"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
keepPatternVariablesFlag)
                    String
"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 []     [String
"instance-search-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
instanceDepthFlag String
"N")
                    String
"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 []     [String
"overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
overlappingInstancesFlag)
                    String
"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 []     [String
"no-overlapping-instances"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noOverlappingInstancesFlag)
                    String
"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 []     [String
"inversion-max-depth"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
inversionMaxDepthFlag String
"N")
                    String
"set maximum depth for pattern match inversion to N (default: 50)"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"safe"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
safeFlag)
                    String
"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 []     [String
"double-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
doubleCheckFlag)
                    String
"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 []     [String
"no-syntactic-equality"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSyntacticEqualityFlag)
                    String
"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 []     [String
"no-sort-comparison"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noSortComparisonFlag)
                    String
"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 [Char
'W']  [String
"warning"] ((String -> Flag PragmaOptions)
-> String -> ArgDescr (Flag PragmaOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag PragmaOptions
warningModeFlag String
"FLAG")
                    (String
"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 []     [String
"no-main"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
compileFlagNoMain)
                    String
"do not treat the requested module as the main module of a program when compiling"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"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)
                    String
"enable caching of typechecking (default)"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"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)
                    String
"disable caching of typechecking"
    , String
-> [String]
-> ArgDescr (Flag PragmaOptions)
-> String
-> OptDescr (Flag PragmaOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"count-clusters"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
countClustersFlag)
                    (String
"count extended grapheme clusters when " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                     String
"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
                     String
"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 []     [String
"no-auto-inline"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noAutoInlineFlag)
                    (String
"disable automatic compile-time inlining " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                     String
"(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 []     [String
"no-print-pattern-synonyms"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noPrintPatSynFlag)
                    String
"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 []     [String
"no-fast-reduce"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
noFastReduceFlag)
                    String
"disable reduction using the Agda Abstract Machine"
    ]

-- | Pragma options of previous versions of Agda.
--   Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
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 []     [String
"guardedness-preserving-type-constructors"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
guardingTypeConstructorFlag)
                    String
"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 []     [String
"no-coverage-check"] (Flag PragmaOptions -> ArgDescr (Flag PragmaOptions)
forall a. a -> ArgDescr a
NoArg Flag PragmaOptions
dontCompletenessCheckFlag)
                    String
"the option has been removed"
    ]

-- | Used for printing usage info.
--   Does not include the dead options.
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

-- | Simple interface for System.Console.GetOpt
--   Could be moved to Agda.Utils.Options (does not exist yet)
getOptSimple
  :: [String]               -- ^ command line argument words
  -> [OptDescr (Flag opts)] -- ^ options handlers
  -> (String -> Flag opts)  -- ^ handler of non-options (only one is allowed)
  -> Flag opts              -- ^ combined opts data structure transformer
getOptSimple :: [String]
-> [OptDescr (Flag opts)] -> (String -> Flag opts) -> Flag opts
getOptSimple [String]
argv [OptDescr (Flag opts)]
opts String -> Flag opts
fileArg = \ 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
    ([Flag opts]
o, [String]
_, []          , [] )  -> (OptM opts -> Flag opts -> OptM opts)
-> OptM opts -> [Flag opts] -> OptM opts
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OptM opts -> Flag opts -> OptM 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
    ([Flag opts]
_, [String]
_, [String]
unrecognized, [String]
errs) -> String -> OptM opts
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> OptM opts) -> String -> OptM opts
forall a b. (a -> b) -> a -> b
$ String
umsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
emsg

      where
      ucap :: String
ucap = String
"Unrecognized " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> ShowS
forall a. [a] -> ShowS
plural [String]
unrecognized String
"option" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"
      ecap :: String
ecap = [String] -> ShowS
forall a. [a] -> ShowS
plural [String]
errs String
"Option error" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"
      umsg :: String
umsg = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
unrecognized then String
"" 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 String
"" 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 [a
_] String
x = String
x
      plural [a]
_   String
x = String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"s"

      -- Suggest alternatives that are at most 3 typos away

      longopts :: [String]
      longopts :: [String]
longopts = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"--" 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 String
_ [String]
long ArgDescr (Flag opts)
_ String
_) -> [String]
long) [OptDescr (Flag opts)]
opts

      dist :: String -> String -> Int
      dist :: String -> String -> Int
dist String
s String
t = EditCosts -> String -> String -> Int
restrictedDamerauLevenshteinDistance EditCosts
defaultEditCosts String
s String
t

      close :: String -> String -> Maybe (Int, String)
      close :: String -> String -> Maybe (Int, String)
close String
s String
t = let d :: Int
d = String -> String -> Int
dist String
s String
t in if Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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 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 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 String
s = case String -> [[String]]
alts String
s of
        []     -> String
s
        [String]
as : [[String]]
_ -> String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (did you mean " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
sugs [String]
as String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ?)"

      sugs :: [String] -> String
      sugs :: [String] -> String
sugs [String
a] = String
a
      sugs [String]
as  = String
"any of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " [String]
as

{- No longer used in favour of parseBackendOptions in Agda.Compiler.Backend
-- | Parse the standard options.
parseStandardOptions :: [String] -> OptM CommandLineOptions
parseStandardOptions argv = parseStandardOptions' argv defaultOptions

parseStandardOptions' :: [String] -> Flag CommandLineOptions
parseStandardOptions' argv opts = do
  opts <- getOptSimple (stripRTS argv) (deadStandardOptions ++ standardOptions) inputFlag opts
  checkOpts opts
-}

-- | Parse options from an options pragma.
parsePragmaOptions
  :: [String]
     -- ^ Pragma options.
  -> CommandLineOptions
     -- ^ Command-line options which should be updated.
  -> OptM PragmaOptions
parsePragmaOptions :: [String] -> CommandLineOptions -> OptM PragmaOptions
parsePragmaOptions [String]
argv 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)
          (\String
s PragmaOptions
_ -> String -> OptM PragmaOptions
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> OptM PragmaOptions) -> String -> OptM PragmaOptions
forall a b. (a -> b) -> a -> b
$ String
"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

-- | Parse options for a plugin.
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts
parsePluginOptions [String]
argv [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
    (\String
s opts
_ -> 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
"Internal error: Flag " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" passed to a plugin")

-- | The usage info message. The argument is the program name (probably
--   agda).
usage :: [OptDescr ()] -> String -> Help -> String
usage :: [OptDescr ()] -> String -> Help -> String
usage [OptDescr ()]
options String
progName Help
GeneralHelp = String -> [OptDescr ()] -> String
forall a. String -> [OptDescr a] -> String
usageInfo (ShowS
header String
progName) [OptDescr ()]
options
    where
        header :: ShowS
header String
progName = [String] -> String
unlines [ String
"Agda version " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
version, String
""
                                  , String
"Usage: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
progName String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" [OPTIONS...] [FILE]" ]

usage [OptDescr ()]
options String
progName (HelpFor HelpTopic
topic) = HelpTopic -> String
helpTopicUsage HelpTopic
topic

-- | Removes RTS options from a list of options.

stripRTS :: [String] -> [String]
stripRTS :: [String] -> [String]
stripRTS [] = []
stripRTS (String
"--RTS" : [String]
argv) = [String]
argv
stripRTS (String
arg : [String]
argv)
  | String -> String -> Bool
is String
"+RTS" String
arg = [String] -> [String]
stripRTS ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
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 String
"-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 String
x String
arg = [String
x] [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
1 (String -> [String]
words String
arg)

------------------------------------------------------------------------
-- Some paths

-- | Returns the absolute default lib dir. This directory is used to
-- store the Primitive.agda file.
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 String
"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
$ String
"The lib directory " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
libdir String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not exist")