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

import Data.Bool
import Data.Function (($), (.))
import Data.Monoid (Monoid)
import Data.Int (Int)
import Data.MonoTraversable (MonoFoldable)
import qualified Data.MonoTraversable as MT

import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function ()
import Language.Symantic.Lib.Int (tyInt)
import Language.Symantic.Lib.List (tyList)
import Language.Symantic.Lib.MonoFunctor (famElement, o0, e1)
import Language.Symantic.Lib.Monoid (tyMonoid)

-- * Class 'Sym_MonoFoldable'
type instance Sym MonoFoldable = Sym_MonoFoldable
class Sym_MonoFoldable term where
        ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
        ofoldr   :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
        ofoldl'  :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
        olength  :: MonoFoldable o => term o -> term Int
        onull    :: MonoFoldable o => term o -> term Bool
        oall     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
        oany     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
        otoList  :: MonoFoldable o => term o -> term [MT.Element o]
        default ofoldMap :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => Monoid m => term (MT.Element o -> m) -> term o -> term m
        default ofoldr   :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
        default ofoldl'  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
        default olength  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Int
        default onull    :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term Bool
        default oall     :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
        default oany     :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
        default otoList  :: Sym_MonoFoldable (UnT term) => Trans term => MonoFoldable o => term o -> term [MT.Element o]
        ofoldMap = trans2 ofoldMap
        ofoldr   = trans3 ofoldr
        ofoldl'  = trans3 ofoldl'
        olength  = trans1 olength
        onull    = trans1 onull
        oall     = trans2 oall
        oany     = trans2 oany
        otoList  = trans1 otoList

-- Interpreting
instance Sym_MonoFoldable Eval where
        ofoldMap = eval2 MT.ofoldMap
        ofoldr   = eval3 MT.ofoldr
        ofoldl'  = eval3 MT.ofoldl'
        olength  = eval1 MT.olength
        onull    = eval1 MT.onull
        oall     = eval2 MT.oall
        oany     = eval2 MT.oany
        otoList  = eval1 MT.otoList
instance Sym_MonoFoldable View where
        ofoldMap = view2 "ofoldMap"
        ofoldr   = view3 "ofoldr"
        ofoldl'  = view3 "ofoldl'"
        olength  = view1 "olength"
        onull    = view1 "onull"
        oall     = view2 "oall"
        oany     = view2 "oany"
        otoList  = view1 "otoList"
instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (Dup r1 r2) where
        ofoldMap = dup2 @Sym_MonoFoldable ofoldMap
        ofoldr   = dup3 @Sym_MonoFoldable ofoldr
        ofoldl'  = dup3 @Sym_MonoFoldable ofoldl'
        olength  = dup1 @Sym_MonoFoldable olength
        onull    = dup1 @Sym_MonoFoldable onull
        oall     = dup2 @Sym_MonoFoldable oall
        oany     = dup2 @Sym_MonoFoldable oany
        otoList  = dup1 @Sym_MonoFoldable otoList

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

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

-- Compiling
instance Gram_Term_AtomsFor src ss g MonoFoldable
instance (Source src, SymInj ss MonoFoldable) => ModuleFor src ss MonoFoldable where
        moduleFor = ["MonoFoldable"] `moduleWhere`
         [ "ofoldMap" := teMonoFoldable_ofoldMap
         , "otoList"  := teMonoFoldable_otoList
         , "ofoldr"   := teMonoFoldable_ofoldr
         , "ofoldl'"  := teMonoFoldable_ofoldl'
         , "olength"  := teMonoFoldable_olength
         , "onull"    := teMonoFoldable_onull
         , "oall"     := teMonoFoldable_oall
         , "oany"     := teMonoFoldable_oany
         ]

-- ** 'Type's
tyMonoFoldable :: Source src => Type src vs a -> Type src vs (MonoFoldable a)
tyMonoFoldable a = tyConstLen @(K MonoFoldable) @MonoFoldable (lenVars a) `tyApp` a

-- ** 'Term's
teMonoFoldable_ofoldMap :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy m] (MonoFoldable o # Monoid m # e #~ MT.Element o #> ((e -> m) -> o -> m))
teMonoFoldable_ofoldMap = Term (tyMonoFoldable o0 # tyMonoid m # e1 #~ famElement o0) ((e1 ~> m) ~> o0 ~> m) $ teSym @MonoFoldable $ lam2 ofoldMap
        where
        m :: Source src => LenInj vs => KindInj (K m) => Type src (Proxy a ': Proxy b ': Proxy m ': vs) m
        m = tyVar "m" $ VarS $ VarS varZ

teMonoFoldable_otoList :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> [MT.Element o]))
teMonoFoldable_otoList = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyList (famElement o0)) $ teSym @MonoFoldable $ lam1 otoList

teMonoFoldable_ofoldr :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((e -> a -> a) -> a -> o -> a))
teMonoFoldable_ofoldr = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> a ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldr f
        where
        a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
        a = tyVar "a" $ VarS $ VarS varZ

teMonoFoldable_ofoldl' :: TermDef MonoFoldable '[Proxy o, Proxy e, Proxy a] (MonoFoldable o # e #~ MT.Element o #> ((a -> e -> a) -> a -> o -> a))
teMonoFoldable_ofoldl' = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((a ~> e1 ~> a) ~> a ~> o0 ~> a) $ teSym @MonoFoldable $ lam1 $ \f -> lam $ lam . ofoldl' f
        where
        a :: Source src => LenInj vs => KindInj (K a) => Type src (Proxy _a ': Proxy b ': Proxy a ': vs) a
        a = tyVar "a" $ VarS $ VarS varZ

teMonoFoldable_olength :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (o -> Int))
teMonoFoldable_olength = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (o0 ~> tyInt) $ teSym @MonoFoldable $ lam1 olength

teMonoFoldable_onull :: TermDef MonoFoldable '[Proxy o] (MonoFoldable o #> (o -> Bool))
teMonoFoldable_onull = Term (tyMonoFoldable o0) (o0 ~> tyBool) $ teSym @MonoFoldable $ lam1 onull

teMonoFoldable_oall :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))
teMonoFoldable_oall = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oall

teMonoFoldable_oany :: TermDef MonoFoldable '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> ((e -> Bool) -> o -> Bool))
teMonoFoldable_oany = Term (tyMonoFoldable o0 # e1 #~ famElement o0) ((e1 ~> tyBool) ~> o0 ~> tyBool) $ teSym @MonoFoldable $ lam2 oany