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

import Test.Tasty
import Test.Tasty.HUnit

import Control.Applicative (Applicative(..))
import Control.Arrow (left)
import Data.Maybe (isJust)
import Data.Proxy
import GHC.Exts (Constraint)
import Prelude hiding (exp)
import qualified Text.Megaparsec as P

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Lib (TyConsts)
import Language.Symantic.Lib.Lambda ((~>))
import Language.Symantic.Helper.Data.Type.List

import Parsing.Test

-- * Tests
type Tys = TyConsts ++ '[Proxy String]
instance
 ( ParsecC e s
 , Gram_Meta meta (P.ParsecT e s m)
 ) => Gram_Type meta (P.ParsecT e s m)

tests :: TestTree
tests = testGroup "Typing" $
 [ testGroup "compile_Type" $
	let run inp exp = testCase inp $ got @?= Right (Right exp)
		where
		got :: Either (P.ParseError Char P.Dec)
		              (Either (Error_Type P.SourcePos '[Proxy Token_Type])
		                      (EType Tys))
		got = compile_EType <$> P.runParser (unCF g) "" inp
		g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
		g = g_type <* eoi in
	let (==>) = run; infixr 0 ==> in
	 [ "Bool"                        ==> EType $ ty @Bool
	 , "[]"                          ==> EType $ ty @[]
	 , "[Char]"                      ==> EType $ ty @[] :$ ty @Char
	 , "[Char -> [Char]]"            ==> EType $ ty @[] :$ (ty @Char ~> ty @[] :$ ty @Char)
	 , "([])"                        ==> EType $ ty @[]
	 , "[()]"                        ==> EType $ ty @[] :$ ty @()
	 , "()"                          ==> EType $ ty @()
	 , "(())"                        ==> EType $ ty @()
	 , "(,)"                         ==> EType $ ty @(,)
	 , "((,))"                       ==> EType $ ty @(,)
	 , "(,) Int"                     ==> EType $ ty @(,) :$ ty @Int
	 , "(Bool)"                      ==> EType $ ty @Bool
	 , "((Bool))"                    ==> EType $ ty @Bool
	 , "(Bool, Int)"                 ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
	 , "((Bool, Int))"               ==> EType $ ty @(,) :$ ty @Bool :$ ty @Int
	 , "((Bool, Int), Char)"         ==> EType $ ty @(,) :$ (ty @(,) :$ ty @Bool :$ ty @Int) :$ ty @Char
	 , "(Bool, Int) -> Char"         ==> EType $ (ty @(,) :$ ty @Bool :$ ty @Int) ~> ty @Char
	 , "(Bool -> Int)"               ==> EType $ ty @Bool ~> ty @Int
	 , "String"                      ==> EType $ ty @[] :$ ty @Char
	 , "[Char] -> String"            ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
	 , "String -> [Char]"            ==> EType $ ty @[] :$ ty @Char ~> ty @[] :$ ty @Char
	 , "Maybe Bool"                  ==> EType $ ty @Maybe :$ ty @Bool
	 , "Either Bool Int"             ==> EType $ ty @Either :$ ty @Bool :$ ty @Int
	 , "Bool -> Int"                 ==> EType $ ty @Bool ~> ty @Int
	 , "(Bool -> Int) -> Char"       ==> EType $ (ty @Bool ~> ty @Int) ~> ty @Char
	 , "Bool -> (Int -> Char)"       ==> EType $ ty @Bool ~> (ty @Int ~> ty @Char)
	 , "Bool -> Int -> Char"         ==> EType $ ty @Bool ~> ty @Int ~> ty @Char
	 , "Bool -> (Int -> Char) -> ()" ==> EType $ ty @Bool ~> (ty @Int ~> ty @Char) ~> ty @()
	 , "IO"                          ==> EType $ ty @IO
	 , "Eq"                          ==> EType $ ty @Eq
	 , "Eq Bool"                     ==> EType $ ty @Eq :$ ty @Bool
	 , "Traversable IO"              ==> EType $ ty @Traversable :$ ty @IO
	 , "Monad IO"                    ==> EType $ ty @Monad :$ ty @IO
	 , "(->) Bool"                   ==> EType $ ty @(->) :$ ty @Bool
	 , "(->) (IO Bool)"              ==> EType $ ty @(->) :$ (ty @IO :$ ty @Bool)
	 , "Monad IO"                    ==> EType $ ty @Monad :$ ty @IO
	 ]
	 , testGroup "Parsing errors" $
		let run inp = testCase inp $ got @?= Left ()
			where
			got :: Either () (TokType P.SourcePos)
			got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
			g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
			g = g_type <* eoi in
		run <$>
		 [ "Bool, Int"
		 , "(Bool -> Int) Char"
		 ]
	 , testGroup "Compiling errors" $
		let run inp = testCase inp $ got @?= Right (Left ())
			where
			got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys))
			got = left (const ()) . compile_EType <$> P.runParser (unCF g) "" inp
			g :: Gram_Type P.SourcePos g => CF g (TokType P.SourcePos)
			g = g_type <* eoi in
		run <$>
		 [ "NonExistingType"
		 , "Bool Int"
		 , "[IO]"
		 , "(->) IO"
		 , "(->) Bool Int Char"
		 , "Monad Eq"
		 ]
 , testGroup "proj_TyCon" $
	let (==>) (typ::Type TyConsts (h::Constraint)) expected =
		testCase (show_Type typ) $
		isJust (proj_TyCon 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
	 ]
 ]