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