Language/Symantic/Expr/Eq.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE TypeOperators #-}
   9 {-# LANGUAGE NoMonomorphismRestriction #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 -- | Expression for 'Eq'.
  12 module Language.Symantic.Expr.Eq where
  13
  14 import Control.Monad
  15 import qualified Data.Eq as Eq
  16 import Data.Monoid
  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         default (==) :: (Trans t repr, Eq a)
  33                      => t repr a -> t repr a -> t repr Bool
  34         (==) = trans_map2 (==)
  35 infix 4 ==
  36 instance Sym_Eq Repr_Host where
  37         (==) = liftM2 (Eq.==)
  38 instance Sym_Eq Repr_Text where
  39         (==) (Repr_Text x) (Repr_Text y) =
  40                 Repr_Text $ \p v ->
  41                         let p' = precedence_Eq in
  42                         paren p p' $
  43                         x p' v <> " == " <> y p' v
  44 instance
  45  ( Sym_Eq r1
  46  , Sym_Eq r2
  47  ) => Sym_Eq (Dup r1 r2) where
  48         (==) (x1 `Dup` x2) (y1 `Dup` y2) = (==) x1 y1 `Dup` (==) x2 y2
  49
  50 -- * Type 'Expr_Eq'
  51 -- | Expression.
  52 data Expr_Eq (root:: *)
  53 type instance Root_of_Expr      (Expr_Eq root)      = root
  54 type instance Type_of_Expr      (Expr_Eq root)      = No_Type
  55 type instance Sym_of_Expr       (Expr_Eq root) repr = (Sym_Eq repr)
  56 type instance Error_of_Expr ast (Expr_Eq root)      = No_Error_Expr
  57
  58 eq_from
  59  :: forall root ty ast hs ret.
  60  ( ty ~ Type_Root_of_Expr (Expr_Eq root)
  61  , Type0_Lift Type_Bool (Type_of_Expr root)
  62  , Type0_Eq ty
  63  , Expr_From ast root
  64  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  65                    (Error_of_Expr ast root)
  66  , Root_of_Expr root ~ root
  67  , Type0_Constraint Eq ty
  68  ) => ast -> ast
  69  -> ExprFrom ast (Expr_Eq root) hs ret
  70 eq_from ast_x ast_y ex ast ctx k =
  71         expr_from (Proxy::Proxy root) ast_x ctx $
  72          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  73         expr_from (Proxy::Proxy root) ast_y ctx $
  74          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  75         check_type0_eq ex ast ty_x ty_y $ \Refl ->
  76         check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict ->
  77         k type_bool $ Forall_Repr_with_Context $
  78          \c -> x c == y c