Language/Symantic/Expr/Monoid.hs

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