Language/Symantic/Expr/Monoid.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 -- | Expression for 'Monoid'.
  13 module Language.Symantic.Expr.Monoid where
  14
  15 import Control.Monad
  16 import Data.Monoid (Monoid)
  17 import qualified Data.Monoid as Monoid
  18 import Data.Proxy (Proxy(..))
  19 import Data.Type.Equality ((:~:)(Refl))
  20 import Prelude hiding ((<$>), Monoid(..))
  21
  22 import Language.Symantic.Type
  23 import Language.Symantic.Repr
  24 import Language.Symantic.Expr.Root
  25 import Language.Symantic.Expr.Error
  26 import Language.Symantic.Expr.From
  27 import Language.Symantic.Trans.Common
  28
  29 -- * Class 'Sym_Monoid'
  30 -- | Symantic.
  31 class Sym_Monoid repr where
  32         mempty  :: Monoid a => repr a
  33         mappend :: Monoid a => repr a -> repr a -> repr a
  34         default mempty  :: (Trans t repr, Monoid a) => t repr a
  35         default mappend :: (Trans t repr, Monoid a) => t repr a -> t repr a -> t repr a
  36         mempty  = trans_lift mempty
  37         mappend = trans_map2 mappend
  38 instance Sym_Monoid Repr_Host where
  39         mempty  = Repr_Host Monoid.mempty
  40         mappend = liftM2 Monoid.mappend
  41 instance Sym_Monoid Repr_Text where
  42         mempty  = Repr_Text $ \_p _v -> "mempty"
  43         mappend = repr_text_app2 "mappend"
  44
  45 -- | 'mappend' alias.
  46 (<>) ::
  47  ( Sym_Monoid repr
  48  , Monoid a )
  49  => repr a -> repr a -> repr a
  50 (<>) = mappend
  51 infixr 6 <>
  52
  53 -- * Type 'Expr_Monoid'
  54 -- | Expression.
  55 data Expr_Monoid (root:: *)
  56 type instance Root_of_Expr      (Expr_Monoid root)      = root
  57 type instance Type_of_Expr      (Expr_Monoid root)      = No_Type
  58 type instance Sym_of_Expr       (Expr_Monoid root) repr = (Sym_Monoid repr)
  59 type instance Error_of_Expr ast (Expr_Monoid root)      = No_Error_Expr
  60
  61 -- | Parse 'mempty'.
  62 mempty_from
  63  :: forall root ty ast hs ret.
  64  ( ty ~ Type_Root_of_Expr (Expr_Monoid root)
  65  , Type0_From ast ty
  66  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  67                    (Error_of_Expr ast root)
  68  , Root_of_Expr root ~ root
  69  , Type0_Constraint Monoid ty
  70  ) => ast
  71  -> ExprFrom ast (Expr_Monoid root) hs ret
  72 mempty_from ast_a ex ast _ctx k =
  73  -- mempty :: Monoid a => a
  74         either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
  75         type0_from (Proxy::Proxy ty) ast_a $ \ty_a -> Right $
  76         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_a $ \Dict ->
  77         k ty_a $ Forall_Repr_with_Context $
  78         const mempty
  79
  80 -- | Parse 'mappend'.
  81 mappend_from
  82  :: forall root ty ast hs ret.
  83  ( ty ~ Type_Root_of_Expr (Expr_Monoid root)
  84  , Type0_Eq ty
  85  , Expr_From ast root
  86  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
  87                    (Error_of_Expr ast root)
  88  , Root_of_Expr root ~ root
  89  , Type0_Constraint Monoid ty
  90  ) => ast -> ast
  91  -> ExprFrom ast (Expr_Monoid root) hs ret
  92 mappend_from ast_x ast_y ex ast ctx k =
  93  -- mappend :: Monoid a => a -> a -> a
  94         expr_from (Proxy::Proxy root) ast_x ctx $
  95          \(ty_x::ty h_x) (Forall_Repr_with_Context x) ->
  96         expr_from (Proxy::Proxy root) ast_y ctx $
  97          \(ty_y::ty h_y) (Forall_Repr_with_Context y) ->
  98         check_type0_eq ex ast ty_x ty_y $ \Refl ->
  99         check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_x $ \Dict ->
 100         k ty_x $ Forall_Repr_with_Context $
 101          \c -> mappend (x c) (y c)