]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Monoid.hs
Renaming textI_app* to textI*.
[haskell/symantic.git] / 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 = textI0 "mempty"
39 mappend = textI2 "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 -- CompileI
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 , Compile is
71 ) => CompileI is (Proxy Monoid) where
72 compileI tok ctx k =
73 case tok of
74 Token_Term_Monoid_mempty tok_ty_a ->
75 -- mempty :: Monoid a => a
76 compile_type 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 $ TermO $ Fun.const mempty
82 Token_Term_Monoid_mappend tok_a ->
83 -- mappend :: Monoid a => a -> a -> a
84 compileO tok_a ctx $ \ty_a (TermO x) ->
85 check_con (At (Just tok_a) (ty @Monoid :$ ty_a)) $ \Con ->
86 k (ty_a ~> ty_a) $ TermO $
87 \c -> lam $ \y -> mappend (x c) y