module Main

import CC.Name
import CC.Term
import CC.Term.Elaborate
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-check [--help|nf|type]",
  "  --help : display this message",
  "  nf     : read & typecheck expression from stdin, print its normal form and type",
  "  type   : read & typecheck expression from stdin, print its type"
  ]



mainWith : IO (List String) -> IO RawTerm -> IO ()
mainWith getOpt getTerm = do
  opts <- getOpt
  case opts of
    [_, "--help"] => putStrLn helpMsg
    [_, "nf"] => do
      rawTerm <- getTerm
      let Right (t, ty) = runElabError $ inferTerm rawTerm
        | Left errs => for_ errs putErr >> exitFailure
      let nf : Term [<] = normalise [<] t
      let ty = quote ty
      putDoc (group $ pretty nf <++> colon <+> line <+> pretty ty)
    [_, "type"] => do
      rawTerm <- getTerm
      let Right (t, ty) = runElabError $ inferTerm rawTerm
        | Left errs => for_ errs putErr >> exitFailure
      putDoc (group $ pretty $ quote ty)
    _ => putErrLn helpMsg >> exitFailure
  where
  putErr : Either Name (String, Maybe Bounds) -> IO ()
  putErr (Left n) = putBoundErrLn (bounds n) "undefined name: \{n}"
  putErr (Right (s, bounds)) = putBoundErrLn bounds s

partial
main : IO ()
main = mainWith getArgs parseStdin

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