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

import Control.Monad
import Data.Proxy (Proxy(..))
import Prelude hiding ((==), (/=))
import qualified Data.Eq as Eq

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

-- * Class 'Sym_Eq'
class Sym_Eq term where
	(==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
	(/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
	
	default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
	default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
	
	(==) = trans_map2 (==)
	(/=) = trans_map2 (/=)

type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
type instance TyConsts_of_Iface (Proxy Eq) = Proxy Eq ': TyConsts_imported_by (Proxy Eq)
type instance TyConsts_imported_by (Proxy Eq) = '[]

instance Sym_Eq HostI where
	(==) = liftM2 (Eq.==)
	(/=) = liftM2 (Eq./=)
instance Sym_Eq TextI where
	(==) = textI_infix "==" (infixN 4)
	(/=) = textI_infix "/=" (infixN 4)
instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
	(==) = dupI2 @Sym_Eq (==)
	(/=) = dupI2 @Sym_Eq (/=)

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

instance Proj_TyConC cs (Proxy Eq)
data instance TokenT meta (ts::[*]) (Proxy Eq)
 = Token_Term_Eq_eq (EToken meta ts)
 | Token_Term_Eq_ne (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Eq))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Eq))

instance -- CompileI
 ( Inj_TyConst cs Bool
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Eq
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Eq) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Eq_eq tok_a -> from_op (==) tok_a
		 Token_Term_Eq_ne tok_a -> from_op (/=) tok_a
		where
		from_op (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) tok_a =
			compile tok_a ctx $ \ty_a (Term a) ->
			check_TyCon (At (Just tok_a) (ty @Eq :$ ty_a)) $ \TyCon ->
			k (ty_a ~> ty @Bool) $ Term $
			 \c -> lam $ op (a c)
instance -- TokenizeT
 Inj_Token meta ts Eq =>
 TokenizeT meta ts (Proxy Eq) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "==" (infixN 4) Token_Term_Eq_eq
		 , tokenize1 "/=" (infixN 4) Token_Term_Eq_ne
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Eq) g