quox/exe/Main.idr

module Main

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 System
import System.File
import Data.IORef
import Control.Eff

%default total

%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

private
step : {default CErr console : ConsoleChannel} ->
       Phase -> OutFile -> Step i o -> i -> Eff CompileStop o
step phase file act x = do
  opts <- askAt OPTS
  res <- lift $ withOutFile console file $ \h => act h x
  when (opts.until == Just phase) stopHere
  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]

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  => 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)
-}