{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Compiling.Bool.Test where

import Test.Tasty

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

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Compiling.Term.Test

import Parsing.Test

-- * 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
-}

-- * Terms
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)

instance
 ( Inj_Token (Syntax Text) ts Bool
 {-, Tokenize (Syntax Text) (Syntax Text) ts-} ) =>
 TokenizeT (Syntax Text) (Syntax Text) ts (Proxy Bool) where
	tokenizeT _t (Syntax "bool" (ast_b : as)) = Just $ do
		b <- read_syntax ast_b
		Right $ (as,) $ EToken $ inj_token (Syntax "bool" [ast_b]) $
			Token_Term_Bool b
	tokenizeT _t (Syntax "xor" as) = Just $
		Right $ (as,) $ EToken $ inj_token (Syntax "xor" []) $
			Token_Term_Bool_xor
	tokenizeT _t (Syntax "not" as) = Just $
		Right $ (as,) $ EToken $ inj_token (Syntax "not" []) $
			Token_Term_Bool_not
	tokenizeT _t _sy = Nothing

-- * Tests
type Ifaces =
 [ Proxy Bool
 , Proxy (->)
 ]
(==>) = test_term_from (Proxy::Proxy Ifaces)

syBool b = Syntax "bool" [Syntax (Text.pack $ show b) []]

tests :: TestTree
tests = testGroup "Bool" $
 [ syBool True ==> Right (ty @Bool, True, "True")
 , Syntax "xor" [syBool True, syBool True] ==> Right
	 (ty @Bool, False, "((\\x0 -> (\\x1 -> x0 `xor` x1)) True) True")
 , syApp (syLam "x" (sy @Bool) (syVar "x")) (syBool True) ==> Right
	 (ty @Bool, True, "(\\x0 -> x0) True")
 , syApp
	 (syLam "x" (sy @Bool)
		 (Syntax "xor" [ syVar "x", syBool True ]))
	 (syBool True) ==> Right
	 (ty @Bool, False, "(\\x0 -> ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True) True" )
 , syLet "x" (syBool True)
	 (Syntax "xor" [ syVar "x", syBool True ]) ==> Right
	 (ty @Bool, False, "let x0 = True in ((\\x1 -> (\\x2 -> x1 `xor` x2)) x0) True")
 , testGroup "Error_Term" $
	 [ (syBool True `syApp` syBool True) ==> Left (ty @Bool,
		Right $ Error_Term_Constraint_Type $
		Right $ Constraint_Type_App $
		At (maybeRight $ tokenize $ syBool True) $
		EType $ ty @Bool)
	 , syApp
		 (syLam "x" (sy @Bool)
			 (Syntax "xor" [ syVar "x", syBool True ]))
		 (sy @Bool) ==> Left (ty @Bool,
		Left $ Error_Syntax_unsupported $
		sy @Bool)
	 , let syn = Syntax " "
		 [ syLam "x" (sy @Bool) (syVar "x")
		 ] in syn ==> Left (ty @Bool,
		Left $ Error_Syntax_unsupported syn)
	 , Syntax " "
		 [ syLam "x" (sy @Bool) (syVar "x")
		 , syBool True
		 , syBool True
		 ] ==> Left (ty @Bool,
		Right $ Error_Term_Constraint_Type $
		Right $ Constraint_Type_App $
		At (maybeRight $ tokenize $
			Syntax " "
			 [ syLam "x" (sy @Bool) (syVar "x")
			 , syBool True
			 ]) $
		EType $ ty @Bool)
	 , let syn =
			syLam "x" (sy @Bool .> sy @Bool)
			 (Syntax " " [syVar "x", syBool True]) in
		syApp syn (syBool True) ==> Left (ty @Bool,
		Right $ Error_Term_Constraint_Type $ Right $
		Constraint_Type_Eq
		 (Right $ At (maybeRight $ tokenize syn) $ EType $ (ty @Bool ~> ty @Bool))
		 (At (maybeRight $ tokenize $ syBool $ True) $ EType $ ty @Bool)
		 )
	 ]
 ]