{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Rank2Types #-}

module Repr.Host.Test where

-- import Data.Function (($))
-- import Data.Functor.Identity (Identity)
import Test.Tasty
import Test.Tasty.HUnit

import TFHOE.Type
import TFHOE.Repr
import TFHOE.Expr
import qualified Expr.Fun.Test as Fun.Test
import qualified Expr.Bool.Test as Bool.Test

tests :: TestTree
tests = testGroup "Host" $
	let (==>) (expr::forall repr. Expr_from_Type (Type_Fun_Bool_End IO) repr => repr h) expected =
		testCase ((string_repr :: Repr_String IO _h -> String) $ expr) $
			(>>= (@?= expected)) $
				host_repr expr in
 [ testGroup "Bool"
	 [ Bool.Test.e1 ==> False
	 , Bool.Test.e2 ==> True
	 , Bool.Test.e3 ==> True
	 , Bool.Test.e4 ==> True
	 ]
 , testGroup "Fun"
	 [ testGroup "Bool"
		 [ (Fun.Test.e1 `app` bool True  `app` bool True)  ==> False
		 , (Fun.Test.e1 `app` bool True  `app` bool False) ==> True
		 , (Fun.Test.e1 `app` bool False `app` bool True)  ==> True
		 , (Fun.Test.e1 `app` bool False `app` bool False) ==> False
		 
		 , (Fun.Test.e2 `app` bool True  `app` bool True)  ==> False
		 , (Fun.Test.e2 `app` bool True  `app` bool False) ==> True
		 , (Fun.Test.e2 `app` bool False `app` bool True)  ==> True
		 , (Fun.Test.e2 `app` bool False `app` bool False) ==> False
		 
		 , Fun.Test.e3 ==> True
		 , Fun.Test.e4 ==> True
		 
		 , (Fun.Test.e5 `app` bool True  `app` bool True)  ==> True
		 , (Fun.Test.e5 `app` bool True  `app` bool False) ==> False
		 , (Fun.Test.e5 `app` bool False `app` bool True)  ==> False
		 , (Fun.Test.e5 `app` bool False `app` bool False) ==> False
		 
		 , Fun.Test.e6 ==> False
		 , (Fun.Test.e7 `app` val id) ==> True
		 , (Fun.Test.e7 `app` val neg) ==> False
		 ]
	 ]
 {-, testGroup "If"
	 [ If.e1 ==> "if True then False else True"
	 , If.e2 ==> "if True & True then False else True"
	 ]
 -}]