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

import Control.Monad (liftM, liftM2, liftM3)
import Data.MonoTraversable (MonoFoldable)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.MonoTraversable as MT

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.MonoFunctor

-- * Class 'Sym_MonoFoldable'
class Sym_MonoFunctor term => 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 :: (Trans t term, MonoFoldable o, Monoid m)
	 => t term (MT.Element o -> m) -> t term o -> t term m
	default ofoldr :: (Trans t term, MonoFoldable o)
	 => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
	default ofoldl' :: (Trans t term, MonoFoldable o)
	 => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
	default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
	default onull   :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
	default oall    :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
	default oany    :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
	default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
	ofoldMap = trans_map2 ofoldMap
	ofoldr   = trans_map3 ofoldr
	ofoldl'  = trans_map3 ofoldl'
	olength  = trans_map1 olength
	onull    = trans_map1 onull
	oall     = trans_map2 oall
	oany     = trans_map2 oany
	otoList  = trans_map1 otoList

type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
type instance TyConsts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': TyConsts_imported_by (Proxy MonoFoldable)
type instance TyConsts_imported_by (Proxy MonoFoldable) =
 [ Proxy (->)
 , Proxy Bool
 , Proxy Int
 , Proxy Monoid
 ]

instance Sym_MonoFoldable HostI where
	ofoldMap = liftM2 MT.ofoldMap
	ofoldr   = liftM3 MT.ofoldr
	ofoldl'  = liftM3 MT.ofoldl'
	olength  = liftM  MT.olength
	onull    = liftM  MT.onull
	oall     = liftM2 MT.oall
	oany     = liftM2 MT.oany
	otoList  = liftM  MT.otoList
instance Sym_MonoFoldable TextI where
	ofoldMap = textI2 "ofoldMap"
	ofoldr   = textI3 "ofoldr"
	ofoldl'  = textI3 "ofoldl'"
	olength  = textI1 "olength"
	onull    = textI1 "onull"
	oall     = textI2 "oall"
	oany     = textI2 "oany"
	otoList  = textI1 "otoList"
instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
	ofoldMap = dupI2 @Sym_MonoFoldable ofoldMap
	ofoldr   = dupI3 @Sym_MonoFoldable ofoldr
	ofoldl'  = dupI3 @Sym_MonoFoldable ofoldl'
	olength  = dupI1 @Sym_MonoFoldable olength
	onull    = dupI1 @Sym_MonoFoldable onull
	oall     = dupI2 @Sym_MonoFoldable oall
	oany     = dupI2 @Sym_MonoFoldable oany
	otoList  = dupI1 @Sym_MonoFoldable otoList

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs MonoFoldable
 ) => Read_TyNameR TyName cs (Proxy MonoFoldable ': rs) where
	read_TyNameR _cs (TyName "MonoFoldable") k = k (ty @MonoFoldable)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy MonoFoldable ': cs) where
	show_TyConst TyConstZ{} = "MonoFoldable"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy MonoFoldable)

