diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr
new file mode 100644
index 0000000..80fa2d3
--- /dev/null
+++ b/exe/CompileMonad.idr
@@ -0,0 +1,134 @@
+module CompileMonad
+
+import Quox.Syntax as Q
+import Quox.Definition as Q
+import Quox.Untyped.Syntax as U
+import Quox.Parser
+import Quox.Untyped.Erase
+import Quox.Untyped.Scheme
+import Quox.Pretty
+import Options
+import Output
+import Error
+
+import System.File
+import Data.IORef
+import Control.Eff
+
+%default total
+
+%hide Doc.(>>=)
+%hide Core.(>>=)
+
+%hide FromParser.Error
+%hide Erase.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+
+public export
+record State where
+  constructor MkState
+  seen : IORef SeenSet
+  defs : IORef Q.Definitions
+  ns   : IORef Mods
+  suf  : IORef NameSuf
+%name CompileMonad.State state
+
+export %inline
+newState : HasIO io => io State
+newState = pure $ MkState {
+  seen = !(newIORef empty),
+  defs = !(newIORef empty),
+  ns   = !(newIORef [<]),
+  suf  = !(newIORef 0)
+}
+
+
+public export
+data CompileTag = OPTS | STATE
+
+public export
+Compile : List (Type -> Type)
+Compile =
+  [Except Error,
+   ReaderL STATE State, ReaderL OPTS Options,
+   LoadFile, IO]
+
+export covering %inline
+runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
+runCompile opts state act = do
+  fromIOErr $ runEff act $ with Union.(::)
+    [handleExcept (\e => ioLeft e),
+     handleReaderConst state,
+     handleReaderConst opts,
+     handleLoadFileIOE loadError ParseError state.seen opts.include,
+     liftIO]
+
+private %inline
+rethrowFileC : String -> Either FileError a -> Eff Compile a
+rethrowFileC f = rethrow . mapFst (WriteError f)
+
+
+export %inline
+outputStr : OpenFile -> Lazy String -> Eff Compile ()
+outputStr ONone           _   = pure ()
+outputStr (OConsole COut) str = putStr str
+outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFileC "<stderr>"
+outputStr (OFile f h)     str = fPutStr h str >>= rethrowFileC f
+
+export %inline
+outputDocs : OpenFile ->
+             ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
+             Eff Compile ()
+outputDocs file docs = do
+  opts <- askAt OPTS
+  for_ (runPretty opts (toOutFile file) docs) $ \x =>
+    outputStr file $ render (Opts opts.width) x
+
+export %inline
+outputDoc : OpenFile ->
+            ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
+outputDoc file doc = outputDocs file $ singleton <$> doc
+
+
+public export
+data StopTag = STOP
+
+public export
+CompileStop : List (Type -> Type)
+CompileStop = FailL STOP :: Compile
+
+export %inline
+withEarlyStop : Eff CompileStop () -> Eff Compile ()
+withEarlyStop = ignore . runFailAt STOP
+
+export %inline
+stopHere : Has (FailL STOP) fs => Eff fs ()
+stopHere = failAt STOP
+
+
+export %inline
+liftFromParser : Eff FromParserIO a -> Eff Compile a
+liftFromParser act =
+  runEff act $ with Union.(::)
+    [handleExcept $ \err => throw $ FromParserError err,
+     handleStateIORef !(asksAt STATE defs),
+     handleStateIORef !(asksAt STATE ns),
+     handleStateIORef !(asksAt STATE suf),
+     \g => send g]
+
+export %inline
+liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
+liftErase defs act =
+  runEff act
+    [handleExcept $ \err => throw $ EraseError err,
+     handleStateIORef !(asksAt STATE suf)]
+
+export %inline
+liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
+liftScheme act = do
+  runEff [|MkPair act (getAt MAIN)|]
+    [handleStateIORef !(newIORef empty),
+     handleStateIORef !(newIORef [])]
diff --git a/exe/Error.idr b/exe/Error.idr
new file mode 100644
index 0000000..03d716c
--- /dev/null
+++ b/exe/Error.idr
@@ -0,0 +1,49 @@
+module Error
+
+import Quox.Pretty
+import Quox.Parser
+import Quox.Untyped.Erase
+import Quox.Untyped.Scheme
+import Options
+import Output
+
+import System.File
+
+
+public export
+data Error =
+  ParseError String Parser.Error
+| FromParserError FromParser.Error
+| EraseError Erase.Error
+| WriteError FilePath FileError
+| NoMain
+| MultipleMains (List Scheme.Id)
+
+%hide FromParser.Error
+%hide Erase.Error
+%hide Lexer.Error
+%hide Parser.Error
+
+
+export
+loadError : Loc -> FilePath -> FileError -> Error
+loadError loc file err = FromParserError $ LoadError loc file err
+
+export
+prettyError : {opts : LayoutOpts} -> Error -> Eff Pretty (Doc opts)
+prettyError (ParseError file e) = prettyParseError file e
+prettyError (FromParserError e) = FromParser.prettyError True e
+prettyError (EraseError      e) = Erase.prettyError True e
+prettyError NoMain              = pure "no #[main] function given"
+prettyError (MultipleMains xs)  =
+  pure $ sep ["multiple #[main] functions given:",
+              separateLoose "," !(traverse prettyId xs)]
+prettyError (WriteError file e) = pure $
+  hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
+
+export
+dieError : Options -> Error -> IO a
+dieError opts e =
+  die (Opts opts.width) $
+  runPretty ({outFile := Console} opts) Console $
+  prettyError e
diff --git a/exe/Main.idr b/exe/Main.idr
index 9385eeb..192ce42 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -8,6 +8,9 @@ import Quox.Untyped.Erase
 import Quox.Untyped.Scheme
 import Quox.Pretty
 import Options
