{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Foldable'.
module Language.Symantic.Expr.Foldable where

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

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.List
import Language.Symantic.Trans.Common

-- * Class 'Sym_Foldable'
-- | Symantic.
class Sym_Foldable repr where
	foldMap    :: (Foldable f, Monoid m) => repr (a -> m) -> repr (f a) -> repr m
	foldr      :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
	foldr'     :: Foldable f => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b
	foldl      :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
	foldl'     :: Foldable f => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b
	length     :: Foldable f => repr (f a) -> repr Int
	null       :: Foldable f => repr (f a) -> repr Bool
	minimum    :: (Foldable f, Ord a) => repr (f a) -> repr a
	maximum    :: (Foldable f, Ord a) => repr (f a) -> repr a
	elem       :: (Foldable f, Eq  a) => repr a -> repr (f a) -> repr Bool
	sum        :: (Foldable f, Num a) => repr (f a) -> repr a
	product    :: (Foldable f, Num a) => repr (f a) -> repr a
	toList     :: Foldable f => repr (f a) -> repr [a]
	all        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
	and        :: Foldable f => repr (f Bool) -> repr Bool
	any        :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr Bool
	concat     :: Foldable f => repr (f [a]) -> repr [a]
	concatMap  :: Foldable f => repr (a -> [b]) -> repr (f a) -> repr [b]
	find       :: Foldable f => repr (a -> Bool) -> repr (f a) -> repr (Maybe a)
	foldlM     :: (Foldable f, Monad m) => repr (b -> a -> m b) -> repr b -> repr (f a) -> repr (m b)
	foldrM     :: (Foldable f, Monad m) => repr (a -> b -> m b) -> repr b -> repr (f a) -> repr (m b)
	forM_      :: (Foldable f, Monad m) => repr (f a) -> repr (a -> m b) -> repr (m ())
	for_       :: (Foldable f, Applicative p) => repr (f a) -> repr (a -> p b) -> repr (p ())
	mapM_      :: (Foldable f, Monad m) => repr (a -> m b) -> repr (f a) -> repr (m ())
	maximumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
	minimumBy  :: Foldable f => repr (a -> a -> Ordering) -> repr (f a) -> repr a
	notElem    :: (Foldable f, Eq a) => repr a -> repr (f a) -> repr Bool
	or         :: Foldable f => repr (f Bool) -> repr Bool
	sequenceA_ :: (Foldable f, Applicative p) => repr (f (p a)) -> repr (p ())
	sequence_  :: (Foldable f, Monad m) => repr (f (m a)) -> repr (m ())
	traverse_  :: (Foldable f, Applicative p) => repr (a -> p b) -> repr (f a) -> repr (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 repr, Foldable f, Monoid m) => t repr (a -> m) -> t repr (f a) -> t repr m
	default foldr      :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldr'     :: (Trans t repr, Foldable f) => t repr (a -> b -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldl      :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
	default foldl'     :: (Trans t repr, Foldable f) => t repr (b -> a -> b) -> t repr b -> t repr (f a) -> t repr b
	default length     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Int
	default null       :: (Trans t repr, Foldable f) => t repr (f a) -> t repr Bool
	default minimum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
	default maximum    :: (Trans t repr, Foldable f, Ord a) => t repr (f a) -> t repr a
	default elem       :: (Trans t repr, Foldable f, Eq  a) => t repr a -> t repr (f a) -> t repr Bool
	default sum        :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
	default product    :: (Trans t repr, Foldable f, Num a) => t repr (f a) -> t repr a
	default toList     :: (Trans t repr, Foldable f) => t repr (f a) -> t repr [a]
	default all        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
	default and        :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
	default any        :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr Bool
	default concat     :: (Trans t repr, Foldable f) => t repr (f [a]) -> t repr [a]
	default concatMap  :: (Trans t repr, Foldable f) => t repr (a -> [b]) -> t repr (f a) -> t repr [b]
	default find       :: (Trans t repr, Foldable f) => t repr (a -> Bool) -> t repr (f a) -> t repr (Maybe a)
	default foldlM     :: (Trans t repr, Foldable f, Monad m) => t repr (b -> a -> m b) -> t repr b -> t repr (f a) -> t repr (m b)
	default foldrM     :: (Trans t repr, Foldable f, Monad m) => t repr (a -> b -> m b) -> t repr b -> t repr (f a) -> t repr (m b)
	default forM_      :: (Trans t repr, Foldable f, Monad m) => t repr (f a) -> t repr (a -> m b) -> t repr (m ())
	default for_       :: (Trans t repr, Foldable f, Applicative p) => t repr (f a) -> t repr (a -> p b) -> t repr (p ())
	default mapM_      :: (Trans t repr, Foldable f, Monad m) => t repr (a -> m b) -> t repr (f a) -> t repr (m ())
	default maximumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
	default minimumBy  :: (Trans t repr, Foldable f) => t repr (a -> a -> Ordering) -> t repr (f a) -> t repr a
	default notElem    :: (Trans t repr, Foldable f, Eq a) => t repr a -> t repr (f a) -> t repr Bool
	default or         :: (Trans t repr, Foldable f) => t repr (f Bool) -> t repr Bool
	default sequenceA_ :: (Trans t repr, Foldable f, Applicative p) => t repr (f (p a)) -> t repr (p ())
	default sequence_  :: (Trans t repr, Foldable f, Monad m) => t repr (f (m a)) -> t repr (m ())
	default traverse_  :: (Trans t repr, Foldable f, Applicative p) => t repr (a -> p b) -> t repr (f a) -> t repr (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_
instance Sym_Foldable Repr_Host 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 Repr_Text where
	foldMap    = repr_text_app2 "foldMap"
	foldr      = repr_text_app3 "foldr"
	foldr'     = repr_text_app3 "foldr'"
	foldl      = repr_text_app3 "foldl"
	foldl'     = repr_text_app3 "foldl'"
	null       = repr_text_app1 "null"
	length     = repr_text_app1 "length"
	minimum    = repr_text_app1 "minimum"
	maximum    = repr_text_app1 "maximum"
	elem       = repr_text_app2 "elem"
	sum        = repr_text_app1 "sum"
	product    = repr_text_app1 "product"
	toList     = repr_text_app1 "toList"
	all        = repr_text_app2 "all"
	and        = repr_text_app1 "and"
	any        = repr_text_app2 "any"
	concat     = repr_text_app1 "concat"
	concatMap  = repr_text_app2 "concatMap"
	find       = repr_text_app2 "find"
	foldlM     = repr_text_app3 "foldlM"
	foldrM     = repr_text_app3 "foldrM"
	forM_      = repr_text_app2 "forM_"
	for_       = repr_text_app2 "for_"
	mapM_      = repr_text_app2 "mapM_"
	maximumBy  = repr_text_app2 "maximumBy"
	minimumBy  = repr_text_app2 "minimumBy"
	notElem    = repr_text_app2 "notElem"
	or         = repr_text_app1 "or"
	sequenceA_ = repr_text_app1 "sequenceA_"
	sequence_  = repr_text_app1 "sequence_"
	traverse_  = repr_text_app2 "traverse_"
instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Repr_Dup r1 r2) where
	foldMap    = repr_dup2 sym_Foldable foldMap
	foldr      = repr_dup3 sym_Foldable foldr
	foldr'     = repr_dup3 sym_Foldable foldr'
	foldl      = repr_dup3 sym_Foldable foldl
	foldl'     = repr_dup3 sym_Foldable foldl'
	null       = repr_dup1 sym_Foldable null
	length     = repr_dup1 sym_Foldable length
	minimum    = repr_dup1 sym_Foldable minimum
	maximum    = repr_dup1 sym_Foldable maximum
	elem       = repr_dup2 sym_Foldable elem
	sum        = repr_dup1 sym_Foldable sum
	product    = repr_dup1 sym_Foldable product
	toList     = repr_dup1 sym_Foldable toList
	all        = repr_dup2 sym_Foldable all
	and        = repr_dup1 sym_Foldable and
	any        = repr_dup2 sym_Foldable any
	concat     = repr_dup1 sym_Foldable concat
	concatMap  = repr_dup2 sym_Foldable concatMap
	find       = repr_dup2 sym_Foldable find
	foldlM     = repr_dup3 sym_Foldable foldlM
	foldrM     = repr_dup3 sym_Foldable foldrM
	forM_      = repr_dup2 sym_Foldable forM_
	for_       = repr_dup2 sym_Foldable for_
	mapM_      = repr_dup2 sym_Foldable mapM_
	maximumBy  = repr_dup2 sym_Foldable maximumBy
	minimumBy  = repr_dup2 sym_Foldable minimumBy
	notElem    = repr_dup2 sym_Foldable notElem
	or         = repr_dup1 sym_Foldable or
	sequenceA_ = repr_dup1 sym_Foldable sequenceA_
	sequence_  = repr_dup1 sym_Foldable sequence_
	traverse_  = repr_dup2 sym_Foldable traverse_

sym_Foldable :: Proxy Sym_Foldable
sym_Foldable = Proxy

-- * Type 'Expr_Foldable'
-- | Expression.
data Expr_Foldable (root:: *)
type instance Root_of_Expr      (Expr_Foldable root)      = root
type instance Type_of_Expr      (Expr_Foldable root)      = No_Type
type instance Sym_of_Expr       (Expr_Foldable root) repr = Sym_Foldable repr
type instance Error_of_Expr ast (Expr_Foldable root)      = No_Error_Expr

-- | Parse 'foldMap'.
foldMap_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type0_Constraint Monoid   ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
foldMap_from ast_f ast_ta ex ast ctx k =
 -- foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_m) ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Monoid) ast ty_f_m $ \Dict ->
	k ty_f_m $ Forall_Repr_with_Context $
	 \c -> foldMap (f c) (ta c)

