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 -- Parse '==' or '/='.
  62 eq_from
  63  :: forall root ty ast hs ret.
  64  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  65  , Type0_Lift Type_Bool (Type_of_Expr root)
  66  , Type0_Eq ty
  67  , Type0_Constraint Eq ty
  68  , Expr_From ast root
  69  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  70                    (Error_of_Expr ast root)
  71  , Root_of_Expr root ~ root
  72  ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool)
  73  -> ast -> ast
  74  -> ExprFrom ast (Expr_Eq root) hs ret
  75 eq_from test ast_x ast_y ex ast ctx k =
  76         expr_from (Proxy::Proxy root) ast_x ctx $
  77          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  78         expr_from (Proxy::Proxy root) ast_y ctx $
  79          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  80         check_type0_eq ex ast ty_x ty_y $ \Refl ->
  81         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
  82         k type_bool $ Forall_Repr_with_Context $
  83          \c -> x c `test` y c
  84
  85 -- Parse '==' or '/=', with only one argument.
  86 eq_from1
  87  :: forall root ty ast hs ret.
  88  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  89  , Type0_Lift Type_Fun  (Type_of_Expr root)
  90  , Type0_Lift Type_Bool (Type_of_Expr root)
  91  , Type0_Eq ty
  92  , Type0_Constraint Eq ty
  93  , Expr_From ast root
  94  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  95                    (Error_of_Expr ast root)
  96  , Root_of_Expr root ~ root
  97  ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool)
  98  -> ast
  99  -> ExprFrom ast (Expr_Eq root) hs ret
 100 eq_from1 test ast_x ex ast ctx k =
 101         expr_from (Proxy::Proxy root) ast_x ctx $
 102          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
 103         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
 104         k (type_fun ty_x type_bool) $ Forall_Repr_with_Context $
 105          \c -> lam $ \y -> x c `test` y