Language/Symantic/Compiling/Monoid.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Monoid'.
   4 module Language.Symantic.Compiling.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.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (Monoid(..))
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling.Term
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy Monoid) = Proxy Monoid ': Consts_imported_by Monoid
  32 type instance Consts_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  = textI_app0 "mempty"
  39         mappend = textI_app2 "mappend"
  40 instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
  41         mempty  = dupI0 (Proxy @Sym_Monoid) mempty
  42         mappend = dupI2 (Proxy @Sym_Monoid) mappend
  43
  44 -- | 'mappend' alias.
  45 (<>) ::
  46  ( Sym_Monoid term
  47  , Monoid a )
  48  => term a -> term a -> term a
  49 (<>) = mappend
  50 infixr 6 <>
  51
  52 instance Const_from Text cs => Const_from Text (Proxy Monoid ': cs) where
  53         const_from "Monoid" k = k (ConstZ kind)
  54         const_from s k = const_from s $ k . ConstS
  55 instance Show_Const cs => Show_Const (Proxy Monoid ': cs) where
  56         show_const ConstZ{} = "Monoid"
  57         show_const (ConstS c) = show_const c
  58
  59 instance Proj_ConC cs (Proxy Monoid)
  60 data instance TokenT meta (ts::[*]) (Proxy Monoid)
  61  = Token_Term_Monoid_mempty  (EToken meta '[Proxy Token_Type])
  62  | Token_Term_Monoid_mappend (EToken meta ts)
  63 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
  64 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
  65 instance -- Term_fromI
  66  ( Const_from Name_LamVar (Consts_of_Ifaces is)
  67  , Inj_Const  (Consts_of_Ifaces is) Monoid
  68  , Inj_Const  (Consts_of_Ifaces is) (->)
  69  , Proj_Con   (Consts_of_Ifaces is)
  70  , Term_from is
  71  ) => Term_fromI is (Proxy Monoid) where
  72         term_fromI tok ctx k =
  73                 case tok of
  74                  Token_Term_Monoid_mempty tok_ty_a ->
  75                         -- mempty :: Monoid a => a
  76                         type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
  77                         check_kind
  78                          (At Nothing SKiType)
  79                          (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
  80                         check_con (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \Con ->
  81                         k ty_a $ TermLC $ Fun.const mempty
  82                  Token_Term_Monoid_mappend tok_a ->
  83                         -- mappend :: Monoid a => a -> a -> a
  84                         term_from tok_a ctx $ \ty_a (TermLC x) ->
  85                         check_con (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \Con ->
  86                         k (ty_a ~> ty_a) $ TermLC $
  87                          \c -> lam $ \y -> mappend (x c) y