{-# 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 ()
import Language.Symantic.Lib.Lambda ((~>))
import Language.Symantic.Helper.Data.Type.List

import Parsing.Test

-- * Tests
type Tys = Constants ++ '[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 (==>) 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 <$>) $ (`runParser` inp) $ unCF p
		p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
		p = typeG <* eoi in
	uncurry (==>) <$>
	 [ ("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 (==>) inp _exp = testCase inp $ got @?= Left ()
			where
			got :: Either () (TokType P.SourcePos)
			got = left (const ()) $ (`runParser` inp) $ unCF p
			p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
			p = typeG <* eoi in
		uncurry (==>) <$>
		 [ ("Bool, Int", ())
		 , ("(Bool -> Int) Char", ())
		 ]
	 , testGroup "Compiling errors" $
		let (==>) inp _exp = testCase inp $ got @?= Right (Left ())
			where
			got :: Either (P.ParseError Char P.Dec) (Either () (EType Tys))
			got = (left (const ()) . compile_EType <$>) $ (`runParser` inp) $ unCF p
			p :: Gram_Type P.SourcePos p => CF p (TokType P.SourcePos)
			p = typeG <* eoi in
		uncurry (==>) <$>
		 [ ("NonExistingType", ())
		 , ("Bool Int", ())
		 , ("[IO]", ())
		 , ("(->) IO", ())
		 , ("(->) Bool Int Char", ())
		 , ("Monad Eq", ())
		 ]
 , testGroup "proj_TyCon" $
	let (==>) (typ::Type Constants (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
	 ]
 ]