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 (Proxy 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 FixityOf Eq
  41 instance ClassInstancesFor Eq
  42 instance TypeInstancesFor Eq
  43
  44 -- Compiling
  45 instance Gram_Term_AtomsFor src ss g Eq
  46 instance (Source src, Inj_Sym ss Eq) => ModuleFor src ss Eq where
  47         moduleFor _s = ["Eq"] `moduleWhere`
  48          [ "==" `withInfixN` 4 := teEq_eq
  49          , "/=" `withInfixN` 4 := teEq_ne
  50          ]
  51
  52 -- ** 'Type's
  53 tyEq :: Source src => Type src vs a -> Type src vs (Eq a)
  54 tyEq a = tyConstLen @(K Eq) @Eq (lenVars a) `tyApp` a
  55
  56 -- ** 'Term's
  57 teEq_eq, teEq_ne :: TermDef Eq '[Proxy a] (Eq a #> (a -> a -> Bool))
  58 teEq_eq = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (==)
  59 teEq_ne = Term (tyEq a0) (a0 ~> a0 ~> tyBool) $ teSym @Eq $ lam2 (/=)