Language/Symantic/Expr/Eq.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# LANGUAGE NoMonomorphismRestriction #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Eq'.
  13 module Language.Symantic.Expr.Eq where
  14
  15 import Control.Monad
  16 import qualified Data.Eq as Eq
  17 import Data.Proxy (Proxy(..))
  18 import Data.Type.Equality ((:~:)(Refl))
  19 import Prelude hiding ((==), (/=))
  20
  21 import Language.Symantic.Type
  22 import Language.Symantic.Repr
  23 import Language.Symantic.Expr.Root
  24 import Language.Symantic.Expr.Error
  25 import Language.Symantic.Expr.From
  26 import Language.Symantic.Trans.Common
  27
  28 -- * Class 'Sym_Eq'
  29 -- | Symantic.
  30 class Sym_Eq repr where
  31         (==) :: Eq a => repr a -> repr a -> repr Bool
  32         (/=) :: Eq a => repr a -> repr a -> repr Bool
  33
  34         default (==) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool
  35         default (/=) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool
  36
  37         (==) = trans_map2 (==)
  38         (/=) = trans_map2 (/=)
  39
  40 infix 4 ==
  41 infix 4 /=
  42
  43 instance Sym_Eq Repr_Host where
  44         (==) = liftM2 (Eq.==)
  45         (/=) = liftM2 (Eq./=)
  46 instance Sym_Eq Repr_Text where
  47         (==) = repr_text_infix "==" (Precedence 4)
  48         (/=) = repr_text_infix "/=" (Precedence 4)
  49 instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Repr_Dup r1 r2) where
  50         (==) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (==) x1 y1 `Repr_Dup` (==) x2 y2
  51         (/=) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (/=) x1 y1 `Repr_Dup` (/=) x2 y2
  52
  53 -- * Type 'Expr_Eq'
  54 -- | Expression.
  55 data Expr_Eq (root:: *)
  56 type instance Root_of_Expr      (Expr_Eq root)      = root
  57 type instance Type_of_Expr      (Expr_Eq root)      = No_Type
  58 type instance Sym_of_Expr       (Expr_Eq root) repr = (Sym_Eq repr)
  59 type instance Error_of_Expr ast (Expr_Eq root)      = No_Error_Expr
  60
  61 eq_from
  62  :: forall root ty ast hs ret.
  63  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  64  , Type0_Lift Type_Bool (Type_of_Expr root)
  65  , Type0_Eq ty
  66  , Expr_From ast root
  67  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  68                    (Error_of_Expr ast root)
  69  , Root_of_Expr root ~ root
  70  , Type0_Constraint Eq ty
  71  ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool)
  72  -> ast -> ast
  73  -> ExprFrom ast (Expr_Eq root) hs ret
  74 eq_from test ast_x ast_y ex ast ctx k =
  75         expr_from (Proxy::Proxy root) ast_x ctx $
  76          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  77         expr_from (Proxy::Proxy root) ast_y ctx $
  78          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  79         check_type0_eq ex ast ty_x ty_y $ \Refl ->
  80         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
  81         k type_bool $ Forall_Repr_with_Context $
  82          \c -> x c `test` y c