+import Output
+import Error
+import CompileMonad
 
 import System
 import System.File
@@ -19,227 +22,27 @@ import Control.Eff
 %hide Doc.(>>=)
 %hide Core.(>>=)
 
-
-private
-die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
-die opts err = do
-  ignore $ fPutStr stderr $ render opts err
-  exitFailure
-
-private
-hlFor : HLType -> OutFile -> HL -> Highlight
-hlFor Guess Console = highlightSGR
-hlFor Guess _       = noHighlight
-hlFor NoHL  _       = noHighlight
-hlFor Term  _       = highlightSGR
-hlFor Html  _       = highlightHtml
-
-private
-runPretty : Options -> OutFile -> Eff Pretty a -> a
-runPretty opts file act =
-  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
-
-private
-record State where
-  constructor MkState
-  seen : IORef SeenSet
-  defs : IORef Q.Definitions
-  ns   : IORef Mods
-  suf  : IORef NameSuf
-%name Main.State state
-
-private
-newState : HasIO io => io State
-newState = pure $ MkState {
-  seen = !(newIORef empty),
-  defs = !(newIORef empty),
-  ns   = !(newIORef [<]),
-  suf  = !(newIORef 0)
-}
-
-private
-data Error =
-  ParseError String Parser.Error
-| FromParserError FromParser.Error
-| EraseError Erase.Error
-| WriteError FilePath FileError
-| NoMain
-| MultipleMains (List Id)
 %hide FromParser.Error
 %hide Erase.Error
 %hide Lexer.Error
 %hide Parser.Error
 
 
