]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Eq.hs
Fix Lib.Text.
[haskell/symantic.git] / 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.Parsing.Grammar
13 import Language.Symantic.Typing
14 import Language.Symantic.Compiling
15 import Language.Symantic.Interpreting
16 import Language.Symantic.Transforming.Trans
17 import Language.Symantic.Lib.Lambda
18
19 -- * Class 'Sym_Eq'
20 class Sym_Eq term where
21 (==) :: Eq a => term a -> term a -> term Bool
22 (/=) :: Eq a => term a -> term a -> term Bool
23
24 default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
25 default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
26
27 (==) = trans_map2 (==)
28 (/=) = trans_map2 (/=)
29
30 infix 4 ==
31 infix 4 /=
32
33 type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
34 type instance Consts_of_Iface (Proxy Eq) = Proxy Eq ': Consts_imported_by Eq
35 type instance Consts_imported_by Eq = '[]
36
37 instance Sym_Eq HostI where
38 (==) = liftM2 (Eq.==)
39 (/=) = liftM2 (Eq./=)
40 instance Sym_Eq TextI where
41 (==) = textI_infix "==" (infixN 4)
42 (/=) = textI_infix "/=" (infixN 4)
43 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
44 (==) = dupI2 (Proxy @Sym_Eq) (==)
45 (/=) = dupI2 (Proxy @Sym_Eq) (/=)
46
47 instance
48 ( Read_TypeNameR Type_Name cs rs
49 , Inj_Const cs Eq
50 ) => Read_TypeNameR Type_Name cs (Proxy Eq ': rs) where
51 read_typenameR _cs (Type_Name "Eq") k = k (ty @Eq)
52 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
53 instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
54 show_const ConstZ{} = "Eq"
55 show_const (ConstS c) = show_const c
56
57 instance Proj_ConC cs (Proxy Eq)
58 data instance TokenT meta (ts::[*]) (Proxy Eq)
59 = Token_Term_Eq_eq (EToken meta ts)
60 | Token_Term_Eq_ne (EToken meta ts)
61 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Eq))
62 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Eq))
63 instance -- CompileI
64 ( Inj_Const (Consts_of_Ifaces is) Bool
65 , Inj_Const (Consts_of_Ifaces is) (->)
66 , Inj_Const (Consts_of_Ifaces is) Eq
67 , Proj_Con (Consts_of_Ifaces is)
68 , Compile is
69 ) => CompileI is (Proxy Eq) where
70 compileI tok ctx k =
71 case tok of
72 Token_Term_Eq_eq tok_a -> from_op (==) tok_a
73 Token_Term_Eq_ne tok_a -> from_op (/=) tok_a
74 where
75 from_op (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) tok_a =
76 compileO tok_a ctx $ \ty_a (TermO a) ->
77 check_con (At (Just tok_a) (ty @Eq :$ ty_a)) $ \Con ->
78 k (ty_a ~> ty @Bool) $ TermO $
79 \c -> lam $ op (a c)
80 instance -- TokenizeT
81 Inj_Token meta ts Eq =>
82 TokenizeT meta ts (Proxy Eq) where
83 tokenizeT _t = mempty
84 { tokenizers_infix = tokenizeTMod []
85 [ tokenize1 "==" (infixN 4) Token_Term_Eq_eq
86 , tokenize1 "/=" (infixN 4) Token_Term_Eq_ne
87 ]
88 }
89 instance Gram_Term_AtomsT meta ts (Proxy Eq) g