data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
 = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
 | Token_Term_MonoFoldable_ofoldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 | Token_Term_MonoFoldable_ofoldl'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 | Token_Term_MonoFoldable_olength  (EToken meta ts)
 | Token_Term_MonoFoldable_onull    (EToken meta ts)
 | Token_Term_MonoFoldable_oall     (EToken meta ts) (EToken meta ts)
 | Token_Term_MonoFoldable_oany     (EToken meta ts) (EToken meta ts)
 | Token_Term_MonoFoldable_otoList  (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
instance -- CompileI
 ( Inj_TyConst cs MonoFoldable
 , Inj_TyConst cs (->)
 , Inj_TyConst cs []
 , Inj_TyConst cs Monoid
 , Inj_TyConst cs Bool
 , Inj_TyConst cs Int
 , Proj_TyCon  cs
 , Proj_TyFam  cs TyFam_MonoElement
 , Compile cs is
 ) => CompileI cs is (Proxy MonoFoldable) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy MonoFoldable)
	 -> CompileT meta ctx ret cs is ls (Proxy MonoFoldable ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
			-- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
			compileO tok_f ctx $ \ty_f (TermO f) ->
			compileO tok_o ctx $ \ty_o (TermO o) ->
			check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
			check_TyCon (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyCon (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \TyCon ->
			check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_TyEq
			 (At Nothing ty_o_e)
			 (At (Just tok_f) ty_f_a) $ \Refl ->
			k ty_m $ TermO $
			 \c -> ofoldMap (f c) (o c)
		 Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
			ofoldr_from tok_e2b2b tok_b tok_o ofoldr
		 Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
			ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
		 Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
		 Token_Term_MonoFoldable_onull   tok_o -> o2ty_from tok_o onull
		 Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
		 Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
		 Token_Term_MonoFoldable_otoList tok_o ->
		 -- otoList :: MonoFoldable o => o -> [MT.Element o]
			compileO tok_o ctx $ \ty_o (TermO o) ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			k (ty @[] :$ ty_o_e) $ TermO $
			 \c -> otoList (o c)
		where
		ofoldr_from tok_e2b2b tok_b tok_o
		 (fold::forall term o b.
			 (Sym_MonoFoldable term, MonoFoldable o)
			 => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
		 -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
			compileO tok_e2b2b ctx $ \ty_e2b2b (TermO e2b2b) ->
			compileO tok_b     ctx $ \ty_b     (TermO b) ->
			compileO tok_o     ctx $ \ty_o     (TermO o) ->
			check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
			check_TyEq2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
			check_TyEq
			 (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
			 (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
			check_TyEq
			 (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
			 (At (Just tok_b) ty_b) $ \Refl ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_TyEq
			 (At (Just tok_e2b2b) ty_e2b2b_e)
			 (At (Just tok_o) ty_o_e) $ \Refl ->
			k ty_b $ TermO $
			 \c -> fold (e2b2b c) (b c) (o c)
		ofoldl_from tok_b2e2b tok_b tok_o
		 (fold::forall term o b.
			 (Sym_MonoFoldable term, MonoFoldable o)
			 => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
			-- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
			compileO tok_b2e2b ctx $ \ty_b2e2b (TermO b2e2b) ->
			compileO tok_b     ctx $ \ty_b     (TermO b) ->
			compileO tok_o     ctx $ \ty_o     (TermO o) ->
			check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
			check_TyEq2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
			check_TyEq
			 (At (Just tok_b2e2b) ty_b2e2b_b)
			 (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
			check_TyEq
			 (At (Just tok_b2e2b) ty_b2e2b_b)
			 (At (Just tok_b) ty_b) $ \Refl ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_TyEq
			 (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
			 (At (Just tok_o) ty_o_e) $ \Refl ->
			k ty_b $ TermO $
			 \c -> fold (b2e2b c) (b c) (o c)
		o2ty_from
		 :: forall typ. Inj_TyConst cs typ
		 => EToken meta is
		 -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
		 -> Either (Error_Term meta cs is) ret
		o2ty_from tok_o f =
			-- olength :: MonoFoldable o => o -> Int
			-- onull   :: MonoFoldable o => o -> Bool
			compileO tok_o ctx $ \ty_o (TermO o) ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			k (TyConst inj_TyConst::Type cs typ) $ TermO $
			 \c -> f (o c)
		oalloany_from
		 tok_e2Bool tok_o
		 (g::forall term o.
			 (Sym_MonoFoldable term, MonoFoldable o)
			 => term (MT.Element o -> Bool) -> term o -> term Bool) =
		 -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
		 -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
			compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
			compileO tok_o ctx $ \ty_o (TermO o) ->
			check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyFam (At (Just tok_o) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_TyEq
			 (At (Just tok_e2Bool) ty_e2Bool_e)
			 (At (Just tok_o) ty_o_e) $ \Refl ->
			check_TyEq
			 (At Nothing (ty @Bool))
			 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			k (ty @Bool) $ TermO $
			 \c -> g (e2Bool c) (o c)
instance -- TokenizeT
 Inj_Token meta ts MonoFoldable =>
 TokenizeT meta ts (Proxy MonoFoldable) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "ofoldMap" infixN5 Token_Term_MonoFoldable_ofoldMap
		 , tokenize3 "ofoldr"   infixN5 Token_Term_MonoFoldable_ofoldr
		 , tokenize3 "ofoldl'"  infixN5 Token_Term_MonoFoldable_ofoldl'
		 , tokenize1 "olength"  infixN5 Token_Term_MonoFoldable_olength
		 , tokenize1 "onull"    infixN5 Token_Term_MonoFoldable_onull
		 , tokenize2 "oall"     infixN5 Token_Term_MonoFoldable_oall
		 , tokenize2 "oany"     infixN5 Token_Term_MonoFoldable_oany
		 , tokenize1 "otoList"  infixN5 Token_Term_MonoFoldable_otoList
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy MonoFoldable) g