-private
-loadError : Loc -> FilePath -> FileError -> Error
-loadError loc file err = FromParserError $ LoadError loc file err
-
-private
-prettyError : {opts : LayoutOpts} -> Error -> Eff Pretty (Doc opts)
-prettyError (ParseError file e) = prettyParseError file e
-prettyError (FromParserError e) = FromParser.prettyError True e
-prettyError (EraseError      e) = Erase.prettyError True e
-prettyError NoMain              = pure "no #[main] function given"
-prettyError (MultipleMains xs)  =
-  pure $ sep ["multiple #[main] functions given:",
-              separateLoose "," !(traverse prettyId xs)]
-prettyError (WriteError file e) = pure $
-  hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
-
-private
-dieError : Options -> Error -> IO a
-dieError opts e =
-  die (Opts opts.width) $
-  runPretty ({outFile := Console} opts) Console $
-  prettyError e
-
-private
-data CompileTag = OPTS | STATE
-
-private
-Compile : List (Type -> Type)
-Compile =
-  [Except Error,
-   ReaderL STATE State, ReaderL OPTS Options,
-   LoadFile, IO]
-
-private covering
-runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
-runCompile opts state act =
-  fromIOErr $ runEff act $ with Union.(::)
-    [handleExcept (\e => ioLeft e),
-     handleReaderConst state,
-     handleReaderConst opts,
-     handleLoadFileIOE loadError ParseError state.seen opts.include,
-     liftIO]
-
-
-private
-data StopTag = STOP
-
-private
-CompileStop : List (Type -> Type)
-CompileStop = FailL STOP :: Compile
-
-private
-withEarlyStop : Has (FailL STOP) fs => Eff fs () -> Eff (fs - FailL STOP) ()
-withEarlyStop = ignore . runFailAt STOP
-
-private
-stopHere : Has (FailL STOP) fs => Eff fs ()
-stopHere = failAt STOP
-
-
-private
-data ConsoleChannel = COut | CErr
-
-private
-data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
-
-private
-rethrowFile : String -> Either FileError a -> Eff Compile a
-rethrowFile f = rethrow . mapFst (WriteError f)
-
-private
-toOutFile : OpenFile -> OutFile
-toOutFile (OConsole _) = Console
-toOutFile (OFile f _)  = File f
-toOutFile ONone        = NoOut
-
-private
-withFileC : String -> (OpenFile -> Eff Compile a) -> Eff Compile a
-withFileC f act =
-  withFile f WriteTruncate pure (Prelude.map Right . act . OFile f) >>=
-  rethrowFile f
-
-private
-withOutFile : ConsoleChannel -> OutFile ->
-              (OpenFile -> Eff Compile a) -> Eff Compile a
-withOutFile _  (File f) act = withFileC f act
-withOutFile ch Console  act = act $ OConsole ch
-withOutFile _  NoOut    act = act ONone
-
-private
-outputStr : OpenFile -> Lazy String -> Eff Compile ()
-outputStr ONone           _   = pure ()
-outputStr (OConsole COut) str = putStr str
-outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFile "<stderr>"
-outputStr (OFile f h)     str = fPutStr h str >>= rethrowFile f
-
-private
-outputDocs : OpenFile ->
-             ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
-             Eff Compile ()
-outputDocs file docs = do
-  opts <- askAt OPTS
-  for_ (runPretty opts (toOutFile file) docs) $ \x =>
-    outputStr file $ render (Opts opts.width) x
-
-private
-outputDoc : OpenFile ->
-            ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
-outputDoc file doc = outputDocs file $ singleton <$> doc
-
-private
-liftFromParser : Eff FromParserIO a -> Eff Compile a
-liftFromParser act =
-  runEff act $ with Union.(::)
-    [handleExcept $ \err => throw $ FromParserError err,
-     handleStateIORef !(asksAt STATE defs),
-     handleStateIORef !(asksAt STATE ns),
-     handleStateIORef !(asksAt STATE suf),
-     \g => send g]
-
-private
-liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
-liftErase defs act =
-  runEff act
-    [handleExcept $ \err => throw $ EraseError err,
-     handleStateIORef !(asksAt STATE suf)]
-
-private
-liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
-liftScheme act = do
-  runEff [|MkPair act (getAt MAIN)|]
-    [handleStateIORef !(newIORef empty),
-     handleStateIORef !(newIORef [])]
-
-
 private
 Step : Type -> Type -> Type
