{-# 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 Prelude hiding (Foldable(..)
 , all, and, any, concat, concatMap
 , mapM_, notElem, or, sequence_)

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; 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    :: 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    = 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

-- 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

-- Transforming
instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)

-- Typing
instance NameTyOf Foldable where
	nameTyOf _c = ["Foldable"] `Mod` "Foldable"
instance FixityOf Foldable
instance ClassInstancesFor Foldable
instance TypeInstancesFor Foldable

-- 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
	 ]

-- ** '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
-}