{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoOverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where

import Test.Tasty
import Test.Tasty.HUnit
-- import Data.Proxy

import Language.Symantic.Typing

tests :: TestTree
tests = testGroup "Typing" $
	let (==>) (stx::Syntax String) expected =
		testCase (show stx) $
		(@?= EType <$> expected) $
		type_from stx (Right . (EType::Type Consts ki h -> EType Consts))
	in
	 [ syBool ==> Right tyBool
	 , syFun [syBool] ==> Right (tyFun :$ tyBool)
	 , syEq [syBool] ==> Right (tyEq :~ tyBool)
	 , syMonad [syIO []] ==> Right (tyMonad :~ tyIO)
	 , syFun [syIO [syBool]] ==> Right (tyFun :$ (tyIO :$ tyBool))
	 , (syBool .> syBool) ==> Right
	   (tyBool ~> tyBool)
	 , ((syBool .> syBool) .> syBool) ==> Right
	   ((tyBool ~> tyBool) ~> tyBool)
	 , ((syBool .> syInt) .> syBool) ==> Right
	   ((tyBool ~> tyInt) ~> tyBool)
	 , (syBool .> syInt .> syBool) ==> Right
	   (tyBool ~> tyInt ~> tyBool)
	 , ((syBool .> (syBool .> syInt)) .> syBool) ==> Right
	   ((tyBool ~> (tyBool ~> tyInt)) ~> tyBool)
	 , testGroup "Error"
		 [ syTraversable [syIO []] ==> Left
			(Error_Type_Constraint_missing
			  (At (syTraversable [syIO []]) $ EType $ tyTraversable :$ tyIO))
		 , syFun [syIO []] ==> Left
			 (Error_Type_Kind_mismatch
				 (At (syFun [syIO []]) $ EKind SKiTerm)
				 (At (syIO []) $ EKind $ SKiTerm `SKiArrow` SKiTerm))
		 , syIO [syEq [syBool]] ==> Left
			 (Error_Type_Kind_mismatch
				 (At (syIO [syEq [syBool]]) $ EKind SKiTerm)
				 (At (syEq [syBool]) $ EKind $ SKiCon))
		 , Syntax "Bool" [syBool] ==> Left
			 (Error_Type_Kind_not_applicable
				 (At (Syntax "Bool"  [syBool]) $ EKind SKiTerm))
		 , Syntax "Unknown" [] ==> Left (Error_Type_Constant_unknown $
			 At (Syntax "Unknown" []) ())
		 ]
	 ]