]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Eq.hs
Fix comment typo.
[haskell/symantic.git] / Language / Symantic / Compiling / Eq.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Eq'.
4 module Language.Symantic.Compiling.Eq where
5
6 import Control.Monad
7 import qualified Data.Eq as Eq
8 import Data.Proxy (Proxy(..))
9 import Data.Text (Text)
10 import Prelude hiding ((==), (/=))
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Typing
14 import Language.Symantic.Compiling.Term
15 import Language.Symantic.Interpreting
16 import Language.Symantic.Transforming.Trans
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 "==" (Precedence 4)
41 (/=) = textI_infix "/=" (Precedence 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 Const_from Text cs => Const_from Text (Proxy Eq ': cs) where
47 const_from "Eq" k = k (ConstZ kind)
48 const_from s k = const_from s $ k . ConstS
49 instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
50 show_const ConstZ{} = "Eq"
51 show_const (ConstS c) = show_const c
52
53 instance Proj_ConC 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_Const (Consts_of_Ifaces is) Bool
61 , Inj_Const (Consts_of_Ifaces is) (->)
62 , Inj_Const (Consts_of_Ifaces is) Eq
63 , Proj_Con (Consts_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_con (At (Just tok_a) (ty @Eq :$ ty_a)) $ \Con ->
74 k (ty_a ~> ty @Bool) $ TermO $
75 \c -> lam $ op (a c)