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 qualified Data.Function as Fun
   8 import Data.Monoid (Monoid)
   9 import qualified Data.Monoid as Monoid
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (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 Monoid
  32 type instance TyConsts_imported_by 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 instance -- CompileI
  61  ( Read_TyName TyName cs
  62  , Inj_TyConst        cs Monoid
  63  , Inj_TyConst        cs (->)
  64  , Proj_TyCon         cs
  65  , Compile cs is
  66  ) => CompileI cs is (Proxy Monoid) where
  67         compileI tok ctx k =
  68                 case tok of
  69                  Token_Term_Monoid_mempty tok_ty_a ->
  70                         -- mempty :: Monoid a => a
  71                         compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
  72                         check_Kind
  73                          (At Nothing SKiType)
  74                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  75                         check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
  76                         k ty_a $ TermO $ Fun.const mempty
  77                  Token_Term_Monoid_mappend tok_a ->
  78                         -- mappend :: Monoid a => a -> a -> a
  79                         compileO tok_a ctx $ \ty_a (TermO x) ->
  80                         check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
  81                         k (ty_a ~> ty_a) $ TermO $
  82                          \c -> lam $ \y -> mappend (x c) y
  83 instance -- TokenizeT
  84  Inj_Token meta ts Monoid =>
  85  TokenizeT meta ts (Proxy Monoid) where
  86         tokenizeT _t = Monoid.mempty
  87          { tokenizers_infix = tokenizeTMod []
  88                  [ (TeName "mempty",) ProTok_Term
  89                          { protok_term = \meta -> ProTokPi $ \a ->
  90                                 ProTok $ inj_EToken meta $ Token_Term_Monoid_mempty a
  91                          , protok_fixity = infixN5
  92                          }
  93                  , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
  94                  ]
  95          }
  96 instance Gram_Term_AtomsT meta ts (Proxy Monoid) g