{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where

import Test.Tasty
import Test.Tasty.HUnit

import Data.Maybe (isJust)
import Data.Proxy
import Data.Text (Text)
import GHC.Exts (Constraint)

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling

import Parsing.Test

-- * Tests
tests :: TestTree
tests = testGroup "Typing" $
 [ testGroup "compile_type" $
	let (==>) (syn::Syntax Text) expected =
		let Right (tok::EToken (Syntax Text) '[Proxy Token_Type]) = tokenize_type syn in
		testCase (Prelude.show syn) $
		(@?= EType Prelude.<$> expected) $
		(compile_type tok (Right . EType)
		 :: Either (Error_Type (Syntax Text) '[Proxy Token_Type])
		           (EType Constants))
	in
	 [ sy @Bool ==> Right (ty @Bool)
	 , sy @IO [] ==> Right (ty @IO)
	 , sy @Eq [] ==> Right (ty @Eq)
	 , sy @(->) [sy @Bool] ==> Right (ty @(->) :$ ty @Bool)
	 , sy @Eq [sy @Bool] ==> Right (ty @Eq :$ ty @Bool)
	 , sy @Monad [sy @IO []] ==> Right (ty @Monad :$ ty @IO)
	 , sy @(->) [sy @IO [sy @Bool]] ==> Right (ty @(->) :$ (ty @IO :$ ty @Bool))
	 , (sy @Bool .> sy @Bool) ==> Right
	   (ty @Bool ~> ty @Bool)
	 , ((sy @Bool .> sy @Bool) .> sy @Bool) ==> Right
	   ((ty @Bool ~> ty @Bool) ~> ty @Bool)
	 , ((sy @Bool .> sy @Int) .> sy @Bool) ==> Right
	   ((ty @Bool ~> ty @Int) ~> ty @Bool)
	 , (sy @Bool .> sy @Int .> sy @Bool) ==> Right
	   (ty @Bool ~> ty @Int ~> ty @Bool)
	 , ((sy @Bool .> (sy @Bool .> sy @Int)) .> sy @Bool) ==> Right
	   ((ty @Bool ~> (ty @Bool ~> ty @Int)) ~> ty @Bool)
	 , testGroup "Error_Type"
		 [ sy @(->) [sy @IO []] ==> Left
			 (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
				 (At (maybeRight $ tokenize_type $ sy @(->) [sy @IO []]) $ EKind SKiType)
				 (At (maybeRight $ tokenize_type $ sy @IO []) $ EKind $ SKiType `SKiArrow` SKiType))
		 , sy @IO [sy @Eq [sy @Bool]] ==> Left
			 (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
				 (At (maybeRight $ tokenize_type $ sy @IO [sy @Eq [sy @Bool]]) $ EKind SKiType)
				 (At (maybeRight $ tokenize_type $ sy @Eq [sy @Bool]) $ EKind $ SKiConstraint))
		 , Syntax "Bool" [sy @Bool] ==> Left
			 (Error_Type_Constraint_Kind $ Constraint_Kind_Arrow
				 (At (maybeRight $ tokenize_type $ Syntax "Bool" [sy @Bool]) $ EKind SKiType))
		 , Syntax ("Unknown"::Text) [] ==> Left
			 (Error_Type_Constant_unknown $
				At (maybeRight $ tokenize_type $ Syntax ("Unknown"::Text) []) "Unknown")
		 ]
	 ]
 , testGroup "proj_con" $
	let (==>) (typ::Type Constants (h::Constraint)) expected =
		testCase (show_type typ) $
		isJust (proj_con typ) @?= expected
	in
	 [ (ty @Eq :$ ty @Bool) ==> True
	 , (ty @Ord :$ ty @Bool) ==> True
	 , (ty @Functor :$ ty @Maybe) ==> True
	 , (ty @Functor :$ ty @IO) ==> True
	 , (ty @Monad :$ ty @IO) ==> True
	 , (ty @Traversable :$ ty @IO) ==> False
	 ]
 ]