-Step i o = OpenFile -> i -> Eff Compile o
-
--- private
--- processFile : String -> Eff Compile ()
--- processFile file = withEarlyStop $ do
---   Just ast <- loadFile noLoc file
---     | Nothing => pure ()
---   -- putErrLn "checking \{file}"
---   when (!(asksAt OPTS until) == Just Parse) $ do
---     lift $ outputStr $ show ast
---     stopHere
---   defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
---   outputDocStopIf Check $
---     traverse (uncurry Q.prettyDef) defList
---   let defs = SortedMap.fromList defList
---   erased <- liftErase defs $
---     traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
---   outputDocStopIf Erase $
---     traverse (uncurry U.prettyDef) erased
---   (scheme, mains) <- liftScheme $ map catMaybes $
---     traverse (uncurry defToScheme) erased
---   outputDocStopIf Scheme $
---     intersperse empty <$> traverse prettySexp scheme
+Step a b = OpenFile -> a -> Eff Compile b
 
 private
 step : {default CErr console : ConsoleChannel} ->
-       Phase -> OutFile -> Step i o -> i -> Eff CompileStop o
+       Phase -> OutFile -> Step a b -> a -> Eff CompileStop b
 step phase file act x = do
   opts <- askAt OPTS
-  res <- lift $ withOutFile console file $ \h => act h x
+  res  <- withOutFile console file fromError $ \h => lift $ act h x
   when (opts.until == Just phase) stopHere
   pure res
+where
+  fromError : String -> FileError -> Eff CompileStop c
+  fromError file err = throw $ WriteError file err
 
 
 private covering
@@ -268,25 +71,23 @@ erase h defList =
 where defs = SortedMap.fromList defList
 
 private covering
-scheme : Step (List U.NDefinition) (List Sexp, Id)
+scheme : Step (List U.NDefinition) (List Sexp, List Id)
 scheme h defs = do
   sexps' <- for defs $ \(x, d) => do
     (msexp, mains) <- liftScheme $ defToScheme x d
-    outputDoc h $ maybe (sayErased x) prettySexp msexp
+    outputDoc h $ case msexp of
+      Just s  => prettySexp s
+      Nothing => pure $ hsep [";;", prettyName x, "erased"]
     pure (msexp, mains)
-  bitraverse (pure . catMaybes) (oneMain . concat) $ unzip sexps'
-where
-  sayErased : {opts : LayoutOpts} -> Name -> Eff Pretty (Doc opts)
-  sayErased x = pure $ hsep [";;", prettyName x, "erased"]
-
-  oneMain : List Id -> Eff Compile Id
-  oneMain [m] = pure m
-  oneMain []  = throw NoMain
-  oneMain ms  = throw $ MultipleMains ms
+  pure $ bimap catMaybes concat $ unzip sexps'
 
 private covering
-output : Step (List Sexp, Id) ()
-output h (sexps, main) =
+output : Step (List Sexp, List Id) ()
+output h (sexps, mains) = do
+  main <- case mains of
+    [m] => pure m
+    []  => throw NoMain
+    _   => throw $ MultipleMains mains
   lift $ outputDocs h $ do
     res    <- traverse prettySexp sexps
     runner <- makeRunMain main
diff --git a/exe/Options.idr b/exe/Options.idr
index 1c444e2..b92b668 100644
--- a/exe/Options.idr
+++ b/exe/Options.idr
@@ -1,6 +1,8 @@
 module Options
 
 import Quox.Pretty
+import Data.DPair
+import Data.SortedMap
 import System
 import System.Console.GetOpt
 import System.File
@@ -42,13 +44,13 @@ record Dump where
 public export
 record Options where
   constructor MkOpts
-  hlType  : HLType
+  include : List String
   dump    : Dump
   outFile : OutFile
   until   : Maybe Phase
+  hlType  : HLType
   flavor  : Pretty.Flavor
   width   : Nat
