{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -- | Expression for 'Eq'. module Language.Symantic.Expr.Eq where import Control.Monad import qualified Data.Eq as Eq import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding ((==), (/=)) import Language.Symantic.Type import Language.Symantic.Repr import Language.Symantic.Expr.Root import Language.Symantic.Expr.Error import Language.Symantic.Expr.From import Language.Symantic.Trans.Common -- * Class 'Sym_Eq' -- | Symantic. class Sym_Eq repr where (==) :: Eq a => repr a -> repr a -> repr Bool (/=) :: Eq a => repr a -> repr a -> repr Bool default (==) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool default (/=) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool (==) = trans_map2 (==) (/=) = trans_map2 (/=) infix 4 == infix 4 /= instance Sym_Eq Repr_Host where (==) = liftM2 (Eq.==) (/=) = liftM2 (Eq./=) instance Sym_Eq Repr_Text where (==) = repr_text_infix "==" (Precedence 4) (/=) = repr_text_infix "/=" (Precedence 4) instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (Repr_Dup r1 r2) where (==) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (==) x1 y1 `Repr_Dup` (==) x2 y2 (/=) (x1 `Repr_Dup` x2) (y1 `Repr_Dup` y2) = (/=) x1 y1 `Repr_Dup` (/=) x2 y2 -- * Type 'Expr_Eq' -- | Expression. data Expr_Eq (root:: *) type instance Root_of_Expr (Expr_Eq root) = root type instance Type_of_Expr (Expr_Eq root) = No_Type type instance Sym_of_Expr (Expr_Eq root) repr = (Sym_Eq repr) type instance Error_of_Expr ast (Expr_Eq root) = No_Error_Expr eq_from :: forall root ty ast hs ret. ( ty ~ Type_Root_of_Expr (Expr_Eq root) , Type0_Lift Type_Bool (Type_of_Expr root) , Type0_Eq ty , Expr_From ast root , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) (Error_of_Expr ast root) , Root_of_Expr root ~ root , Type0_Constraint Eq ty ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool) -> ast -> ast -> ExprFrom ast (Expr_Eq root) hs ret eq_from test ast_x ast_y ex ast ctx k = expr_from (Proxy::Proxy root) ast_x ctx $ \(ty_x::ty h_x) (Forall_Repr_with_Context x) -> expr_from (Proxy::Proxy root) ast_y ctx $ \(ty_y::ty h_y) (Forall_Repr_with_Context y) -> check_type0_eq ex ast ty_x ty_y $ \Refl -> check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict -> k type_bool $ Forall_Repr_with_Context $ \c -> x c `test` y c