]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Map.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Map.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
4 -- | Symantic for 'Map'.
5 module Language.Symantic.Lib.Map where
6
7 import Control.Monad (liftM, liftM2, liftM3)
8 import Data.Map.Strict (Map)
9 import Data.MonoTraversable (MonoFunctor)
10 import Data.Proxy
11 import Data.Type.Equality ((:~:)(Refl))
12 import Prelude hiding (either)
13 import qualified Data.Map.Strict as Map
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming
20 import Language.Symantic.Lib.Lambda
21 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
22
23 -- * Class 'Sym_Map'
24 class Sym_Map term where
25 map_fromList :: Ord k => term [(k, a)] -> term (Map k a)
26 map_mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
27 map_lookup :: Ord k => term k -> term (Map k a) -> term (Maybe a)
28 map_keys :: term (Map k a) -> term [k]
29 map_member :: Ord k => term k -> term (Map k a) -> term Bool
30 map_insert :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
31 map_delete :: Ord k => term k -> term (Map k a) -> term (Map k a)
32 map_difference :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
33 map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
34
35 default map_fromList :: (Trans t term, Ord k) => t term [(k, a)] -> t term (Map k a)
36 default map_mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
37 default map_lookup :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Maybe a)
38 default map_keys :: Trans t term => t term (Map k a) -> t term [k]
39 default map_member :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term Bool
40 default map_insert :: (Trans t term, Ord k) => t term k -> t term a -> t term (Map k a) -> t term (Map k a)
41 default map_delete :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Map k a)
42 default map_difference :: (Trans t term, Ord k) => t term (Map k a) -> t term (Map k b) -> t term (Map k a)
43 default map_foldrWithKey :: Trans t term => t term (k -> a -> b -> b) -> t term b -> t term (Map k a) -> t term b
44
45 map_fromList = trans_map1 map_fromList
46 map_mapWithKey = trans_map2 map_mapWithKey
47 map_lookup = trans_map2 map_lookup
48 map_keys = trans_map1 map_keys
49 map_member = trans_map2 map_member
50 map_insert = trans_map3 map_insert
51 map_delete = trans_map2 map_delete
52 map_difference = trans_map2 map_difference
53 map_foldrWithKey = trans_map3 map_foldrWithKey
54
55 type instance Sym_of_Iface (Proxy Map) = Sym_Map
56 type instance TyConsts_of_Iface (Proxy Map) = Proxy Map ': TyConsts_imported_by (Proxy Map)
57 type instance TyConsts_imported_by (Proxy Map) =
58 [ Proxy (->)
59 , Proxy []
60 , Proxy (,)
61 , Proxy Bool
62 , Proxy Eq
63 , Proxy Foldable
64 , Proxy Functor
65 , Proxy Maybe
66 , Proxy Monad
67 , Proxy MonoFunctor
68 , Proxy Monoid
69 , Proxy Ord
70 , Proxy Traversable
71 , Proxy Show
72 ]
73
74 instance Sym_Map HostI where
75 map_fromList = liftM Map.fromList
76 map_mapWithKey = liftM2 Map.mapWithKey
77 map_lookup = liftM2 Map.lookup
78 map_keys = liftM Map.keys
79 map_member = liftM2 Map.member
80 map_insert = liftM3 Map.insert
81 map_delete = liftM2 Map.delete
82 map_difference = liftM2 Map.difference
83 map_foldrWithKey = liftM3 Map.foldrWithKey
84 instance Sym_Map TextI where
85 map_fromList = textI1 "Map.fromList"
86 map_mapWithKey = textI2 "Map.mapWithKey"
87 map_lookup = textI2 "Map.lookup"
88 map_keys = textI1 "Map.keys"
89 map_member = textI2 "Map.member"
90 map_insert = textI3 "Map.insert"
91 map_delete = textI2 "Map.delete"
92 map_difference = textI2 "Map.difference"
93 map_foldrWithKey = textI3 "Map.foldrWithKey"
94 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where
95 map_fromList = dupI1 @Sym_Map map_fromList
96 map_mapWithKey = dupI2 @Sym_Map map_mapWithKey
97 map_lookup = dupI2 @Sym_Map map_lookup
98 map_keys = dupI1 @Sym_Map map_keys
99 map_member = dupI2 @Sym_Map map_member
100 map_insert = dupI3 @Sym_Map map_insert
101 map_delete = dupI2 @Sym_Map map_delete
102 map_difference = dupI2 @Sym_Map map_difference
103 map_foldrWithKey = dupI3 @Sym_Map map_foldrWithKey
104
105 instance
106 ( Read_TyNameR TyName cs rs
107 , Inj_TyConst cs Map
108 ) => Read_TyNameR TyName cs (Proxy Map ': rs) where
109 read_TyNameR _cs (TyName "Map") k = k (ty @Map)
110 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
111 instance Show_TyConst cs => Show_TyConst (Proxy Map ': cs) where
112 show_TyConst TyConstZ{} = "Map"
113 show_TyConst (TyConstS c) = show_TyConst c
114
115 instance -- Proj_TyFamC TyFam_MonoElement
116 ( Proj_TyConst cs Map
117 ) => Proj_TyFamC cs TyFam_MonoElement Map where
118 proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
119 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
120 , Just Refl <- proj_TyConst c (Proxy @Map)
121 = Just ty_a
122 proj_TyFamC _c _fam _ty = Nothing
123
124 instance -- Proj_TyConC
125 ( Proj_TyConst cs Map
126 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Map))
127 , Proj_TyCon cs
128 , Inj_TyConst cs Ord
129 ) => Proj_TyConC cs (Proxy Map) where
130 proj_TyConC _ (TyConst q :$ (TyConst c :$ _k))
131 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
132 , Just Refl <- proj_TyConst c (Proxy @Map)
133 = case () of
134 _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
135 | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
136 | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
137 _ -> Nothing
138 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
139 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
140 , Just Refl <- proj_TyConst c (Proxy @Map)
141 = case () of
142 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
143 , Just TyCon <- proj_TyCon (t :$ k)
144 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
145 | Just Refl <- proj_TyConst q (Proxy @Ord)
146 , Just TyCon <- proj_TyCon (t :$ k)
147 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
148 | Just Refl <- proj_TyConst q (Proxy @Monoid)
149 , Just TyCon <- proj_TyCon (ty @Ord :$ k) -> Just TyCon
150 | Just Refl <- proj_TyConst q (Proxy @Show)
151 , Just TyCon <- proj_TyCon (t :$ k)
152 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
153 | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
154 _ -> Nothing
155 proj_TyConC _c _q = Nothing
156 data instance TokenT meta (ts::[*]) (Proxy Map)
157 = Token_Term_Map_fromList (EToken meta ts)
158 | Token_Term_Map_mapWithKey (EToken meta ts)
159 | Token_Term_Map_lookup (EToken meta ts) (EToken meta ts)
160 | Token_Term_Map_keys (EToken meta ts)
161 | Token_Term_Map_member (EToken meta ts) (EToken meta ts)
162 | Token_Term_Map_insert (EToken meta ts) (EToken meta ts)
163 | Token_Term_Map_delete (EToken meta ts) (EToken meta ts)
164 | Token_Term_Map_difference (EToken meta ts) (EToken meta ts)
165 | Token_Term_Map_foldrWithKey (EToken meta ts)
166 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Map))
167 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Map))
168
169 instance -- CompileI
170 ( Inj_TyConst cs Map
171 , Inj_TyConst cs (->)
172 , Inj_TyConst cs Bool
173 , Inj_TyConst cs Ord
174 , Inj_TyConst cs Maybe
175 , Inj_TyConst cs []
176 , Inj_TyConst cs (,)
177 , Proj_TyCon cs
178 , Compile cs is
179 ) => CompileI cs is (Proxy Map) where
180 compileI tok ctx k =
181 case tok of
182 Token_Term_Map_fromList tok_l ->
183 -- fromList :: Ord k => [(k, a)] -> Map k a
184 compileO tok_l ctx $ \ty_l (TermO l) ->
185 check_TyEq1 (ty @[]) (At (Just tok_l) ty_l) $ \Refl ty_l_t2 ->
186 check_TyEq2 (ty @(,)) (At (Just tok_l) ty_l_t2) $ \Refl ty_k ty_a ->
187 check_TyCon (At (Just tok_l) (ty @Ord :$ ty_k)) $ \TyCon ->
188 k ((ty @Map :$ ty_k) :$ ty_a) $ TermO $
189 \c -> map_fromList (l c)
190 Token_Term_Map_mapWithKey tok_k2a2b ->
191 -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
192 compileO tok_k2a2b ctx $ \ty_k2a2b (TermO k2a2b) ->
193 check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_k2a2b) $ \Refl ty_k ty_a2b ->
194 check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_a2b) $ \Refl ty_a ty_b ->
195 k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_b) $ TermO $
196 \c -> lam $ map_mapWithKey (k2a2b c)
197 Token_Term_Map_lookup tok_k tok_m ->
198 -- lookup :: Ord k => k -> Map k a -> Maybe a
199 compileO tok_k ctx $ \ty_k (TermO k_) ->
200 compileO tok_m ctx $ \ty_m (TermO m) ->
201 check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
202 check_TyEq
203 (At (Just tok_k) ty_k)
204 (At (Just tok_m) ty_m_k) $ \Refl ->
205 check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
206 k (ty @Maybe :$ ty_m_a) $ TermO $
207 \c -> map_lookup (k_ c) (m c)
208 Token_Term_Map_keys tok_m ->
209 -- keys :: Map k a -> [k]
210 compileO tok_m ctx $ \ty_m (TermO m) ->
211 check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
212 k (ty @[] :$ ty_m_k) $ TermO $
213 \c -> map_keys (m c)
214 Token_Term_Map_member tok_k tok_m ->
215 -- member :: Ord k => k -> Map k a -> Bool
216 compileO tok_k ctx $ \ty_k (TermO k_) ->
217 compileO tok_m ctx $ \ty_m (TermO m) ->
218 check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
219 check_TyEq
220 (At (Just tok_k) ty_k)
221 (At (Just tok_m) ty_m_k) $ \Refl ->
222 check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
223 k (ty @Bool) $ TermO $
224 \c -> map_member (k_ c) (m c)
225 Token_Term_Map_insert tok_k tok_a ->
226 -- insert :: Ord k => k -> a -> Map k a -> Map k a
227 compileO tok_k ctx $ \ty_k (TermO k_) ->
228 compileO tok_a ctx $ \ty_a (TermO a) ->
229 check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
230 k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_a) $ TermO $
231 \c -> lam $ map_insert (k_ c) (a c)
232 Token_Term_Map_delete tok_k tok_m ->
233 -- delete :: Ord k => k -> Map k a -> Map k a
234 compileO tok_k ctx $ \ty_k (TermO k_) ->
235 compileO tok_m ctx $ \ty_m (TermO m) ->
236 check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
237 check_TyEq
238 (At (Just tok_k) ty_k)
239 (At (Just tok_m) ty_m_k) $ \Refl ->
240 check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
241 k (((ty @Map) :$ ty_k) :$ ty_m_a) $ TermO $
242 \c -> map_delete (k_ c) (m c)
243 Token_Term_Map_difference tok_ma tok_mb ->
244 -- difference :: Ord k => Map k a -> Map k b -> Map k a
245 compileO tok_ma ctx $ \ty_ma (TermO ma) ->
246 compileO tok_mb ctx $ \ty_mb (TermO mb) ->
247 check_TyEq2 (ty @Map) (At (Just tok_ma) ty_ma) $ \Refl ty_ma_k ty_ma_a ->
248 check_TyEq2 (ty @Map) (At (Just tok_mb) ty_mb) $ \Refl ty_mb_k _ty_mb_b ->
249 check_TyEq
250 (At (Just tok_ma) ty_ma_k)
251 (At (Just tok_mb) ty_mb_k) $ \Refl ->
252 check_TyCon (At (Just tok_ma) (ty @Ord :$ ty_ma_k)) $ \TyCon ->
253 k ((ty @Map :$ ty_ma_k) :$ ty_ma_a) $ TermO $
254 \c -> map_difference (ma c) (mb c)
255 Token_Term_Map_foldrWithKey tok_f ->
256 -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
257 compileO tok_f ctx $ \ty_f (TermO f) ->
258 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_k ty_fabb ->
259 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fabb) $ \Refl ty_a ty_fbb ->
260 check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fbb) $ \Refl ty_b ty_b' ->
261 check_TyEq
262 (At (Just tok_f) ty_b)
263 (At (Just tok_f) ty_b') $ \Refl ->
264 k (ty_b ~> (ty @Map :$ ty_k) :$ ty_a ~> ty_b) $ TermO $
265 \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m
266 instance -- TokenizeT
267 Inj_Token meta ts Map =>
268 TokenizeT meta ts (Proxy Map) where
269 tokenizeT _t = mempty
270 { tokenizers_infix = tokenizeTMod [Mod_Name "Map"]
271 [ tokenize1 "fromList" infixN5 Token_Term_Map_fromList
272 , tokenize1 "mapWithKey" infixN5 Token_Term_Map_mapWithKey
273 , tokenize2 "lookup" infixN5 Token_Term_Map_lookup
274 , tokenize1 "keys" infixN5 Token_Term_Map_keys
275 , tokenize2 "member" infixN5 Token_Term_Map_member
276 , tokenize2 "insert" infixN5 Token_Term_Map_insert
277 , tokenize2 "delete" infixN5 Token_Term_Map_delete
278 , tokenize2 "difference" infixN5 Token_Term_Map_difference
279 , tokenize1 "foldrWithKey" infixN5 Token_Term_Map_foldrWithKey
280 ]
281 }
282 instance Gram_Term_AtomsT meta ts (Proxy Map) g