Main.hs

module Main where

import Control.Exception
import System.Environment
import System.Exit
import System.Directory
import System.FilePath
import System.Process
import System.IO

import Errors
import Evaluation
import ElabState
import Parser
import Pretty
import StringBuilder
import Elaboration
import Zonk
import qualified Interpreter
import qualified Compiler

--------------------------------------------------------------------------------

helpMsg = unlines [
  "usage: rtcg FILE [--help|elab|zonk|interp|compile|run|nf|type]",
  "  --help    : display this message",
  "  elab      : print elaboration output",
  "  zonk      : print zonking & erasure output",
  "  interp    : run program in interpreter",
  "  compile   : print compiled javascript output",
  "  run       : compile to javascript and run",
  "  nf        : print beta-normal form and beta-normal type",
  "  type      : print type of program"]

mainWith :: IO [String] -> IO ()
mainWith getOpt = do
  hSetBuffering stdout NoBuffering

  (path, opts) <- getOpt >>= \case
    path:opts -> pure (path, opts)
    _         -> putStrLn helpMsg >> exitSuccess

  let handleErr file act = act `catch` \e -> displayError e >> exitSuccess

  let elab = do
        file <- readFile path
        t    <- parseString path file
        res  <- handleErr file (inferTop file t)
        pure (res, file)

  reset
  case opts of
    ["--help"] -> putStrLn helpMsg
    ["nf"]   -> do
      ((t, a), file) <- elab
      putStrLn $ showTm0 $ nf [] t
      putStrLn "  :"
      putStrLn $ showTm0 $ quote 0 a
    ["type"] -> do
      ((t, a), file) <- elab
      putStrLn $ showTm0 $ quote 0 a
    ["elab"] -> do
      ((t, a), file) <- elab
      displayMetas
      putStrLn (replicate 80 '-' ++ "\n")
      putStrLn $ showTm0 t
    ["zonk"] -> do
      ((t, a), file) <- elab
      t <- unzonk <$> handleErr file (zonk0 t)
      putStrLn $ showTm0 t
    ["compile"] -> do
      ((t, a), file) <- elab
      t <- handleErr file (zonk0 t)
      out <- build <$> Compiler.genTop t
      putStrLn out
      dir <- getCurrentDirectory
      putStrLn $ "written to: " ++ (dir </> "out.js")
      writeFile "out.js" out
    ["interp"] -> do
      ((t, a), file) <- elab
      t <- handleErr file (zonk0 t)
      res <- Interpreter.execTop (castTm t)
      res <- pure $ unzonk $ Interpreter.readBackClosed res
      putStrLn "RESULT:"
      putStrLn $ showTm0 res
    ["run"] -> do
      ((t, a), file) <- elab
      t <- handleErr file (zonk0 t)
      out <- build <$> Compiler.genTop t
      writeFile "out.js" out
      callCommand "node out.js"
    _ -> putStrLn helpMsg

main :: IO ()
main = mainWith getArgs

-- | Run main with inputs as function arguments.
main' :: String -> IO ()
main' opts = mainWith (pure $ words opts)

test :: String ->  IO ()
test cmd = main' ("debug.rtcg " ++ cmd)

------------------------------------------------------------