module Minilang.REPLSpec where

import Control.Exception (bracket)
import Data.Either (isRight)
import Data.Text.IO
import Minilang.Lambda.Eval (Term (Lam, Var))
import Minilang.Lambda.Parser (AST (..))
import Minilang.Lambda.Unify (Type (TyVar))
import Minilang.REPL
import Minilang.REPL.Purer (PurerEnv (..))
import Minilang.REPL.Run (loadProgramInEnv)
import Minilang.REPL.Types (Out (Evaluated))
import System.Directory (getTemporaryDirectory, removeFile)
import System.FilePath ((<.>), (</>))
import System.IO (IOMode (..), hClose, withFile)
import System.Posix.Temp (mkstemp)
import Test.Hspec
import Prelude hiding (lines, readFile, writeFile)

spec :: Spec
spec = parallel $
  describe "MiniLang REPL" $ do
    it "evaluates untyped MiniLang terms read from pure Monad" $ do
      let out =
            withInput
              ["((lam (x) x) y)"]

      out
        `shouldBe` [ "Bye!",
                     "y : <?>"
                   ]

    it "evaluates untyped MiniLang terms with definitions" $ do
      let out =
            withInput
              ["(def id (lam (x) x))", "(id y)"]

      out
        `shouldBe` [ "Bye!",
                     "y : <?>",
                     "id : <?>"
                   ]

    it "evaluates typed MiniLang terms with definitions" $ do
      let out =
            withInput
              [ ":lang   Typed",
                "(def id (lam (x) x))",
                "(id y)"
              ]

      out
        `shouldBe` [ "Bye!",
                     "y : a",
                     "id : a -> a",
                     "Language set to Typed"
                   ]

    it "defaults untyped terms" $ do
      let out =
            withInput
              [ "(let ((Succ (lam (n z s) (s n))) \
                \ (Zero (lam (z s) z))) \
                \ (Succ (Succ Zero)))"
              ]

      out
        `shouldBe` [ "Bye!",
                     "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : <?>"
                   ]

    it "do typecheck term when language is set to 'Typed'" $ do
      let out =
            withInput
              [ ":lang   Typed",
                "(let ((Succ (lam (n z s) (s n))) \
                \ (Zero (lam (z s) z))) \
                \ (Succ (Succ Zero)))"
              ]

      out
        `shouldBe` [ "Bye!",
                     "(lam (z s) (s (lam (z s) (s (lam (z s) z))))) : a -> ((c -> ((e -> f -> e) -> g) -> g) -> h) -> h",
                     "Language set to Typed"
                   ]

    it "shows error when trying to load a non-existent file" $ do
      withInput [":load foo"]
        `shouldBe` [ "Bye!",
                     "REPLError \"cannot load file foo in Pure interpreter\""
                   ]

    it "can load 'bool-prog.lisp'" $ do
      boolProg <- readFile "bool-prog.lisp"
      let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg)
      outputs
        `shouldBe` [ Evaluated (Abs ["f", "t"] (Sym "t")) (Lam "f" (Lam "t" (Var "t"))) (TyVar "<?>"),
                     Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) (TyVar "<?>"),
                     Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) (TyVar "<?>")
                   ]

    it "can load 'bool.lisp'" $ do
      boolProg <- readFile "bool.lisp"
      let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg)
      outputs
        `shouldBe` [ Evaluated
                       (Abs ["f", "t"] (Sym "f"))
                       (Lam "f" (Lam "t" (Var "f")))
                       (TyVar "<?>")
                   ]

    it "can load 'fac.lisp'" $ do
      boolProg <- readFile "fac.lisp"
      let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg)
      outputs
        `shouldBe` [ Evaluated
                       (Abs ["f", "t"] (Sym "t"))
                       (Lam "f" (Lam "t" (Var "t")))
                       (TyVar "<?>")
                   ]

    around withTempFile $
      it "evaluates single MiniLang term read from IO" $ \fileName -> do
        let outputFileName = fileName <> ".out"

        writeFile
          fileName
          "(let ((Succ (lam (n z s) (s n))) \
          \ (Zero (lam (z s) z))) \
          \ (Succ Zero))"

        _ <- withFile fileName ReadMode $ \hin ->
          withFile outputFileName AppendMode $ \hout ->
            withHandles hin hout

        out <- readFile outputFileName

        out
          `shouldBe` "\955\928> (lam (z s) (s (lam (z s) z))) : <?>\n\955\928> Bye!\n"

withTempFile :: (String -> IO ()) -> IO ()
withTempFile =
  bracket mkTempFile rmTempFile
  where
    mkTempFile = getTemporaryDirectory >>= \dir -> mkstemp (dir </> "test-repl") >>= \(fp, h) -> hClose h >> pure fp
    rmTempFile fn = removeFile fn >> removeFile (fn <.> "out")