{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where

import Test.Tasty
import Test.Tasty.HUnit

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

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

-- * Tests
tests :: TestTree
tests = testGroup "Typing" $
 [ testGroup "type_from" $
	let (==>) (sy::Syntax Text) expected =
		testCase (show sy) $
		(@?= EType Prelude.<$> expected) $
		type_from sy (\h -> Right (EType h::EType Constants))
	in
	 [ syBool ==> Right tyBool
	 , syIO [] ==> Right tyIO
	 , syEq [] ==> Right tyEq
	 , 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 (Just $ syFun [syIO []]) $ EKind SKiType)
				 (At (Just $ syIO []) $ EKind $ SKiType `SKiArrow` SKiType))
		 , syIO [syEq [syBool]] ==> Left
			 (Error_Type_Kind_mismatch
				 (At (Just $ syIO [syEq [syBool]]) $ EKind SKiType)
				 (At (Just $ syEq [syBool]) $ EKind $ SKiConstraint))
		 , Syntax "Bool" [syBool] ==> Left
			 (Error_Type_Kind_not_applicable
				 (At (Just $ Syntax "Bool"  [syBool]) $ EKind SKiType))
		 , Syntax "Unknown" [] ==> Left (Error_Type_Constant_unknown $
			 At (Just $ Syntax "Unknown" []) "Unknown")
		 ]
	 ]
 , testGroup "proj_con" $
	let (==>) (ty::Type Constants (h::Constraint)) expected =
		testCase (show_type ty) $
		isJust (proj_con ty) @?= expected
	in
	 [ (tyEq :$ tyBool) ==> True
	 , (tyOrd :$ tyBool) ==> True
	 , (tyFunctor :$ tyMaybe) ==> True
	 , (tyFunctor :$ tyIO) ==> True
	 , (tyMonad :$ tyIO) ==> True
	 , (tyTraversable :$ tyIO) ==> False
	 ]
 ]