Here's is the code I'd like reviewed:

module Main where

import Control.Monad ( when )
import System.Exit ( exitSuccess )

import Idris.AbsSyntax
import Idris.Error
import Idris.CmdOptions
import Idris.Info
import Idris.Info.Show
import Idris.Package
import Idris.Main

import Util.System ( setupBundledCC )

processShowOptions :: [Opt] -> Idris ()
processShowOptions opts = runIO $ do
  when (ShowAll `elem` opts)          $ showExitIdrisInfo
  when (ShowLoggingCats `elem` opts)  $ showExitIdrisLoggingCategories
  when (ShowIncs `elem` opts)         $ showExitIdrisFlagsInc
  when (ShowLibs `elem` opts)         $ showExitIdrisFlagsLibs
  when (ShowLibdir `elem` opts)       $ showExitIdrisLibDir
  when (ShowPkgs `elem` opts)         $ showExitIdrisInstalledPackages

check :: [Opt] -> (Opt -> Maybe a) -> ([a] -> Idris ()) -> Idris ()
check opts extractOpts action = do
  case opt extractOpts opts of
    [] -> return ()
    fs -> do action fs
             runIO exitSuccess

processClientOptions :: [Opt] -> Idris ()
processClientOptions opts = check opts getClient $ \fs -> case fs of
  (c:_) -> do
    setVerbose False
    setQuiet True
    case getPort opts of
      Just  DontListen       -> ifail "\"--client\" and \"--port none\" are incompatible"
      Just (ListenPort port) -> runIO $ runClient (Just port) c
      Nothing                -> runIO $ runClient Nothing c

processPackageOptions :: [Opt] -> Idris ()
processPackageOptions opts = do
  check opts getPkgCheck $ \fs -> runIO $ do
    mapM_ (checkPkg opts (WarnOnly `elem` opts) True) fs
  check opts getPkgClean $ \fs -> runIO $ do
    mapM_ (cleanPkg opts) fs
  check opts getPkgMkDoc $ \fs -> runIO $ do
    mapM_ (documentPkg opts) fs
  check opts getPkgTest $ \fs -> runIO $ do
    mapM_ (testPkg opts) fs
  check opts getPkg $ \fs -> runIO $ do
    mapM_ (buildPkg opts (WarnOnly `elem` opts)) fs
  check opts getPkgREPL $ \fs -> case fs of
    [f] -> replPkg opts f
    _   -> ifail "Too many packages"

-- | The main function for the Idris executable.
runIdris :: [Opt] -> Idris ()
runIdris opts = do
  runIO setupBundledCC
  processShowOptions opts    -- Show information then quit.
  processClientOptions opts  -- Be a client to a REPL server.
  processPackageOptions opts -- Work with Idris packages.
  idrisMain opts             -- Launch REPL or compile mode.

-- Main program reads command line options, parses the main program, and gets
-- on with the REPL.
main :: IO ()
main = do
  opts <- runArgParser
  runMain (runIdris opts)

I'd like to improve it. There are two main related problems.

This code uses exitSuccess for early exit. This then leads to a misleading piece of code in runIdris.

I'd prefer runIdris to look something like:

runIdris opts = do
  runIO setupBundledCC
  runIO execute (processShowOptions opts
             <|> processClientOptions opts
             <|> processPackageOptions opts
             <|> idrisMain opts)

I think I've worked out a way forward but would love to hear your thoughts.

  • \$\begingroup\$ You can do case args of "one" : args -> command1 args; "two" : args -> command2 args; _ -> usage. \$\endgroup\$
    – Gurkenglas
    Sep 16 '16 at 21:05
  • \$\begingroup\$ Unfortunately I cannot do that in the real code. I worked out that I can wrap the IO action in a Maybe and use <|>. Additionally, I can wrap the Maybe in a First and use Monoid mconcat. \$\endgroup\$ Sep 16 '16 at 22:05
  • 3
    \$\begingroup\$ It really helps to have at least a worded summary of what the code is doing before jumping straight into a code wall. Please consider adding something to ease the reading experience. \$\endgroup\$
    – Myridium
    Sep 26 '16 at 16:43
  • 1
    \$\begingroup\$ What is Opt type? \$\endgroup\$ Oct 21 '16 at 12:39

This looks fine. There is some replication in processPackageOptions, but that's manageable. Your syntactical variant isn't possible, though, since Idris isn't an instance of Alternative. type Idris = StateT IState (ExceptT Err IO) would only be an instance of Alternative if Err was an instance of Monoid, which it isn't.

You could wrap Idris in another short-circuiting monad, for example Either ExitCode (Idris a) or a transformer variant, but you have to replace all runIO with liftIdrisIO or similar. That might be too much.

But I concur, the exitSuccess in check isn't that obvious and should be made more obvious at type level.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.