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