{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Bool'.
module Language.Symantic.Lib.Bool where

import Control.Monad
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((&&), not, (||))
import qualified Data.Bool as Bool
import qualified Data.Text as Text

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class 'Sym_Bool'
class Sym_Bool term where
	bool ::      Bool -> term Bool
	not  :: term Bool -> term Bool
	(&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&
	(||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
	xor  :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
	xor x y = (x || y) && not (x && y)
	
	default bool :: Trans t term =>        Bool -> t term Bool
	default not  :: Trans t term => t term Bool -> t term Bool
	default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
	default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
	
	bool = trans_lift . bool
	not  = trans_map1 not
	(&&) = trans_map2 (&&)
	(||) = trans_map2 (||)

type instance Sym_of_Iface (Proxy Bool) = Sym_Bool
type instance TyConsts_of_Iface (Proxy Bool) = Proxy Bool ': TyConsts_imported_by (Proxy Bool)
type instance TyConsts_imported_by (Proxy Bool) =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Ord
 , Proxy Show
 ]

instance Sym_Bool HostI where
	bool = HostI
	not  = liftM Bool.not
	(&&) = liftM2 (Bool.&&)
	(||) = liftM2 (Bool.||)
instance Sym_Bool TextI where
	bool o = TextI $ \_p _v ->
		Text.pack (show o)
	not  = textI1 "not"
	(&&) = textI_infix "&&"    (infixR 3)
	(||) = textI_infix "||"    (infixR 2)
	xor  = textI_infix "`xor`" (infixR 2)
instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
	bool b = bool b `DupI` bool b
	not  = dupI1 @Sym_Bool not
	(&&) = dupI2 @Sym_Bool (&&)
	(||) = dupI2 @Sym_Bool (||)
	xor  = dupI2 @Sym_Bool xor

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Bool
 ) => Read_TyNameR TyName cs (Proxy Bool ': rs) where
	read_TyNameR _cs (TyName "Bool") k = k (ty @Bool)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Bool ': cs) where
	show_TyConst TyConstZ{} = "Bool"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyFamC cs TyFam_MonoElement Bool

instance -- Proj_TyConC
 ( Proj_TyConst cs Bool
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Bool))
 ) => Proj_TyConC cs (Proxy Bool) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Bool)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Enum)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)    -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Bool)
 = Token_Term_Bool Bool
 | Token_Term_Bool_not
 | Token_Term_Bool_and
 | Token_Term_Bool_or
 | Token_Term_Bool_xor
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Bool))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Bool))

instance -- CompileI
 ( Inj_TyConst cs Bool
 , Inj_TyConst cs (->)
 ) => CompileI cs is (Proxy Bool) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Bool b -> k (ty @Bool) $ Term $ \_c -> bool b
		 Token_Term_Bool_not -> op1_from not
		 Token_Term_Bool_and -> op2_from (&&)
		 Token_Term_Bool_or  -> op2_from (||)
		 Token_Term_Bool_xor -> op2_from xor
		where
		op1_from
		 (op::forall term. Sym_Bool term => term Bool -> term Bool) =
			k (ty @Bool ~> ty @Bool) $ Term $ \_c -> lam op
		op2_from
			(op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
			k (ty @Bool ~> ty @Bool ~> ty @Bool) $ Term $ \_c -> lam $ lam . op
instance -- TokenizeT
 Inj_Token meta ts Bool =>
 TokenizeT meta ts (Proxy Bool) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize0 "False" infixN5 $  Token_Term_Bool False
		 , tokenize0 "True"  infixN5 $  Token_Term_Bool True
		 , tokenize0 "not"   infixN5    Token_Term_Bool_not
		 , tokenize0 "and"   (infixR 3) Token_Term_Bool_and
		 , tokenize0 "or"    (infixR 2) Token_Term_Bool_or
		 , tokenize0 "xor"   (infixR 2) Token_Term_Bool_xor
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Bool) g