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