]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Monad.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / 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.Typing
14 import Language.Symantic.Compiling
15 import Language.Symantic.Interpreting
16 import Language.Symantic.Transforming
17 import Language.Symantic.Lib.Applicative (Sym_Applicative)
18
19 -- * Class 'Sym_Monad'
20 class Sym_Applicative term => Sym_Monad term where
21 return :: Monad m => term a -> term (m a)
22 (>>=) :: Monad m => term (m a) -> term (a -> m b) -> term (m b); infixl 1 >>=
23 join :: Monad m => term (m (m a)) -> term (m a)
24 when :: Applicative f => term Bool -> term (f ()) -> term (f ())
25
26 default return :: (Trans t term, Monad m)
27 => t term a -> t term (m a)
28 default (>>=) :: (Trans t term, Monad m)
29 => t term (m a) -> t term (a -> m b) -> t term (m b)
30 default join :: (Trans t term, Monad m)
31 => t term (m (m a)) -> t term (m a)
32 default when :: (Trans t term, Applicative f)
33 => t term Bool -> t term (f ()) -> t term (f ())
34
35 return = trans_map1 return
36 (>>=) = trans_map2 (>>=)
37 join = trans_map1 join
38 when = trans_map2 when
39
40 type instance Sym_of_Iface (Proxy Monad) = Sym_Monad
41 type instance TyConsts_of_Iface (Proxy Monad) = Proxy Monad ': TyConsts_imported_by Monad
42 type instance TyConsts_imported_by Monad =
43 [ Proxy ()
44 , Proxy Applicative
45 , Proxy Bool
46 ]
47
48 instance Sym_Monad HostI where
49 return = Monad.liftM Monad.return
50 (>>=) = Monad.liftM2 (Monad.>>=)
51 join = Monad.liftM Monad.join
52 when = Monad.liftM2 Monad.when
53 instance Sym_Monad TextI where
54 return = textI1 "return"
55 (>>=) = textI_infix ">>=" (infixL 1)
56 join = textI1 "join"
57 when = textI2 "when"
58 instance (Sym_Monad r1, Sym_Monad r2) => Sym_Monad (DupI r1 r2) where
59 return = dupI1 @Sym_Monad return
60 (>>=) = dupI2 @Sym_Monad (>>=)
61 join = dupI1 @Sym_Monad join
62 when = dupI2 @Sym_Monad when
63
64 instance
65 ( Read_TyNameR TyName cs rs
66 , Inj_TyConst cs Monad
67 ) => Read_TyNameR TyName cs (Proxy Monad ': rs) where
68 read_TyNameR _cs (TyName "Monad") k = k (ty @Monad)
69 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
70 instance Show_TyConst cs => Show_TyConst (Proxy Monad ': cs) where
71 show_TyConst TyConstZ{} = "Monad"
72 show_TyConst (TyConstS c) = show_TyConst c
73
74 instance Proj_TyConC cs (Proxy Monad)
75 data instance TokenT meta (ts::[*]) (Proxy Monad)
76 = Token_Term_Monad_return (EToken meta '[Proxy Token_Type]) (EToken meta ts)
77 | Token_Term_Monad_bind (EToken meta ts) (EToken meta ts)
78 | Token_Term_Monad_join (EToken meta ts)
79 | Token_Term_Monad_when (EToken meta ts) (EToken meta ts)
80 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Monad))
81 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Monad))
82 instance -- CompileI
83 ( Read_TyName TyName (TyConsts_of_Ifaces is)
84 , Inj_TyConst (TyConsts_of_Ifaces is) Monad
85 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
86 , Inj_TyConst (TyConsts_of_Ifaces is) ()
87 , Inj_TyConst (TyConsts_of_Ifaces is) Applicative
88 , Inj_TyConst (TyConsts_of_Ifaces is) Bool
89 , Proj_TyCon (TyConsts_of_Ifaces is)
90 , Compile is
91 ) => CompileI is (Proxy Monad) where
92 compileI tok ctx k =
93 case tok of
94 Token_Term_Monad_return tok_ty_m tok_a ->
95 -- return :: Monad m => a -> m a
96 compile_Type tok_ty_m $ \(ty_m::Type (TyConsts_of_Ifaces is) m) ->
97 check_Kind
98 (At Nothing (SKiType `SKiArrow` SKiType))
99 (At (Just tok_ty_m) $ kind_of ty_m) $ \Refl ->
100 check_TyCon (At (Just tok_ty_m) (ty @Monad :$ ty_m)) $ \TyCon ->
101 compileO tok_a ctx $ \ty_a (TermO a) ->
102 k (ty_m :$ ty_a) $ TermO $
103 \c -> return (a c)
104 Token_Term_Monad_bind tok_ma tok_a2mb ->
105 -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
106 compileO tok_ma ctx $ \ty_ma (TermO ma) ->
107 compileO tok_a2mb ctx $ \ty_a2mb (TermO a2mb) ->
108 check_TyCon1 (ty @Monad) (At (Just tok_ma) ty_ma) $ \Refl TyCon ty_ma_m ty_ma_a ->
109 check_TyEq2 (ty @(->)) (At (Just tok_a2mb) ty_a2mb) $ \Refl ty_a2mb_a ty_a2mb_mb ->
110 check_TyEq1 ty_ma_m (At (Just tok_a2mb) ty_a2mb_mb) $ \Refl _ty_a2mb_mb_b ->
111 check_TyEq
112 (At (Just tok_a2mb) ty_a2mb_a)
113 (At (Just tok_ma) ty_ma_a) $ \Refl ->
114 k ty_a2mb_mb $ TermO $
115 \c -> (>>=) (ma c) (a2mb c)
116 Token_Term_Monad_join tok_mma ->
117 -- join :: Monad m => m (m a) -> m a
118 compileO tok_mma ctx $ \ty_mma (TermO mma) ->
119 check_TyCon1 (ty @Monad) (At (Just tok_mma) ty_mma) $ \Refl TyCon ty_mma_m ty_mma_ma ->
120 check_TyEq1 ty_mma_m (At (Just tok_mma) ty_mma_ma) $ \Refl _ty_mma_ma_a ->
121 k ty_mma_ma $ TermO $
122 \c -> join (mma c)
123 Token_Term_Monad_when tok_cond tok_ok ->
124 -- when :: Applicative f => Bool -> f () -> f ()
125 compileO tok_cond ctx $ \ty_cond (TermO cond) ->
126 compileO tok_ok ctx $ \ty_ok (TermO ok) ->
127 check_TyCon1 (ty @Applicative) (At (Just tok_ok) ty_ok) $ \Refl TyCon _ty_ok_f ty_ok_u ->
128 check_TyEq
129 (At Nothing (ty @Bool))
130 (At (Just tok_cond) ty_cond) $ \Refl ->
131 check_TyEq
132 (At Nothing (ty @()))
133 (At (Just tok_ok) ty_ok_u) $ \Refl ->
134 k ty_ok $ TermO $
135 \c -> when (cond c) (ok c)
136 instance -- TokenizeT
137 Inj_Token meta ts Monad =>
138 TokenizeT meta ts (Proxy Monad) where
139 tokenizeT _t = mempty
140 { tokenizers_infix = tokenizeTMod []
141 [ (Term_Name "Nothing",) Term_ProTok
142 { term_protok = \meta -> ProTokPi $ \m -> ProTokLam $ \a ->
143 ProTok $ inj_EToken meta $ Token_Term_Monad_return m a
144 , term_fixity = infixN5
145 }
146 , tokenize2 ">>=" (infixL 1) Token_Term_Monad_bind
147 , tokenize1 "join" infixN5 Token_Term_Monad_join
148 , tokenize2 "when" infixN5 Token_Term_Monad_when
149 ]
150 }
151 instance Gram_Term_AtomsT meta ts (Proxy Monad) g