Language/Symantic/Compiling/Monoid.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   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 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 -- | Symantic for 'Monoid'.
  14 module Language.Symantic.Compiling.Monoid where
  15
  16 import Control.Monad
  17 import qualified Data.Function as Fun
  18 import Data.Monoid (Monoid)
  19 import qualified Data.Monoid as Monoid
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (Monoid(..))
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Interpreting
  29 import Language.Symantic.Transforming.Trans
  30
  31 -- * Class 'Sym_Monoid'
  32 class Sym_Monoid term where
  33         mempty  :: Monoid a => term a
  34         mappend :: Monoid a => term a -> term a -> term a
  35         default mempty  :: (Trans t term, Monoid a) => t term a
  36         default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
  37         mempty  = trans_lift mempty
  38         mappend = trans_map2 mappend
  39
  40 type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
  41 type instance Consts_of_Iface (Proxy Monoid) = Proxy Monoid ': Consts_imported_by Monoid
  42 type instance Consts_imported_by Monoid = '[]
  43
  44 instance Sym_Monoid HostI where
  45         mempty  = HostI Monoid.mempty
  46         mappend = liftM2 Monoid.mappend
  47 instance Sym_Monoid TextI where
  48         mempty  = textI_app0 "mempty"
  49         mappend = textI_app2 "mappend"
  50 instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
  51         mempty  = dupI0 sym_Monoid mempty
  52         mappend = dupI2 sym_Monoid mappend
  53
  54 -- | 'mappend' alias.
  55 (<>) ::
  56  ( Sym_Monoid term
  57  , Monoid a )
  58  => term a -> term a -> term a
  59 (<>) = mappend
  60 infixr 6 <>
  61
  62 instance Const_from Text cs => Const_from Text (Proxy Monoid ': cs) where
  63         const_from "Monoid" k = k (ConstZ kind)
  64         const_from s k = const_from s $ k . ConstS
  65 instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
  66         show_const ConstZ{} = "Monoid"
  67         show_const (ConstS c) = show_const c
  68
  69 instance -- Proj_ConC
  70  Proj_ConC cs (Proxy Monoid)
  71 instance -- Term_fromI
  72  ( AST ast
  73  , Lexem ast ~ LamVarName
  74  , Const_from (Lexem ast) (Consts_of_Ifaces is)
  75  , Inj_Const  (Consts_of_Ifaces is) Monoid
  76  , Inj_Const  (Consts_of_Ifaces is) (->)
  77  , Proj_Con   (Consts_of_Ifaces is)
  78  , Term_from is ast
  79  ) => Term_fromI is (Proxy Monoid) ast where
  80         term_fromI ast ctx k =
  81                 case ast_lexem ast of
  82                  "mempty"  -> mempty_from
  83                  "mappend" -> mappend_from
  84                  "<>"      -> mappend_from
  85                  _ -> Left $ Error_Term_unsupported
  86                 where
  87                 mempty_from =
  88                  -- mempty :: Monoid a => a
  89                         from_ast1 ast $ \ast_ty_x as ->
  90                         either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
  91                         type_from ast_ty_x $ \ty_x -> Right $
  92                         check_kind ast SKiType (At (Just ast_ty_x) ty_x) $ \Refl ->
  93                         check_constraint (At (Just ast_ty_x) (tyMonoid :$ ty_x)) $ \Con ->
  94                         k as ty_x $ TermLC $ Fun.const mempty
  95                 mappend_from =
  96                  -- mappend :: Monoid a => a -> a -> a
  97                         from_ast1 ast $ \ast_x as ->
  98                         term_from ast_x ctx $ \ty_x (TermLC x) ->
  99                         check_constraint (At (Just ast_x) (tyMonoid :$ ty_x)) $ \Con ->
 100                         k as (ty_x ~> ty_x) $ TermLC $
 101                          \c -> lam $ \y -> mappend (x c) y
 102
 103 -- | The 'Monoid' 'Type'
 104 tyMonoid :: Inj_Const cs Monoid => Type cs Monoid
 105 tyMonoid = TyConst inj_const
 106
 107 sym_Monoid :: Proxy Sym_Monoid
 108 sym_Monoid = Proxy
 109
 110 syMonoid :: IsString a => [Syntax a] -> Syntax a
 111 syMonoid = Syntax "Monoid"