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