-{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Foldable'.
module Language.Symantic.Lib.Foldable where
+import Control.Applicative (Alternative)
+import Control.Monad (MonadPlus)
import Data.Foldable (Foldable)
import qualified Data.Foldable as Foldable
-import Control.Monad (liftM, liftM2, liftM3)
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Foldable(..)
, all, and, any, concat, concatMap
- , mapM_, notElem, or, sequence, sequence_)
+ , mapM_, notElem, or, sequence_)
-import Language.Symantic.Parsing hiding (any)
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
+import Language.Symantic
+import Language.Symantic.Lib.Alternative (tyAlternative)
+import Language.Symantic.Lib.Bool (tyBool)
+import Language.Symantic.Lib.Eq (tyEq)
+import Language.Symantic.Lib.Function (a0, b1)
+import Language.Symantic.Lib.Functor (f2)
+import Language.Symantic.Lib.Int (tyInt)
+import Language.Symantic.Lib.List (tyList)
+import Language.Symantic.Lib.Monoid (tyMonoid)
+import Language.Symantic.Lib.Num (tyNum)
+import Language.Symantic.Lib.Ord (tyOrd)
-- * Class 'Sym_Foldable'
+type instance Sym Foldable = Sym_Foldable
class Sym_Foldable term where
- foldMap :: (Foldable f, Monoid m) => term (a -> m) -> term (f a) -> term m
- foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
- foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
- foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
- foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
- length :: Foldable f => term (f a) -> term Int
- null :: Foldable f => term (f a) -> term Bool
- minimum :: (Foldable f, Ord a) => term (f a) -> term a
- maximum :: (Foldable f, Ord a) => term (f a) -> term a
- elem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
- sum :: (Foldable f, Num a) => term (f a) -> term a
- product :: (Foldable f, Num a) => term (f a) -> term a
- toList :: Foldable f => term (f a) -> term [a]
- all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
- and :: Foldable f => term (f Bool) -> term Bool
- any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
- concat :: Foldable f => term (f [a]) -> term [a]
- concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
- find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
- foldlM :: (Foldable f, Monad m) => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
- foldrM :: (Foldable f, Monad m) => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
- forM_ :: (Foldable f, Monad m) => term (f a) -> term (a -> m b) -> term (m ())
- for_ :: (Foldable f, Applicative p) => term (f a) -> term (a -> p b) -> term (p ())
- mapM_ :: (Foldable f, Monad m) => term (a -> m b) -> term (f a) -> term (m ())
- maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
- minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
- notElem :: (Foldable f, Eq a) => term a -> term (f a) -> term Bool
- or :: Foldable f => term (f Bool) -> term Bool
- sequenceA_ :: (Foldable f, Applicative p) => term (f (p a)) -> term (p ())
- sequence_ :: (Foldable f, Monad m) => term (f (m a)) -> term (m ())
- traverse_ :: (Foldable f, Applicative p) => term (a -> p b) -> term (f a) -> term (p ())
- -- asum :: (Foldable t, GHC.Base.Alternative f) => t (f a) -> f a
- -- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m a
+ foldMap :: Foldable f => Monoid m => term (a -> m) -> term (f a) -> term m
+ foldr :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
+ foldr' :: Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
+ foldl :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
+ foldl' :: Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
+ length :: Foldable f => term (f a) -> term Int
+ null :: Foldable f => term (f a) -> term Bool
+ minimum :: Foldable f => Ord a => term (f a) -> term a
+ maximum :: Foldable f => Ord a => term (f a) -> term a
+ elem :: Foldable f => Eq a => term a -> term (f a) -> term Bool; infix 4 `elem`
+ sum :: Foldable f => Num a => term (f a) -> term a
+ product :: Foldable f => Num a => term (f a) -> term a
+ toList :: Foldable f => term (f a) -> term [a]
+ all :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
+ and :: Foldable f => term (f Bool) -> term Bool
+ any :: Foldable f => term (a -> Bool) -> term (f a) -> term Bool
+ concat :: Foldable f => term (f [a]) -> term [a]
+ concatMap :: Foldable f => term (a -> [b]) -> term (f a) -> term [b]
+ find :: Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
+ foldlM :: Foldable f => Monad m => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
+ foldrM :: Foldable f => Monad m => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
+ forM_ :: Foldable f => Monad m => term (f a) -> term (a -> m b) -> term (m ())
+ for_ :: Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())
+ mapM_ :: Foldable f => Monad m => term (a -> m b) -> term (f a) -> term (m ())
+ maximumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
+ minimumBy :: Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
+ notElem :: Foldable f => Eq a => term a -> term (f a) -> term Bool
+ or :: Foldable f => term (f Bool) -> term Bool
+ sequenceA_ :: Foldable f => Applicative p => term (f (p a)) -> term (p ())
+ sequence_ :: Foldable f => Monad m => term (f (m a)) -> term (m ())
+ traverse_ :: Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())
+ asum :: Foldable f => Alternative p => term (f (p a)) -> term (p a)
+ msum :: Foldable f => MonadPlus p => term (f (p a)) -> term (p a)
- default foldMap :: (Trans t term, Foldable f, Monoid m) => t term (a -> m) -> t term (f a) -> t term m
- default foldr :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
- default foldr' :: (Trans t term, Foldable f) => t term (a -> b -> b) -> t term b -> t term (f a) -> t term b
- default foldl :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
- default foldl' :: (Trans t term, Foldable f) => t term (b -> a -> b) -> t term b -> t term (f a) -> t term b
- default length :: (Trans t term, Foldable f) => t term (f a) -> t term Int
- default null :: (Trans t term, Foldable f) => t term (f a) -> t term Bool
- default minimum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
- default maximum :: (Trans t term, Foldable f, Ord a) => t term (f a) -> t term a
- default elem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
- default sum :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
- default product :: (Trans t term, Foldable f, Num a) => t term (f a) -> t term a
- default toList :: (Trans t term, Foldable f) => t term (f a) -> t term [a]
- default all :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
- default and :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
- default any :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term Bool
- default concat :: (Trans t term, Foldable f) => t term (f [a]) -> t term [a]
- default concatMap :: (Trans t term, Foldable f) => t term (a -> [b]) -> t term (f a) -> t term [b]
- default find :: (Trans t term, Foldable f) => t term (a -> Bool) -> t term (f a) -> t term (Maybe a)
- 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)
- 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)
- default forM_ :: (Trans t term, Foldable f, Monad m) => t term (f a) -> t term (a -> m b) -> t term (m ())
- default for_ :: (Trans t term, Foldable f, Applicative p) => t term (f a) -> t term (a -> p b) -> t term (p ())
- default mapM_ :: (Trans t term, Foldable f, Monad m) => t term (a -> m b) -> t term (f a) -> t term (m ())
- default maximumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
- default minimumBy :: (Trans t term, Foldable f) => t term (a -> a -> Ordering) -> t term (f a) -> t term a
- default notElem :: (Trans t term, Foldable f, Eq a) => t term a -> t term (f a) -> t term Bool
- default or :: (Trans t term, Foldable f) => t term (f Bool) -> t term Bool
- default sequenceA_ :: (Trans t term, Foldable f, Applicative p) => t term (f (p a)) -> t term (p ())
- default sequence_ :: (Trans t term, Foldable f, Monad m) => t term (f (m a)) -> t term (m ())
- default traverse_ :: (Trans t term, Foldable f, Applicative p) => t term (a -> p b) -> t term (f a) -> t term (p ())
+ default foldMap :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monoid m => term (a -> m) -> term (f a) -> term m
+ default foldr :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
+ default foldr' :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> b -> b) -> term b -> term (f a) -> term b
+ default foldl :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
+ default foldl' :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (b -> a -> b) -> term b -> term (f a) -> term b
+ default length :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term Int
+ default null :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term Bool
+ default minimum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a => term (f a) -> term a
+ default maximum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a => term (f a) -> term a
+ default elem :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a => term a -> term (f a) -> term Bool
+ default sum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a => term (f a) -> term a
+ default product :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a => term (f a) -> term a
+ default toList :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f a) -> term [a]
+ default all :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term Bool
+ default and :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f Bool) -> term Bool
+ default any :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term Bool
+ default concat :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f [a]) -> term [a]
+ default concatMap :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> [b]) -> term (f a) -> term [b]
+ default find :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> Bool) -> term (f a) -> term (Maybe a)
+ 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)
+ 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)
+ default forM_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (f a) -> term (a -> m b) -> term (m ())
+ default for_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())
+ default mapM_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (a -> m b) -> term (f a) -> term (m ())
+ default maximumBy :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
+ default minimumBy :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (a -> a -> Ordering) -> term (f a) -> term a
+ default notElem :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a => term a -> term (f a) -> term Bool
+ default or :: Sym_Foldable (UnT term) => Trans term => Foldable f => term (f Bool) -> term Bool
+ default sequenceA_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (f (p a)) -> term (p ())
+ default sequence_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m => term (f (m a)) -> term (m ())
+ default traverse_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())
+ default asum :: Sym_Foldable (UnT term) => Trans term => Foldable f => Alternative m => term (f (m a)) -> term (m a)
+ default msum :: Sym_Foldable (UnT term) => Trans term => Foldable f => MonadPlus m => term (f (m a)) -> term (m a)
- foldMap = trans_map2 foldMap
- foldr = trans_map3 foldr
- foldr' = trans_map3 foldr'
- foldl = trans_map3 foldl
- foldl' = trans_map3 foldl'
- length = trans_map1 length
- null = trans_map1 null
- minimum = trans_map1 minimum
- maximum = trans_map1 maximum
- elem = trans_map2 elem
- sum = trans_map1 sum
- product = trans_map1 product
- toList = trans_map1 toList
- all = trans_map2 all
- and = trans_map1 and
- any = trans_map2 any
- concat = trans_map1 concat
- concatMap = trans_map2 concatMap
- find = trans_map2 find
- foldlM = trans_map3 foldlM
- foldrM = trans_map3 foldrM
- forM_ = trans_map2 forM_
- for_ = trans_map2 for_
- mapM_ = trans_map2 mapM_
- maximumBy = trans_map2 maximumBy
- minimumBy = trans_map2 minimumBy
- notElem = trans_map2 notElem
- or = trans_map1 or
- sequenceA_ = trans_map1 sequenceA_
- sequence_ = trans_map1 sequence_
- traverse_ = trans_map2 traverse_
+ foldMap = trans2 foldMap
+ foldr = trans3 foldr
+ foldr' = trans3 foldr'
+ foldl = trans3 foldl
+ foldl' = trans3 foldl'
+ length = trans1 length
+ null = trans1 null
+ minimum = trans1 minimum
+ maximum = trans1 maximum
+ elem = trans2 elem
+ sum = trans1 sum
+ product = trans1 product
+ toList = trans1 toList
+ all = trans2 all
+ and = trans1 and
+ any = trans2 any
+ concat = trans1 concat
+ concatMap = trans2 concatMap
+ find = trans2 find
+ foldlM = trans3 foldlM
+ foldrM = trans3 foldrM
+ forM_ = trans2 forM_
+ for_ = trans2 for_
+ mapM_ = trans2 mapM_
+ maximumBy = trans2 maximumBy
+ minimumBy = trans2 minimumBy
+ notElem = trans2 notElem
+ or = trans1 or
+ sequenceA_ = trans1 sequenceA_
+ sequence_ = trans1 sequence_
+ traverse_ = trans2 traverse_
+ asum = trans1 asum
+ msum = trans1 msum
-infix 4 `elem`
+-- Interpreting
+instance Sym_Foldable Eval where
+ foldMap = eval2 Foldable.foldMap
+ foldr = eval3 Foldable.foldr
+ foldr' = eval3 Foldable.foldr'
+ foldl = eval3 Foldable.foldl
+ foldl' = eval3 Foldable.foldl'
+ null = eval1 Foldable.null
+ length = eval1 Foldable.length
+ minimum = eval1 Foldable.minimum
+ maximum = eval1 Foldable.maximum
+ elem = eval2 Foldable.elem
+ sum = eval1 Foldable.sum
+ product = eval1 Foldable.product
+ toList = eval1 Foldable.toList
+ all = eval2 Foldable.all
+ and = eval1 Foldable.and
+ any = eval2 Foldable.any
+ concat = eval1 Foldable.concat
+ concatMap = eval2 Foldable.concatMap
+ find = eval2 Foldable.find
+ foldlM = eval3 Foldable.foldlM
+ foldrM = eval3 Foldable.foldrM
+ forM_ = eval2 Foldable.forM_
+ for_ = eval2 Foldable.for_
+ mapM_ = eval2 Foldable.mapM_
+ maximumBy = eval2 Foldable.maximumBy
+ minimumBy = eval2 Foldable.minimumBy
+ notElem = eval2 Foldable.notElem
+ or = eval1 Foldable.or
+ sequenceA_ = eval1 Foldable.sequenceA_
+ sequence_ = eval1 Foldable.sequence_
+ traverse_ = eval2 Foldable.traverse_
+ asum = eval1 Foldable.asum
+ msum = eval1 Foldable.msum
+instance Sym_Foldable View where
+ foldMap = view2 "foldMap"
+ foldr = view3 "foldr"
+ foldr' = view3 "foldr'"
+ foldl = view3 "foldl"
+ foldl' = view3 "foldl'"
+ null = view1 "null"
+ length = view1 "length"
+ minimum = view1 "minimum"
+ maximum = view1 "maximum"
+ elem = view2 "elem"
+ sum = view1 "sum"
+ product = view1 "product"
+ toList = view1 "toList"
+ all = view2 "all"
+ and = view1 "and"
+ any = view2 "any"
+ concat = view1 "concat"
+ concatMap = view2 "concatMap"
+ find = view2 "find"
+ foldlM = view3 "foldlM"
+ foldrM = view3 "foldrM"
+ forM_ = view2 "forM_"
+ for_ = view2 "for_"
+ mapM_ = view2 "mapM_"
+ maximumBy = view2 "maximumBy"
+ minimumBy = view2 "minimumBy"
+ notElem = view2 "notElem"
+ or = view1 "or"
+ sequenceA_ = view1 "sequenceA_"
+ sequence_ = view1 "sequence_"
+ traverse_ = view2 "traverse_"
+ asum = view1 "asum"
+ msum = view1 "msum"
+instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Dup r1 r2) where
+ foldMap = dup2 @Sym_Foldable foldMap
+ foldr = dup3 @Sym_Foldable foldr
+ foldr' = dup3 @Sym_Foldable foldr'
+ foldl = dup3 @Sym_Foldable foldl
+ foldl' = dup3 @Sym_Foldable foldl'
+ null = dup1 @Sym_Foldable null
+ length = dup1 @Sym_Foldable length
+ minimum = dup1 @Sym_Foldable minimum
+ maximum = dup1 @Sym_Foldable maximum
+ elem = dup2 @Sym_Foldable elem
+ sum = dup1 @Sym_Foldable sum
+ product = dup1 @Sym_Foldable product
+ toList = dup1 @Sym_Foldable toList
+ all = dup2 @Sym_Foldable all
+ and = dup1 @Sym_Foldable and
+ any = dup2 @Sym_Foldable any
+ concat = dup1 @Sym_Foldable concat
+ concatMap = dup2 @Sym_Foldable concatMap
+ find = dup2 @Sym_Foldable find
+ foldlM = dup3 @Sym_Foldable foldlM
+ foldrM = dup3 @Sym_Foldable foldrM
+ forM_ = dup2 @Sym_Foldable forM_
+ for_ = dup2 @Sym_Foldable for_
+ mapM_ = dup2 @Sym_Foldable mapM_
+ maximumBy = dup2 @Sym_Foldable maximumBy
+ minimumBy = dup2 @Sym_Foldable minimumBy
+ notElem = dup2 @Sym_Foldable notElem
+ or = dup1 @Sym_Foldable or
+ sequenceA_ = dup1 @Sym_Foldable sequenceA_
+ sequence_ = dup1 @Sym_Foldable sequence_
+ traverse_ = dup2 @Sym_Foldable traverse_
+ asum = dup1 @Sym_Foldable asum
+ msum = dup1 @Sym_Foldable msum
-type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
-type instance TyConsts_of_Iface (Proxy Foldable) = Proxy Foldable ': TyConsts_imported_by Foldable
-type instance TyConsts_imported_by Foldable = '[]
+-- Transforming
+instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)
-instance Sym_Foldable HostI where
- foldMap = liftM2 Foldable.foldMap
- foldr = liftM3 Foldable.foldr
- foldr' = liftM3 Foldable.foldr'
- foldl = liftM3 Foldable.foldl
- foldl' = liftM3 Foldable.foldl'
- null = liftM Foldable.null
- length = liftM Foldable.length
- minimum = liftM Foldable.minimum
- maximum = liftM Foldable.maximum
- elem = liftM2 Foldable.elem
- sum = liftM Foldable.sum
- product = liftM Foldable.product
- toList = liftM Foldable.toList
- all = liftM2 Foldable.all
- and = liftM Foldable.and
- any = liftM2 Foldable.any
- concat = liftM Foldable.concat
- concatMap = liftM2 Foldable.concatMap
- find = liftM2 Foldable.find
- foldlM = liftM3 Foldable.foldlM
- foldrM = liftM3 Foldable.foldrM
- forM_ = liftM2 Foldable.forM_
- for_ = liftM2 Foldable.for_
- mapM_ = liftM2 Foldable.mapM_
- maximumBy = liftM2 Foldable.maximumBy
- minimumBy = liftM2 Foldable.minimumBy
- notElem = liftM2 Foldable.notElem
- or = liftM Foldable.or
- sequenceA_ = liftM Foldable.sequenceA_
- sequence_ = liftM Foldable.sequence_
- traverse_ = liftM2 Foldable.traverse_
-instance Sym_Foldable TextI where
- foldMap = textI2 "foldMap"
- foldr = textI3 "foldr"
- foldr' = textI3 "foldr'"
- foldl = textI3 "foldl"
- foldl' = textI3 "foldl'"
- null = textI1 "null"
- length = textI1 "length"
- minimum = textI1 "minimum"
- maximum = textI1 "maximum"
- elem = textI2 "elem"
- sum = textI1 "sum"
- product = textI1 "product"
- toList = textI1 "toList"
- all = textI2 "all"
- and = textI1 "and"
- any = textI2 "any"
- concat = textI1 "concat"
- concatMap = textI2 "concatMap"
- find = textI2 "find"
- foldlM = textI3 "foldlM"
- foldrM = textI3 "foldrM"
- forM_ = textI2 "forM_"
- for_ = textI2 "for_"
- mapM_ = textI2 "mapM_"
- maximumBy = textI2 "maximumBy"
- minimumBy = textI2 "minimumBy"
- notElem = textI2 "notElem"
- or = textI1 "or"
- sequenceA_ = textI1 "sequenceA_"
- sequence_ = textI1 "sequence_"
- traverse_ = textI2 "traverse_"
-instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (DupI r1 r2) where
- foldMap = dupI2 (Proxy @Sym_Foldable) foldMap
- foldr = dupI3 (Proxy @Sym_Foldable) foldr
- foldr' = dupI3 (Proxy @Sym_Foldable) foldr'
- foldl = dupI3 (Proxy @Sym_Foldable) foldl
- foldl' = dupI3 (Proxy @Sym_Foldable) foldl'
- null = dupI1 (Proxy @Sym_Foldable) null
- length = dupI1 (Proxy @Sym_Foldable) length
- minimum = dupI1 (Proxy @Sym_Foldable) minimum
- maximum = dupI1 (Proxy @Sym_Foldable) maximum
- elem = dupI2 (Proxy @Sym_Foldable) elem
- sum = dupI1 (Proxy @Sym_Foldable) sum
- product = dupI1 (Proxy @Sym_Foldable) product
- toList = dupI1 (Proxy @Sym_Foldable) toList
- all = dupI2 (Proxy @Sym_Foldable) all
- and = dupI1 (Proxy @Sym_Foldable) and
- any = dupI2 (Proxy @Sym_Foldable) any
- concat = dupI1 (Proxy @Sym_Foldable) concat
- concatMap = dupI2 (Proxy @Sym_Foldable) concatMap
- find = dupI2 (Proxy @Sym_Foldable) find
- foldlM = dupI3 (Proxy @Sym_Foldable) foldlM
- foldrM = dupI3 (Proxy @Sym_Foldable) foldrM
- forM_ = dupI2 (Proxy @Sym_Foldable) forM_
- for_ = dupI2 (Proxy @Sym_Foldable) for_
- mapM_ = dupI2 (Proxy @Sym_Foldable) mapM_
- maximumBy = dupI2 (Proxy @Sym_Foldable) maximumBy
- minimumBy = dupI2 (Proxy @Sym_Foldable) minimumBy
- notElem = dupI2 (Proxy @Sym_Foldable) notElem
- or = dupI1 (Proxy @Sym_Foldable) or
- sequenceA_ = dupI1 (Proxy @Sym_Foldable) sequenceA_
- sequence_ = dupI1 (Proxy @Sym_Foldable) sequence_
- traverse_ = dupI2 (Proxy @Sym_Foldable) traverse_
+-- Typing
+instance NameTyOf Foldable where
+ nameTyOf _c = ["Foldable"] `Mod` "Foldable"
+instance FixityOf Foldable
+instance ClassInstancesFor Foldable
+instance TypeInstancesFor Foldable
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Foldable
- ) => Read_TyNameR TyName cs (Proxy Foldable ': rs) where
- read_TyNameR _cs (TyName "Foldable") k = k (ty @Foldable)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Foldable ': cs) where
- show_TyConst TyConstZ{} = "Foldable"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Foldable
+instance (Source src, SymInj ss Foldable) => ModuleFor src ss Foldable where
+ moduleFor = ["Foldable"] `moduleWhere`
+ [ "foldMap" := teFoldable_foldMap
+ , "foldr" := teFoldable_foldr
+ , "foldr'" := teFoldable_foldr'
+ , "foldl" := teFoldable_foldl
+ , "elem" `withInfixN` 4 := teFoldable_elem
+ , "sum" := teFoldable_sum
+ , "product" := teFoldable_product
+ , "toList" := teFoldable_toList
+ , "all" := teFoldable_all
+ , "any" := teFoldable_any
+ , "and" := teFoldable_and
+ , "or" := teFoldable_or
+ , "concat" := teFoldable_concat
+ , "asum" := teFoldable_asum
+ -- , "msum" := teFoldable_msum
+ ]
-instance Proj_TyConC cs (Proxy Foldable)
-data instance TokenT meta (ts::[*]) (Proxy Foldable)
- = Token_Term_Foldable_foldMap (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_foldr (EToken meta ts) (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_foldr' (EToken meta ts) (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_foldl (EToken meta ts) (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_elem (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_null (EToken meta ts)
- | Token_Term_Foldable_length (EToken meta ts)
- | Token_Term_Foldable_minimum (EToken meta ts)
- | Token_Term_Foldable_maximum (EToken meta ts)
- | Token_Term_Foldable_sum (EToken meta ts)
- | Token_Term_Foldable_product (EToken meta ts)
- | Token_Term_Foldable_toList (EToken meta ts)
- | Token_Term_Foldable_all (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_any (EToken meta ts) (EToken meta ts)
- | Token_Term_Foldable_and (EToken meta ts)
- | Token_Term_Foldable_or (EToken meta ts)
- | Token_Term_Foldable_concat (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Foldable))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Foldable))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Foldable
- , Inj_TyConst (TyConsts_of_Ifaces is) Monoid
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Inj_TyConst (TyConsts_of_Ifaces is) Int
- , Inj_TyConst (TyConsts_of_Ifaces is) Bool
- , Inj_TyConst (TyConsts_of_Ifaces is) Eq
- , Inj_TyConst (TyConsts_of_Ifaces is) Ord
- , Inj_TyConst (TyConsts_of_Ifaces is) Num
- , Inj_TyConst (TyConsts_of_Ifaces is) []
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Foldable) where
- compileI
- :: forall meta ctx ret ls rs.
- TokenT meta is (Proxy Foldable)
- -> CompileT meta ctx ret is ls (Proxy Foldable ': rs)
- compileI tok ctx k =
- case tok of
- Token_Term_Foldable_foldMap tok_a2m tok_ta ->
- -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
- compileO tok_a2m ctx $ \ty_a2m (TermO a2m) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2m) ty_a2m) $ \Refl ty_a2m_a ty_a2m_m ->
- check_TyCon (At (Just tok_a2m) (ty @Monoid :$ ty_a2m_m)) $ \TyCon ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyEq
- (At (Just tok_a2m) ty_a2m_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- k ty_a2m_m $ TermO $
- \c -> foldMap (a2m c) (ta c)
- Token_Term_Foldable_foldr tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr
- Token_Term_Foldable_foldr' tok_a2b2b tok_b tok_ta -> foldr_from tok_a2b2b tok_b tok_ta foldr'
- Token_Term_Foldable_foldl tok_b2a2b tok_b tok_ta -> foldl_from tok_b2a2b tok_b tok_ta foldl
- Token_Term_Foldable_elem tok_a tok_ta ->
- -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
- compileO tok_a ctx $ \ty_a (TermO a) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyCon (At (Just tok_ta) (ty @Eq :$ ty_ta_a)) $ \TyCon ->
- check_TyEq
- (At (Just tok_a) ty_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- k (ty @Bool) $ TermO $
- \c -> a c `elem` ta c
- Token_Term_Foldable_null tok_ta -> ta2ty_from tok_ta null
- Token_Term_Foldable_length tok_ta -> ta2ty_from tok_ta length
- Token_Term_Foldable_minimum tok_ta -> ta2a_from tok_ta (ty @Ord) minimum
- Token_Term_Foldable_maximum tok_ta -> ta2a_from tok_ta (ty @Ord) maximum
- Token_Term_Foldable_sum tok_ta -> ta2a_from tok_ta (ty @Num) sum
- Token_Term_Foldable_product tok_ta -> ta2a_from tok_ta (ty @Num) product
- Token_Term_Foldable_toList tok_ta ->
- -- toList :: Foldable t => t a -> [a]
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- k (ty @[] :$ ty_ta_a) $ TermO $
- \c -> toList (ta c)
- Token_Term_Foldable_all tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta all
- Token_Term_Foldable_any tok_a2Bool tok_ta -> allany_from tok_a2Bool tok_ta any
- Token_Term_Foldable_and tok_tBool -> andor_from tok_tBool and
- Token_Term_Foldable_or tok_tBool -> andor_from tok_tBool or
- Token_Term_Foldable_concat tok_tla ->
- -- concat :: Foldable t => t [a] -> [a]
- compileO tok_tla ctx $ \ty_tla (TermO tla) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_tla) ty_tla) $ \Refl TyCon _ty_tla_t ty_tla_la ->
- check_TyEq1 (ty @[]) (At (Just tok_tla) ty_tla_la) $ \Refl ty_tla_la_a ->
- k (ty @[] :$ ty_tla_la_a) $ TermO $
- \c -> concat (tla c)
- where
- foldr_from tok_a2b2b tok_b tok_ta
- (fold::forall term f a b.
- (Sym_Foldable term, Foldable f)
- => term (a -> b -> b) -> term b -> term (f a) -> term b) =
- -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
- -- foldr' :: Foldable t => (a -> b -> b) -> b -> t a -> b
- compileO tok_a2b2b ctx $ \ty_a2b2b (TermO a2b2b) ->
- compileO tok_b ctx $ \ty_b (TermO b) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b) $ \Refl ty_a2b2b_a ty_a2b2b_b2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2b2b) ty_a2b2b_b2b) $ \Refl ty_a2b2b_b2b_b0 ty_a2b2b_b2b_b1 ->
- check_TyEq
- (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
- (At (Just tok_a2b2b) ty_a2b2b_b2b_b1) $ \Refl ->
- check_TyEq
- (At (Just tok_a2b2b) ty_a2b2b_b2b_b0)
- (At (Just tok_b) ty_b) $ \Refl ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyEq
- (At (Just tok_a2b2b) ty_a2b2b_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- k ty_b $ TermO $
- \c -> fold (a2b2b c) (b c) (ta c)
- foldl_from tok_b2a2b tok_b tok_ta
- (fold::forall term f a b.
- (Sym_Foldable term, Foldable f)
- => term (b -> a -> b) -> term b -> term (f a) -> term b) =
- -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
- compileO tok_b2a2b ctx $ \ty_b2a2b (TermO b2a2b) ->
- compileO tok_b ctx $ \ty_b (TermO b) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyEq2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b) $ \Refl ty_b2a2b_b ty_b2a2b_a2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_b2a2b) ty_b2a2b_a2b) $ \Refl ty_b2a2b_a2b_a ty_b2a2b_a2b_b ->
- check_TyEq
- (At (Just tok_b2a2b) ty_b2a2b_b)
- (At (Just tok_b2a2b) ty_b2a2b_a2b_b) $ \Refl ->
- check_TyEq
- (At (Just tok_b2a2b) ty_b2a2b_b)
- (At (Just tok_b) ty_b) $ \Refl ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyEq
- (At (Just tok_b2a2b) ty_b2a2b_a2b_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- k ty_b $ TermO $
- \c -> fold (b2a2b c) (b c) (ta c)
- ta2ty_from
- :: forall typ. Inj_TyConst (TyConsts_of_Ifaces is) typ
- => EToken meta is
- -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ)
- -> Either (Error_Term meta is) ret
- ta2ty_from tok_ta f =
- -- length :: Foldable t => t a -> Int
- -- null :: Foldable t => t a -> Bool
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t _ty_ta_a ->
- k (TyConst inj_TyConst::Type (TyConsts_of_Ifaces is) typ) $ TermO $
- \c -> f (ta c)
- ta2a_from
- :: forall con.
- EToken meta is
- -> Type (TyConsts_of_Ifaces is) con
- -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
- -> Either (Error_Term meta is) ret
- ta2a_from tok_ta q f =
- -- minimum :: (Foldable t, Ord a) => t a -> a
- -- maximum :: (Foldable t, Ord a) => t a -> a
- -- sum :: (Foldable t, Num a) => t a -> a
- -- product :: (Foldable t, Num a) => t a -> a
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyCon (At (Just tok_ta) (q :$ ty_ta_a)) $ \TyCon ->
- k ty_ta_a $ TermO $
- \c -> f (ta c)
- allany_from tok_a2Bool tok_ta
- (g::forall term f a.
- (Sym_Foldable term, Foldable f)
- => term (a -> Bool) -> term (f a) -> term Bool) =
- -- all :: Foldable t => (a -> Bool) -> t a -> Bool
- -- any :: Foldable t => (a -> Bool) -> t a -> Bool
- compileO tok_a2Bool ctx $ \ty_a2Bool (TermO a2Bool) ->
- compileO tok_ta ctx $ \ty_ta (TermO ta) ->
- check_TyEq2 (ty @(->)) (At (Just tok_a2Bool) ty_a2Bool) $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
- check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
- check_TyEq
- (At (Just tok_a2Bool) ty_a2Bool_a)
- (At (Just tok_ta) ty_ta_a) $ \Refl ->
- check_TyEq
- (At Nothing (ty @Bool))
- (At (Just tok_a2Bool) ty_a2Bool_Bool) $ \Refl ->
- k (ty @Bool) $ TermO $
- \c -> g (a2Bool c) (ta c)
- andor_from tok_tBool
- (g::forall term f.
- (Sym_Foldable term, Foldable f)
- => term (f Bool) -> term Bool) =
- -- and :: Foldable t => t Bool -> Bool
- -- or :: Foldable t => t Bool -> Bool
- compileO tok_tBool ctx $ \ty_tBool (TermO tBool) ->
- check_TyCon1 (ty @Foldable) (At (Just tok_tBool) ty_tBool) $ \Refl TyCon _ty_tBool_t ty_tBool_Bool ->
- check_TyEq
- (At Nothing (ty @Bool))
- (At (Just tok_tBool) ty_tBool_Bool) $ \Refl ->
- k (ty @Bool) $ TermO $
- \c -> g (tBool c)
-instance -- TokenizeT
- Inj_Token meta ts Foldable =>
- TokenizeT meta ts (Proxy Foldable) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod []
- [ tokenize2 "foldMap" infixN5 Token_Term_Foldable_foldMap
- , tokenize3 "foldr" infixN5 Token_Term_Foldable_foldr
- , tokenize3 "foldr'" infixN5 Token_Term_Foldable_foldr'
- , tokenize3 "foldl" infixN5 Token_Term_Foldable_foldl
- , tokenize2 "elem" (infixN 4) Token_Term_Foldable_elem
- , tokenize1 "sum" infixN5 Token_Term_Foldable_sum
- , tokenize1 "product" infixN5 Token_Term_Foldable_product
- , tokenize1 "toList" infixN5 Token_Term_Foldable_toList
- , tokenize2 "all" infixN5 Token_Term_Foldable_all
- , tokenize2 "any" infixN5 Token_Term_Foldable_any
- , tokenize1 "and" infixN5 Token_Term_Foldable_and
- , tokenize1 "or" infixN5 Token_Term_Foldable_or
- , tokenize1 "concat" infixN5 Token_Term_Foldable_concat
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Foldable) g
+-- ** 'Type's
+tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)
+tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a
+
+t0 :: Source src => LenInj vs => KindInj (K t) =>
+ Type src (Proxy t ': vs) t
+t0 = tyVar "t" $ varZ
+
+t1 :: Source src => LenInj vs => KindInj (K t) =>
+ Type src (a ': Proxy t ': vs) t
+t1 = tyVar "t" $ VarS varZ
+
+t2 :: Source src => LenInj vs => KindInj (K t) =>
+ Type src (a ': b ': Proxy t ': vs) t
+t2 = tyVar "t" $ VarS $ VarS varZ
+
+-- ** 'Term's
+teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))
+teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap
+ where
+ m :: Source src => LenInj vs => KindInj (K m) =>
+ Type src (a ': b ': Proxy m ': vs) m
+ m = tyVar "m" $ VarS $ VarS varZ
+
+teFoldable_elem :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Eq a #> (a -> t a -> Bool))
+teFoldable_elem = Term (tyFoldable t1 # tyEq a0) (a0 ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 elem
+
+teFoldable_toList :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> [a]))
+teFoldable_toList = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyList a0) $ teSym @Foldable $ lam1 toList
+
+teFoldable_concat :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t [a] -> [a]))
+teFoldable_concat = Term (tyFoldable t1) (t1 `tyApp` (tyList a0) ~> tyList a0) $ teSym @Foldable $ lam1 concat
+
+teFoldable_foldr, teFoldable_foldr' :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((a -> b -> b) -> b -> t a -> b))
+teFoldable_foldr = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr
+
+teFoldable_foldr' = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr'
+
+teFoldable_foldl :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((b -> a -> b) -> b -> t a -> b))
+teFoldable_foldl = Term (tyFoldable t2) ((b1 ~> a0 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldl
+
+teFoldable_length :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Int))
+teFoldable_length = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyInt) $ teSym @Foldable $ lam1 length
+
+teFoldable_null :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Bool))
+teFoldable_null = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam1 null
+
+teFoldable_minimum, teFoldable_maximum :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Ord a #> (t a -> a))
+teFoldable_minimum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 minimum
+teFoldable_maximum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 maximum
+
+teFoldable_sum, teFoldable_product :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Num a #> (t a -> a))
+teFoldable_sum = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 sum
+teFoldable_product = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 product
+
+teFoldable_all, teFoldable_any :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> ((a -> Bool) -> t a -> Bool))
+teFoldable_all = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 all
+teFoldable_any = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 any
+
+teFoldable_and, teFoldable_or :: TermDef Foldable '[Proxy t] (Foldable t #> (t Bool -> Bool))
+teFoldable_and = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 and
+teFoldable_or = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 or
+
+teFoldable_asum :: TermDef Foldable '[Proxy a, Proxy t, Proxy f] ((Foldable t # Alternative f) #> (t (f a) -> f a))
+teFoldable_asum = Term (tyFoldable t1 # tyAlternative f2) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $ teSym @Foldable $ lam1 asum
+
+{- TODO: when MonadPlus will be supported
+teFoldable_msum ::
+ Source src => SymInj ss Foldable =>
+ Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))
+teFoldable_msum =
+ Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
+ teSym @Foldable $ lam1 msum
+-}
sourcephile / git / haskell / symantic.git / blobdiff