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.Parsing.Grammar
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20 import Language.Symantic.Lib.Lambda
  21
  22 -- * Class 'Sym_Monoid'
  23 class Sym_Monoid term where
  24         mempty  :: Monoid a => term a
  25         mappend :: Monoid a => term a -> term a -> term a
  26         default mempty  :: (Trans t term, Monoid a) => t term a
  27         default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
  28         mempty  = trans_lift mempty
  29         mappend = trans_map2 mappend
  30
  31 type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
  32 type instance Consts_of_Iface (Proxy Monoid) = Proxy Monoid ': Consts_imported_by Monoid
  33 type instance Consts_imported_by Monoid = '[]
  34
  35 instance Sym_Monoid HostI where
  36         mempty  = HostI Monoid.mempty
  37         mappend = liftM2 Monoid.mappend
  38 instance Sym_Monoid TextI where
  39         mempty  = textI0 "mempty"
  40         mappend = textI2 "mappend"
  41 instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
  42         mempty  = dupI0 (Proxy @Sym_Monoid) mempty
  43         mappend = dupI2 (Proxy @Sym_Monoid) mappend
  44
  45 -- | 'mappend' alias.
  46 --
  47 -- TODO: move to Semigroup
  48 (<>) ::
  49  ( Sym_Monoid term
  50  , Monoid a )
  51  => term a -> term a -> term a
  52 (<>) = mappend
  53 infixr 6 <>
  54
  55 instance
  56  ( Read_TypeNameR Type_Name cs rs
  57  , Inj_Const cs Monoid
  58  ) => Read_TypeNameR Type_Name cs (Proxy Monoid ': rs) where
  59         read_typenameR _cs (Type_Name "Monoid") k = k (ty @Monoid)
  60         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  61 instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
  62         show_const ConstZ{} = "Monoid"
  63         show_const (ConstS c) = show_const c
  64
  65 instance Proj_ConC cs (Proxy Monoid)
  66 data instance TokenT meta (ts::[*]) (Proxy Monoid)
  67  = Token_Term_Monoid_mempty  (EToken meta '[Proxy Token_Type])
  68  | Token_Term_Monoid_mappend (EToken meta ts)
  69 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
  70 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
  71 instance -- CompileI
  72  ( Read_TypeName Type_Name (Consts_of_Ifaces is)
  73  , Inj_Const  (Consts_of_Ifaces is) Monoid
  74  , Inj_Const  (Consts_of_Ifaces is) (->)
  75  , Proj_Con   (Consts_of_Ifaces is)
  76  , Compile is
  77  ) => CompileI is (Proxy Monoid) where
  78         compileI tok ctx k =
  79                 case tok of
  80                  Token_Term_Monoid_mempty tok_ty_a ->
  81                         -- mempty :: Monoid a => a
  82                         compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
  83                         check_kind
  84                          (At Nothing SKiType)
  85                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  86                         check_con (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \Con ->
  87                         k ty_a $ TermO $ Fun.const mempty
  88                  Token_Term_Monoid_mappend tok_a ->
  89                         -- mappend :: Monoid a => a -> a -> a
  90                         compileO tok_a ctx $ \ty_a (TermO x) ->
  91                         check_con (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \Con ->
  92                         k (ty_a ~> ty_a) $ TermO $
  93                          \c -> lam $ \y -> mappend (x c) y
  94 instance -- TokenizeT
  95  Inj_Token meta ts Monoid =>
  96  TokenizeT meta ts (Proxy Monoid) where
  97         tokenizeT _t = Monoid.mempty
  98          { tokenizers_infix = tokenizeTMod []
  99                  [ (Term_Name "mempty",) Term_ProTok
 100                          { term_protok = \meta -> ProTokPi $ \a ->
 101                                 ProTok $ inj_etoken meta $ Token_Term_Monoid_mempty a
 102                          , term_fixity = infixN5
 103                          }
 104                  , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
 105                  , tokenize1 "<>" (infixR 6) Token_Term_Monoid_mappend
 106                  ]
 107          }
 108 instance Gram_Term_AtomsT meta ts (Proxy Monoid) g