symantic-lib/Language/Symantic/Lib/Eq.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Eq'.
   4 module Language.Symantic.Lib.Eq where
   5
   6 import Prelude hiding ((==), (/=))
   7 import qualified Data.Eq as Eq
   8
   9 import Language.Symantic
  10 import Language.Symantic.Lib.Bool (tyBool)
  11 import Language.Symantic.Lib.Function (a0)
  12
  13 -- * Class 'Sym_Eq'
  14 type instance Sym Eq = Sym_Eq
  15 class Sym_Eq term where
  16         (==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
  17         (/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
  18
  19         default (==) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
  20         default (/=) :: Sym_Eq (UnT term) => Trans term => Eq a => term a -> term a -> term Bool
  21
  22         (==) = trans2 (==)
  23         (/=) = trans2 (/=)
  24
  25 -- Interpreting
  26 instance Sym_Eq Eval where
  27         (==) = eval2 (Eq.==)
  28         (/=) = eval2 (Eq./=)
  29 instance Sym_Eq View where
  30         (==) = viewInfix "==" (infixN 4)
  31         (/=) = viewInfix "/=" (infixN 4)
  32 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Dup r1 r2) where
  33         (==) = dup2 @Sym_Eq (==)
  34         (/=) = dup2 @Sym_Eq (/=)
  35
  36 -- Transforming
  37 instance (Sym_Eq term, Sym_Lambda term) => Sym_Eq (BetaT term)
  38
  39 -- Typing
  40 instance NameTyOf Eq where
  41         nameTyOf _c = ["Eq"] `Mod` "Eq"
  42 instance FixityOf Eq
  43 instance ClassInstancesFor Eq
  44 instance TypeInstancesFor Eq
  45
  46 -- Compiling
  47 instance Gram_Term_AtomsFor src ss g Eq
  48 instance (Source src, SymInj ss Eq) => ModuleFor src ss Eq where
  49         moduleFor = ["Eq"] `moduleWhere`
  50          [ "==" `withInfixN` 4 := teEq_eq
  51          , "/=" `withInfixN` 4 := teEq_ne
  52          ]
  53
  54 -- ** 'Type's
  55 tyEq :: Source src => Type src vs a -> Type src vs (Eq a)
  56 tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a
  57
  58 -- ** 'Term's
  59 teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))
  60 teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)
  61 teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)