module Minilang.Lambda.InferSpec (spec) where

import Minilang.Lambda.Eval (Term (..))
import Minilang.Lambda.Infer (TypeError (..), annotate)
import qualified Minilang.Lambda.Infer as Ann
import Minilang.Lambda.Unify (Type (..), UnifyError (..))
import Test.Hspec (Spec, describe, it, shouldBe)

spec :: Spec
spec = do
  describe "annotate" $ do
    it "annotates unknown variable with fresh type variable" $ do
      let term = Var "x"
      annotate term `shouldBe` Right (Ann.Var "x" (TyVar "a"))
    it "annotates bound λ variable with fresh type variable" $ do
      let term = Lam "x" (Var "x")
      annotate term `shouldBe` Right (Ann.Lam "x" (Ann.Var "x" (TyVar "a")) (TyVar "a" :-> TyVar "a"))
    it "annotates application with fresh type variables" $ do
      let term = App (Var "x") (Var "y")
      annotate term `shouldBe` Right (Ann.App (Ann.Var "x" (TyVar "a")) (Ann.Var "y" (TyVar "b")) (TyVar "c"))
    it "reuse free variables types" $ do
      let term = App (Var "x") (Var "x")
      annotate term `shouldBe` Right (Ann.App (Ann.Var "x" (TyVar "a")) (Ann.Var "x" (TyVar "a")) (TyVar "b"))
  describe "infer" $ do
    it "infers correctly some expressions" $ do
      let id' = Lam "x" (Var "x")
      let fst' = Lam "x" (Lam "y" (Var "x"))
      let snd' = Lam "x" (Lam "y" (Var "y"))
      let comp = Lam "f" (Lam "g" (Lam "x" (App (Var "f") (App (Var "g") (Var "x")))))
      let k = Lam "x" (Lam "y" (Lam "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))

      Ann.infer id' `shouldBe` Right (TyVar "a" :-> TyVar "a")
      Ann.infer fst' `shouldBe` Right (TyVar "a" :-> (TyVar "b" :-> TyVar "a"))
      Ann.infer snd' `shouldBe` Right (TyVar "a" :-> (TyVar "b" :-> TyVar "b"))
      Ann.infer comp `shouldBe` Right ((TyVar "d" :-> TyVar "e") :-> ((TyVar "c" :-> TyVar "d") :-> (TyVar "c" :-> TyVar "e")))
      Ann.infer k
        `shouldBe` Right
          ( (TyVar "c" :-> TyVar "e" :-> TyVar "f")
              :-> (TyVar "c" :-> TyVar "e")
              :-> TyVar "c"
              :-> TyVar "f"
          )

    it "rejects circular references" $ do
      let circ = Lam "f" (App (Lam "x" (App (App (Var "f") (Var "x")) (Var "x"))) (Lam "y" (App (App (Var "f") (Var "y")) (Var "y"))))

      Ann.infer circ `shouldBe` Left (UnifyError $ Circularity "e" (TyVar "e" :-> TyVar "g"))