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

module Expr.Monad.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.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((&&), not, (||), (==), (<$>), (+), Applicative(..), Monad(..), Monad(..))

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 = (>>=) (list $ int Functor.<$> [1..3])
           (lam $ \i -> list [i, i])

-- * Tests
type Ex = Expr_Root
 (   Expr_Lambda
 .|. Expr_List
 .|. Expr_Maybe
 .|. Expr_Int
 .|. Expr_Bool
 .|. Expr_Functor
 .|. Expr_Applicative
 .|. Expr_Monad
 .|. Expr_Either
 )
ex_from = root_expr_from (Proxy::Proxy Ex)

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

tests :: TestTree
tests = testGroup "Monad"
 [ AST ">>="
	 [ AST "list"
		 [ AST "Int" []
		 , AST "int" [AST "1" []]
		 , AST "int" [AST "2" []]
		 , AST "int" [AST "3" []]
		 ]
	 , AST "\\"
		 [ AST "x" [], AST "Int" []
		 , AST "list"
			 [ AST "Int" []
			 , AST "var" [ AST "x" [] ]
			 , AST "var" [ AST "x" [] ]
			 ]
		 ]
	 ] ==> Right
	 ( type_list type_int
	 , [1, 1, 2, 2, 3, 3]
	 , "[1, 2, 3] >>= (\\x0 -> [x0, x0])" )
 , AST ">>="
	 [ AST "just" [ AST "int" [AST "1" []] ]
	 , AST "\\"
		 [ AST "x" [], AST "Int" []
		 , AST "nothing"
			 [ AST "Int" []
			 ]
		 ]
	 ] ==> Right
	 ( type_maybe type_int
	 , Nothing
	 , "just 1 >>= (\\x0 -> nothing)" )
 , AST ">>="
	 [ AST "right"
		 [ AST "Bool" []
		 , AST "int" [AST "1" []]
		 ]
	 , AST "\\"
		 [ AST "x" [], AST "Int" []
		 , AST "left"
			 [ AST "Int" []
			 , AST "bool" [AST "True" []]
			 ]
		 ]
	 ] ==> Right
	 ( type_either type_bool type_int
	 , Left True
	 , "right 1 >>= (\\x0 -> left True)" )
 ]