{-# 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 Prelude hiding (and, not, or)

import Language.LOL.Symantic.Repr
import Language.LOL.Symantic.Expr
import qualified Expr.Lambda.Test as Lambda.Test
import qualified Expr.Bool.Test as Bool.Test
import qualified Expr.Maybe.Test as Maybe.Test

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