refactor Main a whole lot

exe/Main.idr

@@ -1,22 +1,21 @@
 module Main
 
 import Quox.Syntax as Q
-import Quox.Parser
 import Quox.Definition as Q
-import Quox.Pretty
 import Quox.Untyped.Syntax as U
+import Quox.Parser
 import Quox.Untyped.Erase
 import Quox.Untyped.Scheme
+import Quox.Pretty
 import Options
 
-import Data.IORef
-import Data.SortedSet
-import Text.Show.PrettyVal
-import Text.Show.Pretty
 import System
 import System.File
+import Data.IORef
 import Control.Eff
 
+%default total
+
 %hide Doc.(>>=)
 %hide Core.(>>=)
 
@@ -36,13 +35,9 @@ hlFor Term  _       = highlightSGR
 hlFor Html  _       = highlightHtml
 
 private
-runPretty : Options -> Eff Pretty a -> a
+runPretty : Options -> OutFile -> Eff Pretty a -> a
-runPretty opts act =
+runPretty opts file act =
-  runPrettyWith Outer opts.flavor (hlFor opts.hlType opts.outFile) 2 act
+  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
-
-private
-putErrLn : HasIO io => String -> io ()
-putErrLn = ignore . fPutStrLn stderr
 
 private
 record State where
@@ -92,6 +87,13 @@ prettyError (MultipleMains 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
 
@@ -102,7 +104,7 @@ Compile =
    ReaderL STATE State, ReaderL OPTS Options,
    LoadFile, IO]
 
-private
+private covering
 runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
 runCompile opts state act =
   fromIOErr $ runEff act $ with Union.(::)
@@ -130,38 +132,57 @@ stopHere = failAt STOP
 
 
 private
-FlexDoc : Type
+data ConsoleChannel = COut | CErr
-FlexDoc = {opts : LayoutOpts} -> Doc opts
-
 
 private
-outputStr : Lazy String -> Eff Compile ()
+data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
-outputStr str =
-  case !(asksAt OPTS outFile) of
-    NoOut   => pure ()
-    Console => putStr str
-    File f  => do
-      res <- withFile f WriteTruncate pure $ \h => fPutStr h str
-      rethrow $ mapFst (WriteError f) res
 
 private
-outputDocs : (opts : Options) ->
+rethrowFile : String -> Either FileError a -> Eff Compile a
-             ({opts : LayoutOpts} -> List (Doc opts)) -> Eff Compile ()
+rethrowFile f = rethrow . mapFst (WriteError f)
-outputDocs opts doc =
-  outputStr $ concat $ map (render (Opts opts.width)) doc
 
 private
-outputDocStopIf : Phase ->
+toOutFile : OpenFile -> OutFile
-                  ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
+toOutFile (OConsole _) = Console
-                  Eff CompileStop ()
+toOutFile (OFile f _)  = File f
-outputDocStopIf p docs = do
+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
-  when (opts.until == Just p) $ Prelude.do
+  for_ (runPretty opts (toOutFile file) docs) $ \x =>
-    lift $ outputDocs !(askAt OPTS) (runPretty opts docs)
+    outputStr file $ render (Opts opts.width) x
-    stopHere
 
 private
-liftFromParser : Eff FromParserIO a -> Eff CompileStop a
+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,
@@ -171,14 +192,14 @@ liftFromParser act =
      \g => send g]
 
 private
-liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
+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 CompileStop (a, List Id)
+liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
 liftScheme act = do
   runEff [|MkPair act (getAt MAIN)|]
     [handleStateIORef !(newIORef empty),
@@ -186,49 +207,110 @@ liftScheme act = do
 
 
 private
-oneMain : Has (Except Error) fs => List Id -> Eff fs Id
+Step : Type -> Type -> Type
-oneMain []    = throw NoMain
+Step i o = OpenFile -> i -> Eff Compile o
-oneMain [x]   = pure x
-oneMain mains = throw $ MultipleMains mains
 
+-- 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
 
 private
-processFile : String -> Eff Compile ()
+step : {default CErr console : ConsoleChannel} ->
-processFile file = withEarlyStop $ do
+       Phase -> OutFile -> Step i o -> i -> Eff CompileStop o
-  Just ast <- loadFile noLoc file
+step phase file act x = do
-    | 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
   opts <- askAt OPTS
-  main <- oneMain mains
+  res <- lift $ withOutFile console file $ \h => act h x
-  lift $ outputDocs opts $ intersperse empty $ runPretty opts $ do
+  when (opts.until == Just phase) stopHere
-    res    <- traverse prettySexp scheme
+  pure res
+
+
+private covering
+parse : Step String PFile
+parse h file = do
+  Just ast <- loadFile noLoc file
+    | Nothing => pure []
+  outputStr h $ show ast
+  pure ast
+
+private covering
+check : Step PFile (List Q.NDefinition)
+check h decls =
+  map concat $ for decls $ \decl => do
+    defs <- liftFromParser $ fromPTopLevel decl
+    outputDocs h $ traverse (\(x, d) => prettyDef x d) defs
+    pure defs
+
+private covering
+erase : Step (List Q.NDefinition) (List U.NDefinition)
+erase h defList =
+  for defList $ \(x, def) => do
+    def <- liftErase defs $ eraseDef defs x def
+    outputDoc h $ U.prettyDef x def
+    pure (x, def)
+where defs = SortedMap.fromList defList
+
+private covering
+scheme : Step (List U.NDefinition) (List Sexp, Id)
+scheme h defs = do
+  sexps' <- for defs $ \(x, d) => do
+    (msexp, mains) <- liftScheme $ defToScheme x d
+    outputDoc h $ maybe (sayErased x) prettySexp msexp
+    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
+
+private covering
+output : Step (List Sexp, Id) ()
+output h (sexps, main) =
+  lift $ outputDocs h $ do
+    res    <- traverse prettySexp sexps
     runner <- makeRunMain main
     pure $ text Scheme.prelude :: res ++ [runner]
 
-export
+private covering
+processFile : String -> Eff Compile ()
+processFile file = withEarlyStop $ pipeline !(askAt OPTS) file where
+  pipeline : Options -> String -> Eff CompileStop ()
+  pipeline opts =
+    step Parse  opts.dump.parse  Main.parse  >=>
+    step Check  opts.dump.check  Main.check  >=>
+    step Erase  opts.dump.erase  Main.erase  >=>
+    step Scheme opts.dump.scheme Main.scheme >=>
+    step End    opts.outFile     Main.output {console = COut}
+
+
+export covering
 main : IO ()
 main = do
   (_, opts, files) <- options
   case !(runCompile opts !newState $ traverse_ processFile files) of
     Right () => pure ()
-    Left  e  => die (Opts opts.width) $
+    Left  e  => dieError opts e
-                runPretty ({outFile := Console} opts) $
-                prettyError e
 
 
 -----------------------------------
@@ -244,6 +326,13 @@ text _ =
    #" /_/"#,
    ""]
 
+--   ["",
+--    #" __ _ _  _ _____ __"#,
+--    #"/ _` | || / _ \ \ /"#,
+--    #"\__, |\_,_\___/_\_\"#,
+--    #"   |_|"#,
+--    ""]
+
 private
 qtuwu : PrettyOpts -> List String
 qtuwu opts =

exe/Options.idr

@@ -16,27 +16,35 @@ data OutFile = File String | Console | NoOut
 %runElab derive "OutFile" [Eq, Ord, Show]
 
 public export
-data Phase = Parse | Check | Erase | Scheme
+data Phase = Parse | Check | Erase | Scheme | End
 %name Phase p
 %runElab derive "Phase" [Eq, Ord, Show]
 
-||| a list of all `Phase`s
+||| a list of all intermediate `Phase`s (excluding `End`)
 public export %inline
 allPhases : List Phase
 allPhases = %runElab do
   -- as a script so it stays up to date
   cs <- getCons $ fst !(lookupName "Phase")
-  traverse (check . var) cs
+  traverse (check . var) $ fromMaybe [] $ init' cs
 
-||| "guess" is Term for a terminal and NoHL for a file
+||| `Guess` is `Term` for a terminal and `NoHL` for a file
 public export
 data HLType = Guess | NoHL | Term | Html
 %runElab derive "HLType" [Eq, Ord, Show]
 
+public export
+record Dump where
+  constructor MkDump
+  parse, check, erase, scheme : OutFile
+%name Dump dump
+%runElab derive "Dump" [Show]
+
 public export
 record Options where
   constructor MkOpts
   hlType  : HLType
+  dump    : Dump
   outFile : OutFile
   until   : Maybe Phase
   flavor  : Pretty.Flavor
