]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Monoid.hs
Fix Inj_ConstP -> Inj_TyConstP.
[haskell/symantic.git] / 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 -- | 'mappend' alias.
45 --
46 -- TODO: move to Semigroup
47 (<>) ::
48 ( Sym_Monoid term
49 , Monoid a )
50 => term a -> term a -> term a
51 (<>) = mappend
52 infixr 6 <>
53
54 instance
55 ( Read_TyNameR TyName cs rs
56 , Inj_TyConst cs Monoid
57 ) => Read_TyNameR TyName cs (Proxy Monoid ': rs) where
58 read_TyNameR _cs (TyName "Monoid") k = k (ty @Monoid)
59 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
60 instance Show_TyConst cs => Show_TyConst (Proxy Monoid ': cs) where
61 show_TyConst TyConstZ{} = "Monoid"
62 show_TyConst (TyConstS c) = show_TyConst c
63
64 instance Proj_TyConC cs (Proxy Monoid)
65 data instance TokenT meta (ts::[*]) (Proxy Monoid)
66 = Token_Term_Monoid_mempty (EToken meta '[Proxy Token_Type])
67 | Token_Term_Monoid_mappend (EToken meta ts)
68 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monoid))
69 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monoid))
70 instance -- CompileI
71 ( Read_TyName TyName (TyConsts_of_Ifaces is)
72 , Inj_TyConst (TyConsts_of_Ifaces is) Monoid
73 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
74 , Proj_TyCon (TyConsts_of_Ifaces is)
75 , Compile is
76 ) => CompileI is (Proxy Monoid) where
77 compileI tok ctx k =
78 case tok of
79 Token_Term_Monoid_mempty tok_ty_a ->
80 -- mempty :: Monoid a => a
81 compile_Type tok_ty_a $ \(ty_a::Type (TyConsts_of_Ifaces is) a) ->
82 check_Kind
83 (At Nothing SKiType)
84 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
85 check_TyCon (At (Just tok_ty_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
86 k ty_a $ TermO $ Fun.const mempty
87 Token_Term_Monoid_mappend tok_a ->
88 -- mappend :: Monoid a => a -> a -> a
89 compileO tok_a ctx $ \ty_a (TermO x) ->
90 check_TyCon (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \TyCon ->
91 k (ty_a ~> ty_a) $ TermO $
92 \c -> lam $ \y -> mappend (x c) y
93 instance -- TokenizeT
94 Inj_Token meta ts Monoid =>
95 TokenizeT meta ts (Proxy Monoid) where
96 tokenizeT _t = Monoid.mempty
97 { tokenizers_infix = tokenizeTMod []
98 [ (Term_Name "mempty",) Term_ProTok
99 { term_protok = \meta -> ProTokPi $ \a ->
100 ProTok $ inj_EToken meta $ Token_Term_Monoid_mempty a
101 , term_fixity = infixN5
102 }
103 , tokenize1 "mappend" infixN5 Token_Term_Monoid_mappend
104 , tokenize1 "<>" (infixR 6) Token_Term_Monoid_mappend
105 ]
106 }
107 instance Gram_Term_AtomsT meta ts (Proxy Monoid) g