module Main

import CC.Name
import CC.Term
import CC.Term.Eval
import CC.Term.Parse
import CC.Term.Pretty
import CC.Term.Raw

import Data.String

import System
import System.File.ReadWrite
import System.File.Virtual

import Text.Parser
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal

--- Error Reporting ------------------------------------------------------------

putErrLn : HasIO io => String -> io ()
putErrLn str = do
  Right () <- fPutStrLn stderr str
    | Left e => pure ()
  pure ()

putBoundErrLn : HasIO io => Maybe Bounds -> String -> io ()
putBoundErrLn Nothing str = putErrLn str
putBoundErrLn (Just bounds) str =
  let startLine = padLeft 3 '0' $ show (1 + bounds.startLine) in
  let startCol = padLeft 2 '0' $ show bounds.startCol in
  let endLine = padLeft 3 '0' $ show (1 + bounds.endLine) in
  let endCol = padLeft 2 '0' $ show bounds.endCol in
  putErrLn "\{startLine}:\{startCol}--\{endLine}:\{endCol}: \{str}"

-- Parsing ---------------------------------------------------------------------

parse : String -> IO RawTerm
parse str =
  case parseString str of
    Left errs => for_ errs putErr >> exitFailure
    Right v => pure v
  where
  putErr : ParsingError CCToken -> IO ()
  putErr (Error str bounds) = putBoundErrLn bounds ("parse error: \{str}" )

partial
parseStdin : IO RawTerm
parseStdin = do
  Right str <- fRead stdin
    | Left err => putErrLn "failed to read input: \{show err}" >> exitFailure
  parse str

-- Main Function ---------------------------------------------------------------

helpMsg : String
helpMsg = unlines [
  "usage: cc-eval [--help|nf]",
  "  --help : display this message",
  "  nf     : read expression from stdin, print its normal form"
  ]

mainWith : IO (List String) -> IO RawTerm -> IO ()
mainWith getOpt getTerm = do
  [_, "nf"] <- getOpt
    | [_, "--help"] => putStrLn helpMsg
    | _ => putErrLn helpMsg >> exitFailure
  rawTerm <- getTerm
  let Right term = runNameError $ translate [<] rawTerm
    | Left errs => for_ errs putErr >> exitFailure
  let nf : Term [<] = normalise [<] term
  putDoc (pretty nf)
  where
  putErr : Name -> IO ()
  putErr n = putBoundErrLn (bounds n) "undefined name: \{n}"

partial
main : IO ()
main = mainWith getArgs parseStdin

main' : String -> String -> IO ()
main' mode src = mainWith (pure [mode]) (parse src)