{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}

module Expr.Traversable.Test where

import Test.Tasty
import Test.Tasty.HUnit

import qualified Control.Arrow as Arrow
import qualified Control.Monad as Monad
import qualified Data.Functor as Functor
import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((&&), not, (||), (==), (<$>), (+), Applicative(..), Monad(..), Traversable(..))

import Language.Symantic.Type
import Language.Symantic.Expr as Expr
import Language.Symantic.Repr

import AST.Test

-- * Expressions
t = bool True
f = bool False
e1 = traverse (val Right)
              (list $ int Functor.<$> [1..3])

-- * Tests
type Ex lam = Expr_Root
 (   Expr_Lambda_App lam
 .|. Expr_Lambda_Val lam
 .|. Expr_List lam
 .|. Expr_Maybe lam
 .|. Expr_Int
 .|. Expr_Bool
 .|. Expr_Functor lam
 .|. Expr_Applicative lam
 .|. Expr_Traversable lam
 .|. Expr_Either
 )
ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)

(==>) ast expected =
	testCase (show ast) $
	case ex_from ast of
	 Left err -> Left err @?= snd `Arrow.left` expected
	 Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
		case expected of
		 Left (_, err) -> Right ("…"::String) @?= Left err
		 Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
			(Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
			case ty `eq_type` ty_expected of
			 Nothing -> Monad.return $ Left $
				error_expr (Proxy::Proxy (Ex Identity)) $
				Error_Expr_Type_mismatch ast
				 (Exists_Type ty)
				 (Exists_Type ty_expected)
			 Just Refl -> do
				let h = runIdentity $ host_from_expr r
				Monad.return $
					Right
					 ( ty
					 , h
					 , text_from_expr r
					 -- , (text_from_expr :: Repr_Text Identity h -> Text) r
					 )

tests :: TestTree
tests = testGroup "Traversable"
 [ AST "traverse"
	 [ AST "val"
		 [ AST "x" [], AST "Int" []
		 , AST "just" [ AST "var" [ AST "x" [] ] ]
		 ]
	 , AST "list"
		 [ AST "Int" []
		 , AST "int" [AST "1" []]
		 , AST "int" [AST "2" []]
		 , AST "int" [AST "3" []]
		 ]
	 ] ==> Right
	 ( type_maybe (type_list type_int)
	 , Just [1, 2, 3]
	 , "traverse (\\x0 -> just x0) [1, 2, 3]" )
 , AST "traverse"
	 [ AST "val"
		 [ AST "x" [], AST "Int" []
		 , AST "right" [ AST "Int" [], AST "var" [ AST "x" [] ] ]
		 ]
	 , AST "list"
		 [ AST "Int" []
		 , AST "int" [AST "1" []]
		 , AST "int" [AST "2" []]
		 , AST "int" [AST "3" []]
		 ]
	 ] ==> Right
	 ( type_either type_int (type_list type_int)
	 , Right [1, 2, 3]
	 , "traverse (\\x0 -> right x0) [1, 2, 3]" )
 ]