{-# LANGUAGE FlexibleContexts #-}
module Type.Test where

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

import Language.LOL.Symantic.Raw
import Language.LOL.Symantic.Type

tests :: TestTree
tests = testGroup "Type" $
	let (==>) raw expected p =
		testCase (show raw) $
		type_from p raw (Right . Exists_Type) @?=
		(Exists_Type <$> expected) in
	 [ testGroup "Fun_Bool" $
		 [ Raw "Bool" []
		   ==> Right (type_bool :: Type_Fun_Bool lam Bool) $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [Raw "Bool" []]
		   ==> Left (Just $ error_type_lift $ Error_Type_Fun_Wrong_number_of_arguments 2 (Raw "->" [Raw "Bool" []])) $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [Raw "Bool" [], Raw "Bool" []]
		   ==> Right (type_bool `type_fun` type_bool
		   :: Type_Fun_Bool lam (lam Bool -> lam Bool)) $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [ Raw "->" [Raw "Bool" [], Raw "Bool" []]
		            , Raw "Bool" [] ]
		   ==> Right ((type_bool `type_fun` type_bool) `type_fun` type_bool
		   :: Type_Fun_Bool lam (lam (lam Bool -> lam Bool) -> lam Bool)) $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [ Raw "Bool" []
		            , Raw "->" [Raw "Bool" [], Raw "Bool" []] ]
		   ==> Right (type_bool `type_fun` (type_bool `type_fun` type_bool)
		   :: Type_Fun_Bool lam (lam Bool -> lam (lam Bool -> lam Bool))) $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "Int" []
		   ==> Left Nothing $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [Raw "Bool" [], Raw "Int" []]
		   ==> Left Nothing $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 , Raw "->" [ Raw "->" [Raw "Int" [], Raw "Bool" []]
		            , Raw "Int" [] ]
		   ==> Left Nothing $
		   (Proxy :: Proxy (Type_Fun_Bool lam))
		 ]
	 , testGroup "Fun_Bool_Int" $
		 [ Raw "Int"  []
		   ==> Right (type_int :: Type_Fun_Bool_Int lam Int) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int lam))
		 , Raw "->" [Raw "Bool" [], Raw "Int" []]
		   ==> Right (type_bool `type_fun` type_int :: Type_Fun_Bool_Int lam (lam Bool -> lam Int)) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int lam))
		 , Raw "->" [ Raw "->" [Raw "Int" [], Raw "Bool" []]
		            , Raw "Int" [] ]
		   ==> Right ((type_int `type_fun` type_bool) `type_fun` type_int
		   :: Type_Fun_Bool_Int lam (lam (lam Int -> lam Bool) -> lam Int)) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int lam))
		 ]
	 ]