{-# 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
-}