]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Foldable.hs
Move libraries in Lib.
[haskell/symantic.git] / Language / Symantic / Lib / Foldable.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 -- | Symantic for 'Foldable'.
5 module Language.Symantic.Lib.Foldable where
6
7 import Data.Foldable (Foldable)
8 import qualified Data.Foldable as Foldable
9 import Control.Monad (liftM, liftM2, liftM3)
10 import Data.Proxy
11 import Data.Type.Equality ((:~:)(Refl))
12 import Prelude hiding (Foldable(..)
13 , all, and, any, concat, concatMap
14 , mapM_, notElem, or, sequence, sequence_)
15
16 import Language.Symantic.Parsing
17 import Language.Symantic.Parsing.Grammar hiding (any)
18 import Language.Symantic.Typing
19 import Language.Symantic.Compiling
20 import Language.Symantic.Interpreting
21 import Language.Symantic.Transforming.Trans
22
23 -- * Class 'Sym_Foldable'
24 class Sym_Foldable term where
25 foldMap :: (Foldable f, Monoid m) => term (a -> m) -> term (f a) -> term m
26 foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
27 foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
28 foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
29 foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
30 length :: Foldable f => term (f a) -> term Int
31 null :: Foldable f => term (f a) -> term Bool
32 minimum :: (Foldable f, Ord a) => term (f a) -> term a
33 maximum :: (Foldable f, Ord a) => term (f a) -> term a
34 elem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
35 sum :: (Foldable f, Num a) => term (f a) -> term a
36 product :: (Foldable f, Num a) => term (f a) -> term a
37 toList :: Foldable f => term (f a) -> term [a]
38 all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
39 and :: Foldable f => term (f Bool) -> term Bool
40 any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
41 concat :: Foldable f => term (f [a]) -> term [a]
42 concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
43 find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
44 foldlM :: (Foldable f, Monad m) => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
45 foldrM :: (Foldable f, Monad m) => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
46 forM_ :: (Foldable f, Monad m) => term (f a) -> term (a -> m b) -> term (m ())
47 for_ :: (Foldable f, Applicative p) => term (f a) -> term (a -> p b) -> term (p ())
48 mapM_ :: (Foldable f, Monad m) => term (a -> m b) -> term (f a) -> term (m ())
49 maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
50 minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
51 notElem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
52 or :: Foldable f => term (f Bool) -> term Bool
53 sequenceA_ :: (Foldable f, Applicative p) => term (f (p a)) -> term (p ())
54 sequence_ :: (Foldable f, Monad m) => term (f (m a)) -> term (m ())
55 traverse_ :: (Foldable f, Applicative p) => term (a -> p b) -> term (f a) -> term (p ())
56 -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
57 -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
58
59 default foldMap :: (Trans t term, Foldable f, Monoid m) => t term (a -> m) -> t term (f a) -> t term m
60 default foldr :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
61 default foldr' :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
62 default foldl :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
63 default foldl' :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
64 default length :: (Trans t term, Foldable f) => t term (f a) -> t term Int
65 default null :: (Trans t term, Foldable f) => t term (f a) -> t term Bool
66 default minimum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
67 default maximum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
68 default elem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
69 default sum :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
70 default product :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
71 default toList :: (Trans t term, Foldable f) => t term (f a) -> t term [a]
72 default all :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
73 default and :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
74 default any :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
75 default concat :: (Trans t term, Foldable f) => t term (f [a]) -> t term [a]
76 default concatMap :: (Trans t term, Foldable f) => t term (a -> [b]) -> t term (f a) -> t term [b]
77 default find :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term (Maybe a)
78 default foldlM :: (Trans t term, Foldable f, Monad m) => t term (b -> a -> m b) -> t term b -> t term (f a) -> t term (m b)
79 default foldrM :: (Trans t term, Foldable f, Monad m) => t term (a -> b -> m b) -> t term b -> t term (f a) -> t term (m b)
80 default forM_ :: (Trans t term, Foldable f, Monad m) => t term (f a) -> t term (a -> m b) -> t term (m ())
81 default for_ :: (Trans t term, Foldable f, Applicative p) => t term (f a) -> t term (a -> p b) -> t term (p ())
82 default mapM_ :: (Trans t term, Foldable f, Monad m) => t term (a -> m b) -> t term (f a) -> t term (m ())
83 default maximumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
84 default minimumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
85 default notElem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
86 default or :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
87 default sequenceA_ :: (Trans t term, Foldable f, Applicative p) => t term (f (p a)) -> t term (p ())
88 default sequence_ :: (Trans t term, Foldable f, Monad m) => t term (f (m a)) -> t term (m ())
89 default traverse_ :: (Trans t term, Foldable f, Applicative p) => t term (a -> p b) -> t term (f a) -> t term (p ())
90
91 foldMap = trans_map2 foldMap
92 foldr = trans_map3 foldr
93 foldr' = trans_map3 foldr'
94 foldl = trans_map3 foldl
95 foldl' = trans_map3 foldl'
96 length = trans_map1 length
97 null = trans_map1 null
98 minimum = trans_map1 minimum
99 maximum = trans_map1 maximum
100 elem = trans_map2 elem
101 sum = trans_map1 sum
102 product = trans_map1 product
103 toList = trans_map1 toList
104 all = trans_map2 all
105 and = trans_map1 and
106 any = trans_map2 any
107 concat = trans_map1 concat
108 concatMap = trans_map2 concatMap
109 find = trans_map2 find
110 foldlM = trans_map3 foldlM
111 foldrM = trans_map3 foldrM
112 forM_ = trans_map2 forM_
113 for_ = trans_map2 for_
114 mapM_ = trans_map2 mapM_
115 maximumBy = trans_map2 maximumBy
116 minimumBy = trans_map2 minimumBy
117 notElem = trans_map2 notElem
118 or = trans_map1 or
119 sequenceA_ = trans_map1 sequenceA_
120 sequence_ = trans_map1 sequence_
121 traverse_ = trans_map2 traverse_
122
123 infix 4 `elem`
124
125 type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
126 type instance Consts_of_Iface (Proxy Foldable) = Proxy Foldable ': Consts_imported_by Foldable
127 type instance Consts_imported_by Foldable = '[]
128
129 instance Sym_Foldable HostI where
130 foldMap = liftM2 Foldable.foldMap
131 foldr = liftM3 Foldable.foldr
132 foldr' = liftM3 Foldable.foldr'
133 foldl = liftM3 Foldable.foldl
134 foldl' = liftM3 Foldable.foldl'
135 null = liftM Foldable.null
136 length = liftM Foldable.length
137 minimum = liftM Foldable.minimum
138 maximum = liftM Foldable.maximum
139 elem = liftM2 Foldable.elem
140 sum = liftM Foldable.sum
141 product = liftM Foldable.product
142 toList = liftM Foldable.toList
143 all = liftM2 Foldable.all
144 and = liftM Foldable.and
145 any = liftM2 Foldable.any
146 concat = liftM Foldable.concat
147 concatMap = liftM2 Foldable.concatMap
148 find = liftM2 Foldable.find
149 foldlM = liftM3 Foldable.foldlM
150 foldrM = liftM3 Foldable.foldrM
151 forM_ = liftM2 Foldable.forM_
152 for_ = liftM2 Foldable.for_
153 mapM_ = liftM2 Foldable.mapM_
154 maximumBy = liftM2 Foldable.maximumBy
155 minimumBy = liftM2 Foldable.minimumBy
156 notElem = liftM2 Foldable.notElem
157 or = liftM Foldable.or
158 sequenceA_ = liftM Foldable.sequenceA_
159 sequence_ = liftM Foldable.sequence_
160 traverse_ = liftM2 Foldable.traverse_
161 instance Sym_Foldable TextI where
162 foldMap = textI2 "foldMap"
163 foldr = textI3 "foldr"
164 foldr' = textI3 "foldr'"
165 foldl = textI3 "foldl"
166 foldl' = textI3 "foldl'"
167 null = textI1 "null"
168 length = textI1 "length"
169 minimum = textI1 "minimum"
170 maximum = textI1 "maximum"
171 elem = textI2 "elem"
172 sum = textI1 "sum"
173 product = textI1 "product"
174 toList = textI1 "toList"
175 all = textI2 "all"
176 and = textI1 "and"
177 any = textI2 "any"
178 concat = textI1 "concat"
179 concatMap = textI2 "concatMap"
180 find = textI2 "find"
181 foldlM = textI3 "foldlM"
182 foldrM = textI3 "foldrM"
183 forM_ = textI2 "forM_"
184 for_ = textI2 "for_"
185 mapM_ = textI2 "mapM_"
186 maximumBy = textI2 "maximumBy"
187 minimumBy = textI2 "minimumBy"
188 notElem = textI2 "notElem"
189 or = textI1 "or"
190 sequenceA_ = textI1 "sequenceA_"
191 sequence_ = textI1 "sequence_"
192 traverse_ = textI2 "traverse_"
193 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where
194 foldMap = dupI2 (Proxy @Sym_Foldable) foldMap
195 foldr = dupI3 (Proxy @Sym_Foldable) foldr
196 foldr' = dupI3 (Proxy @Sym_Foldable) foldr'
197 foldl = dupI3 (Proxy @Sym_Foldable) foldl
198 foldl' = dupI3 (Proxy @Sym_Foldable) foldl'
199 null = dupI1 (Proxy @Sym_Foldable) null
200 length = dupI1 (Proxy @Sym_Foldable) length
201 minimum = dupI1 (Proxy @Sym_Foldable) minimum
202 maximum = dupI1 (Proxy @Sym_Foldable) maximum
203 elem = dupI2 (Proxy @Sym_Foldable) elem
204 sum = dupI1 (Proxy @Sym_Foldable) sum
205 product = dupI1 (Proxy @Sym_Foldable) product
206 toList = dupI1 (Proxy @Sym_Foldable) toList
207 all = dupI2 (Proxy @Sym_Foldable) all
208 and = dupI1 (Proxy @Sym_Foldable) and
209 any = dupI2 (Proxy @Sym_Foldable) any
210 concat = dupI1 (Proxy @Sym_Foldable) concat
211 concatMap = dupI2 (Proxy @Sym_Foldable) concatMap
212 find = dupI2 (Proxy @Sym_Foldable) find
213 foldlM = dupI3 (Proxy @Sym_Foldable) foldlM
214 foldrM = dupI3 (Proxy @Sym_Foldable) foldrM
215 forM_ = dupI2 (Proxy @Sym_Foldable) forM_
216 for_ = dupI2 (Proxy @Sym_Foldable) for_
217 mapM_ = dupI2 (Proxy @Sym_Foldable) mapM_
218 maximumBy = dupI2 (Proxy @Sym_Foldable) maximumBy
219 minimumBy = dupI2 (Proxy @Sym_Foldable) minimumBy
220 notElem = dupI2 (Proxy @Sym_Foldable) notElem
221 or = dupI1 (Proxy @Sym_Foldable) or
222 sequenceA_ = dupI1 (Proxy @Sym_Foldable) sequenceA_
223 sequence_ = dupI1 (Proxy @Sym_Foldable) sequence_
224 traverse_ = dupI2 (Proxy @Sym_Foldable) traverse_
225
226 instance
227 ( Read_TypeNameR Type_Name cs rs
228 , Inj_Const cs Foldable
229 ) => Read_TypeNameR Type_Name cs (Proxy Foldable ': rs) where
230 read_typenameR _cs (Type_Name "Foldable") k = k (ty @Foldable)
231 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
232 instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
233 show_const ConstZ{} = "Foldable"
234 show_const (ConstS c) = show_const c
235
236 instance Proj_ConC cs (Proxy Foldable)
237 data instance TokenT meta (ts::[*]) (Proxy Foldable)
238 = Token_Term_Foldable_foldMap (EToken meta ts) (EToken meta ts)
239 | Token_Term_Foldable_foldr (EToken meta ts) (EToken meta ts) (EToken meta ts)
240 | Token_Term_Foldable_foldr' (EToken meta ts) (EToken meta ts) (EToken meta ts)
241 | Token_Term_Foldable_foldl (EToken meta ts) (EToken meta ts) (EToken meta ts)
242 | Token_Term_Foldable_elem (EToken meta ts) (EToken meta ts)
243 | Token_Term_Foldable_null (EToken meta ts)
244 | Token_Term_Foldable_length (EToken meta ts)
245 | Token_Term_Foldable_minimum (EToken meta ts)
246 | Token_Term_Foldable_maximum (EToken meta ts)
247 | Token_Term_Foldable_sum (EToken meta ts)
248 | Token_Term_Foldable_product (EToken meta ts)
249 | Token_Term_Foldable_toList (EToken meta ts)
250 | Token_Term_Foldable_all (EToken meta ts) (EToken meta ts)
251 | Token_Term_Foldable_any (EToken meta ts) (EToken meta ts)
252 | Token_Term_Foldable_and (EToken meta ts)
253 | Token_Term_Foldable_or (EToken meta ts)
254 | Token_Term_Foldable_concat (EToken meta ts)
255 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Foldable))
256 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Foldable))
257 instance -- CompileI
258 ( Inj_Const (Consts_of_Ifaces is) Foldable
259 , Inj_Const (Consts_of_Ifaces is) Monoid
260 , Inj_Const (Consts_of_Ifaces is) (->)
261 , Inj_Const (Consts_of_Ifaces is) Int
262 , Inj_Const (Consts_of_Ifaces is) Bool
263 , Inj_Const (Consts_of_Ifaces is) Eq
264 , Inj_Const (Consts_of_Ifaces is) Ord
265 , Inj_Const (Consts_of_Ifaces is) Num
266 , Inj_Const (Consts_of_Ifaces is) []
267 , Proj_Con (Consts_of_Ifaces is)
268 , Compile is
269 ) => CompileI is (Proxy Foldable) where
270 compileI
271 :: forall meta ctx ret ls rs.
272 TokenT meta is (Proxy Foldable)
273 -> CompileT meta ctx ret is ls (Proxy Foldable ': rs)
274 compileI tok ctx k =
275 case tok of
276 Token_Term_Foldable_foldMap tok_a2m tok_ta ->
277 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
278 compileO tok_a2m ctx $ \ty_a2m (TermO a2m) ->
279 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
280 check_type2 (ty @(->)) (At (Just tok_a2m) ty_a2m) $ \Refl ty_a2m_a ty_a2m_m ->
281 check_con (At (Just tok_a2m) (ty @Monoid :$ ty_a2m_m)) $ \Con ->
282 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
283 check_type
284 (At (Just tok_a2m) ty_a2m_a)
285 (At (Just tok_ta) ty_ta_a) $ \Refl ->
286 k ty_a2m_m $ TermO $
287 \c -> foldMap (a2m c) (ta c)
288 Token_Term_Foldable_foldr tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr
289 Token_Term_Foldable_foldr' tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr'
290 Token_Term_Foldable_foldl tok_b2a2b tok_b tok_ta -> foldl_from tok_b2a2b tok_b tok_ta foldl
291 Token_Term_Foldable_elem tok_a tok_ta ->
292 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
293 compileO tok_a ctx $ \ty_a (TermO a) ->
294 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
295 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
296 check_con (At (Just tok_ta) (ty @Eq :$ ty_ta_a)) $ \Con ->
297 check_type
298 (At (Just tok_a) ty_a)
299 (At (Just tok_ta) ty_ta_a) $ \Refl ->
300 k (ty @Bool) $ TermO $
301 \c -> a c `elem` ta c
302 Token_Term_Foldable_null tok_ta -> ta2ty_from tok_ta null
303 Token_Term_Foldable_length tok_ta -> ta2ty_from tok_ta length
304 Token_Term_Foldable_minimum tok_ta -> ta2a_from tok_ta (ty @Ord) minimum
305 Token_Term_Foldable_maximum tok_ta -> ta2a_from tok_ta (ty @Ord) maximum
306 Token_Term_Foldable_sum tok_ta -> ta2a_from tok_ta (ty @Num) sum
307 Token_Term_Foldable_product tok_ta -> ta2a_from tok_ta (ty @Num) product
308 Token_Term_Foldable_toList tok_ta ->
309 -- toList :: Foldable t => t a -> [a]
310 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
311 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
312 k (ty @[] :$ ty_ta_a) $ TermO $
313 \c -> toList (ta c)
314 Token_Term_Foldable_all tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta all
315 Token_Term_Foldable_any tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta any
316 Token_Term_Foldable_and tok_tBool -> andor_from tok_tBool and
317 Token_Term_Foldable_or tok_tBool -> andor_from tok_tBool or
318 Token_Term_Foldable_concat tok_tla ->
319 -- concat :: Foldable t => t [a] -> [a]
320 compileO tok_tla ctx $ \ty_tla (TermO tla) ->
321 check_con1 (ty @Foldable) (At (Just tok_tla) ty_tla) $ \Refl Con _ty_tla_t ty_tla_la ->
322 check_type1 (ty @[]) (At (Just tok_tla) ty_tla_la) $ \Refl ty_tla_la_a ->
323 k (ty @[] :$ ty_tla_la_a) $ TermO $
324 \c -> concat (tla c)
325 where
326 foldr_from tok_a2b2b tok_b tok_ta
327 (fold::forall term f a b.
328 (Sym_Foldable term, Foldable f)
329 => term (a -> b -> b) -> term b -> term (f a) -> term b) =
330 -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
331 -- foldr' :: Foldable t => (a -> b -> b) -> b -> t a -> b
332 compileO tok_a2b2b ctx $ \ty_a2b2b (TermO a2b2b) ->
333 compileO tok_b ctx $ \ty_b (TermO b) ->
334 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
335 check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b) $ \Refl ty_a2b2b_a ty_a2b2b_b2b ->
336 check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b_b2b) $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 ->
337 check_type
338 (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
339 (At (Just tok_a2b2b) ty_a2b2b_b2b_b1) $ \Refl ->
340 check_type
341 (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
342 (At (Just tok_b) ty_b) $ \Refl ->
343 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
344 check_type
345 (At (Just tok_a2b2b) ty_a2b2b_a)
346 (At (Just tok_ta) ty_ta_a) $ \Refl ->
347 k ty_b $ TermO $
348 \c -> fold (a2b2b c) (b c) (ta c)
349 foldl_from tok_b2a2b tok_b tok_ta
350 (fold::forall term f a b.
351 (Sym_Foldable term, Foldable f)
352 => term (b -> a -> b) -> term b -> term (f a) -> term b) =
353 -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
354 compileO tok_b2a2b ctx $ \ty_b2a2b (TermO b2a2b) ->
355 compileO tok_b ctx $ \ty_b (TermO b) ->
356 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
357 check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b) $ \Refl ty_b2a2b_b ty_b2a2b_a2b ->
358 check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b_a2b) $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b ->
359 check_type
360 (At (Just tok_b2a2b) ty_b2a2b_b)
361 (At (Just tok_b2a2b) ty_b2a2b_a2b_b) $ \Refl ->
362 check_type
363 (At (Just tok_b2a2b) ty_b2a2b_b)
364 (At (Just tok_b) ty_b) $ \Refl ->
365 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
366 check_type
367 (At (Just tok_b2a2b) ty_b2a2b_a2b_a)
368 (At (Just tok_ta) ty_ta_a) $ \Refl ->
369 k ty_b $ TermO $
370 \c -> fold (b2a2b c) (b c) (ta c)
371 ta2ty_from
372 :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
373 => EToken meta is
374 -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ)
375 -> Either (Error_Term meta is) ret
376 ta2ty_from tok_ta f =
377 -- length :: Foldable t => t a -> Int
378 -- null :: Foldable t => t a -> Bool
379 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
380 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t _ty_ta_a ->
381 k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $
382 \c -> f (ta c)
383 ta2a_from
384 :: forall con.
385 EToken meta is
386 -> Type (Consts_of_Ifaces is) con
387 -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
388 -> Either (Error_Term meta is) ret
389 ta2a_from tok_ta q f =
390 -- minimum :: (Foldable t, Ord a) => t a -> a
391 -- maximum :: (Foldable t, Ord a) => t a -> a
392 -- sum :: (Foldable t, Num a) => t a -> a
393 -- product :: (Foldable t, Num a) => t a -> a
394 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
395 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
396 check_con (At (Just tok_ta) (q :$ ty_ta_a)) $ \Con ->
397 k ty_ta_a $ TermO $
398 \c -> f (ta c)
399 allany_from tok_a2Bool tok_ta
400 (g::forall term f a.
401 (Sym_Foldable term, Foldable f)
402 => term (a -> Bool) -> term (f a) -> term Bool) =
403 -- all :: Foldable t => (a -> Bool) -> t a -> Bool
404 -- any :: Foldable t => (a -> Bool) -> t a -> Bool
405 compileO tok_a2Bool ctx $ \ty_a2Bool (TermO a2Bool) ->
406 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
407 check_type2 (ty @(->)) (At (Just tok_a2Bool) ty_a2Bool) $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
408 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
409 check_type
410 (At (Just tok_a2Bool) ty_a2Bool_a)
411 (At (Just tok_ta) ty_ta_a) $ \Refl ->
412 check_type
413 (At Nothing (ty @Bool))
414 (At (Just tok_a2Bool) ty_a2Bool_Bool) $ \Refl ->
415 k (ty @Bool) $ TermO $
416 \c -> g (a2Bool c) (ta c)
417 andor_from tok_tBool
418 (g::forall term f.
419 (Sym_Foldable term, Foldable f)
420 => term (f Bool) -> term Bool) =
421 -- and :: Foldable t => t Bool -> Bool
422 -- or :: Foldable t => t Bool -> Bool
423 compileO tok_tBool ctx $ \ty_tBool (TermO tBool) ->
424 check_con1 (ty @Foldable) (At (Just tok_tBool) ty_tBool) $ \Refl Con _ty_tBool_t ty_tBool_Bool ->
425 check_type
426 (At Nothing (ty @Bool))
427 (At (Just tok_tBool) ty_tBool_Bool) $ \Refl ->
428 k (ty @Bool) $ TermO $
429 \c -> g (tBool c)
430 instance -- TokenizeT
431 Inj_Token meta ts Foldable =>
432 TokenizeT meta ts (Proxy Foldable) where
433 tokenizeT _t = mempty
434 { tokenizers_infix = tokenizeTMod []
435 [ tokenize2 "foldMap" infixN5 Token_Term_Foldable_foldMap
436 , tokenize3 "foldr" infixN5 Token_Term_Foldable_foldr
437 , tokenize3 "foldr'" infixN5 Token_Term_Foldable_foldr'
438 , tokenize3 "foldl" infixN5 Token_Term_Foldable_foldl
439 , tokenize2 "elem" (infixN 4) Token_Term_Foldable_elem
440 , tokenize1 "sum" infixN5 Token_Term_Foldable_sum
441 , tokenize1 "product" infixN5 Token_Term_Foldable_product
442 , tokenize1 "toList" infixN5 Token_Term_Foldable_toList
443 , tokenize2 "all" infixN5 Token_Term_Foldable_all
444 , tokenize2 "any" infixN5 Token_Term_Foldable_any
445 , tokenize1 "and" infixN5 Token_Term_Foldable_and
446 , tokenize1 "or" infixN5 Token_Term_Foldable_or
447 , tokenize1 "concat" infixN5 Token_Term_Foldable_concat
448 ]
449 }
450 instance Gram_Term_AtomsT meta ts (Proxy Foldable) g