-- | Symantic for 'Monoid'.
module Language.Symantic.Lib.Monoid where
-import Control.Monad
-import qualified Data.Function as Fun
import Data.Monoid (Monoid)
-import qualified Data.Monoid as Monoid
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Monoid(..))
+import qualified Data.Monoid as Monoid
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic
+import Language.Symantic.Lib.Function (a0)
-- * Class 'Sym_Monoid'
+type instance Sym Monoid = Sym_Monoid
class Sym_Monoid term where
mempty :: Monoid a => term a
mappend :: Monoid a => term a -> term a -> term a
- default mempty :: (Trans t term, Monoid a) => t term a
- default mappend :: (Trans t term, Monoid a) => t term a -> t term a -> t term a
- mempty = trans_lift mempty
- mappend = trans_map2 mappend
+ default mempty :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a
+ default mappend :: Sym_Monoid (UnT term) => Trans term => Monoid a => term a -> term a -> term a
+ mempty = trans mempty
+ mappend = trans2 mappend
+
+-- Interpreting
+instance Sym_Monoid Eval where
+ mempty = Eval Monoid.mempty
+ mappend = eval2 Monoid.mappend
+instance Sym_Monoid View where
+ mempty = view0 "mempty"
+ mappend = view2 "mappend"
+instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (Dup r1 r2) where
+ mempty = dup0 @Sym_Monoid mempty
+ mappend = dup2 @Sym_Monoid mappend
+
+-- Transforming
+instance (Sym_Monoid term, Sym_Lambda term) => Sym_Monoid (BetaT term)
+
+-- Typing
+instance NameTyOf Monoid where
+ nameTyOf _c = ["Monoid"] `Mod` "Monoid"
+instance FixityOf Monoid
+instance ClassInstancesFor Monoid
+instance TypeInstancesFor Monoid
-type instance Sym_of_Iface (Proxy Monoid) = Sym_Monoid
-type instance TyConsts_of_Iface (Proxy Monoid) = Proxy Monoid ': TyConsts_imported_by Monoid
-type instance TyConsts_imported_by Monoid = '[]
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Monoid
+instance (Source src, SymInj ss Monoid) => ModuleFor src ss Monoid where
+ moduleFor = ["Monoid"] `moduleWhere`
+ [ "mempty" := teMonoid_mempty
+ , "mappend" := teMonoid_mappend
+ ]
-instance Sym_Monoid HostI where
- mempty = HostI Monoid.mempty
- mappend = liftM2 Monoid.mappend
-instance Sym_Monoid TextI where
- mempty = textI0 "mempty"
- mappend = textI2 "mappend"
-instance (Sym_Monoid r1, Sym_Monoid r2) => Sym_Monoid (DupI r1 r2) where
- mempty = dupI0 @Sym_Monoid mempty
- mappend = dupI2 @Sym_Monoid mappend
+-- ** 'Type's
+tyMonoid :: Source src => Type src vs a -> Type src vs (Monoid a)
+tyMonoid a = tyConstLen @(K Monoid) @Monoid (lenVars a) `tyApp` a
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Monoid
- ) => Read_TyNameR TyName cs (Proxy Monoid ': rs) where
- read_TyNameR _cs (TyName "Monoid") k = k (ty @Monoid)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Monoid ': cs) where
- show_TyConst TyConstZ{} = "Monoid"
- show_TyConst (TyConstS c) = show_TyConst c
+-- ** 'Term's
+teMonoid_mempty :: TermDef Monoid '[Proxy a] (Monoid a #> a)
+teMonoid_mempty = Term (tyMonoid a0) a0 $ teSym @Monoid $ mempty
-instance Proj_TyConC cs (Proxy Monoid)
-data instance TokenT meta (ts::[*]) (Proxy Monoid)
- = Token_Term_Monoid_mempty (EToken meta '[Proxy Token_Type])
- | Token_Term_Monoid_mappend (EToken meta ts)
-deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
-deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
-instance -- CompileI
- ( Read_TyName TyName (TyConsts_of_Ifaces is)
- , Inj_TyConst (TyConsts_of_Ifaces is) Monoid
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Monoid) where
- compileI tok ctx k =
- case tok of
- Token_Term_Monoid_mempty tok_ty_a ->
- -- mempty :: Monoid a => a
- compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
- check_Kind
- (At Nothing SKiType)
- (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
- check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
- k ty_a $ TermO $ Fun.const mempty
- Token_Term_Monoid_mappend tok_a ->
- -- mappend :: Monoid a => a -> a -> a
- compileO tok_a ctx $ \ty_a (TermO x) ->
- check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
- k (ty_a ~> ty_a) $ TermO $
- \c -> lam $ \y -> mappend (x c) y
-instance -- TokenizeT
- Inj_Token meta ts Monoid =>
- TokenizeT meta ts (Proxy Monoid) where
- tokenizeT _t = Monoid.mempty
- { tokenizers_infix = tokenizeTMod []
- [ (Term_Name "mempty",) Term_ProTok
- { term_protok = \meta -> ProTokPi $ \a ->
- ProTok $ inj_EToken meta $ Token_Term_Monoid_mempty a
- , term_fixity = infixN5
- }
- , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Monoid) g
+teMonoid_mappend :: TermDef Monoid '[Proxy a] (Monoid a #> (a -> a -> a))
+teMonoid_mappend = Term (tyMonoid a0) (a0 ~> a0 ~> a0) $ teSym @Monoid $ lam2 mappend