{-# LANGUAGE LambdaCase, OverloadedStrings #-}
module Main (main) where

import System.Exit
import System.Environment

import Hm.Layout ( resolveLayout )
import Hm.Lex    ( Token, mkPosToken )
import Hm.Par    ( pExp, pListDef, myLexer )
import Hm.Print  ( Print, printTree )

import Data.Text (Text)
import qualified Data.Text.IO as T

import qualified Data.Set as S
import qualified Data.Map as M

import Type (initialState, emptySubst, apply)
import TC (runInfer, infer)
import TC.Helpers (generalize)
import Solve (runSolve)
import PostProcess (expToExp, runProcess)
import Pretty (pretty)
import Toplevel (check)

inferType :: Text -> IO ()
inferType s = case pExp ts of
    Left err -> do
      putStrLn "\nParse              Failed...\n"
      putStrLn  "Tokens:"
      mapM_ (putStrLn . showPosToken . mkPosToken) ts
      putStrLn err
      exitFailure
    Right tree -> do
      putStrLn "\nParse Successful!"
      putStrLn (printTree tree)

      let action = runProcess (expToExp tree) S.empty >>= infer
      let result = runInfer M.empty action

      case result of
        Left  err -> print err
        Right (t,_,c) -> case runSolve (emptySubst, c) of
                           Left err -> print err
                           Right subst -> case runInfer M.empty (generalize (apply subst t)) of
                               Left err -> print err
                               Right (t,_,_) -> T.putStrLn (pretty t)
                            
  where
    ts = init (resolveLayout True (myLexer s))
    showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ]

checkFile :: Text -> IO ()
checkFile s = case pListDef ts of
    Left err -> do
      putStrLn "\nParse              Failed...\n"
      putStrLn  "Tokens:"
      mapM_ (putStrLn . showPosToken . mkPosToken) ts
      putStrLn err
      exitFailure
    Right tree -> do
      putStrLn "\nParse Successful!"
      putStrLn (printTree tree)

      case check tree of
        Left  err -> T.putStrLn ("Type Error: " <> pretty err)
        Right _   -> putStrLn "Type check Successful!"
                            
  where
    ts = resolveLayout True (myLexer s)
    showPosToken ((l,c),t) = concat [ show l, ":", show c, "\t", show t ]

main :: IO ()
main = getArgs >>= \case
    ("tl":_) -> T.getContents >>= checkFile
    _        -> T.getContents >>= inferType