]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Foldable.hs
Reorganize symantic-document modules.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Foldable.hs
1 {-# LANGUAGE PolyKinds #-}
2 {-# LANGUAGE UndecidableInstances #-}
3 {-# OPTIONS_GHC -fno-warn-orphans #-}
4 -- | Symantic for 'Foldable'.
5 module Language.Symantic.Lib.Foldable where
6
7 import Control.Applicative (Alternative)
8 import Control.Monad (MonadPlus)
9 import Data.Foldable (Foldable)
10 import qualified Data.Foldable as Foldable
11 import Prelude hiding (Foldable(..)
12 , all, and, any, concat, concatMap
13 , mapM_, notElem, or, sequence_)
14
15 import Language.Symantic
16 import Language.Symantic.Lib.Alternative (tyAlternative)
17 import Language.Symantic.Lib.Bool (tyBool)
18 import Language.Symantic.Lib.Eq (tyEq)
19 import Language.Symantic.Lib.Function (a0, b1)
20 import Language.Symantic.Lib.Functor (f2)
21 import Language.Symantic.Lib.Int (tyInt)
22 import Language.Symantic.Lib.List (tyList)
23 import Language.Symantic.Lib.Monoid (tyMonoid)
24 import Language.Symantic.Lib.Num (tyNum)
25 import Language.Symantic.Lib.Ord (tyOrd)
26
27 -- * Class 'Sym_Foldable'
28 type instance Sym Foldable = Sym_Foldable
29 class Sym_Foldable term where
30 foldMap :: Foldable f => Monoid m => term (a -> m) -> term (f a) -> term m
31 foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
32 foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
33 foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
34 foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
35 length :: Foldable f => term (f a) -> term Int
36 null :: Foldable f => term (f a) -> term Bool
37 minimum :: Foldable f => Ord a => term (f a) -> term a
38 maximum :: Foldable f => Ord a => term (f a) -> term a
39 elem :: Foldable f => Eq a => term a -> term (f a) -> term Bool; infix 4 `elem`
40 sum :: Foldable f => Num a => term (f a) -> term a
41 product :: Foldable f => Num a => term (f a) -> term a
42 toList :: Foldable f => term (f a) -> term [a]
43 all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
44 and :: Foldable f => term (f Bool) -> term Bool
45 any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
46 concat :: Foldable f => term (f [a]) -> term [a]
47 concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
48 find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
49 foldlM :: Foldable f => Monad m => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
50 foldrM :: Foldable f => Monad m => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
51 forM_ :: Foldable f => Monad m => term (f a) -> term (a -> m b) -> term (m ())
52 for_ :: Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())
53 mapM_ :: Foldable f => Monad m => term (a -> m b) -> term (f a) -> term (m ())
54 maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
55 minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
56 notElem :: Foldable f => Eq a => term a -> term (f a) -> term Bool
57 or :: Foldable f => term (f Bool) -> term Bool
58 sequenceA_ :: Foldable f => Applicative p => term (f (p a)) -> term (p ())
59 sequence_ :: Foldable f => Monad m => term (f (m a)) -> term (m ())
60 traverse_ :: Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())
61 asum :: Foldable f => Alternative p => term (f (p a)) -> term (p a)
62 msum :: Foldable f => MonadPlus p => term (f (p a)) -> term (p a)
63
64 default foldMap :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monoid m => term (a -> m) -> term (f a) -> term m
65 default foldr :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
66 default foldr' :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
67 default foldl :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
68 default foldl' :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
69 default length :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term Int
70 default null :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term Bool
71 default minimum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a => term (f a) -> term a
72 default maximum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a => term (f a) -> term a
73 default elem :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a => term a -> term (f a) -> term Bool
74 default sum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a => term (f a) -> term a
75 default product :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a => term (f a) -> term a
76 default toList :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term [a]
77 default all :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term Bool
78 default and :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f Bool) -> term Bool
79 default any :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term Bool
80 default concat :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f [a]) -> term [a]
81 default concatMap :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> [b]) -> term (f a) -> term [b]
82 default find :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
83 default foldlM :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
84 default foldrM :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
85 default forM_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (f a) -> term (a -> m b) -> term (m ())
86 default for_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())
87 default mapM_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (a -> m b) -> term (f a) -> term (m ())
88 default maximumBy :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
89 default minimumBy :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
90 default notElem :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a => term a -> term (f a) -> term Bool
91 default or :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f Bool) -> term Bool
92 default sequenceA_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (f (p a)) -> term (p ())
93 default sequence_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (f (m a)) -> term (m ())
94 default traverse_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())
95 default asum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Alternative m => term (f (m a)) -> term (m a)
96 default msum :: Sym_Foldable (UnT term) => Trans term => Foldable f => MonadPlus m => term (f (m a)) -> term (m a)
97
98 foldMap = trans2 foldMap
99 foldr = trans3 foldr
100 foldr' = trans3 foldr'
101 foldl = trans3 foldl
102 foldl' = trans3 foldl'
103 length = trans1 length
104 null = trans1 null
105 minimum = trans1 minimum
106 maximum = trans1 maximum
107 elem = trans2 elem
108 sum = trans1 sum
109 product = trans1 product
110 toList = trans1 toList
111 all = trans2 all
112 and = trans1 and
113 any = trans2 any
114 concat = trans1 concat
115 concatMap = trans2 concatMap
116 find = trans2 find
117 foldlM = trans3 foldlM
118 foldrM = trans3 foldrM
119 forM_ = trans2 forM_
120 for_ = trans2 for_
121 mapM_ = trans2 mapM_
122 maximumBy = trans2 maximumBy
123 minimumBy = trans2 minimumBy
124 notElem = trans2 notElem
125 or = trans1 or
126 sequenceA_ = trans1 sequenceA_
127 sequence_ = trans1 sequence_
128 traverse_ = trans2 traverse_
129 asum = trans1 asum
130 msum = trans1 msum
131
132 -- Interpreting
133 instance Sym_Foldable Eval where
134 foldMap = eval2 Foldable.foldMap
135 foldr = eval3 Foldable.foldr
136 foldr' = eval3 Foldable.foldr'
137 foldl = eval3 Foldable.foldl
138 foldl' = eval3 Foldable.foldl'
139 null = eval1 Foldable.null
140 length = eval1 Foldable.length
141 minimum = eval1 Foldable.minimum
142 maximum = eval1 Foldable.maximum
143 elem = eval2 Foldable.elem
144 sum = eval1 Foldable.sum
145 product = eval1 Foldable.product
146 toList = eval1 Foldable.toList
147 all = eval2 Foldable.all
148 and = eval1 Foldable.and
149 any = eval2 Foldable.any
150 concat = eval1 Foldable.concat
151 concatMap = eval2 Foldable.concatMap
152 find = eval2 Foldable.find
153 foldlM = eval3 Foldable.foldlM
154 foldrM = eval3 Foldable.foldrM
155 forM_ = eval2 Foldable.forM_
156 for_ = eval2 Foldable.for_
157 mapM_ = eval2 Foldable.mapM_
158 maximumBy = eval2 Foldable.maximumBy
159 minimumBy = eval2 Foldable.minimumBy
160 notElem = eval2 Foldable.notElem
161 or = eval1 Foldable.or
162 sequenceA_ = eval1 Foldable.sequenceA_
163 sequence_ = eval1 Foldable.sequence_
164 traverse_ = eval2 Foldable.traverse_
165 asum = eval1 Foldable.asum
166 msum = eval1 Foldable.msum
167 instance Sym_Foldable View where
168 foldMap = view2 "foldMap"
169 foldr = view3 "foldr"
170 foldr' = view3 "foldr'"
171 foldl = view3 "foldl"
172 foldl' = view3 "foldl'"
173 null = view1 "null"
174 length = view1 "length"
175 minimum = view1 "minimum"
176 maximum = view1 "maximum"
177 elem = view2 "elem"
178 sum = view1 "sum"
179 product = view1 "product"
180 toList = view1 "toList"
181 all = view2 "all"
182 and = view1 "and"
183 any = view2 "any"
184 concat = view1 "concat"
185 concatMap = view2 "concatMap"
186 find = view2 "find"
187 foldlM = view3 "foldlM"
188 foldrM = view3 "foldrM"
189 forM_ = view2 "forM_"
190 for_ = view2 "for_"
191 mapM_ = view2 "mapM_"
192 maximumBy = view2 "maximumBy"
193 minimumBy = view2 "minimumBy"
194 notElem = view2 "notElem"
195 or = view1 "or"
196 sequenceA_ = view1 "sequenceA_"
197 sequence_ = view1 "sequence_"
198 traverse_ = view2 "traverse_"
199 asum = view1 "asum"
200 msum = view1 "msum"
201 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Dup r1 r2) where
202 foldMap = dup2 @Sym_Foldable foldMap
203 foldr = dup3 @Sym_Foldable foldr
204 foldr' = dup3 @Sym_Foldable foldr'
205 foldl = dup3 @Sym_Foldable foldl
206 foldl' = dup3 @Sym_Foldable foldl'
207 null = dup1 @Sym_Foldable null
208 length = dup1 @Sym_Foldable length
209 minimum = dup1 @Sym_Foldable minimum
210 maximum = dup1 @Sym_Foldable maximum
211 elem = dup2 @Sym_Foldable elem
212 sum = dup1 @Sym_Foldable sum
213 product = dup1 @Sym_Foldable product
214 toList = dup1 @Sym_Foldable toList
215 all = dup2 @Sym_Foldable all
216 and = dup1 @Sym_Foldable and
217 any = dup2 @Sym_Foldable any
218 concat = dup1 @Sym_Foldable concat
219 concatMap = dup2 @Sym_Foldable concatMap
220 find = dup2 @Sym_Foldable find
221 foldlM = dup3 @Sym_Foldable foldlM
222 foldrM = dup3 @Sym_Foldable foldrM
223 forM_ = dup2 @Sym_Foldable forM_
224 for_ = dup2 @Sym_Foldable for_
225 mapM_ = dup2 @Sym_Foldable mapM_
226 maximumBy = dup2 @Sym_Foldable maximumBy
227 minimumBy = dup2 @Sym_Foldable minimumBy
228 notElem = dup2 @Sym_Foldable notElem
229 or = dup1 @Sym_Foldable or
230 sequenceA_ = dup1 @Sym_Foldable sequenceA_
231 sequence_ = dup1 @Sym_Foldable sequence_
232 traverse_ = dup2 @Sym_Foldable traverse_
233 asum = dup1 @Sym_Foldable asum
234 msum = dup1 @Sym_Foldable msum
235
236 -- Transforming
237 instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)
238
239 -- Typing
240 instance NameTyOf Foldable where
241 nameTyOf _c = ["Foldable"] `Mod` "Foldable"
242 instance FixityOf Foldable
243 instance ClassInstancesFor Foldable
244 instance TypeInstancesFor Foldable
245
246 -- Compiling
247 instance Gram_Term_AtomsFor src ss g Foldable
248 instance (Source src, SymInj ss Foldable) => ModuleFor src ss Foldable where
249 moduleFor = ["Foldable"] `moduleWhere`
250 [ "foldMap" := teFoldable_foldMap
251 , "foldr" := teFoldable_foldr
252 , "foldr'" := teFoldable_foldr'
253 , "foldl" := teFoldable_foldl
254 , "elem" `withInfixN` 4 := teFoldable_elem
255 , "sum" := teFoldable_sum
256 , "product" := teFoldable_product
257 , "toList" := teFoldable_toList
258 , "all" := teFoldable_all
259 , "any" := teFoldable_any
260 , "and" := teFoldable_and
261 , "or" := teFoldable_or
262 , "concat" := teFoldable_concat
263 , "asum" := teFoldable_asum
264 -- , "msum" := teFoldable_msum
265 ]
266
267 -- ** 'Type's
268 tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)
269 tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a
270
271 t0 :: Source src => LenInj vs => KindInj (K t) =>
272 Type src (Proxy t ': vs) t
273 t0 = tyVar "t" $ varZ
274
275 t1 :: Source src => LenInj vs => KindInj (K t) =>
276 Type src (a ': Proxy t ': vs) t
277 t1 = tyVar "t" $ VarS varZ
278
279 t2 :: Source src => LenInj vs => KindInj (K t) =>
280 Type src (a ': b ': Proxy t ': vs) t
281 t2 = tyVar "t" $ VarS $ VarS varZ
282
283 -- ** 'Term's
284 teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))
285 teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap
286 where
287 m :: Source src => LenInj vs => KindInj (K m) =>
288 Type src (a ': b ': Proxy m ': vs) m
289 m = tyVar "m" $ VarS $ VarS varZ
290
291 teFoldable_elem :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Eq a #> (a -> t a -> Bool))
292 teFoldable_elem = Term (tyFoldable t1 # tyEq a0) (a0 ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 elem
293
294 teFoldable_toList :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> [a]))
295 teFoldable_toList = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyList a0) $ teSym @Foldable $ lam1 toList
296
297 teFoldable_concat :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t [a] -> [a]))
298 teFoldable_concat = Term (tyFoldable t1) (t1 `tyApp` (tyList a0) ~> tyList a0) $ teSym @Foldable $ lam1 concat
299
300 teFoldable_foldr, teFoldable_foldr' :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((a -> b -> b) -> b -> t a -> b))
301 teFoldable_foldr = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr
302
303 teFoldable_foldr' = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr'
304
305 teFoldable_foldl :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((b -> a -> b) -> b -> t a -> b))
306 teFoldable_foldl = Term (tyFoldable t2) ((b1 ~> a0 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldl
307
308 teFoldable_length :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Int))
309 teFoldable_length = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyInt) $ teSym @Foldable $ lam1 length
310
311 teFoldable_null :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Bool))
312 teFoldable_null = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam1 null
313
314 teFoldable_minimum, teFoldable_maximum :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Ord a #> (t a -> a))
315 teFoldable_minimum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 minimum
316 teFoldable_maximum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 maximum
317
318 teFoldable_sum, teFoldable_product :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Num a #> (t a -> a))
319 teFoldable_sum = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 sum
320 teFoldable_product = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 product
321
322 teFoldable_all, teFoldable_any :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> ((a -> Bool) -> t a -> Bool))
323 teFoldable_all = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 all
324 teFoldable_any = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 any
325
326 teFoldable_and, teFoldable_or :: TermDef Foldable '[Proxy t] (Foldable t #> (t Bool -> Bool))
327 teFoldable_and = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 and
328 teFoldable_or = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 or
329
330 teFoldable_asum :: TermDef Foldable '[Proxy a, Proxy t, Proxy f] ((Foldable t # Alternative f) #> (t (f a) -> f a))
331 teFoldable_asum = Term (tyFoldable t1 # tyAlternative f2) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $ teSym @Foldable $ lam1 asum
332
333 {- TODO: when MonadPlus will be supported
334 teFoldable_msum ::
335 Source src => SymInj ss Foldable =>
336 Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))
337 teFoldable_msum =
338 Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
339 teSym @Foldable $ lam1 msum
340 -}