{-# 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.Maybe (isJust)
-- import Data.Proxy
-- import GHC.Prim (Constraint)

import Language.Symantic.Typing

tests :: TestTree
tests = testGroup "Typing" $
	 [ testGroup "type_from" $
		let (==>) (sy::Syntax String) expected =
			testCase (show sy) $
			(@?= EType <$> expected) $
			type_from sy (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_Type"
			 [ 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" []) ())
			 ]
		 ]
	 , testGroup "proj_con" $
		let (==>) (ty::Type Consts 'KiCon h) expected =
			testCase (show_type ty) $
			isJust (proj_con ty) @?= expected
		in
		 [ (tyEq :$ tyBool) ==> True
		 , (tyMonad :$ tyIO) ==> True
		 , (tyTraversable :$ tyIO) ==> False
		 ]
	 ]