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
  50  ( Sym_Eq r1
  51  , Sym_Eq r2
  52  ) => Sym_Eq (Dup r1 r2) where
  53         (==) (x1 `Dup` x2) (y1 `Dup` y2) = (==) x1 y1 `Dup` (==) x2 y2
  54         (/=) (x1 `Dup` x2) (y1 `Dup` y2) = (/=) x1 y1 `Dup` (/=) x2 y2
  55
  56 -- * Type 'Expr_Eq'
  57 -- | Expression.
  58 data Expr_Eq (root:: *)
  59 type instance Root_of_Expr      (Expr_Eq root)      = root
  60 type instance Type_of_Expr      (Expr_Eq root)      = No_Type
  61 type instance Sym_of_Expr       (Expr_Eq root) repr = (Sym_Eq repr)
  62 type instance Error_of_Expr ast (Expr_Eq root)      = No_Error_Expr
  63
  64 eq_from
  65  :: forall root ty ast hs ret.
  66  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  67  , Type0_Lift Type_Bool (Type_of_Expr root)
  68  , Type0_Eq ty
  69  , Expr_From ast root
  70  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  71                    (Error_of_Expr ast root)
  72  , Root_of_Expr root ~ root
  73  , Type0_Constraint Eq ty
  74  ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool)
  75  -> ast -> ast
  76  -> ExprFrom ast (Expr_Eq root) hs ret
  77 eq_from test ast_x ast_y ex ast ctx k =
  78         expr_from (Proxy::Proxy root) ast_x ctx $
  79          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  80         expr_from (Proxy::Proxy root) ast_y ctx $
  81          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  82         check_type0_eq ex ast ty_x ty_y $ \Refl ->
  83         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
  84         k type_bool $ Forall_Repr_with_Context $
  85          \c -> x c `test` y c