quox/exe/Main.idr

277 lines
6.9 KiB
Idris
Raw Normal View History

2022-04-27 14:04:03 -04:00
module Main
2021-07-07 07:11:39 -04:00
2023-10-20 11:42:01 -04:00
import Quox.Syntax as Q
2023-03-31 13:31:29 -04:00
import Quox.Parser
2023-10-20 11:42:01 -04:00
import Quox.Definition as Q
2023-03-31 13:31:29 -04:00
import Quox.Pretty
2023-10-20 11:42:01 -04:00
import Quox.Untyped.Syntax as U
import Quox.Untyped.Erase
2023-10-24 17:52:19 -04:00
import Quox.Untyped.Scheme
2023-10-20 11:42:01 -04:00
import Options
2021-07-20 16:05:19 -04:00
2023-03-31 13:31:29 -04:00
import Data.IORef
import Data.SortedSet
2023-10-20 11:42:01 -04:00
import Text.Show.PrettyVal
import Text.Show.Pretty
import System
import System.File
2023-03-31 13:31:29 -04:00
import Control.Eff
2021-07-20 16:05:19 -04:00
2023-10-20 11:42:01 -04:00
%hide Doc.(>>=)
%hide Core.(>>=)
2023-10-24 17:52:19 -04:00
private
die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
die opts err = do
ignore $ fPutStr stderr $ render opts err
exitFailure
2023-10-20 11:42:01 -04:00
2023-11-05 09:47:52 -05:00
private
hlFor : HLType -> OutFile -> HL -> Highlight
hlFor Guess Console = highlightSGR
hlFor Guess _ = noHighlight
hlFor NoHL _ = noHighlight
hlFor Term _ = highlightSGR
hlFor Html _ = highlightHtml
2023-10-20 11:42:01 -04:00
private
runPretty : Options -> Eff Pretty a -> a
runPretty opts act =
2023-11-05 09:47:52 -05:00
runPrettyWith Outer opts.flavor (hlFor opts.hlType opts.outFile) 2 act
2023-10-20 11:42:01 -04:00
private
putErrLn : HasIO io => String -> io ()
putErrLn = ignore . fPutStrLn stderr
2023-05-14 13:58:46 -04:00
private
2023-10-20 11:42:01 -04:00
record State where
constructor MkState
seen : IORef SeenSet
defs : IORef Q.Definitions
ns : IORef Mods
suf : IORef NameSuf
%name Main.State state
2023-05-14 13:58:46 -04:00
private
2023-10-20 11:42:01 -04:00
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)
2023-10-20 11:42:01 -04:00
%hide FromParser.Error
%hide Erase.Error
%hide Lexer.Error
%hide Parser.Error
2023-10-20 11:42:01 -04:00
private
loadError : Loc -> FilePath -> FileError -> Error
loadError loc file err = FromParserError $ LoadError loc file err
2023-10-24 17:52:19 -04:00
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)]
2023-10-24 17:52:19 -04:00
prettyError (WriteError file e) = pure $
hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
2023-10-20 11:42:01 -04:00
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]
2023-05-14 13:58:46 -04:00
private
2023-10-20 11:42:01 -04:00
data StopTag = STOP
2023-05-14 13:58:46 -04:00
private
2023-10-20 11:42:01 -04:00
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
2023-10-24 17:52:19 -04:00
outputStr : Lazy String -> Eff Compile ()
outputStr str =
2023-10-20 11:42:01 -04:00
case !(asksAt OPTS outFile) of
2023-11-05 09:47:52 -05:00
NoOut => pure ()
Console => putStr str
File f => do
2023-10-24 17:52:19 -04:00
res <- withFile f WriteTruncate pure $ \h => fPutStr h str
2023-10-20 11:42:01 -04:00
rethrow $ mapFst (WriteError f) res
private
outputDocs : (opts : Options) ->
({opts : LayoutOpts} -> List (Doc opts)) -> Eff Compile ()
outputDocs opts doc =
outputStr $ concat $ map (render (Opts opts.width)) doc
2023-10-24 17:52:19 -04:00
private
outputDocStopIf : Phase ->
({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
Eff CompileStop ()
outputDocStopIf p docs = do
opts <- askAt OPTS
when (opts.until == Just p) $ Prelude.do
lift $ outputDocs !(askAt OPTS) (runPretty opts docs)
2023-10-20 11:42:01 -04:00
stopHere
private
liftFromParser : Eff FromParserIO a -> Eff CompileStop a
liftFromParser act =
runEff act $ with Union.(::)
[handleExcept $ \err => throw $ FromParserError err,
2023-10-20 11:42:01 -04:00
handleStateIORef !(asksAt STATE defs),
handleStateIORef !(asksAt STATE ns),
handleStateIORef !(asksAt STATE suf),
\g => send g]
2023-10-20 11:42:01 -04:00
private
liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
liftErase defs act =
runEff act
[handleExcept $ \err => throw $ EraseError err,
2023-10-20 11:42:01 -04:00
handleStateIORef !(asksAt STATE suf)]
2023-10-24 17:52:19 -04:00
private
liftScheme : Eff Scheme a -> Eff CompileStop (a, List Id)
liftScheme act = do
runEff [|MkPair act (getAt MAIN)|]
[handleStateIORef !(newIORef empty),
handleStateIORef !(newIORef [])]
2023-10-24 17:52:19 -04:00
private
oneMain : Has (Except Error) fs => List Id -> Eff fs Id
oneMain [] = throw NoMain
oneMain [x] = pure x
oneMain mains = throw $ MultipleMains mains
2023-10-20 11:42:01 -04:00
2023-11-05 09:47:52 -05:00
2023-10-20 11:42:01 -04:00
private
processFile : String -> Eff Compile ()
processFile file = withEarlyStop $ do
Just ast <- loadFile noLoc file
| Nothing => pure ()
2023-10-24 17:52:19 -04:00
-- putErrLn "checking \{file}"
when (!(asksAt OPTS until) == Just Parse) $ do
lift $ outputStr $ show ast
stopHere
2023-10-20 11:42:01 -04:00
defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
2023-10-24 17:52:19 -04:00
outputDocStopIf Check $
traverse (uncurry Q.prettyDef) defList
2023-10-20 11:42:01 -04:00
let defs = SortedMap.fromList defList
erased <- liftErase defs $
traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
2023-10-24 17:52:19 -04:00
outputDocStopIf Erase $
traverse (uncurry U.prettyDef) erased
(scheme, mains) <- liftScheme $ map catMaybes $
2023-10-24 17:52:19 -04:00
traverse (uncurry defToScheme) erased
outputDocStopIf Scheme $
intersperse empty <$> traverse prettySexp scheme
opts <- askAt OPTS
main <- oneMain mains
lift $ outputDocs opts $ intersperse empty $ runPretty opts $ do
res <- traverse prettySexp scheme
runner <- makeRunMain main
pure $ text Scheme.prelude :: res ++ [runner]
2023-10-20 11:42:01 -04:00
2023-03-31 13:31:29 -04:00
export
main : IO ()
main = do
2023-10-20 11:42:01 -04:00
(_, opts, files) <- options
case !(runCompile opts !newState $ traverse_ processFile files) of
Right () => pure ()
Left e => die (Opts opts.width) $
runPretty ({outFile := Console} opts) $
prettyError e
2023-10-20 11:42:01 -04:00
2023-03-31 13:31:29 -04:00
-----------------------------------
2023-05-14 13:58:46 -04:00
{-
2021-07-20 16:05:19 -04:00
2022-04-11 08:09:37 -04:00
private
2022-04-11 15:58:33 -04:00
text : PrettyOpts -> List String
2022-04-11 08:09:37 -04:00
text _ =
["",
#" ___ ___ _____ __ __"#,
#"/ _ `/ // / _ \\ \ /"#,
#"\_, /\_,_/\___/_\_\"#,
#" /_/"#,
""]
2022-03-06 19:19:26 -05:00
2022-04-11 08:09:37 -04:00
private
2022-04-11 15:58:33 -04:00
qtuwu : PrettyOpts -> List String
2022-04-11 08:09:37 -04:00
qtuwu opts =
if opts.unicode then
[#" ___,-´⎠ "#,
#"(·`──´ ◡ -´⎠"#,
2023-02-26 04:58:47 -05:00
#" \/\/──´⎞/`──´ "#,
#" ⎜⎟───,-₎ ⎞ "#,
#" ⎝⎠ (‾‾) ⎟ "#,
2022-04-11 08:09:37 -04:00
#" (‾‾‾) ⎟ "#]
else
[#" ___,-´/ "#,
#"(.`--´ u -´/"#,
#" \/\/--´|/`--´ "#,
2023-02-26 04:58:47 -05:00
#" ||---,-, \ "#,
#" `´ (--) | "#,
2022-04-11 08:09:37 -04:00
#" (---) | "#]
private
2022-04-11 15:58:33 -04:00
join1 : PrettyOpts -> String -> String -> String
2022-04-11 08:09:37 -04:00
join1 opts l r =
if opts.color then
" " <+> show (colored Green l) <+> " " <+> show (colored Magenta r)
else
" " <+> l <+> " " <+> r
export
2022-04-11 15:58:33 -04:00
banner : PrettyOpts -> String
2022-04-11 08:09:37 -04:00
banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
2023-05-14 13:58:46 -04:00
-}