{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Foldable'.
module Language.Symantic.Lib.Foldable where

import Control.Monad (liftM, liftM2, liftM3)
import Data.Foldable (Foldable)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Foldable as Foldable
import Prelude hiding (Foldable(..)
 , all, and, any, concat, concatMap
 , mapM_, notElem, or, sequence, sequence_)

import Language.Symantic.Parsing hiding (any)
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming

-- * Class '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; 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 t, GHC.Base.Alternative f) => t (f a) -> f a
	-- msum :: (Foldable t, GHC.Base.MonadPlus m) => t (m a) -> m 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 ())
	
	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_

type instance Sym_of_Iface (Proxy Foldable) = Sym_Foldable
type instance TyConsts_of_Iface (Proxy Foldable) = Proxy Foldable ': TyConsts_imported_by (Proxy Foldable)
type instance TyConsts_imported_by (Proxy Foldable) = '[]

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 @Sym_Foldable foldMap
	foldr      = dupI3 @Sym_Foldable foldr
	foldr'     = dupI3 @Sym_Foldable foldr'
	foldl      = dupI3 @Sym_Foldable foldl
	foldl'     = dupI3 @Sym_Foldable foldl'
	null       = dupI1 @Sym_Foldable null
	length     = dupI1 @Sym_Foldable length
	minimum    = dupI1 @Sym_Foldable minimum
	maximum    = dupI1 @Sym_Foldable maximum
	elem       = dupI2 @Sym_Foldable elem
	sum        = dupI1 @Sym_Foldable sum
	product    = dupI1 @Sym_Foldable product
	toList     = dupI1 @Sym_Foldable toList
	all        = dupI2 @Sym_Foldable all
	and        = dupI1 @Sym_Foldable and
	any        = dupI2 @Sym_Foldable any
	concat     = dupI1 @Sym_Foldable concat
	concatMap  = dupI2 @Sym_Foldable concatMap
	find       = dupI2 @Sym_Foldable find
	foldlM     = dupI3 @Sym_Foldable foldlM
	foldrM     = dupI3 @Sym_Foldable foldrM
	forM_      = dupI2 @Sym_Foldable forM_
	for_       = dupI2 @Sym_Foldable for_
	mapM_      = dupI2 @Sym_Foldable mapM_
	maximumBy  = dupI2 @Sym_Foldable maximumBy
	minimumBy  = dupI2 @Sym_Foldable minimumBy
	notElem    = dupI2 @Sym_Foldable notElem
	or         = dupI1 @Sym_Foldable or
	sequenceA_ = dupI1 @Sym_Foldable sequenceA_
	sequence_  = dupI1 @Sym_Foldable sequence_
	traverse_  = dupI2 @Sym_Foldable traverse_

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

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 cs Foldable
 , Inj_TyConst cs Monoid
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Int
 , Inj_TyConst cs Bool
 , Inj_TyConst cs Eq
 , Inj_TyConst cs Ord
 , Inj_TyConst cs Num
 , Inj_TyConst cs []
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Foldable) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy Foldable)
	 -> Compiler meta ctx ret cs 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
			compile tok_a2m ctx $ \ty_a2m (Term a2m) ->
			compile tok_ta  ctx $ \ty_ta  (Term 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 $ Term $
			 \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
			compile tok_a  ctx $ \ty_a  (Term a) ->
			compile tok_ta ctx $ \ty_ta (Term 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) $ Term $
			 \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]
			compile tok_ta ctx $ \ty_ta (Term ta) ->
			check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t ty_ta_a ->
			k (ty @[] :$ ty_ta_a) $ Term $
			 \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]
			compile tok_tla ctx $ \ty_tla (Term 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) $ Term $
			 \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
			compile tok_a2b2b ctx $ \ty_a2b2b (Term a2b2b) ->
			compile tok_b     ctx $ \ty_b     (Term b) ->
			compile tok_ta    ctx $ \ty_ta    (Term 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 $ Term $
			 \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
			compile tok_b2a2b ctx $ \ty_b2a2b (Term b2a2b) ->
			compile tok_b     ctx $ \ty_b     (Term b) ->
			compile tok_ta    ctx $ \ty_ta    (Term 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 $ Term $
			 \c -> fold (b2a2b c) (b c) (ta c)
		ta2ty_from
		 :: forall typ. Inj_TyConst cs typ
		 => EToken meta is
		 -> (forall term t a. (Sym_Foldable term, Foldable t) => term (t a) -> term typ)
		 -> Either (Error_Term meta cs is) ret
		ta2ty_from tok_ta f =
		 -- length :: Foldable t => t a -> Int
		 -- null   :: Foldable t => t a -> Bool
			compile tok_ta ctx $ \ty_ta (Term ta) ->
			check_TyCon1 (ty @Foldable) (At (Just tok_ta) ty_ta) $ \Refl TyCon _ty_ta_t _ty_ta_a ->
			k (TyConst inj_TyConst::Type cs typ) $ Term $
			 \c -> f (ta c)
		ta2a_from
		 :: forall con.
		    EToken meta is
		 -> Type cs con
		 -> (forall term t a. (Sym_Foldable term, Foldable t, con a) => term (t a) -> term a)
		 -> Either (Error_Term meta cs 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
			compile tok_ta ctx $ \ty_ta (Term 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 $ Term $
			 \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
			compile tok_a2Bool ctx $ \ty_a2Bool (Term a2Bool) ->
			compile tok_ta ctx $ \ty_ta (Term 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) $ Term $
			 \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
			compile tok_tBool ctx $ \ty_tBool (Term 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) $ Term $
			 \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