{-# 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 NameTyOf Eq where
        nameTyOf _c = ["Eq"] `Mod` "Eq"
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 (/=)