diff --git a/exe/Main.idr b/exe/Main.idr index e522169..dbb7897 100644 --- a/exe/Main.idr +++ b/exe/Main.idr @@ -1,46 +1,201 @@ module Main -import Quox.Syntax +import Quox.Syntax as Q import Quox.Parser -import Quox.Definition +import Quox.Definition as Q import Quox.Pretty +import Quox.Untyped.Syntax as U +import Quox.Untyped.Erase +import Options -import System import Data.IORef import Data.SortedSet +import Text.Show.PrettyVal +import Text.Show.Pretty +import System +import System.File import Control.Eff -private -Opts : LayoutOpts -Opts = Opts 80 +%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 -putDoc : Doc Opts -> IO () -putDoc = putStr . render Opts +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 -die : Doc Opts -> IO a -die err = do putDoc err; exitFailure +putErrLn : HasIO io => String -> io () +putErrLn = ignore . fPutStrLn stderr private -prettySig : Name -> Definition -> Eff Pretty (Doc Opts) -prettySig name def = do - qty <- prettyQty def.qty.qty - name <- prettyFree name - type <- prettyTerm [<] [<] def.type - hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type +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.(::) + [\g => send g, + handleExcept (\err => throw $ FromParserError err), + handleStateIORef !(asksAt STATE defs), + handleStateIORef !(asksAt STATE ns), + handleStateIORef !(asksAt STATE suf)] + +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 - seen <- newIORef SortedSet.empty - defs <- newIORef SortedMap.empty - suf <- newIORef 0 - for_ (drop 1 !getArgs) $ \file => do - putStrLn "checking \{file}" - Right res <- fromParserIO ["."] seen suf defs $ loadProcessFile noLoc file - | Left err => die $ runPrettyColor $ prettyError True err - for_ res $ \(name, def) => putDoc $ runPrettyColor $ prettySig name def + (_, opts, files) <- options + case !(runCompile opts !newState $ traverse_ processFile files) of + Right () => pure () + Left e => dieError opts e + ----------------------------------- {- diff --git a/exe/Options.idr b/exe/Options.idr new file mode 100644 index 0000000..58b545b --- /dev/null +++ b/exe/Options.idr @@ -0,0 +1,158 @@ +module Options + +import Quox.Pretty +import System +import System.Console.GetOpt +import System.File +import System.Term +import Derive.Prelude + +%language ElabReflection + +public export +data OutFile = File String | Stdout | None +%name OutFile f +%runElab derive "OutFile" [Eq, Ord, Show] + +public export +data Phase = Parse | Check | Erase +%name Phase p +%runElab derive "Phase" [Eq, Ord, Show] + +||| a list of all `Phase`s +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 + +public export +record Options where + constructor MkOpts + color : Bool + outFile : OutFile + until : Maybe Phase + flavor : Pretty.Flavor + width : Nat + include : List String +%name Options opts +%runElab derive "Options" [Show] + +export +defaultOpts : IO Options +defaultOpts = pure $ MkOpts { + color = True, + outFile = Stdout, + until = Nothing, + flavor = Unicode, + width = cast !getTermCols, + include = ["."] +} + +private +data HelpType = Common | All + +private +data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options) +%name OptAction act + +private +toOutFile : String -> OptAction +toOutFile "" = Ok {outFile := None} +toOutFile "-" = Ok {outFile := Stdout} +toOutFile f = Ok {outFile := File f} + +private +phaseName : Phase -> String +phaseName Parse = "parse" +phaseName Check = "check" +phaseName Erase = "erase" + +private +toPhase : String -> OptAction +toPhase str = case toLower str of + "parse" => Ok {until := Just Parse} + "check" => Ok {until := Just Check} + "erase" => Ok {until := Just Erase} + _ => Err "unknown phase name \{show str}\nphases: \{phaseNames}" +where phaseNames = joinBy ", " $ map phaseName allPhases + +private +toWidth : String -> OptAction +toWidth s = case parsePositive s of + Just n => Ok {width := n} + Nothing => Err "invalid width: \{show s}" + +private +commonOptDescrs' : List (OptDescr OptAction) +commonOptDescrs' = [ + MkOpt ['i'] ["include"] (ReqArg (\i => Ok {include $= (i ::)}) "