]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Foldable.hs
Fix Lib.Ord : Ordering.
[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 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
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 infix 4 `elem`
123
124 type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
125 type instance Consts_of_Iface (Proxy Foldable) = Proxy Foldable ': Consts_imported_by Foldable
126 type instance Consts_imported_by Foldable = '[]
127
128 instance Sym_Foldable HostI where
129 foldMap = liftM2 Foldable.foldMap
130 foldr = liftM3 Foldable.foldr
131 foldr' = liftM3 Foldable.foldr'
132 foldl = liftM3 Foldable.foldl
133 foldl' = liftM3 Foldable.foldl'
134 null = liftM Foldable.null
135 length = liftM Foldable.length
136 minimum = liftM Foldable.minimum
137 maximum = liftM Foldable.maximum
138 elem = liftM2 Foldable.elem
139 sum = liftM Foldable.sum
140 product = liftM Foldable.product
141 toList = liftM Foldable.toList
142 all = liftM2 Foldable.all
143 and = liftM Foldable.and
144 any = liftM2 Foldable.any
145 concat = liftM Foldable.concat
146 concatMap = liftM2 Foldable.concatMap
147 find = liftM2 Foldable.find
148 foldlM = liftM3 Foldable.foldlM
149 foldrM = liftM3 Foldable.foldrM
150 forM_ = liftM2 Foldable.forM_
151 for_ = liftM2 Foldable.for_
152 mapM_ = liftM2 Foldable.mapM_
153 maximumBy = liftM2 Foldable.maximumBy
154 minimumBy = liftM2 Foldable.minimumBy
155 notElem = liftM2 Foldable.notElem
156 or = liftM Foldable.or
157 sequenceA_ = liftM Foldable.sequenceA_
158 sequence_ = liftM Foldable.sequence_
159 traverse_ = liftM2 Foldable.traverse_
160 instance Sym_Foldable TextI where
161 foldMap = textI2 "foldMap"
162 foldr = textI3 "foldr"
163 foldr' = textI3 "foldr'"
164 foldl = textI3 "foldl"
165 foldl' = textI3 "foldl'"
166 null = textI1 "null"
167 length = textI1 "length"
168 minimum = textI1 "minimum"
169 maximum = textI1 "maximum"
170 elem = textI2 "elem"
171 sum = textI1 "sum"
172 product = textI1 "product"
173 toList = textI1 "toList"
174 all = textI2 "all"
175 and = textI1 "and"
176 any = textI2 "any"
177 concat = textI1 "concat"
178 concatMap = textI2 "concatMap"
179 find = textI2 "find"
180 foldlM = textI3 "foldlM"
181 foldrM = textI3 "foldrM"
182 forM_ = textI2 "forM_"
183 for_ = textI2 "for_"
184 mapM_ = textI2 "mapM_"
185 maximumBy = textI2 "maximumBy"
186 minimumBy = textI2 "minimumBy"
187 notElem = textI2 "notElem"
188 or = textI1 "or"
189 sequenceA_ = textI1 "sequenceA_"
190 sequence_ = textI1 "sequence_"
191 traverse_ = textI2 "traverse_"
192 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where
193 foldMap = dupI2 (Proxy @Sym_Foldable) foldMap
194 foldr = dupI3 (Proxy @Sym_Foldable) foldr
195 foldr' = dupI3 (Proxy @Sym_Foldable) foldr'
196 foldl = dupI3 (Proxy @Sym_Foldable) foldl
197 foldl' = dupI3 (Proxy @Sym_Foldable) foldl'
198 null = dupI1 (Proxy @Sym_Foldable) null
199 length = dupI1 (Proxy @Sym_Foldable) length
200 minimum = dupI1 (Proxy @Sym_Foldable) minimum
201 maximum = dupI1 (Proxy @Sym_Foldable) maximum
202 elem = dupI2 (Proxy @Sym_Foldable) elem
203 sum = dupI1 (Proxy @Sym_Foldable) sum
204 product = dupI1 (Proxy @Sym_Foldable) product
205 toList = dupI1 (Proxy @Sym_Foldable) toList
206 all = dupI2 (Proxy @Sym_Foldable) all
207 and = dupI1 (Proxy @Sym_Foldable) and
208 any = dupI2 (Proxy @Sym_Foldable) any
209 concat = dupI1 (Proxy @Sym_Foldable) concat
210 concatMap = dupI2 (Proxy @Sym_Foldable) concatMap
211 find = dupI2 (Proxy @Sym_Foldable) find
212 foldlM = dupI3 (Proxy @Sym_Foldable) foldlM
213 foldrM = dupI3 (Proxy @Sym_Foldable) foldrM
214 forM_ = dupI2 (Proxy @Sym_Foldable) forM_
215 for_ = dupI2 (Proxy @Sym_Foldable) for_
216 mapM_ = dupI2 (Proxy @Sym_Foldable) mapM_
217 maximumBy = dupI2 (Proxy @Sym_Foldable) maximumBy
218 minimumBy = dupI2 (Proxy @Sym_Foldable) minimumBy
219 notElem = dupI2 (Proxy @Sym_Foldable) notElem
220 or = dupI1 (Proxy @Sym_Foldable) or
221 sequenceA_ = dupI1 (Proxy @Sym_Foldable) sequenceA_
222 sequence_ = dupI1 (Proxy @Sym_Foldable) sequence_
223 traverse_ = dupI2 (Proxy @Sym_Foldable) traverse_
224
225 instance
226 ( Read_TypeNameR Type_Name cs rs
227 , Inj_Const cs Foldable
228 ) => Read_TypeNameR Type_Name cs (Proxy Foldable ': rs) where
229 read_typenameR _cs (Type_Name "Foldable") k = k (ty @Foldable)
230 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
231 instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
232 show_const ConstZ{} = "Foldable"
233 show_const (ConstS c) = show_const c
234
235 instance Proj_ConC cs (Proxy Foldable)
236 data instance TokenT meta (ts::[*]) (Proxy Foldable)
237 = Token_Term_Foldable_foldMap (EToken meta ts) (EToken meta ts)
238 | Token_Term_Foldable_foldr (EToken meta ts) (EToken meta ts) (EToken meta ts)
239 | Token_Term_Foldable_foldr' (EToken meta ts) (EToken meta ts) (EToken meta ts)
240 | Token_Term_Foldable_foldl (EToken meta ts) (EToken meta ts) (EToken meta ts)
241 | Token_Term_Foldable_elem (EToken meta ts) (EToken meta ts)
242 | Token_Term_Foldable_null (EToken meta ts)
243 | Token_Term_Foldable_length (EToken meta ts)
244 | Token_Term_Foldable_minimum (EToken meta ts)
245 | Token_Term_Foldable_maximum (EToken meta ts)
246 | Token_Term_Foldable_sum (EToken meta ts)
247 | Token_Term_Foldable_product (EToken meta ts)
248 | Token_Term_Foldable_toList (EToken meta ts)
249 | Token_Term_Foldable_all (EToken meta ts) (EToken meta ts)
250 | Token_Term_Foldable_any (EToken meta ts) (EToken meta ts)
251 | Token_Term_Foldable_and (EToken meta ts)
252 | Token_Term_Foldable_or (EToken meta ts)
253 | Token_Term_Foldable_concat (EToken meta ts)
254 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Foldable))
255 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Foldable))
256 instance -- CompileI
257 ( Inj_Const (Consts_of_Ifaces is) Foldable
258 , Inj_Const (Consts_of_Ifaces is) Monoid
259 , Inj_Const (Consts_of_Ifaces is) (->)
260 , Inj_Const (Consts_of_Ifaces is) Int
261 , Inj_Const (Consts_of_Ifaces is) Bool
262 , Inj_Const (Consts_of_Ifaces is) Eq
263 , Inj_Const (Consts_of_Ifaces is) Ord
264 , Inj_Const (Consts_of_Ifaces is) Num
265 , Inj_Const (Consts_of_Ifaces is) []
266 , Proj_Con (Consts_of_Ifaces is)
267 , Compile is
268 ) => CompileI is (Proxy Foldable) where
269 compileI
270 :: forall meta ctx ret ls rs.
271 TokenT meta is (Proxy Foldable)
272 -> CompileT meta ctx ret is ls (Proxy Foldable ': rs)
273 compileI tok ctx k =
274 case tok of
275 Token_Term_Foldable_foldMap tok_a2m tok_ta ->
276 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
277 compileO tok_a2m ctx $ \ty_a2m (TermO a2m) ->
278 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
279 check_type2 (ty @(->)) (At (Just tok_a2m) ty_a2m) $ \Refl ty_a2m_a ty_a2m_m ->
280 check_con (At (Just tok_a2m) (ty @Monoid :$ ty_a2m_m)) $ \Con ->
281 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
282 check_type
283 (At (Just tok_a2m) ty_a2m_a)
284 (At (Just tok_ta) ty_ta_a) $ \Refl ->
285 k ty_a2m_m $ TermO $
286 \c -> foldMap (a2m c) (ta c)
287 Token_Term_Foldable_foldr tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr
288 Token_Term_Foldable_foldr' tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr'
289 Token_Term_Foldable_foldl tok_b2a2b tok_b tok_ta -> foldl_from tok_b2a2b tok_b tok_ta foldl
290 Token_Term_Foldable_elem tok_a tok_ta ->
291 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
292 compileO tok_a ctx $ \ty_a (TermO a) ->
293 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
294 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
295 check_con (At (Just tok_ta) (ty @Eq :$ ty_ta_a)) $ \Con ->
296 check_type
297 (At (Just tok_a) ty_a)
298 (At (Just tok_ta) ty_ta_a) $ \Refl ->
299 k (ty @Bool) $ TermO $
300 \c -> a c `elem` ta c
301 Token_Term_Foldable_null tok_ta -> ta2ty_from tok_ta null
302 Token_Term_Foldable_length tok_ta -> ta2ty_from tok_ta length
303 Token_Term_Foldable_minimum tok_ta -> ta2a_from tok_ta (ty @Ord) minimum
304 Token_Term_Foldable_maximum tok_ta -> ta2a_from tok_ta (ty @Ord) maximum
305 Token_Term_Foldable_sum tok_ta -> ta2a_from tok_ta (ty @Num) sum
306 Token_Term_Foldable_product tok_ta -> ta2a_from tok_ta (ty @Num) product
307 Token_Term_Foldable_toList tok_ta ->
308 -- toList :: Foldable t => t a -> [a]
309 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
310 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
311 k (ty @[] :$ ty_ta_a) $ TermO $
312 \c -> toList (ta c)
313 Token_Term_Foldable_all tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta all
314 Token_Term_Foldable_any tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta any
315 Token_Term_Foldable_and tok_tBool -> andor_from tok_tBool and
316 Token_Term_Foldable_or tok_tBool -> andor_from tok_tBool or
317 Token_Term_Foldable_concat tok_tla ->
318 -- concat :: Foldable t => t [a] -> [a]
319 compileO tok_tla ctx $ \ty_tla (TermO tla) ->
320 check_con1 (ty @Foldable) (At (Just tok_tla) ty_tla) $ \Refl Con _ty_tla_t ty_tla_la ->
321 check_type1 (ty @[]) (At (Just tok_tla) ty_tla_la) $ \Refl ty_tla_la_a ->
322 k (ty @[] :$ ty_tla_la_a) $ TermO $
323 \c -> concat (tla c)
324 where
325 foldr_from tok_a2b2b tok_b tok_ta
326 (fold::forall term f a b.
327 (Sym_Foldable term, Foldable f)
328 => term (a -> b -> b) -> term b -> term (f a) -> term b) =
329 -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
330 -- foldr' :: Foldable t => (a -> b -> b) -> b -> t a -> b
331 compileO tok_a2b2b ctx $ \ty_a2b2b (TermO a2b2b) ->
332 compileO tok_b ctx $ \ty_b (TermO b) ->
333 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
334 check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b) $ \Refl ty_a2b2b_a ty_a2b2b_b2b ->
335 check_type2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b_b2b) $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 ->
336 check_type
337 (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
338 (At (Just tok_a2b2b) ty_a2b2b_b2b_b1) $ \Refl ->
339 check_type
340 (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
341 (At (Just tok_b) ty_b) $ \Refl ->
342 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
343 check_type
344 (At (Just tok_a2b2b) ty_a2b2b_a)
345 (At (Just tok_ta) ty_ta_a) $ \Refl ->
346 k ty_b $ TermO $
347 \c -> fold (a2b2b c) (b c) (ta c)
348 foldl_from tok_b2a2b tok_b tok_ta
349 (fold::forall term f a b.
350 (Sym_Foldable term, Foldable f)
351 => term (b -> a -> b) -> term b -> term (f a) -> term b) =
352 -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
353 compileO tok_b2a2b ctx $ \ty_b2a2b (TermO b2a2b) ->
354 compileO tok_b ctx $ \ty_b (TermO b) ->
355 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
356 check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b) $ \Refl ty_b2a2b_b ty_b2a2b_a2b ->
357 check_type2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b_a2b) $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b ->
358 check_type
359 (At (Just tok_b2a2b) ty_b2a2b_b)
360 (At (Just tok_b2a2b) ty_b2a2b_a2b_b) $ \Refl ->
361 check_type
362 (At (Just tok_b2a2b) ty_b2a2b_b)
363 (At (Just tok_b) ty_b) $ \Refl ->
364 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
365 check_type
366 (At (Just tok_b2a2b) ty_b2a2b_a2b_a)
367 (At (Just tok_ta) ty_ta_a) $ \Refl ->
368 k ty_b $ TermO $
369 \c -> fold (b2a2b c) (b c) (ta c)
370 ta2ty_from
371 :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
372 => EToken meta is
373 -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ)
374 -> Either (Error_Term meta is) ret
375 ta2ty_from tok_ta f =
376 -- length :: Foldable t => t a -> Int
377 -- null :: Foldable t => t a -> Bool
378 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
379 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t _ty_ta_a ->
380 k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $
381 \c -> f (ta c)
382 ta2a_from
383 :: forall con.
384 EToken meta is
385 -> Type (Consts_of_Ifaces is) con
386 -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
387 -> Either (Error_Term meta is) ret
388 ta2a_from tok_ta q f =
389 -- minimum :: (Foldable t, Ord a) => t a -> a
390 -- maximum :: (Foldable t, Ord a) => t a -> a
391 -- sum :: (Foldable t, Num a) => t a -> a
392 -- product :: (Foldable t, Num a) => t a -> a
393 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
394 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
395 check_con (At (Just tok_ta) (q :$ ty_ta_a)) $ \Con ->
396 k ty_ta_a $ TermO $
397 \c -> f (ta c)
398 allany_from tok_a2Bool tok_ta
399 (g::forall term f a.
400 (Sym_Foldable term, Foldable f)
401 => term (a -> Bool) -> term (f a) -> term Bool) =
402 -- all :: Foldable t => (a -> Bool) -> t a -> Bool
403 -- any :: Foldable t => (a -> Bool) -> t a -> Bool
404 compileO tok_a2Bool ctx $ \ty_a2Bool (TermO a2Bool) ->
405 compileO tok_ta ctx $ \ty_ta (TermO ta) ->
406 check_type2 (ty @(->)) (At (Just tok_a2Bool) ty_a2Bool) $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
407 check_con1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl Con _ty_ta_t ty_ta_a ->
408 check_type
409 (At (Just tok_a2Bool) ty_a2Bool_a)
410 (At (Just tok_ta) ty_ta_a) $ \Refl ->
411 check_type
412 (At Nothing (ty @Bool))
413 (At (Just tok_a2Bool) ty_a2Bool_Bool) $ \Refl ->
414 k (ty @Bool) $ TermO $
415 \c -> g (a2Bool c) (ta c)
416 andor_from tok_tBool
417 (g::forall term f.
418 (Sym_Foldable term, Foldable f)
419 => term (f Bool) -> term Bool) =
420 -- and :: Foldable t => t Bool -> Bool
421 -- or :: Foldable t => t Bool -> Bool
422 compileO tok_tBool ctx $ \ty_tBool (TermO tBool) ->
423 check_con1 (ty @Foldable) (At (Just tok_tBool) ty_tBool) $ \Refl Con _ty_tBool_t ty_tBool_Bool ->
424 check_type
425 (At Nothing (ty @Bool))
426 (At (Just tok_tBool) ty_tBool_Bool) $ \Refl ->
427 k (ty @Bool) $ TermO $
428 \c -> g (tBool c)
429 instance -- TokenizeT
430 Inj_Token meta ts Foldable =>
431 TokenizeT meta ts (Proxy Foldable) where
432 tokenizeT _t = mempty
433 { tokenizers_infix = tokenizeTMod []
434 [ tokenize2 "foldMap" infixN5 Token_Term_Foldable_foldMap
435 , tokenize3 "foldr" infixN5 Token_Term_Foldable_foldr
436 , tokenize3 "foldr'" infixN5 Token_Term_Foldable_foldr'
437 , tokenize3 "foldl" infixN5 Token_Term_Foldable_foldl
438 , tokenize2 "elem" (infixN 4) Token_Term_Foldable_elem
439 , tokenize1 "sum" infixN5 Token_Term_Foldable_sum
440 , tokenize1 "product" infixN5 Token_Term_Foldable_product
441 , tokenize1 "toList" infixN5 Token_Term_Foldable_toList
442 , tokenize2 "all" infixN5 Token_Term_Foldable_all
443 , tokenize2 "any" infixN5 Token_Term_Foldable_any
444 , tokenize1 "and" infixN5 Token_Term_Foldable_and
445 , tokenize1 "or" infixN5 Token_Term_Foldable_or
446 , tokenize1 "concat" infixN5 Token_Term_Foldable_concat
447 ]
448 }
449 instance Gram_Term_AtomsT meta ts (Proxy Foldable) g