]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/MonoFunctor.hs
Renaming textI_app* to textI*.
[haskell/symantic.git] / Language / Symantic / Compiling / MonoFunctor.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
4 -- | Symantic for 'MonoFunctor'.
5 module Language.Symantic.Compiling.MonoFunctor where
6
7 import Control.Monad (liftM2)
8 import Data.Map.Strict (Map)
9 import Data.MonoTraversable (MonoFunctor)
10 import qualified Data.MonoTraversable as MT
11 import Data.Proxy
12 import Data.Text (Text)
13 import Data.Type.Equality ((:~:)(Refl))
14 import GHC.Exts (Constraint)
15 import qualified System.IO as IO
16
17 import Language.Symantic.Parsing
18 import Language.Symantic.Typing
19 import Language.Symantic.Compiling.Term
20 import Language.Symantic.Interpreting
21 import Language.Symantic.Transforming.Trans
22 import Language.Symantic.Lib.Data.Type.List hiding (Map)
23
24 -- * Class 'Sym_MonoFunctor'
25 class Sym_MonoFunctor term where
26 omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
27 default omap :: (Trans t term, MonoFunctor o)
28 => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
29 omap = trans_map2 omap
30
31 type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
32 type instance Consts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': Consts_imported_by MonoFunctor
33 type instance Consts_imported_by MonoFunctor =
34 [ Proxy (->)
35 , Proxy (,)
36 , Proxy []
37 , Proxy Either
38 , Proxy IO
39 , Proxy Map
40 , Proxy Maybe
41 , Proxy Text
42 ] ++ Consts_imported_by IO
43
44 instance Sym_MonoFunctor HostI where
45 omap = liftM2 MT.omap
46 instance Sym_MonoFunctor TextI where
47 omap = textI2 "omap"
48 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
49 omap = dupI2 (Proxy @Sym_MonoFunctor) omap
50
51 instance Const_from Text cs => Const_from Text (Proxy MonoFunctor ': cs) where
52 const_from "MonoFunctor" k = k (ConstZ kind)
53 const_from s k = const_from s $ k . ConstS
54 instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
55 show_const ConstZ{} = "MonoFunctor"
56 show_const (ConstS c) = show_const c
57
58 -- * Type 'Fam_MonoElement'
59 data Fam_MonoElement
60 = Fam_MonoElement
61 deriving (Eq, Show)
62 type instance Fam Fam_MonoElement '[h] = MT.Element (UnProxy h)
63
64 instance -- Constraint
65 Proj_FamC cs Fam_MonoElement (c::Constraint)
66 instance -- k -> Constraint
67 Proj_FamC cs Fam_MonoElement (c::k -> Constraint)
68 instance -- ()
69 Proj_FamC cs Fam_MonoElement ()
70 instance -- Bool
71 Proj_FamC cs Fam_MonoElement Bool
72 instance -- Char
73 Proj_FamC cs Fam_MonoElement Char
74 instance -- Text
75 ( Proj_Const cs Text
76 , Inj_Const cs (MT.Element Text)
77 ) => Proj_FamC cs Fam_MonoElement Text where
78 proj_famC _c _fam (TyConst c `TypesS` TypesZ)
79 | Just Refl <- eq_skind (kind_of_const c) SKiType
80 , Just Refl <- proj_const c (Proxy::Proxy Text)
81 = Just (TyConst inj_const::Type cs (MT.Element Text))
82 proj_famC _c _fam _ty = Nothing
83 instance -- []
84 ( Proj_Const cs []
85 ) => Proj_FamC cs Fam_MonoElement [] where
86 proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
87 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
88 , Just Refl <- proj_const c (Proxy::Proxy [])
89 = Just ty_a
90 proj_famC _c _fam _ty = Nothing
91 instance -- IO
92 ( Proj_Const cs IO
93 ) => Proj_FamC cs Fam_MonoElement IO where
94 proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
95 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
96 , Just Refl <- proj_const c (Proxy::Proxy IO)
97 = Just ty_a
98 proj_famC _c _fam _ty = Nothing
99 instance -- IO.Handle
100 Proj_FamC cs Fam_MonoElement IO.Handle
101 instance -- IO.IOMode
102 Proj_FamC cs Fam_MonoElement IO.IOMode
103 instance -- Maybe
104 ( Proj_Const cs Maybe
105 ) => Proj_FamC cs Fam_MonoElement Maybe where
106 proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
107 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
108 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
109 = Just ty_a
110 proj_famC _c _fam _ty = Nothing
111 instance -- (->)
112 ( Proj_Const cs (->)
113 ) => Proj_FamC cs Fam_MonoElement (->) where
114 proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
115 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
116 , Just Refl <- proj_const c (Proxy::Proxy (->))
117 = Just ty_a
118 proj_famC _c _fam _ty = Nothing
119 instance -- (,)
120 ( Proj_Const cs (,)
121 ) => Proj_FamC cs Fam_MonoElement (,) where
122 proj_famC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
123 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
124 , Just Refl <- proj_const c (Proxy::Proxy (,))
125 = Just ty_b
126 proj_famC _c _fam _ty = Nothing
127 instance -- Either
128 ( Proj_Const cs Either
129 ) => Proj_FamC cs Fam_MonoElement Either where
130 proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
131 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
132 , Just Refl <- proj_const c (Proxy::Proxy Either)
133 = Just ty_r
134 proj_famC _c _fam _ty = Nothing
135 instance -- Map
136 ( Proj_Const cs Map
137 ) => Proj_FamC cs Fam_MonoElement Map where
138 proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
139 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
140 , Just Refl <- proj_const c (Proxy::Proxy Map)
141 = Just ty_a
142 proj_famC _c _fam _ty = Nothing
143
144 instance -- Proj_ConC
145 ( Proj_Const cs MonoFunctor
146 , Proj_Consts cs (Consts_imported_by MonoFunctor)
147 ) => Proj_ConC cs (Proxy MonoFunctor) where
148 proj_conC _ (TyConst q :$ typ)
149 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
150 , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
151 = case typ of
152 TyConst c
153 | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
154 TyConst c :$ _a
155 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
156 -> case () of
157 _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
158 | Just Refl <- proj_const c (Proxy::Proxy IO) -> Just Con
159 | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
160 _ -> Nothing
161 TyConst c :$ _a :$ _b
162 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
163 -> case () of
164 _ | Just Refl <- proj_const c (Proxy::Proxy (->)) -> Just Con
165 | Just Refl <- proj_const c (Proxy::Proxy (,)) -> Just Con
166 | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
167 | Just Refl <- proj_const c (Proxy::Proxy Map) -> Just Con
168 _ -> Nothing
169 _ -> Nothing
170 proj_conC _c _q = Nothing
171 data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
172 = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
173 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
174 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
175 instance -- CompileI
176 ( Inj_Const (Consts_of_Ifaces is) MonoFunctor
177 , Inj_Const (Consts_of_Ifaces is) (->)
178 , Proj_Con (Consts_of_Ifaces is)
179 , Proj_Fam (Consts_of_Ifaces is) Fam_MonoElement
180 , Compile is
181 ) => CompileI is (Proxy MonoFunctor) where
182 compileI tok ctx k =
183 case tok of
184 Token_Term_MonoFunctor_omap tok_f tok_o ->
185 -- omap :: (Element o -> Element o) -> o -> o
186 compileO tok_f ctx $ \ty_f (TermO f) ->
187 compileO tok_o ctx $ \ty_o (TermO m) ->
188 check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
189 check_type
190 (At (Just tok_f) ty_f_a)
191 (At (Just tok_f) ty_f_b) $ \Refl ->
192 check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
193 check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
194 check_type
195 (At Nothing ty_o_e)
196 (At (Just tok_f) ty_f_a) $ \Refl ->
197 k ty_o $ TermO $
198 \c -> omap (f c) (m c)