forked from agda/agda
/
Options.hs
1215 lines (1044 loc) · 51.1 KB
/
Options.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
module Agda.Interaction.Options
( CommandLineOptions(..)
, PragmaOptions(..)
, OptionsPragma
, Flag, OptM, runOptM, OptDescr(..), ArgDescr(..)
, Verbosity, VerboseKey, VerboseLevel
, HtmlHighlight(..)
, WarningMode(..)
, checkOpts
, parsePragmaOptions
, parsePluginOptions
, stripRTS
, defaultOptions
, defaultInteractionOptions
, defaultVerbosity
, defaultCutOff
, defaultPragmaOptions
, standardOptions_
, unsafePragmaOptions
, restartOptions
, infectiveOptions
, coinfectiveOptions
, safeFlag
, mapFlag
, usage
, defaultLibDir
-- Reused by PandocAgda
, inputFlag
, standardOptions, deadStandardOptions
, getOptSimple
) where
import Control.Monad ( when, void )
import Control.Monad.Except
import Control.Monad.Trans
import Data.IORef
import Data.Function
import Data.Maybe
import Data.List ( intercalate )
import qualified Data.Set as Set
import System.Console.GetOpt ( getOpt', usageInfo, ArgOrder(ReturnInOrder)
, OptDescr(..), ArgDescr(..)
)
import System.Directory ( doesFileExist, doesDirectoryExist )
import Text.EditDistance
import Text.Read ( readMaybe )
import Agda.Termination.CutOff ( CutOff(..) )
import Agda.Interaction.Library
import Agda.Interaction.Options.Help
import Agda.Interaction.Options.IORefs
import Agda.Interaction.Options.Warnings
import Agda.Utils.FileName ( absolute, AbsolutePath, filePath )
import Agda.Utils.Functor ( (<&>) )
import Agda.Utils.Lens ( Lens', over )
import Agda.Utils.List ( groupOn, wordsBy )
import Agda.Utils.Monad ( ifM )
import Agda.Utils.Trie ( Trie )
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.WithDefault
import Agda.Version
-- Paths_Agda.hs is in $(BUILD_DIR)/build/autogen/.
import Paths_Agda ( getDataFileName )
-- OptDescr is a Functor --------------------------------------------------
type VerboseKey = String
type VerboseLevel = Int
type Verbosity = Trie VerboseKey VerboseLevel
data HtmlHighlight = HighlightAll | HighlightCode | HighlightAuto
deriving (Show, Eq)
-- Don't forget to update
-- doc/user-manual/tools/command-line-options.rst
-- if you make changes to the command-line options!
data CommandLineOptions = Options
{ optProgramName :: String
, optInputFile :: Maybe FilePath
, optIncludePaths :: [FilePath]
, optAbsoluteIncludePaths :: [AbsolutePath]
, optLibraries :: [LibName]
, optOverrideLibrariesFile :: Maybe FilePath
-- ^ Use this (if Just) instead of .agda/libraries
, optDefaultLibs :: Bool
-- ^ Use ~/.agda/defaults
, optUseLibs :: Bool
-- ^ look for .agda-lib files
, optShowVersion :: Bool
, optShowHelp :: Maybe Help
, optInteractive :: Bool
-- ^ Agda REPL (-I).
, optGHCiInteraction :: Bool
, optJSONInteraction :: Bool
, optOptimSmashing :: Bool
, optCompileDir :: Maybe FilePath
-- ^ In the absence of a path the project root is used.
, optGenerateVimFile :: Bool
, optGenerateLaTeX :: Bool
, optGenerateHTML :: Bool
, optHTMLHighlight :: HtmlHighlight
, optDependencyGraph :: Maybe FilePath
, optLaTeXDir :: FilePath
, optHTMLDir :: FilePath
, optCSSFile :: Maybe FilePath
, optHighlightOccurrences :: Bool
, optIgnoreInterfaces :: Bool
, optIgnoreAllInterfaces :: Bool
, optLocalInterfaces :: Bool
, optPragmaOptions :: PragmaOptions
, optOnlyScopeChecking :: Bool
-- ^ Should the top-level module only be scope-checked, and not
-- type-checked?
, optWithCompiler :: Maybe FilePath
-- ^ Use the compiler at PATH instead of ghc / js / etc.
}
deriving Show
-- | Options which can be set in a pragma.
data PragmaOptions = PragmaOptions
{ optShowImplicit :: Bool
, optShowIrrelevant :: Bool
, optUseUnicode :: Bool
, optVerbose :: Verbosity
, optProp :: Bool
, optAllowUnsolved :: Bool
, optAllowIncompleteMatch :: Bool
, optDisablePositivity :: Bool
, optTerminationCheck :: Bool
, optTerminationDepth :: CutOff
-- ^ Cut off structural order comparison at some depth in termination checker?
, optCompletenessCheck :: Bool
, optUniverseCheck :: Bool
, optOmegaInOmega :: Bool
, optSubtyping :: WithDefault 'False
, optCumulativity :: Bool
, optSizedTypes :: WithDefault 'True
, optGuardedness :: WithDefault 'True
, optInjectiveTypeConstructors :: Bool
, optUniversePolymorphism :: Bool
, optIrrelevantProjections :: Bool
, optExperimentalIrrelevance :: Bool -- ^ irrelevant levels, irrelevant data matching
, optWithoutK :: WithDefault 'False
, optCopatterns :: Bool -- ^ Allow definitions by copattern matching?
, optPatternMatching :: Bool -- ^ Is pattern matching allowed in the current file?
, optExactSplit :: Bool
, optEta :: Bool
, optForcing :: Bool -- ^ Perform the forcing analysis on data constructors?
, optProjectionLike :: Bool -- ^ Perform the projection-likeness analysis on functions?
, optRewriting :: Bool -- ^ Can rewrite rules be added and used?
, optCubical :: Bool
, optPostfixProjections :: Bool
-- ^ Should system generated projections 'ProjSystem' be printed
-- postfix (True) or prefix (False).
, optKeepPatternVariables :: Bool
-- ^ Should case splitting replace variables with dot patterns
-- (False) or keep them as variables (True).
, optTopLevelInteractionNoPrivate :: Bool
-- ^ If @True@, disable reloading mechanism introduced in issue #4647
-- that brings private declarations in main module into scope
-- to remedy not-in-scope errors in top-level interaction commands.
, optInstanceSearchDepth :: Int
, optOverlappingInstances :: Bool
, optQualifiedInstances :: Bool -- ^ Should instance search consider instances with qualified names?
, optInversionMaxDepth :: Int
, optSafe :: Bool
, optDoubleCheck :: Bool
, optSyntacticEquality :: Bool -- ^ Should conversion checker use syntactic equality shortcut?
, optCompareSorts :: Bool -- ^ Should conversion checker compare sorts of types?
, optWarningMode :: WarningMode
, optCompileNoMain :: Bool
, optCaching :: Bool
, optCountClusters :: Bool
-- ^ Count extended grapheme clusters rather than code points when
-- generating LaTeX.
, optAutoInline :: Bool
-- ^ Automatic compile-time inlining for simple definitions (unless marked
-- NOINLINE).
, optPrintPatternSynonyms :: Bool
, optFastReduce :: Bool
-- ^ Use the Agda abstract machine (fastReduce)?
, optCallByName :: Bool
-- ^ Use call-by-name instead of call-by-need
, optConfluenceCheck :: Bool
-- ^ Check confluence of rewrite rules?
, optFlatSplit :: Bool
-- ^ Can we split on a (x :{flat} A) argument?
}
deriving (Show, Eq)
-- | The options from an @OPTIONS@ pragma.
--
-- In the future it might be nice to switch to a more structured
-- representation. Note that, currently, there is not a one-to-one
-- correspondence between list elements and options.
type OptionsPragma = [String]
-- | Map a function over the long options. Also removes the short options.
-- Will be used to add the plugin name to the plugin options.
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr
defaultVerbosity :: Verbosity
defaultVerbosity = Trie.singleton [] 1
defaultInteractionOptions :: PragmaOptions
defaultInteractionOptions = defaultPragmaOptions
defaultOptions :: CommandLineOptions
defaultOptions = Options
{ optProgramName = "agda"
, optInputFile = Nothing
, optIncludePaths = []
, optAbsoluteIncludePaths = []
, optLibraries = []
, optOverrideLibrariesFile = Nothing
, optDefaultLibs = True
, optUseLibs = True
, optShowVersion = False
, optShowHelp = Nothing
, optInteractive = False
, optGHCiInteraction = False
, optJSONInteraction = False
, optOptimSmashing = True
, optCompileDir = Nothing
, optGenerateVimFile = False
, optGenerateLaTeX = False
, optGenerateHTML = False
, optHTMLHighlight = HighlightAll
, optDependencyGraph = Nothing
, optLaTeXDir = defaultLaTeXDir
, optHTMLDir = defaultHTMLDir
, optCSSFile = Nothing
-- Don't enable by default because it causes potential
-- performance problems
, optHighlightOccurrences = False
, optIgnoreInterfaces = False
, optIgnoreAllInterfaces = False
, optLocalInterfaces = False
, optPragmaOptions = defaultPragmaOptions
, optOnlyScopeChecking = False
, optWithCompiler = Nothing
}
defaultPragmaOptions :: PragmaOptions
defaultPragmaOptions = PragmaOptions
{ optShowImplicit = False
, optShowIrrelevant = False
, optUseUnicode = True
, optVerbose = defaultVerbosity
, optProp = False
, optExperimentalIrrelevance = False
, optIrrelevantProjections = False -- off by default in > 2.5.4, see issue #2170
, optAllowUnsolved = False
, optAllowIncompleteMatch = False
, optDisablePositivity = False
, optTerminationCheck = True
, optTerminationDepth = defaultCutOff
, optCompletenessCheck = True
, optUniverseCheck = True
, optOmegaInOmega = False
, optSubtyping = Default
, optCumulativity = False
, optSizedTypes = Default
, optGuardedness = Default
, optInjectiveTypeConstructors = False
, optUniversePolymorphism = True
, optWithoutK = Default
, optCopatterns = True
, optPatternMatching = True
, optExactSplit = False
, optEta = True
, optForcing = True
, optProjectionLike = True
, optRewriting = False
, optCubical = False
, optPostfixProjections = False
, optKeepPatternVariables = False
, optTopLevelInteractionNoPrivate = False
, optInstanceSearchDepth = 500
, optOverlappingInstances = False
, optQualifiedInstances = True
, optInversionMaxDepth = 50
, optSafe = False
, optDoubleCheck = False
, optSyntacticEquality = True
, optCompareSorts = True
, optWarningMode = defaultWarningMode
, optCompileNoMain = False
, optCaching = True
, optCountClusters = False
, optAutoInline = True
, optPrintPatternSynonyms = True
, optFastReduce = True
, optCallByName = False
, optConfluenceCheck = False
, optFlatSplit = True
}
-- | The default termination depth.
defaultCutOff :: CutOff
defaultCutOff = CutOff 0 -- minimum value
-- | The default output directory for LaTeX.
defaultLaTeXDir :: String
defaultLaTeXDir = "latex"
-- | The default output directory for HTML.
defaultHTMLDir :: String
defaultHTMLDir = "html"
type OptM = ExceptT String IO
runOptM :: OptM a -> IO (Either String a)
runOptM = runExceptT
{- | @f :: Flag opts@ is an action on the option record that results from
parsing an option. @f opts@ produces either an error message or an
updated options record
-}
type Flag opts = opts -> OptM opts
-- | Checks that the given options are consistent.
checkOpts :: Flag CommandLineOptions
checkOpts opts
| htmlRelated = throwError htmlRelatedMessage
| matches [optGHCiInteraction, optJSONInteraction, isJust . optInputFile] > 1 =
throwError "Choose at most one: input file, --interactive, or --interaction-json.\n"
| or [ p opts && matches ps > 1 | (p, ps) <- exclusive ] =
throwError exclusiveMessage
| otherwise = return opts
where
matches = length . filter ($ opts)
optionChanged opt = ((/=) `on` opt) opts defaultOptions
atMostOne =
[ optGenerateHTML
, isJust . optDependencyGraph
] ++
map fst exclusive
exclusive =
[ ( optOnlyScopeChecking
, optGenerateVimFile :
atMostOne
)
, ( optInteractive
, optGenerateLaTeX : atMostOne
)
, ( optGHCiInteraction
, optGenerateLaTeX : atMostOne
)
, ( optJSONInteraction
, optGenerateLaTeX : atMostOne
)
]
exclusiveMessage = unlines $
[ "The options --interactive, --interaction, --interaction-json and"
, "--only-scope-checking cannot be combined with each other or"
, "with --html or --dependency-graph. Furthermore"
, "--interactive and --interaction cannot be combined with"
, "--latex, and --only-scope-checking cannot be combined with"
, "--vim."
]
htmlRelated = not (optGenerateHTML opts) &&
( optionChanged optHTMLDir
|| optionChanged optHTMLHighlight
|| optionChanged optCSSFile
|| optionChanged optHighlightOccurrences
)
htmlRelatedMessage = unlines $
[ "The options --html-highlight, --css-dir, --highlight-occurrences"
, "and --html-dir only be used along with --html flag."
]
-- | Check for unsafe pragmas. Gives a list of used unsafe flags.
unsafePragmaOptions :: CommandLineOptions -> PragmaOptions -> [String]
unsafePragmaOptions clo opts =
[ "--allow-unsolved-metas" | optAllowUnsolved opts
, not $ optInteractive clo ] ++
[ "--allow-incomplete-matches" | optAllowIncompleteMatch opts ] ++
[ "--no-positivity-check" | optDisablePositivity opts ] ++
[ "--no-termination-check" | not (optTerminationCheck opts) ] ++
[ "--type-in-type" | not (optUniverseCheck opts) ] ++
[ "--omega-in-omega" | optOmegaInOmega opts ] ++
-- [ "--sized-types" | optSizedTypes opts ] ++
[ "--sized-types and --guardedness" | collapseDefault (optSizedTypes opts)
, collapseDefault (optGuardedness opts) ] ++
[ "--injective-type-constructors" | optInjectiveTypeConstructors opts ] ++
[ "--irrelevant-projections" | optIrrelevantProjections opts ] ++
[ "--experimental-irrelevance" | optExperimentalIrrelevance opts ] ++
[ "--rewriting" | optRewriting opts ] ++
[ "--cubical and --with-K" | optCubical opts
, not (collapseDefault $ optWithoutK opts) ] ++
[ "--cumulativity" | optCumulativity opts ] ++
[]
-- | If any these options have changed, then the file will be
-- rechecked. Boolean options are negated to mention non-default
-- options, where possible.
restartOptions :: [(PragmaOptions -> RestartCodomain, String)]
restartOptions =
[ (C . optTerminationDepth, "--termination-depth")
, (B . not . optUseUnicode, "--no-unicode")
, (B . optAllowUnsolved, "--allow-unsolved-metas")
, (B . optAllowIncompleteMatch, "--allow-incomplete-matches")
, (B . optDisablePositivity, "--no-positivity-check")
, (B . optTerminationCheck, "--no-termination-check")
, (B . not . optUniverseCheck, "--type-in-type")
, (B . optOmegaInOmega, "--omega-in-omega")
, (B . collapseDefault . optSubtyping, "--subtyping")
, (B . optCumulativity, "--cumulativity")
, (B . not . collapseDefault . optSizedTypes, "--no-sized-types")
, (B . not . collapseDefault . optGuardedness, "--no-guardedness")
, (B . optInjectiveTypeConstructors, "--injective-type-constructors")
, (B . optProp, "--prop")
, (B . not . optUniversePolymorphism, "--no-universe-polymorphism")
, (B . optIrrelevantProjections, "--irrelevant-projections")
, (B . optExperimentalIrrelevance, "--experimental-irrelevance")
, (B . collapseDefault . optWithoutK, "--without-K")
, (B . optExactSplit, "--exact-split")
, (B . not . optEta, "--no-eta-equality")
, (B . optRewriting, "--rewriting")
, (B . optCubical, "--cubical")
, (B . optOverlappingInstances, "--overlapping-instances")
, (B . optQualifiedInstances, "--qualified-instances")
, (B . not . optQualifiedInstances, "--no-qualified-instances")
, (B . optSafe, "--safe")
, (B . optDoubleCheck, "--double-check")
, (B . not . optSyntacticEquality, "--no-syntactic-equality")
, (B . not . optCompareSorts, "--no-sort-comparison")
, (B . not . optAutoInline, "--no-auto-inline")
, (B . not . optFastReduce, "--no-fast-reduce")
, (B . optCallByName, "--call-by-name")
, (I . optInstanceSearchDepth, "--instance-search-depth")
, (I . optInversionMaxDepth, "--inversion-max-depth")
, (W . optWarningMode, "--warning")
, (B . optConfluenceCheck, "--confluence-check")
]
-- to make all restart options have the same type
data RestartCodomain = C CutOff | B Bool | I Int | W WarningMode
deriving Eq
-- | An infective option is an option that if used in one module, must
-- be used in all modules that depend on this module.
infectiveOptions :: [(PragmaOptions -> Bool, String)]
infectiveOptions =
[ (optCubical, "--cubical")
, (optProp, "--prop")
]
-- | A coinfective option is an option that if used in one module, must
-- be used in all modules that this module depends on.
coinfectiveOptions :: [(PragmaOptions -> Bool, String)]
coinfectiveOptions =
[ (optSafe, "--safe")
, (collapseDefault . optWithoutK, "--without-K")
, (not . optUniversePolymorphism, "--no-universe-polymorphism")
, (not . collapseDefault . optSizedTypes, "--no-sized-types")
, (not . collapseDefault . optGuardedness, "--no-guardedness")
, (not . collapseDefault . optSubtyping, "--no-subtyping")
, (not . optCumulativity, "--no-cumulativity")
]
inputFlag :: FilePath -> Flag CommandLineOptions
inputFlag f o =
case optInputFile o of
Nothing -> return $ o { optInputFile = Just f }
Just _ -> throwError "only one input file allowed"
versionFlag :: Flag CommandLineOptions
versionFlag o = return $ o { optShowVersion = True }
helpFlag :: Maybe String -> Flag CommandLineOptions
helpFlag Nothing o = return $ o { optShowHelp = Just GeneralHelp }
helpFlag (Just str) o = case string2HelpTopic str of
Just hpt -> return $ o { optShowHelp = Just (HelpFor hpt) }
Nothing -> throwError $ "unknown help topic " ++ str ++ " (available: " ++
intercalate ", " (map fst allHelpTopics) ++ ")"
safeFlag :: Flag PragmaOptions
safeFlag o = do
let guardedness = optGuardedness o
let sizedTypes = optSizedTypes o
return $ o { optSafe = True
, optGuardedness = setDefault False guardedness
, optSizedTypes = setDefault False sizedTypes
}
flatSplitFlag :: Flag PragmaOptions
flatSplitFlag o = return $ o { optFlatSplit = True }
noFlatSplitFlag :: Flag PragmaOptions
noFlatSplitFlag o = return $ o { optFlatSplit = False }
doubleCheckFlag :: Flag PragmaOptions
doubleCheckFlag o = return $ o { optDoubleCheck = True }
noSyntacticEqualityFlag :: Flag PragmaOptions
noSyntacticEqualityFlag o = return $ o { optSyntacticEquality = False }
noSortComparisonFlag :: Flag PragmaOptions
noSortComparisonFlag o = return $ o { optCompareSorts = False }
sharingFlag :: Bool -> Flag CommandLineOptions
sharingFlag _ _ = throwError $
"Feature --sharing has been removed (in favor of the Agda abstract machine)."
cachingFlag :: Bool -> Flag PragmaOptions
cachingFlag b o = return $ o { optCaching = b }
propFlag :: Flag PragmaOptions
propFlag o = return $ o { optProp = True }
noPropFlag :: Flag PragmaOptions
noPropFlag o = return $ o { optProp = False }
experimentalIrrelevanceFlag :: Flag PragmaOptions
experimentalIrrelevanceFlag o = return $ o { optExperimentalIrrelevance = True }
irrelevantProjectionsFlag :: Flag PragmaOptions
irrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = True }
noIrrelevantProjectionsFlag :: Flag PragmaOptions
noIrrelevantProjectionsFlag o = return $ o { optIrrelevantProjections = False }
ignoreInterfacesFlag :: Flag CommandLineOptions
ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True }
ignoreAllInterfacesFlag :: Flag CommandLineOptions
ignoreAllInterfacesFlag o = return $ o { optIgnoreAllInterfaces = True }
localInterfacesFlag :: Flag CommandLineOptions
localInterfacesFlag o = return $ o { optLocalInterfaces = True }
allowUnsolvedFlag :: Flag PragmaOptions
allowUnsolvedFlag o = do
let upd = over warningSet (Set.\\ unsolvedWarnings)
return $ o { optAllowUnsolved = True
, optWarningMode = upd (optWarningMode o)
}
allowIncompleteMatchFlag :: Flag PragmaOptions
allowIncompleteMatchFlag o = do
let upd = over warningSet (Set.\\ incompleteMatchWarnings)
return $ o { optAllowIncompleteMatch = True
, optWarningMode = upd (optWarningMode o)
}
showImplicitFlag :: Flag PragmaOptions
showImplicitFlag o = return $ o { optShowImplicit = True }
showIrrelevantFlag :: Flag PragmaOptions
showIrrelevantFlag o = return $ o { optShowIrrelevant = True }
asciiOnlyFlag :: Flag PragmaOptions
asciiOnlyFlag o = do
lift $ writeIORef unicodeOrAscii AsciiOnly
return $ o { optUseUnicode = False }
ghciInteractionFlag :: Flag CommandLineOptions
ghciInteractionFlag o = return $ o { optGHCiInteraction = True }
jsonInteractionFlag :: Flag CommandLineOptions
jsonInteractionFlag o = return $ o { optJSONInteraction = True }
vimFlag :: Flag CommandLineOptions
vimFlag o = return $ o { optGenerateVimFile = True }
latexFlag :: Flag CommandLineOptions
latexFlag o = return $ o { optGenerateLaTeX = True }
onlyScopeCheckingFlag :: Flag CommandLineOptions
onlyScopeCheckingFlag o = return $ o { optOnlyScopeChecking = True }
countClustersFlag :: Flag PragmaOptions
countClustersFlag o =
#ifdef COUNT_CLUSTERS
return $ o { optCountClusters = True }
#else
throwError
"Cluster counting has not been enabled in this build of Agda."
#endif
noAutoInlineFlag :: Flag PragmaOptions
noAutoInlineFlag o = return $ o { optAutoInline = False }
noPrintPatSynFlag :: Flag PragmaOptions
noPrintPatSynFlag o = return $ o { optPrintPatternSynonyms = False }
noFastReduceFlag :: Flag PragmaOptions
noFastReduceFlag o = return $ o { optFastReduce = False }
callByNameFlag :: Flag PragmaOptions
callByNameFlag o = return $ o { optCallByName = True }
latexDirFlag :: FilePath -> Flag CommandLineOptions
latexDirFlag d o = return $ o { optLaTeXDir = d }
noPositivityFlag :: Flag PragmaOptions
noPositivityFlag o = do
let upd = over warningSet (Set.delete NotStrictlyPositive_)
return $ o { optDisablePositivity = True
, optWarningMode = upd (optWarningMode o)
}
dontTerminationCheckFlag :: Flag PragmaOptions
dontTerminationCheckFlag o = do
let upd = over warningSet (Set.delete TerminationIssue_)
return $ o { optTerminationCheck = False
, optWarningMode = upd (optWarningMode o)
}
-- The option was removed. See Issue 1918.
dontCompletenessCheckFlag :: Flag PragmaOptions
dontCompletenessCheckFlag _ =
throwError "The --no-coverage-check option has been removed."
dontUniverseCheckFlag :: Flag PragmaOptions
dontUniverseCheckFlag o = return $ o { optUniverseCheck = False }
omegaInOmegaFlag :: Flag PragmaOptions
omegaInOmegaFlag o = return $ o { optOmegaInOmega = True }
subtypingFlag :: Flag PragmaOptions
subtypingFlag o = return $ o { optSubtyping = Value True }
noSubtypingFlag :: Flag PragmaOptions
noSubtypingFlag o = return $ o { optSubtyping = Value False }
cumulativityFlag :: Flag PragmaOptions
cumulativityFlag o =
return $ o { optCumulativity = True
, optSubtyping = setDefault True $ optSubtyping o
}
noCumulativityFlag :: Flag PragmaOptions
noCumulativityFlag o = return $ o { optCumulativity = False }
--UNUSED Liang-Ting Chen 2019-07-16
--etaFlag :: Flag PragmaOptions
--etaFlag o = return $ o { optEta = True }
noEtaFlag :: Flag PragmaOptions
noEtaFlag o = return $ o { optEta = False }
sizedTypes :: Flag PragmaOptions
sizedTypes o =
return $ o { optSizedTypes = Value True
--, optSubtyping = setDefault True $ optSubtyping o
}
noSizedTypes :: Flag PragmaOptions
noSizedTypes o = return $ o { optSizedTypes = Value False }
guardedness :: Flag PragmaOptions
guardedness o = return $ o { optGuardedness = Value True }
noGuardedness :: Flag PragmaOptions
noGuardedness o = return $ o { optGuardedness = Value False }
injectiveTypeConstructorFlag :: Flag PragmaOptions
injectiveTypeConstructorFlag o = return $ o { optInjectiveTypeConstructors = True }
guardingTypeConstructorFlag :: Flag PragmaOptions
guardingTypeConstructorFlag _ = throwError $
"Experimental feature --guardedness-preserving-type-constructors has been removed."
universePolymorphismFlag :: Flag PragmaOptions
universePolymorphismFlag o = return $ o { optUniversePolymorphism = True }
noUniversePolymorphismFlag :: Flag PragmaOptions
noUniversePolymorphismFlag o = return $ o { optUniversePolymorphism = False }
noForcingFlag :: Flag PragmaOptions
noForcingFlag o = return $ o { optForcing = False }
noProjectionLikeFlag :: Flag PragmaOptions
noProjectionLikeFlag o = return $ o { optProjectionLike = False }
withKFlag :: Flag PragmaOptions
withKFlag o = return $ o { optWithoutK = Value False }
withoutKFlag :: Flag PragmaOptions
withoutKFlag o = return $ o { optWithoutK = Value True }
copatternsFlag :: Flag PragmaOptions
copatternsFlag o = return $ o { optCopatterns = True }
noCopatternsFlag :: Flag PragmaOptions
noCopatternsFlag o = return $ o { optCopatterns = False }
noPatternMatchingFlag :: Flag PragmaOptions
noPatternMatchingFlag o = return $ o { optPatternMatching = False }
exactSplitFlag :: Flag PragmaOptions
exactSplitFlag o = do
let upd = over warningSet (Set.insert CoverageNoExactSplit_)
return $ o { optExactSplit = True
, optWarningMode = upd (optWarningMode o)
}
noExactSplitFlag :: Flag PragmaOptions
noExactSplitFlag o = do
let upd = over warningSet (Set.delete CoverageNoExactSplit_)
return $ o { optExactSplit = False
, optWarningMode = upd (optWarningMode o)
}
rewritingFlag :: Flag PragmaOptions
rewritingFlag o = return $ o { optRewriting = True }
cubicalFlag :: Flag PragmaOptions
cubicalFlag o = do
let withoutK = optWithoutK o
return $ o { optCubical = True
, optWithoutK = setDefault True withoutK
}
postfixProjectionsFlag :: Flag PragmaOptions
postfixProjectionsFlag o = return $ o { optPostfixProjections = True }
keepPatternVariablesFlag :: Flag PragmaOptions
keepPatternVariablesFlag o = return $ o { optKeepPatternVariables = True }
topLevelInteractionNoPrivateFlag :: Flag PragmaOptions
topLevelInteractionNoPrivateFlag o = return $ o { optTopLevelInteractionNoPrivate = True }
instanceDepthFlag :: String -> Flag PragmaOptions
instanceDepthFlag s o = do
d <- integerArgument "--instance-search-depth" s
return $ o { optInstanceSearchDepth = d }
overlappingInstancesFlag :: Flag PragmaOptions
overlappingInstancesFlag o = return $ o { optOverlappingInstances = True }
noOverlappingInstancesFlag :: Flag PragmaOptions
noOverlappingInstancesFlag o = return $ o { optOverlappingInstances = False }
qualifiedInstancesFlag :: Flag PragmaOptions
qualifiedInstancesFlag o = return $ o { optQualifiedInstances = True }
noQualifiedInstancesFlag :: Flag PragmaOptions
noQualifiedInstancesFlag o = return $ o { optQualifiedInstances = False }
inversionMaxDepthFlag :: String -> Flag PragmaOptions
inversionMaxDepthFlag s o = do
d <- integerArgument "--inversion-max-depth" s
return $ o { optInversionMaxDepth = d }
interactiveFlag :: Flag CommandLineOptions
interactiveFlag o = do
prag <- allowUnsolvedFlag (optPragmaOptions o)
return $ o { optInteractive = True
, optPragmaOptions = prag
}
compileFlagNoMain :: Flag PragmaOptions
compileFlagNoMain o = return $ o { optCompileNoMain = True }
compileDirFlag :: FilePath -> Flag CommandLineOptions
compileDirFlag f o = return $ o { optCompileDir = Just f }
htmlFlag :: Flag CommandLineOptions
htmlFlag o = return $ o { optGenerateHTML = True }
htmlHighlightFlag :: String -> Flag CommandLineOptions
htmlHighlightFlag "code" o = return $ o { optHTMLHighlight = HighlightCode }
htmlHighlightFlag "all" o = return $ o { optHTMLHighlight = HighlightAll }
htmlHighlightFlag "auto" o = return $ o { optHTMLHighlight = HighlightAuto }
htmlHighlightFlag opt o = throwError $ "Invalid option <" ++ opt
++ ">, expected <all>, <auto> or <code>"
dependencyGraphFlag :: FilePath -> Flag CommandLineOptions
dependencyGraphFlag f o = return $ o { optDependencyGraph = Just f }
htmlDirFlag :: FilePath -> Flag CommandLineOptions
htmlDirFlag d o = return $ o { optHTMLDir = d }
cssFlag :: FilePath -> Flag CommandLineOptions
cssFlag f o = return $ o { optCSSFile = Just f }
highlightOccurrencesFlag :: Flag CommandLineOptions
highlightOccurrencesFlag o = return $ o { optHighlightOccurrences = True }
includeFlag :: FilePath -> Flag CommandLineOptions
includeFlag d o = return $ o { optIncludePaths = d : optIncludePaths o }
libraryFlag :: String -> Flag CommandLineOptions
libraryFlag s o = return $ o { optLibraries = optLibraries o ++ [s] }
overrideLibrariesFileFlag :: String -> Flag CommandLineOptions
overrideLibrariesFileFlag s o = do
ifM (liftIO $ doesFileExist s)
{-then-} (return $ o { optOverrideLibrariesFile = Just s
, optUseLibs = True
})
{-else-} (throwError $ "Libraries file not found: " ++ s)
noDefaultLibsFlag :: Flag CommandLineOptions
noDefaultLibsFlag o = return $ o { optDefaultLibs = False }
noLibsFlag :: Flag CommandLineOptions
noLibsFlag o = return $ o { optUseLibs = False }
verboseFlag :: String -> Flag PragmaOptions
verboseFlag s o =
do (k,n) <- parseVerbose s
return $ o { optVerbose = Trie.insert k n $ optVerbose o }
where
parseVerbose s = case wordsBy (`elem` (":." :: String)) s of
[] -> usage
ss -> do
n <- maybe usage return $ readMaybe (last ss)
return (init ss, n)
usage = throwError "argument to verbose should be on the form x.y.z:N or N"
warningModeFlag :: String -> Flag PragmaOptions
warningModeFlag s o = case warningModeUpdate s of
Just upd -> return $ o { optWarningMode = upd (optWarningMode o) }
Nothing -> throwError $ "unknown warning flag " ++ s ++ ". See --help=warning."
terminationDepthFlag :: String -> Flag PragmaOptions
terminationDepthFlag s o =
do k <- maybe usage return $ readMaybe s
when (k < 1) $ usage -- or: turn termination checking off for 0
return $ o { optTerminationDepth = CutOff $ k-1 }
where usage = throwError "argument to termination-depth should be >= 1"
confluenceCheckFlag :: Flag PragmaOptions
confluenceCheckFlag o = return $ o { optConfluenceCheck = True }
noConfluenceCheckFlag :: Flag PragmaOptions
noConfluenceCheckFlag o = return $ o { optConfluenceCheck = False }
withCompilerFlag :: FilePath -> Flag CommandLineOptions
withCompilerFlag fp o = case optWithCompiler o of
Nothing -> pure o { optWithCompiler = Just fp }
Just{} -> throwError "only one compiler path allowed"
integerArgument :: String -> String -> OptM Int
integerArgument flag s = maybe usage return $ readMaybe s
where
usage = throwError $ "option '" ++ flag ++ "' requires an integer argument"
standardOptions :: [OptDescr (Flag CommandLineOptions)]
standardOptions =
[ Option ['V'] ["version"] (NoArg versionFlag) "show version number"
, Option ['?'] ["help"] (OptArg helpFlag "TOPIC")
("show help for TOPIC (available: "
++ intercalate ", " (map fst allHelpTopics)
++ ")")
, Option ['I'] ["interactive"] (NoArg interactiveFlag)
"start in interactive mode"
, Option [] ["interaction"] (NoArg ghciInteractionFlag)
"for use with the Emacs mode"
, Option [] ["interaction-json"] (NoArg jsonInteractionFlag)
"for use with other editors such as Atom"
, Option [] ["compile-dir"] (ReqArg compileDirFlag "DIR")
("directory for compiler output (default: the project root)")
, Option [] ["vim"] (NoArg vimFlag)
"generate Vim highlighting files"
, Option [] ["latex"] (NoArg latexFlag)
"generate LaTeX with highlighted source code"
, Option [] ["latex-dir"] (ReqArg latexDirFlag "DIR")
("directory in which LaTeX files are placed (default: " ++
defaultLaTeXDir ++ ")")
, Option [] ["html"] (NoArg htmlFlag)
"generate HTML files with highlighted source code"
, Option [] ["html-dir"] (ReqArg htmlDirFlag "DIR")
("directory in which HTML files are placed (default: " ++
defaultHTMLDir ++ ")")
, Option [] ["highlight-occurrences"] (NoArg highlightOccurrencesFlag)
("highlight all occurrences of hovered symbol in generated " ++
"HTML files")
, Option [] ["css"] (ReqArg cssFlag "URL")
"the CSS file used by the HTML files (can be relative)"
, Option [] ["html-highlight"] (ReqArg htmlHighlightFlag "[code,all,auto]")
("whether to highlight only the code parts (code) or " ++
"the file as a whole (all) or " ++
"decide by source file type (auto)")
, Option [] ["dependency-graph"] (ReqArg dependencyGraphFlag "FILE")
"generate a Dot file with a module dependency graph"
, Option [] ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)
"ignore interface files (re-type check everything)"
, Option [] ["local-interfaces"] (NoArg localInterfacesFlag)
"put interface files next to the Agda files they correspond to"
, Option ['i'] ["include-path"] (ReqArg includeFlag "DIR")
"look for imports in DIR"
, Option ['l'] ["library"] (ReqArg libraryFlag "LIB")
"use library LIB"
, Option [] ["library-file"] (ReqArg overrideLibrariesFileFlag "FILE")
"use FILE instead of the standard libraries file"
, Option [] ["no-libraries"] (NoArg noLibsFlag)
"don't use any library files"
, Option [] ["no-default-libraries"] (NoArg noDefaultLibsFlag)
"don't use default libraries"
, Option [] ["only-scope-checking"] (NoArg onlyScopeCheckingFlag)
"only scope-check the top-level module, do not type-check it"
, Option [] ["with-compiler"] (ReqArg withCompilerFlag "PATH")
"use the compiler available at PATH"
] ++ map (fmap lensPragmaOptions) pragmaOptions
-- | Defined locally here since module ''Agda.Interaction.Options.Lenses''
-- has cyclic dependency.
lensPragmaOptions :: Lens' PragmaOptions CommandLineOptions
lensPragmaOptions f st = f (optPragmaOptions st) <&> \ opts -> st { optPragmaOptions = opts }
-- | Command line options of previous versions of Agda.
-- Should not be listed in the usage info, put parsed by GetOpt for good error messaging.
deadStandardOptions :: [OptDescr (Flag CommandLineOptions)]
deadStandardOptions =
[ Option [] ["sharing"] (NoArg $ sharingFlag True)
"DEPRECATED: does nothing"
, Option [] ["no-sharing"] (NoArg $ sharingFlag False)
"DEPRECATED: does nothing"
, Option [] ["ignore-all-interfaces"] (NoArg ignoreAllInterfacesFlag) -- not deprecated! Just hidden
"ignore all interface files (re-type check everything, including builtin files)"
] ++ map (fmap lensPragmaOptions) deadPragmaOptions
pragmaOptions :: [OptDescr (Flag PragmaOptions)]
pragmaOptions =
[ Option [] ["show-implicit"] (NoArg showImplicitFlag)
"show implicit arguments when printing"
, Option [] ["show-irrelevant"] (NoArg showIrrelevantFlag)
"show irrelevant arguments when printing"
, Option [] ["no-unicode"] (NoArg asciiOnlyFlag)
"don't use unicode characters when printing terms"
, Option ['v'] ["verbose"] (ReqArg verboseFlag "N")
"set verbosity level to N"
, Option [] ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)
"succeed and create interface file regardless of unsolved meta variables"
, Option [] ["allow-incomplete-matches"] (NoArg allowIncompleteMatchFlag)
"succeed and create interface file regardless of incomplete pattern matches"
, Option [] ["no-positivity-check"] (NoArg noPositivityFlag)
"do not warn about not strictly positive data types"
, Option [] ["no-termination-check"] (NoArg dontTerminationCheckFlag)
"do not warn about possibly nonterminating code"
, Option [] ["termination-depth"] (ReqArg terminationDepthFlag "N")
"allow termination checker to count decrease/increase upto N (default N=1)"
, Option [] ["type-in-type"] (NoArg dontUniverseCheckFlag)
"ignore universe levels (this makes Agda inconsistent)"
, Option [] ["omega-in-omega"] (NoArg omegaInOmegaFlag)
"enable typing rule Setω : Setω (this makes Agda inconsistent)"
, Option [] ["subtyping"] (NoArg subtypingFlag)
"enable subtyping rules in general (e.g. for irrelevance and erasure)"
, Option [] ["no-subtyping"] (NoArg noSubtypingFlag)
"disable subtyping rules in general (e.g. for irrelevance and erasure) (default)"
, Option [] ["cumulativity"] (NoArg cumulativityFlag)
"enable subtyping of universes (e.g. Set =< Set₁) (implies --subtyping)"
, Option [] ["no-cumulativity"] (NoArg noCumulativityFlag)
"disable subtyping of universes (default)"
, Option [] ["prop"] (NoArg propFlag)
"enable the use of the Prop universe"
, Option [] ["no-prop"] (NoArg noPropFlag)
"disable the use of the Prop universe (default)"
, Option [] ["sized-types"] (NoArg sizedTypes)
"enable sized types (default, inconsistent with --guardedness, implies --subtyping)"
, Option [] ["no-sized-types"] (NoArg noSizedTypes)
"disable sized types"
, Option [] ["flat-split"] (NoArg flatSplitFlag)
"allow split on (x :{flat} A) arguments (default)"
, Option [] ["no-flat-split"] (NoArg noFlatSplitFlag)
"disable split on (x :{flat} A) arguments"
, Option [] ["guardedness"] (NoArg guardedness)
"enable constructor-based guarded corecursion (default, inconsistent with --sized-types)"
, Option [] ["no-guardedness"] (NoArg noGuardedness)
"disable constructor-based guarded corecursion"
, Option [] ["injective-type-constructors"] (NoArg injectiveTypeConstructorFlag)
"enable injective type constructors (makes Agda anti-classical and possibly inconsistent)"
, Option [] ["no-universe-polymorphism"] (NoArg noUniversePolymorphismFlag)
"disable universe polymorphism"
, Option [] ["universe-polymorphism"] (NoArg universePolymorphismFlag)
"enable universe polymorphism (default)"