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