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

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

import Language.Symantic.Type

import AST.Test

type Type_Fun_Bool     = Type_Root (Type_Fun :|: Type_Bool)
type Type_Fun_Bool_Int = Type_Root (Type_Fun :|: Type_Bool :|: Type_Int)
type Type_Fun_Int      = Type_Root (Type_Fun :|: Type_Int)

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 Bool) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [AST "Bool" []]
			 ==> Left (lift_error_type $
			 Error_Type_Wrong_number_of_arguments (AST "->" [AST "Bool" []]) 2) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [AST "Bool" [], AST "Bool" []]
			 ==> Right (type_bool `type_fun` type_bool
			 :: Type_Fun_Bool ((->) Bool Bool)) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [ AST "->" [AST "Bool" [], AST "Bool" []]
			          , AST "Bool" [] ]
			 ==> Right ((type_bool `type_fun` type_bool) `type_fun` type_bool
			 :: Type_Fun_Bool ((->) ((->) Bool Bool) Bool)) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [ AST "Bool" []
			          , AST "->" [AST "Bool" [], AST "Bool" []] ]
			 ==> Right (type_bool `type_fun` (type_bool `type_fun` type_bool)
			 :: Type_Fun_Bool ((->) Bool ((->) Bool Bool))) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "Int" []
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [AST "Bool" [], AST "Int" []]
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
			          , AST "Int" [] ]
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Int" []) $
			 (Proxy :: Proxy (Type_Fun_Bool))
		 ]
	 , testGroup "Int"
		 [ AST "Int" []
			 ==> Right (type_int :: Type_Fun_Int Int) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [AST "Int" []]
			 ==> Left (lift_error_type $
			 Error_Type_Wrong_number_of_arguments (AST "->" [AST "Int" []]) 2) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [AST "Int" [], AST "Int" []]
			 ==> Right (type_int `type_fun` type_int
			 :: Type_Fun_Int ((->) Int Int)) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Int" []]
			          , AST "Int" [] ]
			 ==> Right ((type_int `type_fun` type_int) `type_fun` type_int
			 :: Type_Fun_Int ((->) ((->) Int Int) Int)) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [ AST "Int" []
			          , AST "->" [AST "Int" [], AST "Int" []] ]
			 ==> Right (type_int `type_fun` (type_int `type_fun` type_int)
			 :: Type_Fun_Int ((->) Int ((->) Int Int))) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "Bool" []
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [AST "Int" [], AST "Bool" []]
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 , AST "->" [ AST "->" [AST "Bool" [], AST "Int" []]
			          , AST "Bool" [] ]
			 ==> Left (lift_error_type $ Error_Type_Unsupported $ AST "Bool" []) $
			 (Proxy :: Proxy (Type_Fun_Int))
		 ]
	 , testGroup "Fun" $
		 [ AST "Int"  []
		   ==> Right (type_int :: Type_Fun_Bool_Int Int) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int))
		 , AST "->" [AST "Bool" [], AST "Int" []]
		   ==> Right (type_bool `type_fun` type_int
		   :: Type_Fun_Bool_Int ((->) Bool Int)) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int))
		 , AST "->" [ AST "->" [AST "Int" [], AST "Bool" []]
		            , AST "Int" [] ]
		   ==> Right ((type_int `type_fun` type_bool) `type_fun` type_int
		   :: Type_Fun_Bool_Int ((->) ((->) Int Bool) Int)) $
		   (Proxy :: Proxy (Type_Fun_Bool_Int))
		 ]
	 ]