-  include : List String
 %name Options opts
 %runElab derive "Options" [Show]
 
@@ -61,13 +63,13 @@ defaultWidth = do
 export
 defaultOpts : IO Options
 defaultOpts = pure $ MkOpts {
-  hlType  = Guess,
+  include = ["."],
   dump    = MkDump NoOut NoOut NoOut NoOut,
   outFile = Console,
   until   = Nothing,
+  hlType  = Guess,
   flavor  = Unicode,
-  width   = !defaultWidth,
-  include = ["."]
+  width   = !defaultWidth
 }
 
 private
@@ -118,11 +120,12 @@ toHLType str = case toLower str of
   "html" => Ok {hlType := Html}
   _      => Err "unknown highlighting type \{show str}\ntypes: term, html, none"
 
-||| like ghc, -i '' clears the search path; -i a:b:c adds a,b,c to the end
+||| like ghc, `-i ""` clears the search path;
+||| `-i a:b:c` adds `a`, `b`, `c` to the end
 private
 dirListFlag : String -> List String -> List String
-dirListFlag arg val =
-  if null arg then [] else val ++ toList (split (== ':') arg)
+dirListFlag ""   val = []
+dirListFlag dirs val = val ++ toList (split (== ':') dirs)
 
 private
 commonOptDescrs' : List (OptDescr OptAction)
@@ -148,13 +151,17 @@ extraOptDescrs = [
   MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
     "select highlighting type",
 
-  MkOpt [] ["dparse"] (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
+  MkOpt [] ["dump-parse"]
+    (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
     "dump AST",
-  MkOpt [] ["dcheck"] (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
+  MkOpt [] ["dump-check"]
+    (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
     "dump typechecker output",
-  MkOpt [] ["derase"] (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
+  MkOpt [] ["dump-erase"]
+    (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
     "dump erasure output",
-  MkOpt [] ["dscheme"] (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
+  MkOpt [] ["dump-scheme"]
+    (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
     "dump scheme output (without prelude)"
 ]
 
diff --git a/exe/Output.idr b/exe/Output.idr
new file mode 100644
index 0000000..77eed61
--- /dev/null
+++ b/exe/Output.idr
@@ -0,0 +1,59 @@
+module Output
+
+import Quox.Pretty
+import Options
+
+import System.File
+import System
+
+public export
+data ConsoleChannel = COut | CErr
+
+export
+consoleHandle : ConsoleChannel -> File
+consoleHandle COut = stdout
+consoleHandle CErr = stderr
+
+public export
+data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
+
+export
+toOutFile : OpenFile -> OutFile
+toOutFile (OConsole _) = Console
+toOutFile (OFile f _)  = File f
+toOutFile ONone        = NoOut
+
+export
+withFile : HasIO m => String -> (String -> FileError -> m a) ->
+           (OpenFile -> m a) -> m a
+withFile f catch act = Prelude.do
+  res <- withFile f WriteTruncate pure (Prelude.map Right . act . OFile f)
+  either (catch f) pure res
+
+export
+withOutFile : HasIO m => ConsoleChannel -> OutFile ->
+              (String -> FileError -> m a) -> (OpenFile -> m a) -> m a
+withOutFile _  (File f) catch act = withFile f catch act
+withOutFile ch Console  catch act = act $ OConsole ch
+withOutFile _  NoOut    catch act = act ONone
+
+
+
+private
+hlFor : HLType -> OutFile -> HL -> Highlight
+hlFor Guess Console = highlightSGR
+hlFor Guess _       = noHighlight
+hlFor NoHL  _       = noHighlight
+hlFor Term  _       = highlightSGR
+hlFor Html  _       = highlightHtml
+
+export
+runPretty : Options -> OutFile -> Eff Pretty a -> a
+runPretty opts file act =
+  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
+
+export
+die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
+die opts err = do
+  ignore $ fPutStr stderr $ render opts err
+  exitFailure