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

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