]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Eq.hs
Add TyApp pattern synonyms (:$) and (:@).
[haskell/symantic.git] / 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 (/=)