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

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

import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0)

-- * Class 'Sym_Eq'
type instance Sym Eq = 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 (==) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
	default (/=) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
	
	(==) = trans2 (==)
	(/=) = trans2 (/=)

-- Interpreting
instance Sym_Eq Eval where
	(==) = eval2 (Eq.==)
	(/=) = eval2 (Eq./=)
instance Sym_Eq View where
	(==) = viewInfix "==" (infixN 4)
	(/=) = viewInfix "/=" (infixN 4)
instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
	(==) = dup2 @Sym_Eq (==)
	(/=) = dup2 @Sym_Eq (/=)

-- Transforming
instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)

-- Typing
instance FixityOf Eq
instance ClassInstancesFor Eq
instance TypeInstancesFor Eq

-- Compiling
instance Gram_Term_AtomsFor src ss g Eq
instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where
	moduleFor = ["Eq"] `moduleWhere`
	 [ "==" `withInfixN` 4 := teEq_eq
	 , "/=" `withInfixN` 4 := teEq_ne
	 ]

-- ** 'Type's
tyEq :: Source src => Type src vs a -> Type src vs (Eq a)
tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a

-- ** 'Term's
teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))
teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)
teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)