Language/Symantic/Compiling/Eq.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Eq'.
  14 module Language.Symantic.Compiling.Eq where
  15
  16 import Control.Monad
  17 import qualified Data.Eq as Eq
  18 import Data.Proxy (Proxy(..))
  19 import Data.String (IsString)
  20 import Data.Text (Text)
  21 import Prelude hiding ((==), (/=))
  22
  23 import Language.Symantic.Typing
  24 import Language.Symantic.Compiling.Term
  25 import Language.Symantic.Compiling.Bool
  26 import Language.Symantic.Interpreting
  27 import Language.Symantic.Transforming.Trans
  28
  29 -- * Class 'Sym_Eq'
  30 class Sym_Eq term where
  31         (==) :: Eq a => term a -> term a -> term Bool
  32         (/=) :: Eq a => term a -> term a -> term Bool
  33
  34         default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  35         default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
  36
  37         (==) = trans_map2 (==)
  38         (/=) = trans_map2 (/=)
  39
  40 infix 4 ==
  41 infix 4 /=
  42
  43 type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
  44 type instance Consts_of_Iface (Proxy Eq) = Proxy Eq ': Consts_imported_by Eq
  45 type instance Consts_imported_by Eq = '[]
  46
  47 instance Sym_Eq HostI where
  48         (==) = liftM2 (Eq.==)
  49         (/=) = liftM2 (Eq./=)
  50 instance Sym_Eq TextI where
  51         (==) = textI_infix "==" (Precedence 4)
  52         (/=) = textI_infix "/=" (Precedence 4)
  53 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
  54         (==) = dupI2 sym_Eq (==)
  55         (/=) = dupI2 sym_Eq (/=)
  56
  57 instance Const_from Text cs => Const_from Text (Proxy Eq ': cs) where
  58         const_from "Eq" k = k (ConstZ kind)
  59         const_from s k = const_from s $ k . ConstS
  60 instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
  61         show_const ConstZ{} = "Eq"
  62         show_const (ConstS c) = show_const c
  63
  64 instance -- Proj_ConC
  65  Proj_ConC cs (Proxy Eq)
  66 instance -- Term_fromI
  67  ( AST ast
  68  , Lexem ast ~ LamVarName
  69  , Inj_Const (Consts_of_Ifaces is) Bool
  70  , Inj_Const (Consts_of_Ifaces is) (->)
  71  , Inj_Const (Consts_of_Ifaces is) Eq
  72  , Proj_Con (Consts_of_Ifaces is)
  73  , Term_from is ast
  74  ) => Term_fromI is (Proxy Eq) ast where
  75         term_fromI ast ctx k =
  76                 case ast_lexem ast of
  77                  "=="  -> op2_from (==)
  78                  "/="  -> op2_from (/=)
  79                  _ -> Left $ Error_Term_unsupported
  80                 where
  81                 op2_from (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) =
  82                         from_ast1 ast $ \ast_x as ->
  83                         term_from ast_x ctx $ \ty_x (TermLC x) ->
  84                         check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
  85                         k as (ty_x ~> tyBool) $ TermLC $
  86                          \c -> lam $ op (x c)
  87
  88 -- | The 'Eq' 'Type'
  89 tyEq :: Inj_Const cs Eq => Type cs Eq
  90 tyEq = TyConst inj_const
  91
  92 sym_Eq :: Proxy Sym_Eq
  93 sym_Eq = Proxy
  94
  95 syEq :: IsString a => [Syntax a] -> Syntax a
  96 syEq = Syntax "Eq"