]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Expr/Map.hs
explore parsing of partially applied functions
[haskell/symantic.git] / Language / Symantic / Expr / Map.hs
1 {-# LANGUAGE DefaultSignatures #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# OPTIONS_GHC -fno-warn-orphans #-}
9 -- | Expression for 'Map'.
10 module Language.Symantic.Expr.Map where
11
12 import Control.Monad
13 import Data.Map.Strict (Map)
14 import qualified Data.Map.Strict as Map
15 import Data.Proxy (Proxy(..))
16 import Data.Type.Equality ((:~:)(Refl))
17
18 import Language.Symantic.Type
19 import Language.Symantic.Repr
20 import Language.Symantic.Expr.Root
21 import Language.Symantic.Expr.Error
22 import Language.Symantic.Expr.From
23 import Language.Symantic.Expr.Lambda
24 import Language.Symantic.Expr.List
25 import Language.Symantic.Expr.Tuple
26 import Language.Symantic.Trans.Common
27
28 -- * Class 'Sym_Map_Lam'
29 -- | Symantic.
30 class Sym_Map repr where
31 map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
32 mapWithKey :: repr (k -> a -> b) -> repr (Map k a) -> repr (Map k b)
33 map_lookup :: Ord k => repr k -> repr (Map k a) -> repr (Maybe a)
34 map_keys :: repr (Map k a) -> repr [k]
35 map_member :: Ord k => repr k -> repr (Map k a) -> repr Bool
36 map_insert :: Ord k => repr k -> repr a -> repr (Map k a) -> repr (Map k a)
37 map_delete :: Ord k => repr k -> repr (Map k a) -> repr (Map k a)
38 map_difference :: Ord k => repr (Map k a) -> repr (Map k b) -> repr (Map k a)
39 map_foldrWithKey :: repr (k -> a -> b -> b) -> repr b -> repr (Map k a) -> repr b
40
41 default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
42 default mapWithKey :: Trans t repr => t repr (k -> a -> b) -> t repr (Map k a) -> t repr (Map k b)
43 default map_lookup :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Maybe a)
44 default map_keys :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr [k]
45 default map_member :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr Bool
46 default map_insert :: (Trans t repr, Ord k) => t repr k -> t repr a -> t repr (Map k a) -> t repr (Map k a)
47 default map_delete :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Map k a)
48 default map_difference :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr (Map k b) -> t repr (Map k a)
49 default map_foldrWithKey :: Trans t repr => t repr (k -> a -> b -> b) -> t repr b -> t repr (Map k a) -> t repr b
50
51 map_from_list = trans_map1 map_from_list
52 mapWithKey = trans_map2 mapWithKey
53 map_lookup = trans_map2 map_lookup
54 map_keys = trans_map1 map_keys
55 map_member = trans_map2 map_member
56 map_insert = trans_map3 map_insert
57 map_delete = trans_map2 map_delete
58 map_difference = trans_map2 map_difference
59 map_foldrWithKey = trans_map3 map_foldrWithKey
60 instance Sym_Map Repr_Host where
61 map_from_list = liftM Map.fromList
62 mapWithKey = liftM2 Map.mapWithKey
63 map_lookup = liftM2 Map.lookup
64 map_keys = liftM Map.keys
65 map_member = liftM2 Map.member
66 map_insert = liftM3 Map.insert
67 map_delete = liftM2 Map.delete
68 map_difference = liftM2 Map.difference
69 map_foldrWithKey = liftM3 Map.foldrWithKey
70 instance Sym_Map Repr_Text where
71 map_from_list = repr_text_app1 "map_from_list"
72 mapWithKey = repr_text_app2 "mapWithKey"
73 map_lookup = repr_text_app2 "map_lookup"
74 map_keys = repr_text_app1 "map_keys"
75 map_member = repr_text_app2 "map_member"
76 map_insert = repr_text_app3 "map_insert"
77 map_delete = repr_text_app2 "map_delete"
78 map_difference = repr_text_app2 "map_difference"
79 map_foldrWithKey = repr_text_app3 "map_foldrWithKey"
80 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Repr_Dup r1 r2) where
81 map_from_list (l1 `Repr_Dup` l2) =
82 map_from_list l1 `Repr_Dup` map_from_list l2
83 mapWithKey (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
84 mapWithKey f1 m1 `Repr_Dup` mapWithKey f2 m2
85 map_lookup (k1 `Repr_Dup` k2) (m1 `Repr_Dup` m2) =
86 map_lookup k1 m1 `Repr_Dup` map_lookup k2 m2
87 map_keys (m1 `Repr_Dup` m2) =
88 map_keys m1 `Repr_Dup` map_keys m2
89 map_member (k1 `Repr_Dup` k2) (m1 `Repr_Dup` m2) =
90 map_member k1 m1 `Repr_Dup` map_member k2 m2
91 map_insert (k1 `Repr_Dup` k2) (a1 `Repr_Dup` a2) (m1 `Repr_Dup` m2) =
92 map_insert k1 a1 m1 `Repr_Dup` map_insert k2 a2 m2
93 map_delete (k1 `Repr_Dup` k2) (m1 `Repr_Dup` m2) =
94 map_delete k1 m1 `Repr_Dup` map_delete k2 m2
95 map_difference (ma1 `Repr_Dup` ma2) (mb1 `Repr_Dup` mb2) =
96 map_difference ma1 mb1 `Repr_Dup` map_difference ma2 mb2
97 map_foldrWithKey (f1 `Repr_Dup` f2) (b1 `Repr_Dup` b2) (m1 `Repr_Dup` m2) =
98 map_foldrWithKey f1 b1 m1 `Repr_Dup` map_foldrWithKey f2 b2 m2
99
100 -- | Parsing utility to check that the given type is a 'Type_List'
101 -- or raise 'Error_Expr_Type_mismatch'.
102 check_type_map
103 :: forall ast ex root ty h ret.
104 ( root ~ Root_of_Expr ex
105 , ty ~ Type_Root_of_Expr ex
106 , Type0_Lift Type_Map (Type_of_Expr root)
107 , Type0_Unlift Type_Map (Type_of_Expr root)
108 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
109 (Error_of_Expr ast root)
110 )
111 => Proxy ex -> ast -> ty h
112 -> (Type_Map ty h -> Either (Error_of_Expr ast root) ret)
113 -> Either (Error_of_Expr ast root) ret
114 check_type_map ex ast ty k =
115 case type0_unlift $ unType_Root ty of
116 Just ty_l -> k ty_l
117 Nothing -> Left $
118 error_expr ex $
119 Error_Expr_Type_mismatch ast
120 (Exists_Type0 (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
121 :: ty (Map Var0 Var0)))
122 (Exists_Type0 ty)
123
124 -- | Parse 'map_from_list'.
125 map_from_list_from
126 :: forall root ty ast hs ret.
127 ( ty ~ Type_Root_of_Expr (Expr_Map root)
128 , Expr_From ast root
129 , Type0_Lift Type_List (Type_of_Expr root)
130 , Type0_Unlift Type_List (Type_of_Expr root)
131 , Type0_Lift Type_Map (Type_of_Expr root)
132 , Type0_Lift Type_Tuple2 (Type_of_Expr root)
133 , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
134 , Type0_Constraint Ord ty
135 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
136 (Error_of_Expr ast root)
137 , Root_of_Expr root ~ root
138 ) => ast
139 -> ExprFrom ast (Expr_Map root) hs ret
140 map_from_list_from ast_l ex ast ctx k =
141 expr_from (Proxy::Proxy root) ast_l ctx $
142 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
143 check_type_list ex ast ty_l $ \(Type1 _ ty_l_t) ->
144 check_type_tuple2 ex ast ty_l_t $ \(Type2 Proxy ty_k ty_a) ->
145 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
146 k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
147 \c -> map_from_list (l c)
148
149 -- | Parse 'mapWithKey'.
150 mapWithKey_from
151 :: forall root ty ast hs ret.
152 ( ty ~ Type_Root_of_Expr (Expr_Map root)
153 , Type0_Eq ty
154 , Expr_From ast root
155 , Type0_Lift Type_Fun (Type_of_Expr root)
156 , Type0_Unlift Type_Fun (Type_of_Expr root)
157 , Type0_Lift Type_Map (Type_of_Expr root)
158 , Type0_Unlift Type_Map (Type_of_Expr root)
159 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
160 (Error_of_Expr ast root)
161 , Root_of_Expr root ~ root
162 ) => ast -> ast
163 -> ExprFrom ast (Expr_Map root) hs ret
164 mapWithKey_from ast_f ast_m ex ast ctx k =
165 -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
166 expr_from (Proxy::Proxy root) ast_f ctx $
167 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
168 expr_from (Proxy::Proxy root) ast_m ctx $
169 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
170 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_k ty_f_a2b
171 :: Type_Fun ty h_f) ->
172 check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b
173 :: Type_Fun ty h_f_a2b) ->
174 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
175 check_type0_eq ex ast ty_f_k ty_m_k $ \Refl ->
176 check_type0_eq ex ast ty_f_a ty_m_a $ \Refl ->
177 k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
178 \c -> mapWithKey (f c) (m c)
179
180 -- | Parse 'map_lookup'.
181 map_lookup_from
182 :: forall root ty ast hs ret.
183 ( ty ~ Type_Root_of_Expr (Expr_Map root)
184 , Type0_Eq ty
185 , Expr_From ast root
186 , Type0_Lift Type_Map (Type_of_Expr root)
187 , Type0_Unlift Type_Map (Type_of_Expr root)
188 , Type0_Lift Type_Maybe (Type_of_Expr root)
189 , Type0_Constraint Ord ty
190 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
191 (Error_of_Expr ast root)
192 , Root_of_Expr root ~ root
193 ) => ast -> ast
194 -> ExprFrom ast (Expr_Map root) hs ret
195 map_lookup_from ast_k ast_m ex ast ctx k =
196 -- lookup :: Ord k => k -> Map k a -> Maybe a
197 expr_from (Proxy::Proxy root) ast_k ctx $
198 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
199 expr_from (Proxy::Proxy root) ast_m ctx $
200 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
201 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
202 check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
203 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
204 k (type_maybe ty_m_a) $ Forall_Repr_with_Context $
205 \c -> map_lookup (key c) (m c)
206
207 -- | Parse 'map_keys'.
208 map_keys_from
209 :: forall root ty ast hs ret.
210 ( ty ~ Type_Root_of_Expr (Expr_Map root)
211 , Type0_Eq ty
212 , Expr_From ast root
213 , Type0_Lift Type_Map (Type_of_Expr root)
214 , Type0_Unlift Type_Map (Type_of_Expr root)
215 , Type0_Lift Type_List (Type_of_Expr root)
216 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
217 (Error_of_Expr ast root)
218 , Root_of_Expr root ~ root
219 ) => ast
220 -> ExprFrom ast (Expr_Map root) hs ret
221 map_keys_from ast_m ex ast ctx k =
222 -- keys :: Map k a -> [k]
223 expr_from (Proxy::Proxy root) ast_m ctx $
224 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
225 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
226 k (type_list ty_m_k) $ Forall_Repr_with_Context $
227 \c -> map_keys (m c)
228
229 -- | Parse 'map_member'.
230 map_member_from
231 :: forall root ty ast hs ret.
232 ( ty ~ Type_Root_of_Expr (Expr_Map root)
233 , Type0_Eq ty
234 , Expr_From ast root
235 , Type0_Constraint Ord ty
236 , Type0_Lift Type_Map (Type_of_Expr root)
237 , Type0_Unlift Type_Map (Type_of_Expr root)
238 , Type0_Lift Type_Bool (Type_of_Expr root)
239 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
240 (Error_of_Expr ast root)
241 , Root_of_Expr root ~ root
242 ) => ast -> ast
243 -> ExprFrom ast (Expr_Map root) hs ret
244 map_member_from ast_k ast_m ex ast ctx k =
245 -- member :: Ord k => k -> Map k a -> Bool
246 expr_from (Proxy::Proxy root) ast_k ctx $
247 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
248 expr_from (Proxy::Proxy root) ast_m ctx $
249 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
250 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
251 check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
252 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
253 k type_bool $ Forall_Repr_with_Context $
254 \c -> map_member (key c) (m c)
255
256 -- | Parse 'map_insert'.
257 map_insert_from
258 :: forall root ty ast hs ret.
259 ( ty ~ Type_Root_of_Expr (Expr_Map root)
260 , Type0_Eq ty
261 , Expr_From ast root
262 , Type0_Constraint Ord ty
263 , Type0_Lift Type_Map (Type_of_Expr root)
264 , Type0_Unlift Type_Map (Type_of_Expr root)
265 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
266 (Error_of_Expr ast root)
267 , Root_of_Expr root ~ root
268 ) => ast -> ast -> ast
269 -> ExprFrom ast (Expr_Map root) hs ret
270 map_insert_from ast_k ast_a ast_m ex ast ctx k =
271 -- insert :: Ord k => k -> a -> Map k a -> Map k a
272 expr_from (Proxy::Proxy root) ast_k ctx $
273 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
274 expr_from (Proxy::Proxy root) ast_a ctx $
275 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
276 expr_from (Proxy::Proxy root) ast_m ctx $
277 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
278 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
279 check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
280 check_type0_eq ex ast ty_a ty_m_a $ \Refl ->
281 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
282 k ty_m $ Forall_Repr_with_Context $
283 \c -> map_insert (key c) (a c) (m c)
284
285 -- | Parse 'map_delete'.
286 map_delete_from
287 :: forall root ty ast hs ret.
288 ( ty ~ Type_Root_of_Expr (Expr_Map root)
289 , Type0_Eq ty
290 , Expr_From ast root
291 , Type0_Lift Type_Map (Type_of_Expr root)
292 , Type0_Unlift Type_Map (Type_of_Expr root)
293 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
294 (Error_of_Expr ast root)
295 , Type0_Constraint Ord ty
296 , Root_of_Expr root ~ root
297 ) => ast -> ast
298 -> ExprFrom ast (Expr_Map root) hs ret
299 map_delete_from ast_k ast_m ex ast ctx k =
300 -- delete :: Ord k => k -> Map k a -> Map k a
301 expr_from (Proxy::Proxy root) ast_k ctx $
302 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
303 expr_from (Proxy::Proxy root) ast_m ctx $
304 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
305 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
306 check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
307 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
308 k ty_m $ Forall_Repr_with_Context $
309 \c -> map_delete (key c) (m c)
310
311 -- | Parse 'map_difference'.
312 map_difference_from
313 :: forall root ty ast hs ret.
314 ( ty ~ Type_Root_of_Expr (Expr_Map root)
315 , Type0_Eq ty
316 , Expr_From ast root
317 , Type0_Lift Type_Map (Type_of_Expr root)
318 , Type0_Unlift Type_Map (Type_of_Expr root)
319 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
320 (Error_of_Expr ast root)
321 , Type0_Constraint Ord ty
322 , Root_of_Expr root ~ root
323 ) => ast -> ast
324 -> ExprFrom ast (Expr_Map root) hs ret
325 map_difference_from ast_ma ast_mb ex ast ctx k =
326 -- difference :: Ord k => Map k a -> Map k b -> Map k a
327 expr_from (Proxy::Proxy root) ast_ma ctx $
328 \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
329 expr_from (Proxy::Proxy root) ast_mb ctx $
330 \(ty_mb::ty h_mb) (Forall_Repr_with_Context mb) ->
331 check_type_map ex ast ty_ma $ \(Type2 Proxy ty_ma_k _ty_ma_a) ->
332 check_type_map ex ast ty_mb $ \(Type2 Proxy ty_mb_k _ty_mb_b) ->
333 check_type0_eq ex ast ty_ma_k ty_mb_k $ \Refl ->
334 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_ma_k $ \Dict ->
335 k ty_ma $ Forall_Repr_with_Context $
336 \c -> map_difference (ma c) (mb c)
337
338 -- | Parse 'map_foldrWithKey'.
339 map_foldrWithKey_from
340 :: forall root ty ast hs ret.
341 ( ty ~ Type_Root_of_Expr (Expr_Map root)
342 , Type0_Eq ty
343 , Expr_From ast root
344 , Type0_Lift Type_Fun (Type_of_Expr root)
345 , Type0_Unlift Type_Fun (Type_of_Expr root)
346 , Type0_Lift Type_Map (Type_of_Expr root)
347 , Type0_Unlift Type_Map (Type_of_Expr root)
348 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
349 (Error_of_Expr ast root)
350 , Type0_Constraint Ord ty
351 , Root_of_Expr root ~ root
352 ) => ast -> ast -> ast
353 -> ExprFrom ast (Expr_Map root) hs ret
354 map_foldrWithKey_from ast_f ast_b ast_m ex ast ctx k =
355 -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
356 expr_from (Proxy::Proxy root) ast_f ctx $
357 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
358 expr_from (Proxy::Proxy root) ast_b ctx $
359 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
360 expr_from (Proxy::Proxy root) ast_m ctx $
361 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
362 check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_k ty_f_a2b2b) ->
363 check_type_fun ex ast ty_f_a2b2b $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
364 check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
365 check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
366 check_type0_eq ex ast ty_f_k ty_m_k $ \Refl ->
367 check_type0_eq ex ast ty_f_a ty_m_a $ \Refl ->
368 check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
369 check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
370 check_type0_constraint ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
371 k ty_b $ Forall_Repr_with_Context $
372 \c -> map_foldrWithKey (f c) (b c) (m c)
373
374 -- * Type 'Expr_Map'
375 -- | Expression.
376 data Expr_Map (root:: *)
377 type instance Root_of_Expr (Expr_Map root) = root
378 type instance Type_of_Expr (Expr_Map root) = Type_Map
379 type instance Sym_of_Expr (Expr_Map root) repr = (Sym_Map repr)
380 type instance Error_of_Expr ast (Expr_Map root) = No_Error_Expr