]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Foldable.hs
Add Typing.Family and Compiling.MonoFunctor.
[haskell/symantic.git] / Language / Symantic / Compiling / Foldable.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE DefaultSignatures #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE InstanceSigs #-}
7 {-# LANGUAGE MultiParamTypeClasses #-}
8 {-# LANGUAGE OverloadedStrings #-}
9 {-# LANGUAGE Rank2Types #-}
10 {-# LANGUAGE ScopedTypeVariables #-}
11 {-# LANGUAGE TypeFamilies #-}
12 {-# LANGUAGE TypeOperators #-}
13 {-# LANGUAGE UndecidableInstances #-}
14 {-# OPTIONS_GHC -fno-warn-orphans #-}
15 -- | Symantic for 'Foldable'.
16 module Language.Symantic.Compiling.Foldable where
17
18 import Data.Foldable (Foldable)
19 import qualified Data.Foldable as Foldable
20 import Control.Monad (liftM, liftM2, liftM3)
21 import Data.Proxy
22 import Data.String (IsString)
23 import Data.Text (Text)
24 import Data.Type.Equality ((:~:)(Refl))
25 import Prelude hiding (Foldable(..)
26 , all, and, any, concat, concatMap
27 , mapM_, notElem, or, sequence, sequence_)
28
29 import Language.Symantic.Typing
30 import Language.Symantic.Compiling.Term
31 import Language.Symantic.Compiling.Bool (tyBool)
32 import Language.Symantic.Compiling.Eq (tyEq)
33 import Language.Symantic.Compiling.List (tyList)
34 import Language.Symantic.Compiling.Monoid (tyMonoid)
35 import Language.Symantic.Compiling.Num (tyNum)
36 import Language.Symantic.Compiling.Ord (tyOrd)
37 import Language.Symantic.Interpreting
38 import Language.Symantic.Transforming.Trans
39
40 -- * Class 'Sym_Foldable'
41 class Sym_Foldable term where
42 foldMap :: (Foldable f, Monoid m) => term (a -> m) -> term (f a) -> term m
43 foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
44 foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
45 foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
46 foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
47 length :: Foldable f => term (f a) -> term Int
48 null :: Foldable f => term (f a) -> term Bool
49 minimum :: (Foldable f, Ord a) => term (f a) -> term a
50 maximum :: (Foldable f, Ord a) => term (f a) -> term a
51 elem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
52 sum :: (Foldable f, Num a) => term (f a) -> term a
53 product :: (Foldable f, Num a) => term (f a) -> term a
54 toList :: Foldable f => term (f a) -> term [a]
55 all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
56 and :: Foldable f => term (f Bool) -> term Bool
57 any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
58 concat :: Foldable f => term (f [a]) -> term [a]
59 concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
60 find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
61 foldlM :: (Foldable f, Monad m) => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
62 foldrM :: (Foldable f, Monad m) => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
63 forM_ :: (Foldable f, Monad m) => term (f a) -> term (a -> m b) -> term (m ())
64 for_ :: (Foldable f, Applicative p) => term (f a) -> term (a -> p b) -> term (p ())
65 mapM_ :: (Foldable f, Monad m) => term (a -> m b) -> term (f a) -> term (m ())
66 maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
67 minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
68 notElem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
69 or :: Foldable f => term (f Bool) -> term Bool
70 sequenceA_ :: (Foldable f, Applicative p) => term (f (p a)) -> term (p ())
71 sequence_ :: (Foldable f, Monad m) => term (f (m a)) -> term (m ())
72 traverse_ :: (Foldable f, Applicative p) => term (a -> p b) -> term (f a) -> term (p ())
73 -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
74 -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
75
76 default foldMap :: (Trans t term, Foldable f, Monoid m) => t term (a -> m) -> t term (f a) -> t term m
77 default foldr :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
78 default foldr' :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
79 default foldl :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
80 default foldl' :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
81 default length :: (Trans t term, Foldable f) => t term (f a) -> t term Int
82 default null :: (Trans t term, Foldable f) => t term (f a) -> t term Bool
83 default minimum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
84 default maximum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
85 default elem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
86 default sum :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
87 default product :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
88 default toList :: (Trans t term, Foldable f) => t term (f a) -> t term [a]
89 default all :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
90 default and :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
91 default any :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
92 default concat :: (Trans t term, Foldable f) => t term (f [a]) -> t term [a]
93 default concatMap :: (Trans t term, Foldable f) => t term (a -> [b]) -> t term (f a) -> t term [b]
94 default find :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term (Maybe a)
95 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)
96 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)
97 default forM_ :: (Trans t term, Foldable f, Monad m) => t term (f a) -> t term (a -> m b) -> t term (m ())
98 default for_ :: (Trans t term, Foldable f, Applicative p) => t term (f a) -> t term (a -> p b) -> t term (p ())
99 default mapM_ :: (Trans t term, Foldable f, Monad m) => t term (a -> m b) -> t term (f a) -> t term (m ())
100 default maximumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
101 default minimumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
102 default notElem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
103 default or :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
104 default sequenceA_ :: (Trans t term, Foldable f, Applicative p) => t term (f (p a)) -> t term (p ())
105 default sequence_ :: (Trans t term, Foldable f, Monad m) => t term (f (m a)) -> t term (m ())
106 default traverse_ :: (Trans t term, Foldable f, Applicative p) => t term (a -> p b) -> t term (f a) -> t term (p ())
107
108 foldMap = trans_map2 foldMap
109 foldr = trans_map3 foldr
110 foldr' = trans_map3 foldr'
111 foldl = trans_map3 foldl
112 foldl' = trans_map3 foldl'
113 length = trans_map1 length
114 null = trans_map1 null
115 minimum = trans_map1 minimum
116 maximum = trans_map1 maximum
117 elem = trans_map2 elem
118 sum = trans_map1 sum
119 product = trans_map1 product
120 toList = trans_map1 toList
121 all = trans_map2 all
122 and = trans_map1 and
123 any = trans_map2 any
124 concat = trans_map1 concat
125 concatMap = trans_map2 concatMap
126 find = trans_map2 find
127 foldlM = trans_map3 foldlM
128 foldrM = trans_map3 foldrM
129 forM_ = trans_map2 forM_
130 for_ = trans_map2 for_
131 mapM_ = trans_map2 mapM_
132 maximumBy = trans_map2 maximumBy
133 minimumBy = trans_map2 minimumBy
134 notElem = trans_map2 notElem
135 or = trans_map1 or
136 sequenceA_ = trans_map1 sequenceA_
137 sequence_ = trans_map1 sequence_
138 traverse_ = trans_map2 traverse_
139
140 type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
141 type instance Consts_of_Iface (Proxy Foldable) = Proxy Foldable ': Consts_imported_by Foldable
142 type instance Consts_imported_by Foldable = '[]
143
144 instance Sym_Foldable HostI where
145 foldMap = liftM2 Foldable.foldMap
146 foldr = liftM3 Foldable.foldr
147 foldr' = liftM3 Foldable.foldr'
148 foldl = liftM3 Foldable.foldl
149 foldl' = liftM3 Foldable.foldl'
150 null = liftM Foldable.null
151 length = liftM Foldable.length
152 minimum = liftM Foldable.minimum
153 maximum = liftM Foldable.maximum
154 elem = liftM2 Foldable.elem
155 sum = liftM Foldable.sum
156 product = liftM Foldable.product
157 toList = liftM Foldable.toList
158 all = liftM2 Foldable.all
159 and = liftM Foldable.and
160 any = liftM2 Foldable.any
161 concat = liftM Foldable.concat
162 concatMap = liftM2 Foldable.concatMap
163 find = liftM2 Foldable.find
164 foldlM = liftM3 Foldable.foldlM
165 foldrM = liftM3 Foldable.foldrM
166 forM_ = liftM2 Foldable.forM_
167 for_ = liftM2 Foldable.for_
168 mapM_ = liftM2 Foldable.mapM_
169 maximumBy = liftM2 Foldable.maximumBy
170 minimumBy = liftM2 Foldable.minimumBy
171 notElem = liftM2 Foldable.notElem
172 or = liftM Foldable.or
173 sequenceA_ = liftM Foldable.sequenceA_
174 sequence_ = liftM Foldable.sequence_
175 traverse_ = liftM2 Foldable.traverse_
176 instance Sym_Foldable TextI where
177 foldMap = textI_app2 "foldMap"
178 foldr = textI_app3 "foldr"
179 foldr' = textI_app3 "foldr'"
180 foldl = textI_app3 "foldl"
181 foldl' = textI_app3 "foldl'"
182 null = textI_app1 "null"
183 length = textI_app1 "length"
184 minimum = textI_app1 "minimum"
185 maximum = textI_app1 "maximum"
186 elem = textI_app2 "elem"
187 sum = textI_app1 "sum"
188 product = textI_app1 "product"
189 toList = textI_app1 "toList"
190 all = textI_app2 "all"
191 and = textI_app1 "and"
192 any = textI_app2 "any"
193 concat = textI_app1 "concat"
194 concatMap = textI_app2 "concatMap"
195 find = textI_app2 "find"
196 foldlM = textI_app3 "foldlM"
197 foldrM = textI_app3 "foldrM"
198 forM_ = textI_app2 "forM_"
199 for_ = textI_app2 "for_"
200 mapM_ = textI_app2 "mapM_"
201 maximumBy = textI_app2 "maximumBy"
202 minimumBy = textI_app2 "minimumBy"
203 notElem = textI_app2 "notElem"
204 or = textI_app1 "or"
205 sequenceA_ = textI_app1 "sequenceA_"
206 sequence_ = textI_app1 "sequence_"
207 traverse_ = textI_app2 "traverse_"
208 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where
209 foldMap = dupI2 sym_Foldable foldMap
210 foldr = dupI3 sym_Foldable foldr
211 foldr' = dupI3 sym_Foldable foldr'
212 foldl = dupI3 sym_Foldable foldl
213 foldl' = dupI3 sym_Foldable foldl'
214 null = dupI1 sym_Foldable null
215 length = dupI1 sym_Foldable length
216 minimum = dupI1 sym_Foldable minimum
217 maximum = dupI1 sym_Foldable maximum
218 elem = dupI2 sym_Foldable elem
219 sum = dupI1 sym_Foldable sum
220 product = dupI1 sym_Foldable product
221 toList = dupI1 sym_Foldable toList
222 all = dupI2 sym_Foldable all
223 and = dupI1 sym_Foldable and
224 any = dupI2 sym_Foldable any
225 concat = dupI1 sym_Foldable concat
226 concatMap = dupI2 sym_Foldable concatMap
227 find = dupI2 sym_Foldable find
228 foldlM = dupI3 sym_Foldable foldlM
229 foldrM = dupI3 sym_Foldable foldrM
230 forM_ = dupI2 sym_Foldable forM_
231 for_ = dupI2 sym_Foldable for_
232 mapM_ = dupI2 sym_Foldable mapM_
233 maximumBy = dupI2 sym_Foldable maximumBy
234 minimumBy = dupI2 sym_Foldable minimumBy
235 notElem = dupI2 sym_Foldable notElem
236 or = dupI1 sym_Foldable or
237 sequenceA_ = dupI1 sym_Foldable sequenceA_
238 sequence_ = dupI1 sym_Foldable sequence_
239 traverse_ = dupI2 sym_Foldable traverse_
240
241 instance Const_from Text cs => Const_from Text (Proxy Foldable ': cs) where
242 const_from "Foldable" k = k (ConstZ kind)
243 const_from s k = const_from s $ k . ConstS
244 instance Show_Const cs => Show_Const (Proxy Foldable ': cs) where
245 show_const ConstZ{} = "Foldable"
246 show_const (ConstS c) = show_const c
247
248 instance -- Proj_ConC
249 Proj_ConC cs (Proxy Foldable)
250 instance -- Term_fromI
251 ( AST ast
252 , Lexem ast ~ LamVarName
253 , Inj_Const (Consts_of_Ifaces is) Foldable
254 , Inj_Const (Consts_of_Ifaces is) Monoid
255 , Inj_Const (Consts_of_Ifaces is) (->)
256 , Inj_Const (Consts_of_Ifaces is) Int
257 , Inj_Const (Consts_of_Ifaces is) Bool
258 , Inj_Const (Consts_of_Ifaces is) Eq
259 , Inj_Const (Consts_of_Ifaces is) Ord
260 , Inj_Const (Consts_of_Ifaces is) Num
261 , Inj_Const (Consts_of_Ifaces is) []
262 , Proj_Con (Consts_of_Ifaces is)
263 , Term_from is ast
264 ) => Term_fromI is (Proxy Foldable) ast where
265 term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy Foldable ': rs)
266 term_fromI ast ctx k =
267 case ast_lexem ast of
268 "foldMap" -> foldMap_from
269 "foldr" -> foldr_from foldr
270 "foldr'" -> foldr_from foldr'
271 "foldl" -> foldl_from foldl
272 "foldl'" -> foldl_from foldl'
273 "length" -> ta2ty_from length
274 "null" -> ta2ty_from null
275 "minimum" -> ta2a_from tyOrd minimum
276 "maximum" -> ta2a_from tyOrd maximum
277 "sum" -> ta2a_from tyNum sum
278 "product" -> ta2a_from tyNum product
279 "elem" -> elem_from
280 "all" -> allany_from all
281 "any" -> allany_from any
282 "and" -> andor_from and
283 "or" -> andor_from or
284 "toList" -> toList_from
285 "concat" -> concat_from
286 _ -> Left $ Error_Term_unsupported
287 where
288 foldMap_from =
289 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
290 from_ast2 ast $ \ast_a2m ast_ta as ->
291 term_from ast_a2m ctx $ \ty_a2m (TermLC a2m) ->
292 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
293 check_type2 tyFun ast_a2m ty_a2m $ \Refl ty_a2m_a ty_a2m_m ->
294 check_constraint (At (Just ast_a2m) (tyMonoid :$ ty_a2m_m)) $ \Con ->
295 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
296 check_type (At (Just ast_a2m) ty_a2m_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
297 k as ty_a2m_m $ TermLC $
298 \c -> foldMap (a2m c) (ta c)
299 foldr_from
300 (fold::forall term f a b.
301 (Sym_Foldable term, Foldable f)
302 => term (a -> b -> b) -> term b -> term (f a) -> term b) =
303 -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
304 from_ast3 ast $ \ast_a2b2b ast_b ast_ta as ->
305 term_from ast_a2b2b ctx $ \ty_a2b2b (TermLC a2b2b) ->
306 term_from ast_b ctx $ \ty_b (TermLC b) ->
307 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
308 check_type2 tyFun ast_a2b2b ty_a2b2b $ \Refl ty_a2b2b_a ty_a2b2b_b2b ->
309 check_type2 tyFun ast_a2b2b ty_a2b2b_b2b $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 ->
310 check_type (At (Just ast_a2b2b) ty_a2b2b_b2b_b0) (At (Just ast_a2b2b) ty_a2b2b_b2b_b1) $ \Refl ->
311 check_type (At (Just ast_a2b2b) ty_a2b2b_b2b_b0) (At (Just ast_b) ty_b) $ \Refl ->
312 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
313 check_type (At (Just ast_a2b2b) ty_a2b2b_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
314 k as ty_b $ TermLC $
315 \c -> fold (a2b2b c) (b c) (ta c)
316 foldl_from
317 (fold::forall term f a b.
318 (Sym_Foldable term, Foldable f)
319 => term (b -> a -> b) -> term b -> term (f a) -> term b) =
320 -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
321 from_ast3 ast $ \ast_b2a2b ast_b ast_ta as ->
322 term_from ast_b2a2b ctx $ \ty_b2a2b (TermLC b2a2b) ->
323 term_from ast_b ctx $ \ty_b (TermLC b) ->
324 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
325 check_type2 tyFun ast_b2a2b ty_b2a2b $ \Refl ty_b2a2b_b ty_b2a2b_a2b ->
326 check_type2 tyFun ast_b2a2b ty_b2a2b_a2b $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b ->
327 check_type (At (Just ast_b2a2b) ty_b2a2b_b) (At (Just ast_b2a2b) ty_b2a2b_a2b_b) $ \Refl ->
328 check_type (At (Just ast_b2a2b) ty_b2a2b_b) (At (Just ast_b) ty_b) $ \Refl ->
329 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
330 check_type (At (Just ast_b2a2b) ty_b2a2b_a2b_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
331 k as ty_b $ TermLC $
332 \c -> fold (b2a2b c) (b c) (ta c)
333 ta2ty_from
334 :: forall ty. Inj_Const (Consts_of_Ifaces is) ty
335 => (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term ty)
336 -> Either (Error_Term is ast) ret
337 ta2ty_from f =
338 -- length :: Foldable t => t a -> Int
339 -- null :: Foldable t => t a -> Bool
340 from_ast1 ast $ \ast_ta as ->
341 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
342 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t _ty_ta_a ->
343 k as (TyConst inj_const::Type (Consts_of_Ifaces is) ty) $ TermLC $
344 \c -> f (ta c)
345 ta2a_from
346 :: forall con. Type (Consts_of_Ifaces is) con
347 -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
348 -> Either (Error_Term is ast) ret
349 ta2a_from q f =
350 -- minimum :: (Foldable t, Ord a) => t a -> a
351 -- maximum :: (Foldable t, Ord a) => t a -> a
352 -- sum :: (Foldable t, Num a) => t a -> a
353 -- product :: (Foldable t, Num a) => t a -> a
354 from_ast1 ast $ \ast_ta as ->
355 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
356 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
357 check_constraint (At (Just ast_ta) (q :$ ty_ta_a)) $ \Con ->
358 k as ty_ta_a $ TermLC $
359 \c -> f (ta c)
360 elem_from =
361 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
362 from_ast2 ast $ \ast_a ast_ta as ->
363 term_from ast_a ctx $ \ty_a (TermLC a) ->
364 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
365 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
366 check_constraint (At (Just ast_ta) (tyEq :$ ty_ta_a)) $ \Con ->
367 check_type (At (Just ast_a) ty_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
368 k as tyBool $ TermLC $
369 \c -> a c `elem` ta c
370 allany_from
371 (g::forall term f a.
372 (Sym_Foldable term, Foldable f)
373 => term (a -> Bool) -> term (f a) -> term Bool) =
374 -- all :: Foldable t => (a -> Bool) -> t a -> Bool
375 -- any :: Foldable t => (a -> Bool) -> t a -> Bool
376 from_ast2 ast $ \ast_a2Bool ast_ta as ->
377 term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
378 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
379 check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
380 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
381 check_type (At (Just ast_a2Bool) ty_a2Bool_a) (At (Just ast_ta) ty_ta_a) $ \Refl ->
382 check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
383 k as tyBool $ TermLC $
384 \c -> g (a2Bool c) (ta c)
385 andor_from
386 (g::forall term f.
387 (Sym_Foldable term, Foldable f)
388 => term (f Bool) -> term Bool) =
389 -- and :: Foldable t => t Bool -> Bool
390 -- or :: Foldable t => t Bool -> Bool
391 from_ast1 ast $ \ast_tBool as ->
392 term_from ast_tBool ctx $ \ty_tBool (TermLC tBool) ->
393 check_constraint1 tyFoldable ast_tBool ty_tBool $ \Refl Con _ty_tBool_t ty_tBool_Bool ->
394 check_type (At Nothing tyBool) (At (Just ast_tBool) ty_tBool_Bool) $ \Refl ->
395 k as tyBool $ TermLC $
396 \c -> g (tBool c)
397 toList_from =
398 -- toList :: Foldable t => t a -> [a]
399 from_ast1 ast $ \ast_ta as ->
400 term_from ast_ta ctx $ \ty_ta (TermLC ta) ->
401 check_constraint1 tyFoldable ast_ta ty_ta $ \Refl Con _ty_ta_t ty_ta_a ->
402 k as (tyList :$ ty_ta_a) $ TermLC $
403 \c -> toList (ta c)
404 concat_from =
405 -- concat :: Foldable t => t [a] -> [a]
406 from_ast1 ast $ \ast_tla as ->
407 term_from ast_tla ctx $ \ty_tla (TermLC tla) ->
408 check_constraint1 tyFoldable ast_tla ty_tla $ \Refl Con _ty_tla_t ty_tla_la ->
409 check_type1 tyList ast_tla ty_tla_la $ \Refl ty_tla_la_a ->
410 k as (tyList :$ ty_tla_la_a) $ TermLC $
411 \c -> concat (tla c)
412
413 -- | The 'Foldable' 'Type'
414 tyFoldable :: Inj_Const cs Foldable => Type cs Foldable
415 tyFoldable = TyConst inj_const
416
417 sym_Foldable :: Proxy Sym_Foldable
418 sym_Foldable = Proxy
419
420 syFoldable :: IsString a => [Syntax a] -> Syntax a
421 syFoldable = Syntax "Foldable"