{-# 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.Map.Strict (Map)
import Data.Maybe (isJust)
import Data.NonNull (NonNull)
import Data.Proxy
import Data.Ratio (Ratio)
import Data.Text (Text)
import Data.List.NonEmpty (NonEmpty)
import GHC.Exts (Constraint)
import Prelude hiding (exp)
import qualified Data.Function as Fun
import qualified Data.Map.Strict as Map
import qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import qualified System.IO as IO
import qualified Text.Megaparsec as P

import Language.Symantic.Grammar
import Language.Symantic
import Language.Symantic.Lib hiding ((<$>), (<*), show)

import Grammar.Megaparsec

--
-- P.ParsecT instances
--
instance
 ( ParsecC e s
 , Gram_Source src (P.ParsecT e s m)
 ) => Gram_Type src (P.ParsecT e s m)

-- * Tests
type SS =
 [ Proxy (->)
 , Proxy Bool
 , Proxy []
 , Proxy ()
 , Proxy (,)
 , Proxy Char
 , Proxy Either
 , Proxy Int
 , Proxy Integer
 , Proxy IO
 , Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy Ordering
 , Proxy Map
 , Proxy Maybe
 , Proxy NonNull
 , Proxy Ratio
 , Proxy Text
 , Proxy Applicative
 , Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Integral
 , Proxy Monad
 , Proxy Monoid
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 , Proxy Seqs.IsSequence
 , Proxy Seqs.SemiSequence
 , Proxy Show
 , Proxy Traversable
 ]
type SRC = SrcTe (NonEmpty P.SourcePos) SS

cs :: Source src => Name2Type src
cs =
	Map.insert "String"
	 (Len2Type $ \len -> TypeT $
		tyConstLen @(K [])   @[]   len `tyApp`
		tyConstLen @(K Char) @Char len) $
	inj_Name2Type (Proxy @SS)

tests :: TestTree
tests = testGroup "Typing" $
 [ testGroup "readType" $
	let run inp (TypeT exp :: TypeT SRC '[]) =
		testCase inp $ got @?= Right (Right $ TypeVT exp)
		where
		got :: Either (P.ParseError Char P.Dec)
		              (Either (Error_Type SRC) (TypeVT SRC))
		got = readType cs <$> P.runParser (unCF g) "" inp
		g :: Gram_Type SRC g => CF g (AST_Type SRC)
		g = g_type <* eoi in
	let (==>) = run; infixr 0 ==> in
	 [ "Bool"                        ==> TypeT $ tyBool
	 , "(->) Bool"                   ==> TypeT $ tyFun `tyApp` tyBool
	 , "[]"                          ==> TypeT $ tyConst @(K []) @[]
	 , "[Char]"                      ==> TypeT $ tyList tyChar
	 , "[Char -> [Char]]"            ==> TypeT $ tyList (tyChar ~> tyList tyChar)
	 , "([])"                        ==> TypeT $ tyConst @(K []) @[]
	 , "[()]"                        ==> TypeT $ tyList tyUnit
	 , "()"                          ==> TypeT $ tyUnit
	 , "(())"                        ==> TypeT $ tyUnit
	 , "(,)"                         ==> TypeT $ tyConst @(K (,)) @(,)
	 , "((,))"                       ==> TypeT $ tyConst @(K (,)) @(,)
	 , "(,) Int"                     ==> TypeT $ tyConst @(K (,)) @(,) `tyApp` tyInt
	 , "(Bool)"                      ==> TypeT $ tyBool
	 , "((Bool))"                    ==> TypeT $ tyBool
	 , "(Bool, Int)"                 ==> TypeT $ tyBool `tyTuple2` tyInt
	 , "((Bool, Int))"               ==> TypeT $ tyBool `tyTuple2` tyInt
	 , "((Bool, Int), Char)"         ==> TypeT $ (tyBool `tyTuple2` tyInt) `tyTuple2` tyChar
	 , "(Bool, Int) -> Char"         ==> TypeT $ (tyBool `tyTuple2` tyInt) ~> tyChar
	 , "(Bool -> Int)"               ==> TypeT $ tyBool ~> tyInt
	 , "String"                      ==> TypeT $ tyList tyChar
	 , "[Char] -> String"            ==> TypeT $ tyList tyChar ~> tyList tyChar
	 , "String -> [Char]"            ==> TypeT $ tyList tyChar ~> tyList tyChar
	 , "Maybe Bool"                  ==> TypeT $ tyMaybe tyBool
	 , "Either Bool Int"             ==> TypeT $ tyEither tyBool tyInt
	 , "Bool -> Int"                 ==> TypeT $ tyBool ~> tyInt
	 , "(Bool -> Int) -> Char"       ==> TypeT $ (tyBool ~> tyInt) ~> tyChar
	 , "Bool -> (Int -> Char)"       ==> TypeT $ tyBool ~> (tyInt ~> tyChar)
	 , "Bool -> Int -> Char"         ==> TypeT $ tyBool ~> tyInt ~> tyChar
	 , "Bool -> (Int -> Char) -> ()" ==> TypeT $ tyBool ~> (tyInt ~> tyChar) ~> tyUnit
	 , "IO"                          ==> TypeT $ tyConst @(K IO) @IO
	 , "Traversable IO"              ==> TypeT $ tyTraversable (tyConst @(K IO) @IO)
	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
	 , "(->) (IO Bool)"              ==> TypeT $ tyConst @(K (->)) @(->) `tyApp` (tyIO tyBool)
	 , "Monad IO"                    ==> TypeT $ tyMonad (tyConst @(K IO) @IO)
	 , "Eq"                          ==> TypeT $ tyConst @(K Eq) @Eq
	 , "Eq Bool"                     ==> TypeT $ tyEq tyBool
	 ]
	 , testGroup "Parsing errors" $
		let run inp = testCase inp $ got @?= Left ()
			where
			got :: Either () (AST_Type SRC)
			got = left (\(_::P.ParseError (P.Token String) P.Dec) -> ()) $ P.runParser (unCF g) "" inp
			g :: Gram_Type SRC g => CF g (AST_Type SRC)
			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 () (TypeVT SRC))
			got = left (Fun.const ()) . readType cs <$> P.runParser (unCF g) "" inp
			g :: Gram_Type SRC g => CF g (AST_Type SRC)
			g = g_type <* eoi in
		run <$>
		 [ "NonExistingType"
		 , "Bool Int"
		 , "[IO]"
		 , "(->) IO"
		 , "(->) Bool Int Char"
		 , "Monad Eq"
		 ]
 , testGroup "proveConstraint" $
	let (==>) (typ::Type SRC '[] (t::Constraint)) expected =
		testCase (show typ) $
		isJust (proveConstraint typ) @?= expected in
	 [ tyEq          tyBool                      ==> True
	 , tyOrd         tyBool                      ==> True
	 , tyFunctor     (tyConst @(K Maybe) @Maybe) ==> True
	 , tyFunctor     (tyConst @(K IO) @IO)       ==> True
	 , tyMonad       (tyConst @(K IO) @IO)       ==> True
	 , tyTraversable (tyConst @(K IO) @IO)       ==> False
	 ]
 ]