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