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

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

import Language.Symantic.Type

import AST.Test

tests :: TestTree
tests = testGroup "Type" $
	let (==>) ast expected p =
		testCase (show ast) $
		(@?= Exists_Type <$> expected) $
		type_from p ast (Right . Exists_Type) in
	 [ testGroup "Bool"
		 [ AST "Bool" []
			 ==> Right (type_bool :: Type_Fun_Bool lam Bool) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 , AST "->" [AST "Bool" []]
			 ==> Left (error_type_lift $
			 Error_Type_Wrong_number_of_arguments (AST "->" [AST "Bool" []]) 2) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 , AST "->" [AST "Bool" [], AST "Bool" []]
			 ==> Right (type_bool `type_fun` type_bool
			 :: Type_Fun_Bool lam (lam Bool -> lam Bool)) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 , AST "->" [ AST "->" [AST "Bool" [], AST "Bool" []]
			          , AST "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))
		 , AST "->" [ AST "Bool" []
			          , AST "->" [AST "Bool" [], AST "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))
		 , AST "Int" []
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 , AST "->" [AST "Bool" [], AST "Int" []]
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
			          , AST "Int" [] ]
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool lam))
		 ]
	 , testGroup "Int"
		 [ AST "Int" []
			 ==> Right (type_int :: Type_Fun_Int lam Int) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [AST "Int" []]
			 ==> Left (error_type_lift $
			 Error_Type_Wrong_number_of_arguments (AST "->" [AST "Int" []]) 2) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [AST "Int" [], AST "Int" []]
			 ==> Right (type_int `type_fun` type_int
			 :: Type_Fun_Int lam (lam Int -> lam Int)) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Int" []]
			          , AST "Int" [] ]
			 ==> Right ((type_int `type_fun` type_int) `type_fun` type_int
			 :: Type_Fun_Int lam (lam (lam Int -> lam Int) -> lam Int)) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [ AST "Int" []
			          , AST "->" [AST "Int" [], AST "Int" []] ]
			 ==> Right (type_int `type_fun` (type_int `type_fun` type_int)
			 :: Type_Fun_Int lam (lam Int -> lam (lam Int -> lam Int))) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "Bool" []
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [AST "Int" [], AST "Bool" []]
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 , AST "->" [ AST "->" [AST "Bool" [], AST "Int" []]
			          , AST "Bool" [] ]
			 ==> Left (error_type_lift $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int lam))
		 ]
	 , testGroup "Fun" $
		 [ AST "Int"  []
		   ==> Right (type_int :: Type_Fun_Bool_Int lam Int) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int lam))
		 , AST "->" [AST "Bool" [], AST "Int" []]
		   ==> Right (type_bool `type_fun` type_int
		   :: Type_Fun_Bool_Int lam (lam Bool -> lam Int)) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int lam))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
		            , AST "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))
		 ]
	 ]