1{-# LANGUAGE CPP #-} 2{-# LANGUAGE DataKinds #-} 3 4module Agda.Interaction.Options.Base 5 ( CommandLineOptions(..) 6 , PragmaOptions(..) 7 , OptionsPragma 8 , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..) 9 , Verbosity, VerboseKey, VerboseLevel 10 , WarningMode(..) 11 , ConfluenceCheck(..) 12 , UnicodeOrAscii(..) 13 , checkOpts 14 , parsePragmaOptions 15 , parsePluginOptions 16 , stripRTS 17 , defaultOptions 18 , defaultInteractionOptions 19 , defaultVerbosity 20 , defaultCutOff 21 , defaultPragmaOptions 22 , standardOptions_ 23 , unsafePragmaOptions 24 , restartOptions 25 , infectiveOptions 26 , coinfectiveOptions 27 , safeFlag 28 , mapFlag 29 , usage 30 -- Reused by PandocAgda 31 , inputFlag 32 , standardOptions, deadStandardOptions 33 , getOptSimple 34 ) where 35 36import Control.DeepSeq 37import Control.Monad ( when, void ) 38import Control.Monad.Except ( Except, MonadError(throwError), runExcept ) 39 40import qualified System.IO.Unsafe as UNSAFE (unsafePerformIO) 41import Data.Maybe 42import Data.Map ( Map ) 43import qualified Data.Map as Map 44import Data.List ( intercalate ) 45import qualified Data.Set as Set 46 47import GHC.Generics (Generic) 48 49import System.Console.GetOpt ( getOpt', usageInfo, ArgOrder(ReturnInOrder) 50 , OptDescr(..), ArgDescr(..) 51 ) 52import Text.EditDistance 53import Text.Read ( readMaybe ) 54 55import Agda.Termination.CutOff ( CutOff(..), defaultCutOff ) 56 57import Agda.Interaction.Library ( ExeName, LibName ) 58import Agda.Interaction.Options.Help 59 ( Help(HelpFor, GeneralHelp) 60 , string2HelpTopic 61 , allHelpTopics 62 , helpTopicUsage 63 ) 64import Agda.Interaction.Options.Warnings 65import Agda.Syntax.Concrete.Glyph ( unsafeSetUnicodeOrAscii, UnicodeOrAscii(..) ) 66 67import Agda.Utils.FileName ( AbsolutePath ) 68import Agda.Utils.Functor ( (<&>) ) 69import Agda.Utils.Lens ( Lens', over ) 70import Agda.Utils.List ( groupOn, initLast1, wordsBy ) 71import Agda.Utils.Pretty ( singPlural ) 72import Agda.Utils.Trie ( Trie ) 73import qualified Agda.Utils.Trie as Trie 74import Agda.Utils.WithDefault 75 76import Agda.Version 77 78-- OptDescr is a Functor -------------------------------------------------- 79 80type VerboseKey = String 81type VerboseLevel = Int 82type Verbosity = Trie VerboseKey VerboseLevel 83 84-- Don't forget to update 85-- doc/user-manual/tools/command-line-options.rst 86-- if you make changes to the command-line options! 87 88data CommandLineOptions = Options 89 { optProgramName :: String 90 , optInputFile :: Maybe FilePath 91 , optIncludePaths :: [FilePath] 92 , optAbsoluteIncludePaths :: [AbsolutePath] 93 , optLibraries :: [LibName] 94 , optOverrideLibrariesFile :: Maybe FilePath 95 -- ^ Use this (if Just) instead of .agda/libraries 96 , optDefaultLibs :: Bool 97 -- ^ Use ~/.agda/defaults 98 , optUseLibs :: Bool 99 -- ^ look for .agda-lib files 100 , optTrustedExecutables :: Map ExeName FilePath 101 -- ^ Map names of trusted executables to absolute paths 102 , optPrintAgdaDir :: Bool 103 , optPrintVersion :: Bool 104 , optPrintHelp :: Maybe Help 105 , optInteractive :: Bool 106 -- ^ Agda REPL (-I). 107 , optGHCiInteraction :: Bool 108 , optJSONInteraction :: Bool 109 , optOptimSmashing :: Bool 110 , optCompileDir :: Maybe FilePath 111 -- ^ In the absence of a path the project root is used. 112 , optGenerateVimFile :: Bool 113 , optIgnoreInterfaces :: Bool 114 , optIgnoreAllInterfaces :: Bool 115 , optLocalInterfaces :: Bool 116 , optPragmaOptions :: PragmaOptions 117 , optOnlyScopeChecking :: Bool 118 -- ^ Should the top-level module only be scope-checked, and not 119 -- type-checked? 120 } 121 deriving (Show, Generic) 122 123instance NFData CommandLineOptions 124 125-- | Options which can be set in a pragma. 126 127data PragmaOptions = PragmaOptions 128 { optShowImplicit :: Bool 129 , optShowIrrelevant :: Bool 130 , optUseUnicode :: UnicodeOrAscii 131 , optVerbose :: Verbosity 132 , optProp :: Bool 133 , optTwoLevel :: WithDefault 'False 134 , optAllowUnsolved :: Bool 135 , optAllowIncompleteMatch :: Bool 136 , optDisablePositivity :: Bool 137 , optTerminationCheck :: Bool 138 , optTerminationDepth :: CutOff 139 -- ^ Cut off structural order comparison at some depth in termination checker? 140 , optCompletenessCheck :: Bool 141 , optUniverseCheck :: Bool 142 , optOmegaInOmega :: Bool 143 , optSubtyping :: WithDefault 'False 144 , optCumulativity :: Bool 145 , optSizedTypes :: WithDefault 'False 146 , optGuardedness :: WithDefault 'False 147 , optInjectiveTypeConstructors :: Bool 148 , optUniversePolymorphism :: Bool 149 , optIrrelevantProjections :: Bool 150 , optExperimentalIrrelevance :: Bool -- ^ irrelevant levels, irrelevant data matching 151 , optWithoutK :: WithDefault 'False 152 , optCopatterns :: Bool -- ^ Allow definitions by copattern matching? 153 , optPatternMatching :: Bool -- ^ Is pattern matching allowed in the current file? 154 , optExactSplit :: Bool 155 , optEta :: Bool 156 , optForcing :: Bool -- ^ Perform the forcing analysis on data constructors? 157 , optProjectionLike :: Bool -- ^ Perform the projection-likeness analysis on functions? 158 , optRewriting :: Bool -- ^ Can rewrite rules be added and used? 159 , optCubical :: Bool 160 , optGuarded :: Bool 161 , optFirstOrder :: Bool -- ^ Should we speculatively unify function applications as if they were injective? 162 , optPostfixProjections :: Bool 163 -- ^ Should system generated projections 'ProjSystem' be printed 164 -- postfix (True) or prefix (False). 165 , optKeepPatternVariables :: Bool 166 -- ^ Should case splitting replace variables with dot patterns 167 -- (False) or keep them as variables (True). 168 , optInstanceSearchDepth :: Int 169 , optOverlappingInstances :: Bool 170 , optQualifiedInstances :: Bool -- ^ Should instance search consider instances with qualified names? 171 , optInversionMaxDepth :: Int 172 , optSafe :: Bool 173 , optDoubleCheck :: Bool 174 , optSyntacticEquality :: Bool -- ^ Should conversion checker use syntactic equality shortcut? 175 , optWarningMode :: WarningMode 176 , optCompileNoMain :: Bool 177 , optCaching :: Bool 178 , optCountClusters :: Bool 179 -- ^ Count extended grapheme clusters rather than code points when 180 -- generating LaTeX. 181 , optAutoInline :: Bool 182 -- ^ Automatic compile-time inlining for simple definitions (unless marked 183 -- NOINLINE). 184 , optPrintPatternSynonyms :: Bool 185 , optFastReduce :: Bool 186 -- ^ Use the Agda abstract machine (fastReduce)? 187 , optCallByName :: Bool 188 -- ^ Use call-by-name instead of call-by-need 189 , optConfluenceCheck :: Maybe ConfluenceCheck 190 -- ^ Check confluence of rewrite rules? 191 , optFlatSplit :: Bool 192 -- ^ Can we split on a (@flat x : A) argument? 193 , optImportSorts :: Bool 194 -- ^ Should every top-level module start with an implicit statement 195 -- @open import Agda.Primitive using (Set; Prop)@? 196 , optAllowExec :: Bool 197 , optShowIdentitySubstitutions :: Bool 198 -- ^ Show identity substitutions when pretty-printing terms 199 -- (i.e. always show all arguments of a metavariable) 200 } 201 deriving (Show, Eq, Generic) 202 203instance NFData PragmaOptions 204 205data ConfluenceCheck 206 = LocalConfluenceCheck 207 | GlobalConfluenceCheck 208 deriving (Show, Eq, Generic) 209 210instance NFData ConfluenceCheck 211 212-- | The options from an @OPTIONS@ pragma. 213-- 214-- In the future it might be nice to switch to a more structured 215-- representation. Note that, currently, there is not a one-to-one 216-- correspondence between list elements and options. 217type OptionsPragma = [String] 218 219-- | Map a function over the long options. Also removes the short options. 220-- Will be used to add the plugin name to the plugin options. 221mapFlag :: (String -> String) -> OptDescr a -> OptDescr a 222mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr 223 224defaultVerbosity :: Verbosity 225defaultVerbosity = Trie.singleton [] 1 226 227defaultInteractionOptions :: PragmaOptions 228defaultInteractionOptions = defaultPragmaOptions 229 230defaultOptions :: CommandLineOptions 231defaultOptions = Options 232 { optProgramName = "agda" 233 , optInputFile = Nothing 234 , optIncludePaths = [] 235 , optAbsoluteIncludePaths = [] 236 , optLibraries = [] 237 , optOverrideLibrariesFile = Nothing 238 , optDefaultLibs = True 239 , optUseLibs = True 240 , optTrustedExecutables = Map.empty 241 , optPrintAgdaDir = False 242 , optPrintVersion = False 243 , optPrintHelp = Nothing 244 , optInteractive = False 245 , optGHCiInteraction = False 246 , optJSONInteraction = False 247 , optOptimSmashing = True 248 , optCompileDir = Nothing 249 , optGenerateVimFile = False 250 , optIgnoreInterfaces = False 251 , optIgnoreAllInterfaces = False 252 , optLocalInterfaces = False 253 , optPragmaOptions = defaultPragmaOptions 254 , optOnlyScopeChecking = False 255 } 256 257defaultPragmaOptions :: PragmaOptions 258defaultPragmaOptions = PragmaOptions 259 { optShowImplicit = False 260 , optShowIrrelevant = False 261 , optUseUnicode = UnicodeOk 262 , optVerbose = defaultVerbosity 263 , optProp = False 264 , optTwoLevel = Default 265 , optExperimentalIrrelevance = False 266 , optIrrelevantProjections = False -- off by default in > 2.5.4, see issue #2170 267 , optAllowUnsolved = False 268 , optAllowIncompleteMatch = False 269 , optDisablePositivity = False 270 , optTerminationCheck = True 271 , optTerminationDepth = defaultCutOff 272 , optCompletenessCheck = True 273 , optUniverseCheck = True 274 , optOmegaInOmega = False 275 , optSubtyping = Default 276 , optCumulativity = False 277 , optSizedTypes = Default 278 , optGuardedness = Default 279 , optInjectiveTypeConstructors = False 280 , optUniversePolymorphism = True 281 , optWithoutK = Default 282 , optCopatterns = True 283 , optPatternMatching = True 284 , optExactSplit = False 285 , optEta = True 286 , optForcing = True 287 , optProjectionLike = True 288 , optRewriting = False 289 , optCubical = False 290 , optGuarded = False 291 , optFirstOrder = False 292 , optPostfixProjections = False 293 , optKeepPatternVariables = False 294 , optInstanceSearchDepth = 500 295 , optOverlappingInstances = False 296 , optQualifiedInstances = True 297 , optInversionMaxDepth = 50 298 , optSafe = False 299 , optDoubleCheck = False 300 , optSyntacticEquality = True 301 , optWarningMode = defaultWarningMode 302 , optCompileNoMain = False 303 , optCaching = True 304 , optCountClusters = False 305 , optAutoInline = False 306 , optPrintPatternSynonyms = True 307 , optFastReduce = True 308 , optCallByName = False 309 , optConfluenceCheck = Nothing 310 , optFlatSplit = True 311 , optImportSorts = True 312 , optAllowExec = False 313 , optShowIdentitySubstitutions = False 314 } 315 316type OptM = Except String 317 318runOptM :: Monad m => OptM opts -> m (Either String opts) 319runOptM = pure . runExcept 320 321{- | @f :: Flag opts@ is an action on the option record that results from 322 parsing an option. @f opts@ produces either an error message or an 323 updated options record 324-} 325type Flag opts = opts -> OptM opts 326 327-- | Checks that the given options are consistent. 328 329checkOpts :: Flag CommandLineOptions 330checkOpts opts = do 331 -- NOTE: This is a temporary hold-out until --vim can be converted into a backend or plugin, 332 -- whose options compatibility currently is checked in `Agda.Compiler.Backend`. 333 -- 334 -- Additionally, note that some options checking is performed in `Agda.Main` 335 -- in which the top-level frontend and backend interactors are selected. 336 -- 337 -- Those checks are not represented here, because: 338 -- - They are used solely for selecting the initial executon mode; they 339 -- don't need to be checked on a per-module etc basis. 340 -- - I hope/expect that the presence of those specific flags will be eventually 341 -- abstracted out (like the Backends' internal flags), so that they are invisible 342 -- to the rest of the type-checking system. 343 when (optGenerateVimFile opts && optOnlyScopeChecking opts) $ 344 throwError $ "The --only-scope-checking flag cannot be combined with --vim." 345 return opts 346 347-- | Check for unsafe pragmas. Gives a list of used unsafe flags. 348 349unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String] 350unsafePragmaOptions clo opts = 351 [ "--allow-unsolved-metas" | optAllowUnsolved opts ] ++ 352 [ "--allow-incomplete-matches" | optAllowIncompleteMatch opts ] ++ 353 [ "--no-positivity-check" | optDisablePositivity opts ] ++ 354 [ "--no-termination-check" | not (optTerminationCheck opts) ] ++ 355 [ "--type-in-type" | not (optUniverseCheck opts) ] ++ 356 [ "--omega-in-omega" | optOmegaInOmega opts ] ++ 357 [ "--sized-types" | collapseDefault (optSizedTypes opts) ] ++ 358 [ "--injective-type-constructors" | optInjectiveTypeConstructors opts ] ++ 359 [ "--irrelevant-projections" | optIrrelevantProjections opts ] ++ 360 [ "--experimental-irrelevance" | optExperimentalIrrelevance opts ] ++ 361 [ "--rewriting" | optRewriting opts ] ++ 362 [ "--cubical and --with-K" | optCubical opts 363 , not (collapseDefault $ optWithoutK opts) ] ++ 364 [ "--cumulativity" | optCumulativity opts ] ++ 365 [ "--allow-exec" | optAllowExec opts ] ++ 366 [] 367 368-- | If any these options have changed, then the file will be 369-- rechecked. Boolean options are negated to mention non-default 370-- options, where possible. 371 372restartOptions :: [(PragmaOptions -> RestartCodomain, String)] 373restartOptions = 374 [ (C . optTerminationDepth, "--termination-depth") 375 , (B . (/= UnicodeOk) . optUseUnicode, "--no-unicode") 376 , (B . optAllowUnsolved, "--allow-unsolved-metas") 377 , (B . optAllowIncompleteMatch, "--allow-incomplete-matches") 378 , (B . optDisablePositivity, "--no-positivity-check") 379 , (B . optTerminationCheck, "--no-termination-check") 380 , (B . not . optUniverseCheck, "--type-in-type") 381 , (B . optOmegaInOmega, "--omega-in-omega") 382 , (B . collapseDefault . optSubtyping, "--subtyping") 383 , (B . optCumulativity, "--cumulativity") 384 , (B . collapseDefault . optSizedTypes, "--no-sized-types") 385 , (B . collapseDefault . optGuardedness, "--no-guardedness") 386 , (B . optInjectiveTypeConstructors, "--injective-type-constructors") 387 , (B . optProp, "--prop") 388 , (B . collapseDefault . optTwoLevel, "--two-level") 389 , (B . not . optUniversePolymorphism, "--no-universe-polymorphism") 390 , (B . optIrrelevantProjections, "--irrelevant-projections") 391 , (B . optExperimentalIrrelevance, "--experimental-irrelevance") 392 , (B . collapseDefault . optWithoutK, "--without-K") 393 , (B . optExactSplit, "--exact-split") 394 , (B . not . optEta, "--no-eta-equality") 395 , (B . optRewriting, "--rewriting") 396 , (B . optCubical, "--cubical") 397 , (B . optGuarded, "--guarded") 398 , (B . optOverlappingInstances, "--overlapping-instances") 399 , (B . optQualifiedInstances, "--qualified-instances") 400 , (B . not . optQualifiedInstances, "--no-qualified-instances") 401 , (B . optSafe, "--safe") 402 , (B . optDoubleCheck, "--double-check") 403 , (B . not . optSyntacticEquality, "--no-syntactic-equality") 404 , (B . not . optAutoInline, "--no-auto-inline") 405 , (B . not . optFastReduce, "--no-fast-reduce") 406 , (B . optCallByName, "--call-by-name") 407 , (I . optInstanceSearchDepth, "--instance-search-depth") 408 , (I . optInversionMaxDepth, "--inversion-max-depth") 409 , (W . optWarningMode, "--warning") 410 , (B . (== Just LocalConfluenceCheck) . optConfluenceCheck, "--local-confluence-check") 411 , (B . (== Just GlobalConfluenceCheck) . optConfluenceCheck, "--confluence-check") 412 , (B . not . optImportSorts, "--no-import-sorts") 413 , (B . optAllowExec, "--allow-exec") 414 ] 415 416-- to make all restart options have the same type 417data RestartCodomain = C CutOff | B Bool | I Int | W WarningMode 418 deriving Eq 419 420-- | An infective option is an option that if used in one module, must 421-- be used in all modules that depend on this module. 422 423infectiveOptions :: [(PragmaOptions -> Bool, String)] 424infectiveOptions = 425 [ (optCubical, "--cubical") 426 , (optGuarded, "--guarded") 427 , (optProp, "--prop") 428 , (collapseDefault . optTwoLevel, "--two-level") 429 , (optRewriting, "--rewriting") 430 , (collapseDefault . optSizedTypes, "--sized-types") 431 , (collapseDefault . optGuardedness, "--guardedness") 432 ] 433 434-- | A coinfective option is an option that if used in one module, must 435-- be used in all modules that this module depends on. 436 437coinfectiveOptions :: [(PragmaOptions -> Bool, String)] 438coinfectiveOptions = 439 [ (optSafe, "--safe") 440 , (collapseDefault . optWithoutK, "--without-K") 441 , (not . optUniversePolymorphism, "--no-universe-polymorphism") 442 , (not . collapseDefault . optSubtyping, "--no-subtyping") 443 , (not . optCumulativity, "--no-cumulativity") 444 ] 445 446inputFlag :: FilePath -> Flag CommandLineOptions 447inputFlag f o = 448 case optInputFile o of 449 Nothing -> return $ o { optInputFile = Just f } 450 Just _ -> throwError "only one input file allowed" 451 452printAgdaDirFlag :: Flag CommandLineOptions 453printAgdaDirFlag o = return $ o { optPrintAgdaDir = True } 454 455versionFlag :: Flag CommandLineOptions 456versionFlag o = return $ o { optPrintVersion = True } 457 458helpFlag :: Maybe String -> Flag CommandLineOptions 459helpFlag Nothing o = return $ o { optPrintHelp = Just GeneralHelp } 460helpFlag (Just str) o = case string2HelpTopic str of 461 Just hpt -> return $ o { optPrintHelp = Just (HelpFor hpt) } 462 Nothing -> throwError $ "unknown help topic " ++ str ++ " (available: " ++ 463 intercalate ", " (map fst allHelpTopics) ++ ")" 464 465safeFlag :: Flag PragmaOptions 466safeFlag o = do 467 let sizedTypes = optSizedTypes o 468 return $ o { optSafe = True 469 , optSizedTypes = setDefault False sizedTypes 470 } 471 472flatSplitFlag :: Flag PragmaOptions 473flatSplitFlag o = return $ o { optFlatSplit = True } 474 475noFlatSplitFlag :: Flag PragmaOptions 476noFlatSplitFlag o = return $ o { optFlatSplit = False } 477 478doubleCheckFlag :: Bool -> Flag PragmaOptions 479doubleCheckFlag b o = return $ o { optDoubleCheck = b } 480 481noSyntacticEqualityFlag :: Flag PragmaOptions 482noSyntacticEqualityFlag o = return $ o { optSyntacticEquality = False } 483 484noSortComparisonFlag :: Flag PragmaOptions 485noSortComparisonFlag o = return o 486 487sharingFlag :: Bool -> Flag CommandLineOptions 488sharingFlag _ _ = throwError $ 489 "Feature --sharing has been removed (in favor of the Agda abstract machine)." 490 491cachingFlag :: Bool -> Flag PragmaOptions 492cachingFlag b o = return $ o { optCaching = b } 493 494propFlag :: Flag PragmaOptions 495propFlag o = return $ o { optProp = True } 496 497noPropFlag :: Flag PragmaOptions 498noPropFlag o = return $ o { optProp = False } 499 500twoLevelFlag :: Flag PragmaOptions 501twoLevelFlag o = return $ o { optTwoLevel = Value True } 502 503experimentalIrrelevanceFlag :: Flag PragmaOptions 504experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True } 505 506irrelevantProjectionsFlag :: Flag PragmaOptions 507irrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = True } 508 509noIrrelevantProjectionsFlag :: Flag PragmaOptions 510noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False } 511 512ignoreInterfacesFlag :: Flag CommandLineOptions 513ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True } 514 515ignoreAllInterfacesFlag :: Flag CommandLineOptions 516ignoreAllInterfacesFlag o = return $ o { optIgnoreAllInterfaces = True } 517 518localInterfacesFlag :: Flag CommandLineOptions 519localInterfacesFlag o = return $ o { optLocalInterfaces = True } 520 521allowUnsolvedFlag :: Flag PragmaOptions 522allowUnsolvedFlag o = do 523 let upd = over warningSet (Set.\\ unsolvedWarnings) 524 return $ o { optAllowUnsolved = True 525 , optWarningMode = upd (optWarningMode o) 526 } 527 528allowIncompleteMatchFlag :: Flag PragmaOptions 529allowIncompleteMatchFlag o = do 530 let upd = over warningSet (Set.\\ incompleteMatchWarnings) 531 return $ o { optAllowIncompleteMatch = True 532 , optWarningMode = upd (optWarningMode o) 533 } 534 535showImplicitFlag :: Flag PragmaOptions 536showImplicitFlag o = return $ o { optShowImplicit = True } 537 538showIrrelevantFlag :: Flag PragmaOptions 539showIrrelevantFlag o = return $ o { optShowIrrelevant = True } 540 541showIdentitySubstitutionsFlag :: Flag PragmaOptions 542showIdentitySubstitutionsFlag o = return $ o { optShowIdentitySubstitutions = True } 543 544asciiOnlyFlag :: Flag PragmaOptions 545asciiOnlyFlag o = return $ UNSAFE.unsafePerformIO $ do 546 unsafeSetUnicodeOrAscii AsciiOnly 547 return $ o { optUseUnicode = AsciiOnly } 548 549ghciInteractionFlag :: Flag CommandLineOptions 550ghciInteractionFlag o = return $ o { optGHCiInteraction = True } 551 552jsonInteractionFlag :: Flag CommandLineOptions 553jsonInteractionFlag o = return $ o { optJSONInteraction = True } 554 555vimFlag :: Flag CommandLineOptions 556vimFlag o = return $ o { optGenerateVimFile = True } 557 558onlyScopeCheckingFlag :: Flag CommandLineOptions 559onlyScopeCheckingFlag o = return $ o { optOnlyScopeChecking = True } 560 561countClustersFlag :: Flag PragmaOptions 562countClustersFlag o = 563#ifdef COUNT_CLUSTERS 564 return $ o { optCountClusters = True } 565#else 566 throwError 567 "Cluster counting has not been enabled in this build of Agda." 568#endif 569 570noAutoInlineFlag :: Flag PragmaOptions 571noAutoInlineFlag o = return $ o { optAutoInline = False } 572 573autoInlineFlag :: Flag PragmaOptions 574autoInlineFlag o = return $ o { optAutoInline = True } 575 576noPrintPatSynFlag :: Flag PragmaOptions 577noPrintPatSynFlag o = return $ o { optPrintPatternSynonyms = False } 578 579noFastReduceFlag :: Flag PragmaOptions 580noFastReduceFlag o = return $ o { optFastReduce = False } 581 582callByNameFlag :: Flag PragmaOptions 583callByNameFlag o = return $ o { optCallByName = True } 584 585noPositivityFlag :: Flag PragmaOptions 586noPositivityFlag o = do 587 let upd = over warningSet (Set.delete NotStrictlyPositive_) 588 return $ o { optDisablePositivity = True 589 , optWarningMode = upd (optWarningMode o) 590 } 591 592dontTerminationCheckFlag :: Flag PragmaOptions 593dontTerminationCheckFlag o = do 594 let upd = over warningSet (Set.delete TerminationIssue_) 595 return $ o { optTerminationCheck = False 596 , optWarningMode = upd (optWarningMode o) 597 } 598 599-- The option was removed. See Issue 1918. 600dontCompletenessCheckFlag :: Flag PragmaOptions 601dontCompletenessCheckFlag _ = 602 throwError "The --no-coverage-check option has been removed." 603 604dontUniverseCheckFlag :: Flag PragmaOptions 605dontUniverseCheckFlag o = return $ o { optUniverseCheck = False } 606 607omegaInOmegaFlag :: Flag PragmaOptions 608omegaInOmegaFlag o = return $ o { optOmegaInOmega = True } 609 610subtypingFlag :: Flag PragmaOptions 611subtypingFlag o = return $ o { optSubtyping = Value True } 612 613noSubtypingFlag :: Flag PragmaOptions 614noSubtypingFlag o = return $ o { optSubtyping = Value False } 615 616cumulativityFlag :: Flag PragmaOptions 617cumulativityFlag o = 618 return $ o { optCumulativity = True 619 , optSubtyping = setDefault True $ optSubtyping o 620 } 621 622noCumulativityFlag :: Flag PragmaOptions 623noCumulativityFlag o = return $ o { optCumulativity = False } 624 625--UNUSED Liang-Ting Chen 2019-07-16 626--etaFlag :: Flag PragmaOptions 627--etaFlag o = return $ o { optEta = True } 628 629noEtaFlag :: Flag PragmaOptions 630noEtaFlag o = return $ o { optEta = False } 631 632sizedTypes :: Flag PragmaOptions 633sizedTypes o = 634 return $ o { optSizedTypes = Value True 635 --, optSubtyping = setDefault True $ optSubtyping o 636 } 637 638noSizedTypes :: Flag PragmaOptions 639noSizedTypes o = return $ o { optSizedTypes = Value False } 640 641guardedness :: Flag PragmaOptions 642guardedness o = return $ o { optGuardedness = Value True } 643 644noGuardedness :: Flag PragmaOptions 645noGuardedness o = return $ o { optGuardedness = Value False } 646 647injectiveTypeConstructorFlag :: Flag PragmaOptions 648injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True } 649 650guardingTypeConstructorFlag :: Flag PragmaOptions 651guardingTypeConstructorFlag _ = throwError $ 652 "Experimental feature --guardedness-preserving-type-constructors has been removed." 653 654universePolymorphismFlag :: Flag PragmaOptions 655universePolymorphismFlag o = return $ o { optUniversePolymorphism = True } 656 657noUniversePolymorphismFlag :: Flag PragmaOptions 658noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False } 659 660noForcingFlag :: Flag PragmaOptions 661noForcingFlag o = return $ o { optForcing = False } 662 663noProjectionLikeFlag :: Flag PragmaOptions 664noProjectionLikeFlag o = return $ o { optProjectionLike = False } 665 666withKFlag :: Flag PragmaOptions 667withKFlag o = return $ o { optWithoutK = Value False } 668 669withoutKFlag :: Flag PragmaOptions 670withoutKFlag o = return $ o { optWithoutK = Value True } 671 672copatternsFlag :: Flag PragmaOptions 673copatternsFlag o = return $ o { optCopatterns = True } 674 675noCopatternsFlag :: Flag PragmaOptions 676noCopatternsFlag o = return $ o { optCopatterns = False } 677 678noPatternMatchingFlag :: Flag PragmaOptions 679noPatternMatchingFlag o = return $ o { optPatternMatching = False } 680 681exactSplitFlag :: Flag PragmaOptions 682exactSplitFlag o = do 683 let upd = over warningSet (Set.insert CoverageNoExactSplit_) 684 return $ o { optExactSplit = True 685 , optWarningMode = upd (optWarningMode o) 686 } 687 688noExactSplitFlag :: Flag PragmaOptions 689noExactSplitFlag o = do 690 let upd = over warningSet (Set.delete CoverageNoExactSplit_) 691 return $ o { optExactSplit = False 692 , optWarningMode = upd (optWarningMode o) 693 } 694 695rewritingFlag :: Flag PragmaOptions 696rewritingFlag o = return $ o { optRewriting = True } 697 698firstOrderFlag :: Flag PragmaOptions 699firstOrderFlag o = return $ o { optFirstOrder = True } 700 701cubicalFlag :: Flag PragmaOptions 702cubicalFlag o = do 703 let withoutK = optWithoutK o 704 return $ o { optCubical = True 705 , optWithoutK = setDefault True withoutK 706 , optTwoLevel = setDefault True $ optTwoLevel o 707 } 708 709guardedFlag :: Flag PragmaOptions 710guardedFlag o = do 711 return $ o { optGuarded = True } 712 713postfixProjectionsFlag :: Flag PragmaOptions 714postfixProjectionsFlag o = return $ o { optPostfixProjections = True } 715 716keepPatternVariablesFlag :: Flag PragmaOptions 717keepPatternVariablesFlag o = return $ o { optKeepPatternVariables = True } 718 719instanceDepthFlag :: String -> Flag PragmaOptions 720instanceDepthFlag s o = do 721 d <- integerArgument "--instance-search-depth" s 722 return $ o { optInstanceSearchDepth = d } 723 724overlappingInstancesFlag :: Flag PragmaOptions 725overlappingInstancesFlag o = return $ o { optOverlappingInstances = True } 726 727noOverlappingInstancesFlag :: Flag PragmaOptions 728noOverlappingInstancesFlag o = return $ o { optOverlappingInstances = False } 729 730qualifiedInstancesFlag :: Flag PragmaOptions 731qualifiedInstancesFlag o = return $ o { optQualifiedInstances = True } 732 733noQualifiedInstancesFlag :: Flag PragmaOptions 734noQualifiedInstancesFlag o = return $ o { optQualifiedInstances = False } 735 736inversionMaxDepthFlag :: String -> Flag PragmaOptions 737inversionMaxDepthFlag s o = do 738 d <- integerArgument "--inversion-max-depth" s 739 return $ o { optInversionMaxDepth = d } 740 741interactiveFlag :: Flag CommandLineOptions 742interactiveFlag o = return $ o { optInteractive = True } 743 744compileFlagNoMain :: Flag PragmaOptions 745compileFlagNoMain o = return $ o { optCompileNoMain = True } 746 747compileDirFlag :: FilePath -> Flag CommandLineOptions 748compileDirFlag f o = return $ o { optCompileDir = Just f } 749 750includeFlag :: FilePath -> Flag CommandLineOptions 751includeFlag d o = return $ o { optIncludePaths = d : optIncludePaths o } 752 753libraryFlag :: String -> Flag CommandLineOptions 754libraryFlag s o = return $ o { optLibraries = optLibraries o ++ [s] } 755 756overrideLibrariesFileFlag :: String -> Flag CommandLineOptions 757overrideLibrariesFileFlag s o = 758 return $ o 759 { optOverrideLibrariesFile = Just s 760 , optUseLibs = True 761 } 762 763noDefaultLibsFlag :: Flag CommandLineOptions 764noDefaultLibsFlag o = return $ o { optDefaultLibs = False } 765 766noLibsFlag :: Flag CommandLineOptions 767noLibsFlag o = return $ o { optUseLibs = False } 768 769verboseFlag :: String -> Flag PragmaOptions 770verboseFlag s o = 771 do (k,n) <- parseVerbose s 772 return $ o { optVerbose = Trie.insert k n $ optVerbose o } 773 where 774 parseVerbose :: String -> OptM ([VerboseKey], VerboseLevel) 775 parseVerbose s = case wordsBy (`elem` (":." :: String)) s of 776 [] -> usage 777 s0:ss0 -> do 778 let (ss, s) = initLast1 s0 ss0 779 n <- maybe usage return $ readMaybe s 780 return (ss, n) 781 usage = throwError "argument to verbose should be on the form x.y.z:N or N" 782 783warningModeFlag :: String -> Flag PragmaOptions 784warningModeFlag s o = case warningModeUpdate s of 785 Right upd -> return $ o { optWarningMode = upd (optWarningMode o) } 786 Left err -> throwError $ prettyWarningModeError err ++ " See --help=warning." 787 788terminationDepthFlag :: String -> Flag PragmaOptions 789terminationDepthFlag s o = 790 do k <- maybe usage return $ readMaybe s 791 when (k < 1) $ usage -- or: turn termination checking off for 0 792 return $ o { optTerminationDepth = CutOff $ k-1 } 793 where usage = throwError "argument to termination-depth should be >= 1" 794 795confluenceCheckFlag :: ConfluenceCheck -> Flag PragmaOptions 796confluenceCheckFlag f o = return $ o { optConfluenceCheck = Just f } 797 798noConfluenceCheckFlag :: Flag PragmaOptions 799noConfluenceCheckFlag o = return $ o { optConfluenceCheck = Nothing } 800 801noImportSorts :: Flag PragmaOptions 802noImportSorts o = return $ o { optImportSorts = False } 803 804allowExec :: Flag PragmaOptions 805allowExec o = return $ o { optAllowExec = True } 806 807integerArgument :: String -> String -> OptM Int 808integerArgument flag s = maybe usage return $ readMaybe s 809 where 810 usage = throwError $ "option '" ++ flag ++ "' requires an integer argument" 811 812standardOptions :: [OptDescr (Flag CommandLineOptions)] 813standardOptions = 814 [ Option ['V'] ["version"] (NoArg versionFlag) 815 ("print version number and exit") 816 817 , Option ['?'] ["help"] (OptArg helpFlag "TOPIC") $ concat 818 [ "print help and exit; available " 819 , singPlural allHelpTopics "TOPIC" "TOPICs" 820 , ": " 821 , intercalate ", " $ map fst allHelpTopics 822 ] 823 824 , Option [] ["print-agda-dir"] (NoArg printAgdaDirFlag) 825 ("print $AGDA_DIR and exit") 826 827 , Option ['I'] ["interactive"] (NoArg interactiveFlag) 828 "start in interactive mode" 829 , Option [] ["interaction"] (NoArg ghciInteractionFlag) 830 "for use with the Emacs mode" 831 , Option [] ["interaction-json"] (NoArg jsonInteractionFlag) 832 "for use with other editors such as Atom" 833 834 , Option [] ["compile-dir"] (ReqArg compileDirFlag "DIR") 835 ("directory for compiler output (default: the project root)") 836 837 , Option [] ["vim"] (NoArg vimFlag) 838 "generate Vim highlighting files" 839 , Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag) 840 "ignore interface files (re-type check everything)" 841 , Option [] ["local-interfaces"] (NoArg localInterfacesFlag) 842 "put interface files next to the Agda files they correspond to" 843 , Option ['i'] ["include-path"] (ReqArg includeFlag "DIR") 844 "look for imports in DIR" 845 , Option ['l'] ["library"] (ReqArg libraryFlag "LIB") 846 "use library LIB" 847 , Option [] ["library-file"] (ReqArg overrideLibrariesFileFlag "FILE") 848 "use FILE instead of the standard libraries file" 849 , Option [] ["no-libraries"] (NoArg noLibsFlag) 850 "don't use any library files" 851 , Option [] ["no-default-libraries"] (NoArg noDefaultLibsFlag) 852 "don't use default libraries" 853 , Option [] ["only-scope-checking"] (NoArg onlyScopeCheckingFlag) 854 "only scope-check the top-level module, do not type-check it" 855 ] ++ map (fmap lensPragmaOptions) pragmaOptions 856 857-- | Defined locally here since module ''Agda.Interaction.Options.Lenses'' 858-- has cyclic dependency. 859lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions 860lensPragmaOptions f st = f (optPragmaOptions st) <&> \ opts -> st { optPragmaOptions = opts } 861 862-- | Command line options of previous versions of Agda. 863-- Should not be listed in the usage info, put parsed by GetOpt for good error messaging. 864deadStandardOptions :: [OptDescr (Flag CommandLineOptions)] 865deadStandardOptions = 866 [ Option [] ["sharing"] (NoArg $ sharingFlag True) 867 "DEPRECATED: does nothing" 868 , Option [] ["no-sharing"] (NoArg $ sharingFlag False) 869 "DEPRECATED: does nothing" 870 , Option [] ["ignore-all-interfaces"] (NoArg ignoreAllInterfacesFlag) -- not deprecated! Just hidden 871 "ignore all interface files (re-type check everything, including builtin files)" 872 ] ++ map (fmap lensPragmaOptions) deadPragmaOptions 873 874pragmaOptions :: [OptDescr (Flag PragmaOptions)] 875pragmaOptions = 876 [ Option [] ["show-implicit"] (NoArg showImplicitFlag) 877 "show implicit arguments when printing" 878 , Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag) 879 "show irrelevant arguments when printing" 880 , Option [] ["show-identity-substitutions"] (NoArg showIdentitySubstitutionsFlag) 881 "show all arguments of metavariables when printing terms" 882 , Option [] ["no-unicode"] (NoArg asciiOnlyFlag) 883 "don't use unicode characters when printing terms" 884 , Option ['v'] ["verbose"] (ReqArg verboseFlag "N") 885 "set verbosity level to N" 886 , Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag) 887 "succeed and create interface file regardless of unsolved meta variables" 888 , Option [] ["allow-incomplete-matches"] (NoArg allowIncompleteMatchFlag) 889 "succeed and create interface file regardless of incomplete pattern matches" 890 , Option [] ["no-positivity-check"] (NoArg noPositivityFlag) 891 "do not warn about not strictly positive data types" 892 , Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag) 893 "do not warn about possibly nonterminating code" 894 , Option [] ["termination-depth"] (ReqArg terminationDepthFlag "N") 895 "allow termination checker to count decrease/increase upto N (default N=1)" 896 , Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag) 897 "ignore universe levels (this makes Agda inconsistent)" 898 , Option [] ["omega-in-omega"] (NoArg omegaInOmegaFlag) 899 "enable typing rule Setω : Setω (this makes Agda inconsistent)" 900 , Option [] ["subtyping"] (NoArg subtypingFlag) 901 "enable subtyping rules in general (e.g. for irrelevance and erasure)" 902 , Option [] ["no-subtyping"] (NoArg noSubtypingFlag) 903 "disable subtyping rules in general (e.g. for irrelevance and erasure) (default)" 904 , Option [] ["cumulativity"] (NoArg cumulativityFlag) 905 "enable subtyping of universes (e.g. Set =< Set₁) (implies --subtyping)" 906 , Option [] ["no-cumulativity"] (NoArg noCumulativityFlag) 907 "disable subtyping of universes (default)" 908 , Option [] ["prop"] (NoArg propFlag) 909 "enable the use of the Prop universe" 910 , Option [] ["no-prop"] (NoArg noPropFlag) 911 "disable the use of the Prop universe (default)" 912 , Option [] ["two-level"] (NoArg twoLevelFlag) 913 "enable the use of SSet* universes" 914 , Option [] ["sized-types"] (NoArg sizedTypes) 915 "enable sized types (default, inconsistent with --guardedness, implies --subtyping)" 916 , Option [] ["no-sized-types"] (NoArg noSizedTypes) 917 "disable sized types" 918 , Option [] ["flat-split"] (NoArg flatSplitFlag) 919 "allow split on (@flat x : A) arguments (default)" 920 , Option [] ["no-flat-split"] (NoArg noFlatSplitFlag) 921 "disable split on (@flat x : A) arguments" 922 , Option [] ["guardedness"] (NoArg guardedness) 923 "enable constructor-based guarded corecursion (default, inconsistent with --sized-types)" 924 , Option [] ["no-guardedness"] (NoArg noGuardedness) 925 "disable constructor-based guarded corecursion" 926 , Option [] ["injective-type-constructors"] (NoArg injectiveTypeConstructorFlag) 927 "enable injective type constructors (makes Agda anti-classical and possibly inconsistent)" 928 , Option [] ["no-universe-polymorphism"] (NoArg noUniversePolymorphismFlag) 929 "disable universe polymorphism" 930 , Option [] ["universe-polymorphism"] (NoArg universePolymorphismFlag) 931 "enable universe polymorphism (default)" 932 , Option [] ["irrelevant-projections"] (NoArg irrelevantProjectionsFlag) 933 "enable projection of irrelevant record fields and similar irrelevant definitions (inconsistent)" 934 , Option [] ["no-irrelevant-projections"] (NoArg noIrrelevantProjectionsFlag) 935 "disable projection of irrelevant record fields and similar irrelevant definitions (default)" 936 , Option [] ["experimental-irrelevance"] (NoArg experimentalIrrelevanceFlag) 937 "enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching)" 938 , Option [] ["with-K"] (NoArg withKFlag) 939 "enable the K rule in pattern matching (default)" 940 , Option [] ["without-K"] (NoArg withoutKFlag) 941 "disable the K rule in pattern matching" 942 , Option [] ["copatterns"] (NoArg copatternsFlag) 943 "enable definitions by copattern matching (default)" 944 , Option [] ["no-copatterns"] (NoArg noCopatternsFlag) 945 "disable definitions by copattern matching" 946 , Option [] ["no-pattern-matching"] (NoArg noPatternMatchingFlag) 947 "disable pattern matching completely" 948 , Option [] ["exact-split"] (NoArg exactSplitFlag) 949 "require all clauses in a definition to hold as definitional equalities (unless marked CATCHALL)" 950 , Option [] ["no-exact-split"] (NoArg noExactSplitFlag) 951 "do not require all clauses in a definition to hold as definitional equalities (default)" 952 , Option [] ["no-eta-equality"] (NoArg noEtaFlag) 953 "default records to no-eta-equality" 954 , Option [] ["no-forcing"] (NoArg noForcingFlag) 955 "disable the forcing analysis for data constructors (optimisation)" 956 , Option [] ["no-projection-like"] (NoArg noProjectionLikeFlag) 957 "disable the analysis whether function signatures liken those of projections (optimisation)" 958 , Option [] ["rewriting"] (NoArg rewritingFlag) 959 "enable declaration and use of REWRITE rules" 960 , Option [] ["local-confluence-check"] (NoArg $ confluenceCheckFlag LocalConfluenceCheck) 961 "enable checking of local confluence of REWRITE rules" 962 , Option [] ["confluence-check"] (NoArg $ confluenceCheckFlag GlobalConfluenceCheck) 963 "enable global confluence checking of REWRITE rules (more restrictive than --local-confluence-check)" 964 , Option [] ["no-confluence-check"] (NoArg noConfluenceCheckFlag) 965 "disable confluence checking of REWRITE rules (default)" 966 , Option [] ["cubical"] (NoArg cubicalFlag) 967 "enable cubical features (e.g. overloads lambdas for paths), implies --without-K" 968 , Option [] ["guarded"] (NoArg guardedFlag) 969 "enable @lock/@tick attributes" 970 , Option [] ["experimental-lossy-unification"] (NoArg firstOrderFlag) 971 "enable heuristically unifying `f es = f es'` by unifying `es = es'`, even when it could lose solutions." 972 , Option [] ["postfix-projections"] (NoArg postfixProjectionsFlag) 973 "make postfix projection notation the default" 974 , Option [] ["keep-pattern-variables"] (NoArg keepPatternVariablesFlag) 975 "don't replace variables with dot patterns during case splitting" 976 , Option [] ["instance-search-depth"] (ReqArg instanceDepthFlag "N") 977 "set instance search depth to N (default: 500)" 978 , Option [] ["overlapping-instances"] (NoArg overlappingInstancesFlag) 979 "consider recursive instance arguments during pruning of instance candidates" 980 , Option [] ["no-overlapping-instances"] (NoArg noOverlappingInstancesFlag) 981 "don't consider recursive instance arguments during pruning of instance candidates (default)" 982 , Option [] ["qualified-instances"] (NoArg qualifiedInstancesFlag) 983 "use instances with qualified names (default)" 984 , Option [] ["no-qualified-instances"] (NoArg noQualifiedInstancesFlag) 985 "don't use instances with qualified names" 986 , Option [] ["inversion-max-depth"] (ReqArg inversionMaxDepthFlag "N") 987 "set maximum depth for pattern match inversion to N (default: 50)" 988 , Option [] ["safe"] (NoArg safeFlag) 989 "disable postulates, unsafe OPTION pragmas and primEraseEquality, implies --no-sized-types" 990 , Option [] ["double-check"] (NoArg (doubleCheckFlag True)) 991 "enable double-checking of all terms using the internal typechecker" 992 , Option [] ["no-double-check"] (NoArg (doubleCheckFlag False)) 993 "disable double-checking of terms (default)" 994 , Option [] ["no-syntactic-equality"] (NoArg noSyntacticEqualityFlag) 995 "disable the syntactic equality shortcut in the conversion checker" 996 , Option ['W'] ["warning"] (ReqArg warningModeFlag "FLAG") 997 ("set warning flags. See --help=warning.") 998 , Option [] ["no-main"] (NoArg compileFlagNoMain) 999 "do not treat the requested module as the main module of a program when compiling" 1000 , Option [] ["caching"] (NoArg $ cachingFlag True) 1001 "enable caching of typechecking (default)" 1002 , Option [] ["no-caching"] (NoArg $ cachingFlag False) 1003 "disable caching of typechecking" 1004 , Option [] ["count-clusters"] (NoArg countClustersFlag) 1005 ("count extended grapheme clusters when " ++ 1006 "generating LaTeX (note that this flag " ++ 1007#ifdef COUNT_CLUSTERS 1008 "is not enabled in all builds of Agda)" 1009#else 1010 "has not been enabled in this build of Agda)" 1011#endif 1012 ) 1013 , Option [] ["auto-inline"] (NoArg autoInlineFlag) 1014 "enable automatic compile-time inlining" 1015 , Option [] ["no-auto-inline"] (NoArg noAutoInlineFlag) 1016 ("disable automatic compile-time inlining (default), " ++ 1017 "only definitions marked INLINE will be inlined") 1018 , Option [] ["no-print-pattern-synonyms"] (NoArg noPrintPatSynFlag) 1019 "expand pattern synonyms when printing terms" 1020 , Option [] ["no-fast-reduce"] (NoArg noFastReduceFlag) 1021 "disable reduction using the Agda Abstract Machine" 1022 , Option [] ["call-by-name"] (NoArg callByNameFlag) 1023 "use call-by-name evaluation instead of call-by-need" 1024 , Option [] ["no-import-sorts"] (NoArg noImportSorts) 1025 "disable the implicit import of Agda.Primitive using (Set; Prop) at the start of each top-level module" 1026 , Option [] ["allow-exec"] (NoArg allowExec) 1027 "allow system calls to trusted executables with primExec" 1028 ] 1029 1030-- | Pragma options of previous versions of Agda. 1031-- Should not be listed in the usage info, put parsed by GetOpt for good error messaging. 1032deadPragmaOptions :: [OptDescr (Flag PragmaOptions)] 1033deadPragmaOptions = 1034 [ Option [] ["guardedness-preserving-type-constructors"] (NoArg guardingTypeConstructorFlag) 1035 "treat type constructors as inductive constructors when checking productivity" 1036 , Option [] ["no-coverage-check"] (NoArg dontCompletenessCheckFlag) 1037 "the option has been removed" 1038 , Option [] ["no-sort-comparison"] (NoArg noSortComparisonFlag) 1039 "disable the comparison of sorts when checking conversion of types" 1040 ] 1041 1042-- | Used for printing usage info. 1043-- Does not include the dead options. 1044standardOptions_ :: [OptDescr ()] 1045standardOptions_ = map void standardOptions 1046 1047-- | Simple interface for System.Console.GetOpt 1048-- Could be moved to Agda.Utils.Options (does not exist yet) 1049getOptSimple 1050 :: [String] -- ^ command line argument words 1051 -> [OptDescr (Flag opts)] -- ^ options handlers 1052 -> (String -> Flag opts) -- ^ handler of non-options (only one is allowed) 1053 -> Flag opts -- ^ combined opts data structure transformer 1054getOptSimple argv opts fileArg = \ defaults -> 1055 case getOpt' (ReturnInOrder fileArg) opts argv of 1056 (o, _, [] , [] ) -> foldl (>>=) (return defaults) o 1057 (_, _, unrecognized, errs) -> throwError $ umsg ++ emsg 1058 1059 where 1060 ucap = "Unrecognized " ++ plural unrecognized "option" ++ ":" 1061 ecap = plural errs "Option error" ++ ":" 1062 umsg = if null unrecognized then "" else unlines $ 1063 ucap : map suggest unrecognized 1064 emsg = if null errs then "" else unlines $ 1065 ecap : errs 1066 plural [_] x = x 1067 plural _ x = x ++ "s" 1068 1069 -- Suggest alternatives that are at most 3 typos away 1070 1071 longopts :: [String] 1072 longopts = map ("--" ++) $ concatMap (\ (Option _ long _ _) -> long) opts 1073 1074 dist :: String -> String -> Int 1075 dist s t = restrictedDamerauLevenshteinDistance defaultEditCosts s t 1076 1077 close :: String -> String -> Maybe (Int, String) 1078 close s t = let d = dist s t in if d <= 3 then Just (d, t) else Nothing 1079 1080 closeopts :: String -> [(Int, String)] 1081 closeopts s = mapMaybe (close s) longopts 1082 1083 alts :: String -> [[String]] 1084 alts s = map (map snd) $ groupOn fst $ closeopts s 1085 1086 suggest :: String -> String 1087 suggest s = case alts s of 1088 [] -> s 1089 as : _ -> s ++ " (did you mean " ++ sugs as ++ " ?)" 1090 1091 sugs :: [String] -> String 1092 sugs [a] = a 1093 sugs as = "any of " ++ unwords as 1094 1095{- No longer used in favour of parseBackendOptions in Agda.Compiler.Backend 1096-- | Parse the standard options. 1097parseStandardOptions :: [String] -> OptM CommandLineOptions 1098parseStandardOptions argv = parseStandardOptions' argv defaultOptions 1099 1100parseStandardOptions' :: [String] -> Flag CommandLineOptions 1101parseStandardOptions' argv opts = do 1102 opts <- getOptSimple (stripRTS argv) (deadStandardOptions ++ standardOptions) inputFlag opts 1103 checkOpts opts 1104-} 1105 1106-- | Parse options from an options pragma. 1107parsePragmaOptions 1108 :: [String] 1109 -- ^ Pragma options. 1110 -> CommandLineOptions 1111 -- ^ Command-line options which should be updated. 1112 -> OptM PragmaOptions 1113parsePragmaOptions argv opts = do 1114 ps <- getOptSimple argv (deadPragmaOptions ++ pragmaOptions) 1115 (\s _ -> throwError $ "Bad option in pragma: " ++ s) 1116 (optPragmaOptions opts) 1117 _ <- checkOpts (opts { optPragmaOptions = ps }) 1118 return ps 1119 1120-- | Parse options for a plugin. 1121parsePluginOptions :: [String] -> [OptDescr (Flag opts)] -> Flag opts 1122parsePluginOptions argv opts = 1123 getOptSimple argv opts 1124 (\s _ -> throwError $ 1125 "Internal error: Flag " ++ s ++ " passed to a plugin") 1126 1127-- | The usage info message. The argument is the program name (probably 1128-- agda). 1129usage :: [OptDescr ()] -> String -> Help -> String 1130usage options progName GeneralHelp = usageInfo (header progName) options 1131 where 1132 header progName = unlines [ "Agda version " ++ version, "" 1133 , "Usage: " ++ progName ++ " [OPTIONS...] [FILE]" ] 1134 1135usage options progName (HelpFor topic) = helpTopicUsage topic 1136 1137-- | Removes RTS options from a list of options. 1138 1139stripRTS :: [String] -> [String] 1140stripRTS [] = [] 1141stripRTS ("--RTS" : argv) = argv 1142stripRTS (arg : argv) 1143 | is "+RTS" arg = stripRTS $ drop 1 $ dropWhile (not . is "-RTS") argv 1144 | otherwise = arg : stripRTS argv 1145 where 1146 is x arg = [x] == take 1 (words arg) 1147