{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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.Functor.Identity (Identity(..))
import Data.List.NonEmpty (NonEmpty)
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 GHC.Exts (Constraint)
import Prelude hiding (exp)
import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Strict as SS
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 qualified Text.Megaparsec.Prim as P

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

import Grammar.Megaparsec ()

-- * 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

impsTy :: Imports NameTy
impsTy = importTypes @SS []

modsTy :: Source src => ModulesTy src
modsTy =
	Map.insert ([] `Mod` "String")
	 (TypeTLen $ \len -> TypeT $
		tyConstLen @(K [])   @[]   len `tyApp`
		tyConstLen @(K Char) @Char len) $
	modulesTyInj @SS

parseTy ::
 forall src g err inp.
 g ~ P.ParsecT err inp (SS.StateT (Imports NameTy, ModulesTy src) Identity) =>
 P.MonadParsec err inp (P.ParsecT err inp g) =>
 Gram_Type src g =>
 P.Token inp ~ Char =>
 inp -> Either (P.ParseError Char err) (AST_Type src)
parseTy inp =
	runIdentity $
	MC.evalStateStrict (impsTy, modsTy @src) $
	P.runParserT g "" inp
	where g = unCF $ g_type <* eoi

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 <$> parseTy inp
		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) -> ()) $ parseTy inp in
		run <$>
		 [ "Bool, Int"
		 , "(Bool -> Int) Char"
		 , "NonExistingType"
		 ]
	 , 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 <$> parseTy inp in
		run <$>
		 [ "Bool Int"
		 , "[IO]"
		 , "(->) IO"
		 , "(->) Bool Int Char"
		 , "Monad Eq"
		 ]
 , testGroup "proveConstraint" $
	let (==>) (typ::Type SRC SS (t::Constraint)) expected =
		let imps = importTypes @SS [] in
		let conf = config_Doc_Type{config_Doc_Type_imports = imps} in
		testCase (showType conf 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
	 ]
 ]