-- | Parse 'foldr' or |foldr'|.
foldr_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (a -> b -> b) -> repr b -> repr (f a) -> repr b)
 -> ast -> ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
foldr_from fold ast_f ast_b ast_ta ex ast ctx k =
 -- foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
	check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
	check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
	check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> fold (f c) (b c) (ta c)

-- | Parse 'foldl' or |foldl'|.
foldl_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Fun (Type_of_Expr root)
 , Type0_Unlift Type_Fun (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => (forall repr f a b. (Sym_Foldable repr, Foldable f) => repr (b -> a -> b) -> repr b -> repr (f a) -> repr b)
 -> ast -> ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
foldl_from fold ast_f ast_b ast_ta ex ast ctx k =
 -- foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_b ty_f_a2b) ->
	check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b') ->
	check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
	check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _t (ty_t_a::ty h_t_a), Type1_Lift _ty_t) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> fold (f c) (b c) (ta c)

-- | Parse 'length'.
length_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Int (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
length_from ast_ta ex ast ctx k =
 -- length :: Foldable t => t a -> Int
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1{}, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_int $ Forall_Repr_with_Context $
	 \c -> length (ta c)

-- | Parse 'null'.
null_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
null_from ast_ta ex ast ctx k =
 -- null :: Foldable t => t a -> Bool
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1{}, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> null (ta c)

-- | Parse 'minimum'.
minimum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Ord      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
minimum_from ast_ta ex ast ctx k =
 -- minimum :: (Foldable t, Ord a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> minimum (ta c)

-- | Parse 'maximum'.
maximum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Ord      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
maximum_from ast_ta ex ast ctx k =
 -- maximum :: (Foldable t, Ord a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Ord) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> maximum (ta c)

-- | Parse 'elem'.
elem_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint  Eq       ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
elem_from ast_a ast_ta ex ast ctx k =
 -- elem :: (Foldable t, Eq a) => a -> t a -> Bool
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast ty_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Eq) ast ty_a $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> a c `elem` ta c

-- | Parse 'sum'.
sum_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
sum_from ast_ta ex ast ctx k =
 -- sum :: (Foldable t, Num a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> sum (ta c)

-- | Parse 'product'.
product_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
product_from ast_ta ex ast ctx k =
 -- product :: (Foldable t, Num a) => t a -> a
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	check_type0_constraint ex (Proxy::Proxy Num) ast ty_t_a $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> product (ta c)

-- | Parse 'toList'.
toList_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_List (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
toList_from ast_ta ex ast ctx k =
 -- toList :: Foldable t => t a -> [a]
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k (type_list ty_t_a) $ Forall_Repr_with_Context $
	 \c -> toList (ta c)

-- | Parse 'all'.
all_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Bool (Type_of_Expr root)
 , Type0_Lift   Type_Fun  (Type_of_Expr root)
 , Type0_Unlift Type_Fun  (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
all_from ast_f ast_ta ex ast ctx k =
 -- all :: Foldable t => (a -> Bool) -> t a -> Bool
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
	check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> all (f c) (ta c)

-- | Parse 'any'.
any_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_Bool (Type_of_Expr root)
 , Type0_Lift   Type_Fun  (Type_of_Expr root)
 , Type0_Unlift Type_Fun  (Type_of_Expr root)
 , Type0_Constraint Num      ty
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
any_from ast_f ast_ta ex ast ctx k =
 -- any :: Foldable t => (a -> Bool) -> t a -> Bool
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_a ty_f_b) ->
	check_type0_eq ex ast type_bool ty_f_b $ \Refl ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast ty_f_a ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> any (f c) (ta c)

-- | Parse 'and'.
and_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
and_from ast_ta ex ast ctx k =
 -- and :: Foldable t => t Bool -> Bool
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast type_bool ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> and (ta c)

-- | Parse 'or'.
or_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift Type_Bool (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
or_from ast_ta ex ast ctx k =
 -- or :: Foldable t => t Bool -> Bool
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type0_eq ex ast type_bool ty_t_a $ \Refl ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> or (ta c)

-- | Parse 'concat'.
concat_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Foldable root)
 , Expr_From ast root
 , Type0_Eq ty
 , Type0_Lift   Type_List (Type_of_Expr root)
 , Type0_Unlift Type_List (Type_of_Expr root)
 , Type1_Constraint Foldable ty
 , Type1_Unlift (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_Foldable root) hs ret
concat_from ast_ta ex ast ctx k =
 -- concat :: Foldable t => t [a] -> [a]
	expr_from (Proxy::Proxy root) ast_ta ctx $
	 \(ty_ta::ty h_ta) (Forall_Repr_with_Context ta) ->
	check_type1 ex ast ty_ta $ \(Type1 _ ty_t_a, _) ->
	check_type_list ex ast ty_t_a $ \Type1{} ->
	check_type1_constraint ex (Proxy::Proxy Foldable) ast ty_ta $ \Dict ->
	k ty_t_a $ Forall_Repr_with_Context $
	 \c -> concat (ta c)