]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Eq.hs
Fix comment typo.
[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 Control.Monad
7 import qualified Data.Eq as Eq
8 import Data.Proxy (Proxy(..))
9 import Prelude hiding ((==), (/=))
10
11 import Language.Symantic.Parsing
12 import Language.Symantic.Typing
13 import Language.Symantic.Compiling
14 import Language.Symantic.Interpreting
15 import Language.Symantic.Transforming
16 import Language.Symantic.Lib.Lambda
17
18 -- * Class 'Sym_Eq'
19 class Sym_Eq term where
20 (==) :: Eq a => term a -> term a -> term Bool; infix 4 ==
21 (/=) :: Eq a => term a -> term a -> term Bool; infix 4 /=
22
23 default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
24 default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
25
26 (==) = trans_map2 (==)
27 (/=) = trans_map2 (/=)
28
29 type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
30 type instance TyConsts_of_Iface (Proxy Eq) = Proxy Eq ': TyConsts_imported_by Eq
31 type instance TyConsts_imported_by Eq = '[]
32
33 instance Sym_Eq HostI where
34 (==) = liftM2 (Eq.==)
35 (/=) = liftM2 (Eq./=)
36 instance Sym_Eq TextI where
37 (==) = textI_infix "==" (infixN 4)
38 (/=) = textI_infix "/=" (infixN 4)
39 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
40 (==) = dupI2 @Sym_Eq (==)
41 (/=) = dupI2 @Sym_Eq (/=)
42
43 instance
44 ( Read_TyNameR TyName cs rs
45 , Inj_TyConst cs Eq
46 ) => Read_TyNameR TyName cs (Proxy Eq ': rs) where
47 read_TyNameR _cs (TyName "Eq") k = k (ty @Eq)
48 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
49 instance Show_TyConst cs => Show_TyConst (Proxy Eq ': cs) where
50 show_TyConst TyConstZ{} = "Eq"
51 show_TyConst (TyConstS c) = show_TyConst c
52
53 instance Proj_TyConC cs (Proxy Eq)
54 data instance TokenT meta (ts::[*]) (Proxy Eq)
55 = Token_Term_Eq_eq (EToken meta ts)
56 | Token_Term_Eq_ne (EToken meta ts)
57 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Eq))
58 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Eq))
59 instance -- CompileI
60 ( Inj_TyConst (TyConsts_of_Ifaces is) Bool
61 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
62 , Inj_TyConst (TyConsts_of_Ifaces is) Eq
63 , Proj_TyCon (TyConsts_of_Ifaces is)
64 , Compile is
65 ) => CompileI is (Proxy Eq) where
66 compileI tok ctx k =
67 case tok of
68 Token_Term_Eq_eq tok_a -> from_op (==) tok_a
69 Token_Term_Eq_ne tok_a -> from_op (/=) tok_a
70 where
71 from_op (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) tok_a =
72 compileO tok_a ctx $ \ty_a (TermO a) ->
73 check_TyCon (At (Just tok_a) (ty @Eq :$ ty_a)) $ \TyCon ->
74 k (ty_a ~> ty @Bool) $ TermO $
75 \c -> lam $ op (a c)
76 instance -- TokenizeT
77 Inj_Token meta ts Eq =>
78 TokenizeT meta ts (Proxy Eq) where
79 tokenizeT _t = mempty
80 { tokenizers_infix = tokenizeTMod []
81 [ tokenize1 "==" (infixN 4) Token_Term_Eq_eq
82 , tokenize1 "/=" (infixN 4) Token_Term_Eq_ne
83 ]
84 }
85 instance Gram_Term_AtomsT meta ts (Proxy Eq) g