quox/exe/Main.idr

242 lines
5.8 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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.Untyped.Erase
import Options
import Data.IORef
import Data.SortedSet
import Text.Show.PrettyVal
import Text.Show.Pretty
import System
import System.File
import Control.Eff
%hide Doc.(>>=)
%hide Core.(>>=)
parameters {auto _ : HasIO io} (width : Nat)
private
putDoc : Doc (Opts width) -> io ()
putDoc = putStr . render _
private
fPutDoc : File -> Doc (Opts width) -> io (Either FileError ())
fPutDoc h = fPutStr h . render _
private
putDocErr : Doc (Opts width) -> io ()
putDocErr = ignore . fPutDoc stderr
private
die : Doc (Opts width) -> io a
die err = do putDocErr err; exitFailure
private
runPretty : Options -> Eff Pretty a -> a
runPretty opts act =
let doColor = opts.color && opts.outFile == Stdout
hl = if doColor then highlightSGR else noHighlight
in
runPrettyWith Outer opts.flavor hl 2 act
private
putErrLn : HasIO io => String -> io ()
putErrLn = ignore . fPutStrLn stderr
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
%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
data CompileTag = OPTS | STATE
private
Compile : List (Type -> Type)
Compile =
[Except Error,
ReaderL STATE State, ReaderL OPTS Options,
LoadFile, IO]
private
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
FlexDoc : Type
FlexDoc = {opts : LayoutOpts} -> Doc opts
private
outputDoc : FlexDoc -> Eff Compile ()
outputDoc doc =
case !(asksAt OPTS outFile) of
None => pure ()
Stdout => putDoc !(asksAt OPTS width) doc
File f => do
res <- withFile f WriteTruncate pure $ \h =>
fPutDoc !(asksAt OPTS width) h doc
rethrow $ mapFst (WriteError f) res
private
outputDocStopIf : Phase -> FlexDoc -> Eff CompileStop ()
outputDocStopIf p doc =
when (!(asksAt OPTS until) == Just p) $ do
lift (outputDoc doc)
stopHere
private
liftFromParser : Eff FromParserIO a -> Eff CompileStop 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 CompileStop a
liftErase defs act =
runEff act
[\case Err e => throw $ EraseError e,
\case Ask => pure defs,
handleStateIORef !(asksAt STATE suf)]
private
processFile : String -> Eff Compile ()
processFile file = withEarlyStop $ do
Just ast <- loadFile noLoc file
| Nothing => pure ()
putErrLn "checking \{file}"
outputDocStopIf Parse $ dumpDoc ast
defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
outputDocStopIf Check $ runPretty !(askAt OPTS) $
vsep <$> traverse (uncurry Q.prettyDef) defList
let defs = SortedMap.fromList defList
erased <- liftErase defs $
traverse (\(x, d) => (x,) <$> eraseDef x d) defList
outputDocStopIf Erase $ runPretty !(askAt OPTS) $
vsep . catMaybes <$> traverse (uncurry U.prettyDef) erased
die "that's all folks"
private
dieError : HasIO io => Options -> Error -> io a
dieError opts e = do
die opts.width $ runPretty opts $ case e of
ParseError file e => prettyParseError file e
FromParserError e => FromParser.prettyError True e
EraseError e => Erase.prettyError True e
WriteError file e => pure $
hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
export
main : IO ()
main = do
(_, opts, files) <- options
case !(runCompile opts !newState $ traverse_ processFile files) of
Right () => pure ()
Left e => dieError opts e
-----------------------------------
{-
private
text : PrettyOpts -> List String
text _ =
["",
#" ___ ___ _____ __ __"#,
#"/ _ `/ // / _ \\ \ /"#,
#"\_, /\_,_/\___/_\_\"#,
#" /_/"#,
""]
private
qtuwu : PrettyOpts -> List String
qtuwu opts =
if opts.unicode then
[#" ___,-´⎠ "#,
#"(·`──´ ◡ -´⎠"#,
#" \/\/──´⎞/`──´ "#,
#" ⎜⎟───,-₎ ⎞ "#,
#" ⎝⎠ (‾‾) ⎟ "#,
#" (‾‾‾) ⎟ "#]
else
[#" ___,-´/ "#,
#"(.`--´ u -´/"#,
#" \/\/--´|/`--´ "#,
#" ||---,-, \ "#,
#" `´ (--) | "#,
#" (---) | "#]
private
join1 : PrettyOpts -> String -> String -> String
join1 opts l r =
if opts.color then
" " <+> show (colored Green l) <+> " " <+> show (colored Magenta r)
else
" " <+> l <+> " " <+> r
export
banner : PrettyOpts -> String
banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
-}