
   0 | module Idris.CommandLine
   1 | 
   2 | import Idris.Env
   3 | import Idris.Version
   4 | import Idris.Doc.Display
   5 | import Idris.Doc.String
   6 | import Idris.Pretty
   7 | 
   8 | import Core.Options
   9 | 
  10 | import Data.Maybe
  11 | import Data.String
  12 | import Data.Either
  13 | 
  14 | import System
  15 | 
  16 | %default total
  17 | 
  18 | public export
  19 | data PkgCommand
  20 |       = Build
  21 |       | Install
  22 |       | InstallWithSrc
  23 |       | MkDoc
  24 |       | Typecheck
  25 |       | Clean
  26 |       | REPL
  27 |       | Init
  28 |       | DumpJson
  29 |       | DumpInstallDir
  30 | 
  31 | export
  32 | Show PkgCommand where
  33 |   show Build = "--build"
  34 |   show Install = "--install"
  35 |   show InstallWithSrc = "--install-with-src"
  36 |   show MkDoc = "--mkdoc"
  37 |   show Typecheck = "--typecheck"
  38 |   show Clean = "--clean"
  39 |   show REPL = "--repl"
  40 |   show Init = "--init"
  41 |   show DumpJson = "--dump-ipkg-json"
  42 |   show DumpInstallDir = "--dump-installdir"
  43 | 
  44 | public export
  45 | data DirCommand
  46 |       = LibDir | -- show top level package directory
  47 |          ||| Show the installation prefix
  48 |         Prefix |
  49 |         BlodwenPaths
  50 | 
  51 | export
  52 | Show DirCommand where
  53 |   show LibDir = "--libdir"
  54 |   show Prefix = "--prefix"
  55 |   show BlodwenPaths = "--paths"
  56 | 
  57 | ||| Help topics
  58 | public export
  59 | data HelpTopic
  60 |   = ||| Interactive debugging topics
  61 |     HelpLogging
  62 |   | ||| The various pragmas
  63 |     HelpPragma
  64 | 
  65 | recogniseHelpTopic : String -> Maybe HelpTopic
  66 | recogniseHelpTopic "logging"   = pure HelpLogging
  67 | recogniseHelpTopic "pragma" = pure HelpPragma
  68 | recogniseHelpTopic _ = Nothing
  69 | 
  70 | ||| CLOpt - possible command line options
  71 | public export
  72 | data CLOpt
  73 |   =
  74 |    ||| Only typecheck the given file
  75 |   CheckOnly |
  76 |    ||| The output file from the code generator
  77 |   OutputFile String |
  78 |    ||| Execute a given function after checking the source file
  79 |   ExecFn String |
  80 |    ||| Use a specific code generator
  81 |   SetCG String |
  82 |    ||| Pass a directive to the code generator
  83 |   Directive String |
  84 |    ||| Don't implicitly import Prelude
  85 |   NoPrelude |
  86 |    ||| Set source directory
  87 |   SourceDir String |
  88 |    ||| Set build directory
  89 |   BuildDir String |
  90 |    ||| Set output directory
  91 |   OutputDir String |
  92 |    ||| Generate profile data when compiling (backend dependent)
  93 |   Profile |
  94 |    ||| Display Idris version
  95 |   Version |
  96 |    ||| Display the TTC version currently used
  97 |   TTCVersion |
  98 |    ||| Display help text
  99 |   Help (Maybe HelpTopic) |
 100 |    ||| Suppress the banner
 101 |   NoBanner |
 102 |    ||| Run Idris 2 in quiet mode
 103 |   Quiet |
 104 |    ||| Show implicits when pretty printing
 105 |   ShowImplicits |
 106 |    ||| Show machine names when pretty printing
 107 |   ShowMachineNames |
 108 |    ||| Show namespaces when pretty printing
 109 |   ShowNamespaces |
 110 |    ||| Run Idris 2 in verbose mode (cancels quiet if it's the default)
 111 |   Verbose |
 112 |    ||| Set the console width for REPL output
 113 |   ConsoleWidth (Maybe Nat) |
 114 |    ||| Whether to use color in the console output
 115 |   Color Bool |
 116 |    ||| Set the log level globally
 117 |   Logging LogLevel |
 118 |    ||| Add a package as a dependency
 119 |   PkgPath String |
 120 |    ||| List installed packages
 121 |   ListPackages |
 122 |    ||| Build or install a given package, depending on PkgCommand
 123 |   Package PkgCommand (Maybe String) |
 124 |    ||| Show locations of data/library directories
 125 |   Directory DirCommand |
 126 |    ||| The input Idris file
 127 |   InputFile String |
 128 |    ||| Whether or not to run in IdeMode (easily parsable for other tools)
 129 |   IdeMode |
 130 |    ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
 131 |   IdeModeSocket String |
 132 |    ||| Run as a checker for the core language TTImp
 133 |   Yaffle String |
 134 |    ||| Dump metadata from a .ttm file
 135 |   Metadata String |
 136 |    ||| Dump cases before compiling
 137 |   DumpCases String |
 138 |    ||| Dump lambda lifted defs before compiling
 139 |   DumpLifted String |
 140 |    ||| Dump ANF defs before compiling
 141 |   DumpANF String |
 142 |    ||| Dump VM code defs before compiling
 143 |   DumpVMCode String |
 144 |    ||| Run a REPL command then exit immediately
 145 |   RunREPL String |
 146 |   IgnoreMissingIPKG |
 147 |   FindIPKG |
 148 |   Timing (Maybe Nat) |
 149 |   DebugElabCheck |
 150 |   AltErrorCount Nat |
 151 |    ||| Treat warnings as errors
 152 |   WarningsAsErrors |
 153 |    ||| Do not print shadowing warnings
 154 |   IgnoreShadowingWarnings |
 155 |    ||| Use SHA256 hashes to determine if a source file needs rebuilding instead
 156 |    ||| of modification time.
 157 |   HashesInsteadOfModTime |
 158 |    ||| Apply experimental heuristics to case tree generation that
 159 |    ||| sometimes improves performance and reduces compiled code
 160 |    ||| size.
 161 |   CaseTreeHeuristics |
 162 |    ||| Use incremental code generation, if the backend supports it
 163 |   IncrementalCG String |
 164 |    ||| Use whole program compilation - overrides IncrementalCG if set
 165 |   WholeProgram |
 166 |    ||| Generate bash completion info
 167 |   BashCompletion String String |
 168 |    ||| Generate bash completion script
 169 |   BashCompletionScript String |
 170 |    ||| Generate zsh completion script
 171 |   ZshCompletionScript String |
 172 |    ||| Turn on %default total globally
 173 |   Total |
 174 |    ||| Disable common subexpression elimination
 175 |   NoCSE
 176 | 
 177 | ||| Extract the host and port to bind the IDE socket to
 178 | export
 179 | ideSocketModeAddress : List CLOpt -> (String, Int)
 180 | ideSocketModeAddress []  = ("localhost", 0)
 181 | ideSocketModeAddress (IdeModeSocket hp :: _) =
 182 |   let (h, p) = String.break (== ':') hp
 183 |       port = fromMaybe 0 (portPart p >>= parsePositive)
 184 |       host = if h == "" then "localhost" else h
 185 |   in (host, port)
 186 |   where
 187 |     portPart : String -> Maybe String
 188 |     portPart p = if p == ""
 189 |                     then Nothing
 190 |                     else Just $ assert_total $ prim__strTail p
 191 | ideSocketModeAddress (_ :: rest) = ideSocketModeAddress rest
 192 | 
 193 | formatSocketAddress : (String, Int) -> String
 194 | formatSocketAddress (host, port) = host ++ ":" ++ show port
 195 | 
 196 | data OptType
 197 |   = Required String
 198 |    | Optional String
 199 |    | RequiredNat String
 200 |    | AutoNat String
 201 |    | RequiredLogLevel String
 202 | 
 203 | Show OptType where
 204 |   show (Required a) = "<" ++ a ++ ">"
 205 |   show (RequiredNat a) = "<" ++ a ++ ">"
 206 |   show (RequiredLogLevel a) = "<" ++ a ++ ">"
 207 |   show (Optional a) = "[" ++ a ++ "]"
 208 |   show (AutoNat a) = "<" ++ a ++ ">"
 209 | 
 210 | ActType : List OptType -> Type
 211 | ActType [] = List CLOpt
 212 | ActType (Required a :: as) = String -> ActType as
 213 | ActType (RequiredNat a :: as) = Nat -> ActType as
 214 | ActType (RequiredLogLevel a :: as) = LogLevel -> ActType as
 215 | ActType (Optional a :: as) = Maybe String -> ActType as
 216 | ActType (AutoNat a :: as) = Maybe Nat -> ActType as
 217 | 
 218 | record OptDesc where
 219 |   constructor MkOpt
 220 |   flags : List String
 221 |   argdescs : List OptType
 222 |   action : ActType argdescs
 223 |   help : Maybe String
 224 | 
 225 | optSeparator : OptDesc
 226 | optSeparator = MkOpt [] [] [] Nothing
 227 | 
 228 | showDefault : Show a => a -> String
 229 | showDefault x = "(default " ++ show x ++ ")"
 230 | 
 231 | options : List OptDesc
 232 | options = [MkOpt ["--check", "-c"] [] [CheckOnly]
 233 |               (Just "Exit after checking source file"),
 234 |            MkOpt ["--output", "-o"] [Required "file"] (\f => [OutputFile f, Quiet])
 235 |               (Just "Specify output file"),
 236 |            MkOpt ["--exec", "-x"] [Required "name"] (\f => [ExecFn f, Quiet])
 237 |               (Just "Execute expression"),
 238 |            MkOpt ["--no-prelude"] [] [NoPrelude]
 239 |               (Just "Don't implicitly import Prelude"),
 240 |            MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
 241 |               (Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
 242 |            MkOpt ["--incremental-cg", "--inc"] [Required "backend"] (\f => [IncrementalCG f])
 243 |              (Just "Incremental code generation on given backend"),
 244 |            MkOpt ["--whole-program", "--wp"] [] [WholeProgram]
 245 |              (Just "Use whole program compilation (overrides --inc)"),
 246 |            MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
 247 |               (Just $ "Pass a directive to the current code generator"),
 248 |            MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
 249 |               (Just "Add a package as a dependency"),
 250 |            MkOpt ["--source-dir"] [Required "dir"] (\d => [SourceDir d])
 251 |               (Just $ "Set source directory"),
 252 |            MkOpt ["--build-dir"] [Required "dir"] (\d => [BuildDir d])
 253 |               (Just $ "Set build directory"),
 254 |            MkOpt ["--output-dir"] [Required "dir"] (\d => [OutputDir d])
 255 |               (Just $ "Set output directory"),
 256 |            MkOpt ["--profile"] [] [Profile]
 257 |               (Just "Generate profile data when compiling, if supported"),
 258 |            MkOpt ["--no-cse"] [] [NoCSE]
 259 |               (Just "Disable common subexpression elimination"),
 260 | 
 261 |            optSeparator,
 262 |            MkOpt ["--total"] [] [Total]
 263 |               (Just "Require functions to be total by default"),
 264 |            MkOpt ["-Werror"] [] [WarningsAsErrors]
 265 |               (Just "Treat warnings as errors"),
 266 |            MkOpt ["-Wno-shadowing"] [] [IgnoreShadowingWarnings]
 267 |               (Just "Do not print shadowing warnings"),
 268 | 
 269 |            optSeparator,
 270 |            MkOpt ["-Xcheck-hashes"] [] [HashesInsteadOfModTime]
 271 |              (Just "Use SHA256 hashes instead of modification time to determine if a source file needs rebuilding"),
 272 |            MkOpt ["-Xcase-tree-opt"] [] [CaseTreeHeuristics]
 273 |               (Just "Apply experimental optimizations to case tree generation"),
 274 | 
 275 |            optSeparator,
 276 |            MkOpt ["--prefix"] [] [Directory Prefix]
 277 |               (Just "Show installation prefix"),
 278 |            MkOpt ["--paths"] [] [Directory BlodwenPaths]
 279 |               (Just "Show paths"),
 280 |            MkOpt ["--libdir"] [] [Directory LibDir]
 281 |               (Just "Show library directory"),
 282 |            MkOpt ["--list-packages"] [] [ListPackages]
 283 |               (Just "List installed packages"),
 284 | 
 285 |            optSeparator,
 286 |            MkOpt ["--init"] [Optional "package file"]
 287 |               (\ f => [Package Init f])
 288 |               (Just "Interactively initialise a new project"),
 289 |            MkOpt ["--dump-ipkg-json"] [Optional "package file"]
 290 |               (\ f => [Package DumpJson f])
 291 |               (Just "Dump an Idris2 package file in the JSON format"),
 292 |            MkOpt ["--dump-installdir"] [Optional "package file"]
 293 |               (\ f => [Package DumpInstallDir f])
 294 |               (Just "Dump the location where the given package will be installed"),
 295 |            MkOpt ["--build"] [Optional "package file"]
 296 |                (\f => [Package Build f])
 297 |               (Just "Build modules/executable for the given package"),
 298 |            MkOpt ["--install"] [Optional "package file"]
 299 |               (\f => [Package Install f])
 300 |               (Just "Install the given package"),
 301 |            MkOpt ["--install-with-src"] [Optional "package file"]
 302 |               (\f => [Package InstallWithSrc f])
 303 |               (Just "Install the given package"),
 304 |            MkOpt ["--mkdoc"] [Optional "package file"]
 305 |               (\f => [Package MkDoc f])
 306 |               (Just "Build documentation for the given package"),
 307 |            MkOpt ["--typecheck"] [Optional "package file"]
 308 |               (\f => [Package Typecheck f])
 309 |               (Just "Typechecks the given package without code generation"),
 310 |            MkOpt ["--clean"] [Optional "package file"] (\f => [Package Clean f])
 311 |               (Just "Clean intermediate files/executables for the given package"),
 312 |            MkOpt ["--repl"] [Optional "package file"] (\f => [Package REPL f])
 313 |               (Just "Build the given package and launch a REPL instance."),
 314 |            MkOpt ["--find-ipkg"] [] [FindIPKG]
 315 |               (Just "Find and use an .ipkg file in a parent directory."),
 316 |            MkOpt ["--ignore-missing-ipkg"] [] [IgnoreMissingIPKG]
 317 |               (Just "Fail silently if a dependency is missing."),
 318 | 
 319 |            optSeparator,
 320 |            MkOpt ["--ide-mode"] [] [IdeMode]
 321 |               (Just "Run the REPL with machine-readable syntax"),
 322 |            MkOpt ["--ide-mode-socket"] [Optional "host:port"]
 323 |                  (\hp => [IdeModeSocket $ fromMaybe (formatSocketAddress (ideSocketModeAddress [])) hp])
 324 |               (Just $ "Run the ide socket mode on given host and port (random open socket by default)"),
 325 | 
 326 |            optSeparator,
 327 |            MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f])
 328 |               (Just "Run a REPL command then quit immediately"),
 329 |            MkOpt ["--timing"] [AutoNat "level"] (\ n => [Timing n])
 330 |               (Just "Display timing logs"),
 331 | 
 332 |            optSeparator,
 333 |            MkOpt ["--no-banner"] [] [NoBanner]
 334 |               (Just "Suppress the banner"),
 335 |            MkOpt ["--quiet", "-q"] [] [Quiet]
 336 |               (Just "Quiet mode; display fewer messages"),
 337 |            MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l])
 338 |               (Just "Width for console output (0 for unbounded) (auto by default)"),
 339 |           MkOpt ["--show-implicits"] [] [ShowImplicits]
 340 |               (Just "Show implicits when pretty printing"),
 341 |            MkOpt ["--show-machine-names"] [] [ShowMachineNames]
 342 |               (Just "Show machine names when pretty printing"),
 343 |            MkOpt ["--show-namespaces"] [] [ShowNamespaces]
 344 |               (Just "Show namespaces when pretty printing"),
 345 |            MkOpt ["--color", "--colour"] [] ([Color True])
 346 |               (Just "Forces colored console output (enabled by default)"),
 347 |            MkOpt ["--no-color", "--no-colour"] [] ([Color False])
 348 |               (Just "Disables colored console output"),
 349 |            MkOpt ["--verbose"] [] [Verbose]
 350 |               (Just "Verbose mode (default)"),
 351 |            MkOpt ["--log"] [RequiredLogLevel "log level"] (\l => [Logging l])
 352 |               (Just "Global log level (0 by default)"),
 353 | 
 354 |            optSeparator,
 355 |            MkOpt ["--version", "-v"] [] [Version]
 356 |               (Just "Display version string"),
 357 |            MkOpt ["--ttc-version"] [] [TTCVersion]
 358 |               (Just "Display TTC version string"),
 359 |            MkOpt ["--help", "-h", "-?"] [Optional "topic"] (\ tp => [Help (tp >>= recogniseHelpTopic)])
 360 |               (Just "Display help text"),
 361 | 
 362 |            -- Internal debugging options
 363 |            MkOpt ["--yaffle", "--ttimp"] [Required "ttimp file"] (\f => [Yaffle f])
 364 |               Nothing, -- run ttimp REPL rather than full Idris
 365 |            MkOpt ["--ttm" ] [Required "ttimp file"] (\f => [Metadata f])
 366 |               Nothing, -- dump metadata information from the given ttm file
 367 |            MkOpt ["--dumpcases"] [Required "output file"] (\f => [DumpCases f])
 368 |               Nothing, -- dump case trees to the given file
 369 |            MkOpt ["--dumplifted"] [Required "output file"] (\f => [DumpLifted f])
 370 |               Nothing, -- dump lambda lifted trees to the given file
 371 |            MkOpt ["--dumpanf"] [Required "output file"] (\f => [DumpANF f])
 372 |               Nothing, -- dump ANF to the given file
 373 |            MkOpt ["--dumpvmcode"] [Required "output file"] (\f => [DumpVMCode f])
 374 |               Nothing, -- dump VM Code to the given file
 375 |            MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
 376 |               Nothing, -- do more elaborator checks (currently conversion in LinearCheck)
 377 |            MkOpt ["--alt-error-count"] [RequiredNat "alternative count"] (\c => [AltErrorCount c])
 378 |               (Just "Outputs errors for the given number of alternative parsing attempts."),
 379 | 
 380 |            optSeparator,
 381 |            -- bash completion
 382 |            MkOpt ["--bash-completion"]
 383 |                  [ Required "input"
 384 |                  , Required "previous input"]
 385 |                  (\w1,w2 => [BashCompletion w1 w2])
 386 |                  (Just "Print bash autocompletion information"),
 387 |            MkOpt ["--bash-completion-script"]
 388 |                  [ Required "function name" ]
 389 |                  (\n => [BashCompletionScript n])
 390 |                  (Just "Generate a bash script to activate autocompletion for Idris2"),
 391 |            -- zsh completion
 392 |            MkOpt ["--zsh-completion-script"]
 393 |                  [ Required "function name" ]
 394 |                  (\n => [ZshCompletionScript n])
 395 |                  (Just "Generate a zsh script (via bashcompinit) to activate autocompletion for Idris2")
 396 |            ]
 397 | 
 398 | optShow : OptDesc -> (String, Maybe String)
 399 | optShow (MkOpt [] _ _ _) = ("", Just "")
 400 | optShow (MkOpt flags argdescs action help) = (showSep ", " flags ++ " " ++
 401 |                                               showSep " " (map show argdescs),
 402 |                                               help)
 403 |   where
 404 |     showSep : String -> List String -> String
 405 |     showSep sep [] = ""
 406 |     showSep sep [x] = x
 407 |     showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
 408 | 
 409 | firstColumnWidth : Nat
 410 | firstColumnWidth = let maxOpt = foldr max 0 $ map (length . fst . optShow) options
 411 |                        maxEnv = foldr max 0 $ map (length . .name) envs in
 412 |                        max maxOpt maxEnv
 413 | 
 414 | makeTextFromOptionsOrEnvs : List (String, Maybe String) -> String
 415 | makeTextFromOptionsOrEnvs rows = concatMap (optUsage firstColumnWidth) rows
 416 |   where
 417 |     optUsage : Nat -> (String, Maybe String) -> String
 418 |     optUsage maxOpt (optshow, help) = maybe ""  -- Don't show anything if there's no help string (that means
 419 |                                                 -- it's an internal option)
 420 |                                       (\h => "  " ++ optshow ++
 421 |                                              pack (List.replicate (minus (maxOpt + 2) (length optshow)) ' ') ++
 422 |                                              h ++ "\n")
 423 |                                       help
 424 | 
 425 | optsUsage : String
 426 | optsUsage = makeTextFromOptionsOrEnvs $ map optShow options
 427 | 
 428 | envsUsage : String
 429 | envsUsage = makeTextFromOptionsOrEnvs $ map (\e => (e.name, Just e.help)) envs
 430 | 
 431 | export
 432 | versionMsg : String
 433 | versionMsg = "Idris 2, version " ++ show version
 434 | 
 435 | export
 436 | usage : String
 437 | usage = """
 438 |   \{ versionMsg }
 439 |   Usage: idris2 [options] [input file]
 440 | 
 441 |   Available options:
 442 |   \{ optsUsage }
 443 |   Environment variables:
 444 |   \{ envsUsage }
 445 |   """
 446 | 
 447 | checkNat : Integer -> Maybe Nat
 448 | checkNat n = toMaybe (n >= 0) (integerToNat n)
 449 | 
 450 | processArgs : String -> (args : List OptType) -> List String -> ActType args ->
 451 |               Either String (List CLOpt, List String)
 452 | processArgs flag [] xs f = Right (f, xs)
 453 | -- Missing required arguments
 454 | processArgs flag (opt@(Required _) :: as) [] f =
 455 |   Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
 456 | processArgs flag (opt@(RequiredNat _) :: as) [] f =
 457 |   Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
 458 | processArgs flag (opt@(RequiredLogLevel _) :: as) [] f =
 459 |   Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
 460 | processArgs flag (Optional a :: as) [] f =
 461 |   processArgs flag as [] (f Nothing)
 462 | processArgs flag (opt@(AutoNat _) :: as) [] f =
 463 |   Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
 464 | -- Happy cases
 465 | processArgs flag (RequiredNat a :: as) (x :: xs) f =
 466 |   do arg <- maybeToEither ("Expected Nat argument " ++ show x ++ " for flag " ++ flag)
 467 |                           (parseInteger x >>= checkNat)
 468 |      processArgs flag as xs (f arg)
 469 | processArgs flag (RequiredLogLevel a :: as) (x :: xs) f =
 470 |   do arg <- maybeToEither ("Expected LogLevel argument " ++ show x ++ " for flag " ++ flag)
 471 |                           (parseLogLevel x)
 472 |      processArgs flag as xs (f arg)
 473 | processArgs flag (AutoNat a :: as) ("auto" :: xs) f =
 474 |   processArgs flag as xs (f Nothing)
 475 | processArgs flag (AutoNat a :: as) (x :: xs) f =
 476 |   do arg <- maybeToEither ("Expected Nat or \"auto\" argument " ++ show x ++ " for flag " ++ flag)
 477 |                           (parseInteger x >>= checkNat)
 478 |      processArgs flag as xs (f (Just arg))
 479 | processArgs flag (Required a :: as) (x :: xs) f =
 480 |   processArgs flag as xs (f x)
 481 | processArgs flag (Optional a :: as) (x :: xs) f =
 482 |   if isPrefixOf "-" x
 483 |     then processArgs flag as (x :: xs) (f Nothing)
 484 |     else processArgs flag as xs (f $ Just x)
 485 | 
 486 | matchFlag : (d : OptDesc) -> List String ->
 487 |             Either String (Maybe (List CLOpt, List String))
 488 | matchFlag d [] = Right Nothing -- Nothing left to match
 489 | matchFlag d (x :: xs)
 490 |     = if x `elem` flags d
 491 |          then do args <- processArgs x (argdescs d) xs (action d)
 492 |                  Right (Just args)
 493 |          else Right Nothing
 494 | 
 495 | findMatch : List OptDesc -> List String ->
 496 |             Either String (List CLOpt, List String)
 497 | findMatch [] [] = Right ([], [])
 498 | findMatch [] (f :: args) = case unpack f of
 499 |   '-' :: '-' :: _ => Left "Unknown flag \{f}"
 500 |   _ => Right ([InputFile f], args)
 501 | findMatch (d :: ds) args
 502 |     = case !(matchFlag d args) of
 503 |            Nothing => findMatch ds args
 504 |            Just res => Right res
 505 | 
 506 | parseOpts : List OptDesc -> List String -> Either String (List CLOpt)
 507 | parseOpts opts [] = Right []
 508 | parseOpts opts args
 509 |    = do (cl, rest) <- findMatch opts args
 510 |         cls <- assert_total (parseOpts opts rest) -- 'rest' smaller than 'args'
 511 |         pure (cl ++ cls)
 512 | 
 513 | export
 514 | getOpts : List String -> Either String (List CLOpt)
 515 | getOpts opts = parseOpts options opts
 516 | 
 517 | export covering
 518 | getCmdOpts : IO (Either String (List CLOpt))
 519 | getCmdOpts = do (_ :: opts) <- getArgs
 520 |                     | _ => pure (Left "Invalid command line")
 521 |                 pure $ getOpts opts
 522 | 
 523 | ||| Find an opt that would have matched if only the user had prefixed it with
 524 | ||| double-dashes. It is common to see the user error of specifying a command
 525 | ||| like "idris2 repl ..." when they mean to write "idris2 --repl ..."
 526 | export
 527 | findNearMatchOpt : String -> Maybe String
 528 | findNearMatchOpt arg =
 529 |   let argWithDashes = "--\{arg}"
 530 |   in
 531 |   case (getOpts [argWithDashes]) of
 532 |        Right [(InputFile _)] => Nothing
 533 |        Right [_] => Just argWithDashes
 534 |        _ => Nothing
 535 | 
 536 | ||| Suggest an opt that would have matched if only the user had prefixed it with
 537 | ||| double-dashes. It is common to see the user error of specifying a command
 538 | ||| like "idris2 repl ..." when they mean to write "idris2 --repl ..."
 539 | export
 540 | nearMatchOptSuggestion : String -> Maybe (Doc IdrisAnn)
 541 | nearMatchOptSuggestion arg =
 542 |     findNearMatchOpt arg <&>
 543 |       \opt =>
 544 |         (reflow "Did you mean to type" <++>
 545 |           (dquotes . meta $ pretty0 opt) <+> "?")
 546 | 
 547 | ||| List of all command line option flags.
 548 | export
 549 | optionFlags : List String
 550 | optionFlags = options >>= flags
 551 |