{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Lib.Bool.Test where

import Test.Tasty

import Data.Proxy (Proxy(..))
import Prelude hiding ((&&), not, (||))

import Language.Symantic
import Language.Symantic.Lib
-- import Language.Symantic.Lib.Lambda ((~>))
import Compiling.Test

type SS =
 [ Proxy Bool
 , Proxy (->)
 , Proxy Integer
 , Proxy []
 , Proxy Char
 ]
(==>) = readTe @() @SS

tests :: TestTree
tests = testGroup "Bool" $
 [ "True"                           ==> Right (tyBool, True , "True")
 , "xor True True"                  ==> Right (tyBool, False, "True `xor` True")
 , "xor False True"                 ==> Right (tyBool, True , "False `xor` True")
 , "True `xor` True"                ==> Right (tyBool, False, "True `xor` True")
 , "(\\(xy:Bool) -> xy) True"       ==> Right (tyBool, True , "(\\x0 -> x0) True")
 , "(\\(False:Bool) -> False) True" ==> Right (tyBool, True , "(\\x0 -> x0) True")
 , "(\\(lett:Bool) -> lett) True"   ==> Right (tyBool, True , "(\\x0 -> x0) True")
 , "(\\(x:Bool) -> xor x x) True"   ==> Right (tyBool, False, "(\\x0 -> x0 `xor` x0) True")
 , "let x = True in xor x True"     ==> Right (tyBool, False, "let x0 = True in x0 `xor` True")
 , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right (tyBool, True, "(\\x0 -> x0) (False `xor` True)")
 , testGroup "Error_Term"
	 [ "True True" ==> Left (tyBool,
		Right $ Error_Term_Beta $
		Error_Beta_Term_not_a_function $
		TypeVT $ tyBool @_ @'[])
	 , "x" ==> Left (tyBool,
		Right $ Error_Term_unknown $ NameTe "x")
	 , "x `xor` True" ==> Left (tyBool,
		Right $ Error_Term_unknown $ NameTe "x")
	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (tyBool,
		Right $ Error_Term_unknown $ NameTe "Bool")
	 , "(\\(x:Bool) -> x) True True" ==> Left (tyBool,
		Right $ Error_Term_Beta $
		Error_Beta_Term_not_a_function $
		TypeVT $ tyBool @_ @'[])
	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (tyBool,
		Right $ Error_Term_Beta $ Error_Beta_Unify $
		Error_Unify_Const_mismatch
		 (TypeVT $ tyFun @_ @'[])
		 (TypeVT $ tyBool @_ @'[]))
	 ]
 ]

-- * Class 'Sym_Bool_Vars'
-- | A few boolean variables.
class Sym_Bool_Vars repr where
	x :: repr Bool
	y :: repr Bool
	z :: repr Bool
instance Sym_Bool_Vars View where
	x = View $ \_p _v -> "x"
	y = View $ \_p _v -> "y"
	z = View $ \_p _v -> "z"
{-
instance -- Trans_Boo_Const
 ( Sym_Bool repr
 , Sym_Bool_Vars repr
 ) => Sym_Bool_Vars (Trans_Bool_Const repr) where
	x = trans_lift x
	y = trans_lift y
	z = trans_lift z
-}

-- * EDSL tests
te1 = bool True && bool False
te2 = (bool True && bool False) ||  (bool True && bool True)
te3 = (bool True ||  bool False) && (bool True ||  bool True)
te4 = bool True && not (bool False)
te5 = bool True && not x
te6 = x `xor` y
te7 = (x `xor` y) `xor` z
te8 = x `xor` (y `xor` bool True)