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 Data.Proxy (Proxy(..))
   8 import Prelude hiding ((==), (/=))
   9 import qualified Data.Eq as Eq
  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 (Proxy Eq)
  31 type instance TyConsts_imported_by (Proxy 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
  60 instance -- CompileI
  61  ( Inj_TyConst cs Bool
  62  , Inj_TyConst cs (->)
  63  , Inj_TyConst cs Eq
  64  , Proj_TyCon  cs
  65  , Compile cs is
  66  ) => CompileI cs is (Proxy Eq) where
  67         compileI tok ctx k =
  68                 case tok of
  69                  Token_Term_Eq_eq tok_a -> from_op (==) tok_a
  70                  Token_Term_Eq_ne tok_a -> from_op (/=) tok_a
  71                 where
  72                 from_op (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) tok_a =
  73                         compile tok_a ctx $ \ty_a (Term a) ->
  74                         check_TyCon (At (Just tok_a) (ty @Eq :$ ty_a)) $ \TyCon ->
  75                         k (ty_a ~> ty @Bool) $ Term $
  76                          \c -> lam $ op (a c)
  77 instance -- TokenizeT
  78  Inj_Token meta ts Eq =>
  79  TokenizeT meta ts (Proxy Eq) where
  80         tokenizeT _t = mempty
  81          { tokenizers_infix = tokenizeTMod []
  82                  [ tokenize1 "==" (infixN 4) Token_Term_Eq_eq
  83                  , tokenize1 "/=" (infixN 4) Token_Term_Eq_ne
  84                  ]
  85          }
  86 instance Gram_Term_AtomsT meta ts (Proxy Eq) g