module Language.Lambda.SystemF.TypeCheckSpec (spec) where

import Data.Either
import Data.Map
import Prettyprinter
import Test.Hspec

import Language.Lambda.Shared.Errors
import Language.Lambda.SystemF.Expression
import Language.Lambda.SystemF.State
import Language.Lambda.SystemF.TypeCheck

tc uniqs ctx expr = execTypecheck (typecheck expr) (TypecheckState (fromList ctx) uniqs)

spec :: Spec
spec = describe "typecheck" $ do
  it "typechecks simple variables in context" $
    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")

  it "typechecks simple variables not in context" $ 
    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")

  it "typechecks simple abstractions" $
    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))

  it "typechecks simple applications" $ do
    let ctx = [
          ("f", TyArrow (TyVar "T") (TyVar "U")),
          ("a", TyVar "T")
          ]

    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")

  it "apply variable to variable fails" $ do
    let ctx = [
          ("a", TyVar "A"),
          ("b", TyVar "B")
          ]

    tc ["C"] ctx (App (Var "a") (Var "b")) 
      `shouldSatisfy` isLeft

  it "apply arrow to variable of wrong type fails" $ do
    let ctx = [
          ("f", TyArrow (TyVar "F") (TyVar "G")),
          ("b", TyVar "B")
          ]

    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft

  it "typechecks simple type abstractions" $
    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))

  it "typechecks type abstractions with simple abstraction" $
    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) 
      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))

  it "typechecks type abstractions with application" $
    tc [] [("y", TyVar "Y")] 
      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) 
           (Var "y"))
      `shouldBe` Right (TyVar "Y")

  it "typechecks simple type applications" $
    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
      `shouldBe` Right (TyVar "A")

  it "typechecks type applications with simple abstraction" $
    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))
      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))