big Main refactor

This commit is contained in:
rhiannon morris 2024-04-04 18:10:53 +02:00
parent 727f968afb
commit ec839a1d48
5 changed files with 281 additions and 231 deletions

134
exe/CompileMonad.idr Normal file
View File

@ -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 [])]

49
exe/Error.idr Normal file
View File

@ -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

View File

@ -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

View File

@ -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)"
]

59
exe/Output.idr Normal file
View File

@ -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