]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Monad.hs
Fix Lib.Text.
[haskell/symantic.git] / Language / Symantic / Lib / Monad.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Monad'.
4 module Language.Symantic.Lib.Monad where
5
6 import Control.Monad (Monad)
7 import qualified Control.Monad as Monad
8 import Data.Proxy
9 import Data.Type.Equality ((:~:)(Refl))
10 import Prelude hiding (Monad(..))
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Parsing.Grammar
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming.Trans
18 import Language.Symantic.Lib.Applicative (Sym_Applicative)
19
20 -- * Class 'Sym_Monad'
21 class Sym_Applicative term => Sym_Monad term where
22 return :: Monad m => term a -> term (m a)
23 (>>=) :: Monad m => term (m a) -> term (a -> m b) -> term (m b)
24 join :: Monad m => term (m (m a)) -> term (m a)
25 when :: Applicative f => term Bool -> term (f ()) -> term (f ())
26
27 default return :: (Trans t term, Monad m)
28 => t term a -> t term (m a)
29 default (>>=) :: (Trans t term, Monad m)
30 => t term (m a) -> t term (a -> m b) -> t term (m b)
31 default join :: (Trans t term, Monad m)
32 => t term (m (m a)) -> t term (m a)
33 default when :: (Trans t term, Applicative f)
34 => t term Bool -> t term (f ()) -> t term (f ())
35
36 return = trans_map1 return
37 (>>=) = trans_map2 (>>=)
38 join = trans_map1 join
39 when = trans_map2 when
40
41 infixl 1 >>=
42
43 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
44 type instance Consts_of_Iface (Proxy Monad) = Proxy Monad ': Consts_imported_by Monad
45 type instance Consts_imported_by Monad =
46 [ Proxy ()
47 , Proxy Applicative
48 , Proxy Bool
49 ]
50
51 instance Sym_Monad HostI where
52 return = Monad.liftM Monad.return
53 (>>=) = Monad.liftM2 (Monad.>>=)
54 join = Monad.liftM Monad.join
55 when = Monad.liftM2 Monad.when
56 instance Sym_Monad TextI where
57 return = textI1 "return"
58 (>>=) = textI_infix ">>=" (infixL 1)
59 join = textI1 "join"
60 when = textI2 "when"
61 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
62 return = dupI1 (Proxy @Sym_Monad) return
63 (>>=) = dupI2 (Proxy @Sym_Monad) (>>=)
64 join = dupI1 (Proxy @Sym_Monad) join
65 when = dupI2 (Proxy @Sym_Monad) when
66
67 instance
68 ( Read_TypeNameR Type_Name cs rs
69 , Inj_Const cs Monad
70 ) => Read_TypeNameR Type_Name cs (Proxy Monad ': rs) where
71 read_typenameR _cs (Type_Name "Monad") k = k (ty @Monad)
72 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
73 instance Show_Const cs => Show_Const (Proxy Monad ': cs) where
74 show_const ConstZ{} = "Monad"
75 show_const (ConstS c) = show_const c
76
77 instance Proj_ConC cs (Proxy Monad)
78 data instance TokenT meta (ts::[*]) (Proxy Monad)
79 = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
80 | Token_Term_Monad_bind (EToken meta ts) (EToken meta ts)
81 | Token_Term_Monad_join (EToken meta ts)
82 | Token_Term_Monad_when (EToken meta ts) (EToken meta ts)
83 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
84 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
85 instance -- CompileI
86 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
87 , Inj_Const (Consts_of_Ifaces is) Monad
88 , Inj_Const (Consts_of_Ifaces is) (->)
89 , Inj_Const (Consts_of_Ifaces is) ()
90 , Inj_Const (Consts_of_Ifaces is) Applicative
91 , Inj_Const (Consts_of_Ifaces is) Bool
92 , Proj_Con (Consts_of_Ifaces is)
93 , Compile is
94 ) => CompileI is (Proxy Monad) where
95 compileI tok ctx k =
96 case tok of
97 Token_Term_Monad_return tok_ty_m tok_a ->
98 -- return :: Monad m => a -> m a
99 compile_type tok_ty_m $ \(ty_m::Type (Consts_of_Ifaces is) m) ->
100 check_kind
101 (At Nothing (SKiType `SKiArrow` SKiType))
102 (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
103 check_con (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \Con ->
104 compileO tok_a ctx $ \ty_a (TermO a) ->
105 k (ty_m :$ ty_a) $ TermO $
106 \c -> return (a c)
107 Token_Term_Monad_bind tok_ma tok_a2mb ->
108 -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
109 compileO tok_ma ctx $ \ty_ma (TermO ma) ->
110 compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
111 check_con1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl Con ty_ma_m ty_ma_a ->
112 check_type2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
113 check_type1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
114 check_type
115 (At (Just tok_a2mb) ty_a2mb_a)
116 (At (Just tok_ma) ty_ma_a) $ \Refl ->
117 k ty_a2mb_mb $ TermO $
118 \c -> (>>=) (ma c) (a2mb c)
119 Token_Term_Monad_join tok_mma ->
120 -- join :: Monad m => m (m a) -> m a
121 compileO tok_mma ctx $ \ty_mma (TermO mma) ->
122 check_con1 (ty @Monad) (At (Just tok_mma) ty_mma) $ \Refl Con ty_mma_m ty_mma_ma ->
123 check_type1 ty_mma_m (At (Just tok_mma) ty_mma_ma) $ \Refl _ty_mma_ma_a ->
124 k ty_mma_ma $ TermO $
125 \c -> join (mma c)
126 Token_Term_Monad_when tok_cond tok_ok ->
127 -- when :: Applicative f => Bool -> f () -> f ()
128 compileO tok_cond ctx $ \ty_cond (TermO cond) ->
129 compileO tok_ok ctx $ \ty_ok (TermO ok) ->
130 check_con1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl Con _ty_ok_f ty_ok_u ->
131 check_type
132 (At Nothing (ty @Bool))
133 (At (Just tok_cond) ty_cond) $ \Refl ->
134 check_type
135 (At Nothing (ty @()))
136 (At (Just tok_ok) ty_ok_u) $ \Refl ->
137 k ty_ok $ TermO $
138 \c -> when (cond c) (ok c)
139 instance -- TokenizeT
140 Inj_Token meta ts Monad =>
141 TokenizeT meta ts (Proxy Monad) where
142 tokenizeT _t = mempty
143 { tokenizers_infix = tokenizeTMod []
144 [ (Term_Name "Nothing",) Term_ProTok
145 { term_protok = \meta -> ProTokPi $ \m -> ProTokLam $ \a ->
146 ProTok $ inj_etoken meta $ Token_Term_Monad_return m a
147 , term_fixity = infixN5
148 }
149 , tokenize2 ">>=" (infixL 1) Token_Term_Monad_bind
150 , tokenize1 "join" infixN5 Token_Term_Monad_join
151 , tokenize2 "when" infixN5 Token_Term_Monad_when
152 ]
153 }
154 instance Gram_Term_AtomsT meta ts (Proxy Monad) g