{-# 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.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Lib.Bool
import Language.Symantic.Lib.Lambda ((~>))
import Compiling.Term.Test

type Ifaces =
 [ Proxy Bool
 , Proxy (->)
 , Proxy Integer
 ]
(==>) = test_compile @Ifaces

tests :: TestTree
tests = testGroup "Bool" $
 [ "True"            ==> Right (ty @Bool, True, "True")
 , "xor True True"   ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
 , "xor False True"  ==> Right (ty @Bool, True, "((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True")
 , "True `xor` True" ==> Right (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
 , "(\\(xy:Bool) -> xy) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
 , "(\\(False:Bool) -> False) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
 , "(\\(False:Bool) -> False) (False `xor` True)" ==> Right
	 (ty @Bool, True, "(\\x0 -> x0) (((\\x0 -> (\\x1 -> x0 `xor` x1)) False) True)")
 , "(\\(lett:Bool) -> lett) True" ==> Right (ty @Bool, True, "(\\x0 -> x0) True")
 , "(\\(x:Bool) -> xor x x) True" ==> Right
	 (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) x0) True")
 , "let x = True in xor x True" ==> Right
	 (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
 , testGroup "Error_Term"
	 [ "True True" ==> Left (ty @Bool,
		Right $ Error_Term_Con_Type $
		Right $ Con_TyApp $
		At (maybeRight $ test_tokenizer "True") $
		EType $ ty @Bool)
	 , "(\\(x:Bool) -> x `xor` True) Bool" ==> Left (ty @Bool,
		Right $ Error_Term_unbound $ Term_Name "Bool")
	 , "(\\(x:Bool) -> x) True True" ==> Left (ty @Bool,
		Right $ Error_Term_Con_Type $
		Right $ Con_TyApp $
		At (maybeRight $ test_tokenizer "(\\(x:Bool) -> x) True") $
		EType $ ty @Bool)
	 , "(\\(x:Bool -> Bool) -> x True) True" ==> Left (ty @Bool,
		Right $ Error_Term_Con_Type $ Right $
		Con_TyEq
		 (Right $ At (maybeRight $ test_tokenizer "(\\(x:Bool -> Bool) -> x True)") $
			EType $ (ty @Bool ~> ty @Bool))
		 (At (maybeRight $ test_tokenizer "True") $
			EType $ ty @Bool)
		 )
	 ]
 ]

-- * 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 TextI where
	x = TextI $ \_p _v -> "x"
	y = TextI $ \_p _v -> "y"
	z = TextI $ \_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)