@@ -55,6 +63,7 @@ export
 defaultOpts : IO Options
 defaultOpts = pure $ MkOpts {
   hlType  = Guess,
+  dump    = MkDump NoOut NoOut NoOut NoOut,
   outFile = Console,
   until   = Nothing,
   flavor  = Unicode,
@@ -70,19 +79,31 @@ data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
 %name OptAction act
 
 private
-toOutFile : String -> OptAction
+toOutFile : String -> OutFile
-toOutFile ""  = Ok {outFile := NoOut}
+toOutFile ""  = NoOut
-toOutFile "-" = Ok {outFile := Console}
+toOutFile "-" = Console
-toOutFile f   = Ok {outFile := File f}
+toOutFile f   = File f
 
 private
 toPhase : String -> OptAction
 toPhase str =
   let lstr = toLower str in
   case find (\p => toLower (show p) == lstr) allPhases of
-    Just p  => Ok {until := Just p}
+    Just p  => Ok $ setPhase p
     Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
-where phaseNames = joinBy ", " $ map (toLower . show) allPhases
+where
+  phaseNames = joinBy ", " $ map (toLower . show) allPhases
+
+  defConsole : OutFile -> OutFile
+  defConsole NoOut = Console
+  defConsole f     = f
+
+  setPhase : Phase -> Options -> Options
+  setPhase Parse  = {until := Just Parse,  dump.parse  $= defConsole}
+  setPhase Check  = {until := Just Check,  dump.check  $= defConsole}
+  setPhase Erase  = {until := Just Erase,  dump.erase  $= defConsole}
+  setPhase Scheme = {until := Just Scheme, dump.scheme $= defConsole}
+  setPhase End    = id
 
 private
 toWidth : String -> OptAction
@@ -96,17 +117,24 @@ toHLType str = case toLower str of
   "none" => Ok {hlType := NoHL}
   "term" => Ok {hlType := Term}
   "html" => Ok {hlType := Html}
-  _      => Err "unknown highlighting type \{str}\ntypes: term, html, none"
+  _      => 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
+private
+dirListFlag : String -> List String -> List String
+dirListFlag arg val =
+  if null arg then [] else val ++ toList (split (== ':') arg)
 
 private
 commonOptDescrs' : List (OptDescr OptAction)
 commonOptDescrs' = [
-  MkOpt ['i'] ["include"] (ReqArg (\i => Ok {include $= (i ::)}) "<dir>")
+  MkOpt ['i'] ["include"]
-    "add a directory to look for source files",
+    (ReqArg (\is => Ok {include $= dirListFlag is}) "<dir>:<dir>...")
-  MkOpt ['o'] ["output"] (ReqArg toOutFile "<file>")
+    "add directories to look for source files",
+  MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "<file>")
     "output file (\"-\" for stdout, \"\" for no output)",
   MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
-    "phase to stop at (by default go as far as exists)"
+    "stop after the given phase"
 ]
 
 private
@@ -119,7 +147,16 @@ extraOptDescrs = [
   MkOpt [] ["width"] (ReqArg toWidth "<width>")
     "max output width (defaults to terminal width)",
   MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
-    "select highlighting type"
+    "select highlighting type",
+
+  MkOpt [] ["dparse"] (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
+    "dump AST",
+  MkOpt [] ["dcheck"] (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
+    "dump typechecker output",
+  MkOpt [] ["derase"] (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
+    "dump erasure output",
+  MkOpt [] ["dscheme"] (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
+    "dump scheme output (without prelude)"
 ]
 
 private
@@ -152,10 +189,6 @@ applyAction opts (ShowHelp All)    = usage allOptDescrs
 applyAction opts (Err err)         = die err
 applyAction opts (Ok f)            = pure $ f opts
 
-private
-finalise : Options -> Options
-finalise = {include $= reverse}
-
 export
 options : IO (String, Options, List String)
 options = do
@@ -167,4 +200,4 @@ options = do
   unless (null res.unrecognized) $
     die "unrecognised options: \{joinBy ", " res.unrecognized}"
   opts <- foldlM applyAction !defaultOpts res.options
-  pure (app, finalise opts, res.nonOptions)
+  pure (app, opts, res.nonOptions)

lib/Quox/Untyped/Scheme.idr

@@ -70,7 +70,7 @@ public export
 data Id = I String Nat
 %runElab derive "Id" [Eq, Ord]
 
-private
+export
 prettyId' : {opts : LayoutOpts} -> Id -> Doc opts
 prettyId' (I str 0) = text $ escId str
 prettyId' (I str k) = text $ escId "\{str}:\{show k}"