{-# 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 (/=)