symantic-lib/Language/Symantic/Lib/Monoid.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Monoid'.
   4 module Language.Symantic.Lib.Monoid where
   5
   6 import Control.Monad
   7 import Data.Monoid (Monoid)
   8 import Data.Proxy
   9 import Data.Type.Equality ((:~:)(Refl))
  10 import Prelude hiding (Monoid(..))
  11 import qualified Data.Function as Fun
  12 import qualified Data.Monoid as Monoid
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Typing
  16 import Language.Symantic.Compiling
  17 import Language.Symantic.Interpreting
  18 import Language.Symantic.Transforming
  19 import Language.Symantic.Lib.Lambda
  20
  21 -- * Class 'Sym_Monoid'
  22 class Sym_Monoid term where
  23         mempty  :: Monoid a => term a
  24         mappend :: Monoid a => term a -> term a -> term a
  25         default mempty  :: (Trans t term, Monoid a) => t term a
  26         default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
  27         mempty  = trans_lift mempty
  28         mappend = trans_map2 mappend
  29
  30 type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
  31 type instance TyConsts_of_Iface (Proxy Monoid) = Proxy Monoid ': TyConsts_imported_by (Proxy Monoid)
  32 type instance TyConsts_imported_by (Proxy Monoid) = '[]
  33
  34 instance Sym_Monoid HostI where
  35         mempty  = HostI Monoid.mempty
  36         mappend = liftM2 Monoid.mappend
  37 instance Sym_Monoid TextI where
  38         mempty  = textI0 "mempty"
  39         mappend = textI2 "mappend"
  40 instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
  41         mempty  = dupI0 @Sym_Monoid mempty
  42         mappend = dupI2 @Sym_Monoid mappend
  43
  44 instance
  45  ( Read_TyNameR TyName cs rs
  46  , Inj_TyConst cs Monoid
  47  ) => Read_TyNameR TyName cs (Proxy Monoid ': rs) where
  48         read_TyNameR _cs (TyName "Monoid") k = k (ty @Monoid)
  49         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  50 instance Show_TyConst cs => Show_TyConst (Proxy Monoid ': cs) where
  51         show_TyConst TyConstZ{} = "Monoid"
  52         show_TyConst (TyConstS c) = show_TyConst c
  53
  54 instance Proj_TyConC cs (Proxy Monoid)
  55 data instance TokenT meta (ts::[*]) (Proxy Monoid)
  56  = Token_Term_Monoid_mempty  (EToken meta '[Proxy Token_Type])
  57  | Token_Term_Monoid_mappend (EToken meta ts)
  58 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
  59 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
  60
  61 instance -- CompileI
  62  ( Read_TyName TyName cs
  63  , Inj_TyConst        cs Monoid
  64  , Inj_TyConst        cs (->)
  65  , Proj_TyCon         cs
  66  , Compile cs is
  67  ) => CompileI cs is (Proxy Monoid) where
  68         compileI tok ctx k =
  69                 case tok of
  70                  Token_Term_Monoid_mempty tok_ty_a ->
  71                         -- mempty :: Monoid a => a
  72                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  73                         check_Kind
  74                          (At Nothing SKiType)
  75                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  76                         check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
  77                         k ty_a $ Term $ Fun.const mempty
  78                  Token_Term_Monoid_mappend tok_a ->
  79                         -- mappend :: Monoid a => a -> a -> a
  80                         compile tok_a ctx $ \ty_a (Term x) ->
  81                         check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
  82                         k (ty_a ~> ty_a) $ Term $
  83                          \c -> lam $ \y -> mappend (x c) y
  84 instance -- TokenizeT
  85  Inj_Token meta ts Monoid =>
  86  TokenizeT meta ts (Proxy Monoid) where
  87         tokenizeT _t = Monoid.mempty
  88          { tokenizers_infix = tokenizeTMod []
  89                  [ (TeName "mempty",) ProTok_Term
  90                          { protok_term = \meta -> ProTokPi $ \a ->
  91                                 ProTokTe $ inj_EToken meta $ Token_Term_Monoid_mempty a
  92                          , protok_fixity = infixN5
  93                          }
  94                  , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
  95                  ]
  96          }
  97 instance Gram_Term_AtomsT meta ts (Proxy Monoid) g