{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
-- | Symantic for 'MonoFoldable'.
module Language.Symantic.Compiling.MonoFoldable where

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

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool (tyBool)
import Language.Symantic.Compiling.List (tyList)
import Language.Symantic.Compiling.MonoFunctor
import Language.Symantic.Compiling.Monoid (tyMonoid)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class '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 :: (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 Consts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': Consts_imported_by MonoFoldable
type instance Consts_imported_by MonoFoldable =
 [ Proxy (->)
 , Proxy (,)
 , Proxy []
 , Proxy Bool
 , Proxy Either
 , Proxy Int
 , Proxy Maybe
 , Proxy Monoid
 , Proxy String
 , Proxy Text
 ]

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 = textI_app2 "ofoldMap"
	ofoldr   = textI_app3 "ofoldr"
	ofoldl'  = textI_app3 "ofoldl'"
	olength  = textI_app1 "olength"
	onull    = textI_app1 "onull"
	oall     = textI_app2 "oall"
	oany     = textI_app2 "oany"
	otoList  = textI_app1 "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 Const_from Text cs => Const_from Text (Proxy MonoFoldable ': cs) where
	const_from "MonoFoldable" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
	show_const ConstZ{} = "MonoFoldable"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs MonoFoldable
 , Proj_Consts cs (Consts_imported_by MonoFoldable)
 ) => Proj_ConC cs (Proxy MonoFoldable) where
	proj_conC _ (TyConst q :$ ty)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy::Proxy MonoFoldable)
	 = case ty of
		 TyConst c
		  | Just Refl <- proj_const c (Proxy::Proxy String) -> Just Con
		  | Just Refl <- proj_const c (Proxy::Proxy Text)   -> Just Con
		 TyConst c :$ _a
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
		  -> case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
			   | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
			 _ -> Nothing
		 TyConst c :$ _a :$ _b
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
		  -> case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
			   | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) []
 , Inj_Const (Consts_of_Ifaces is) Monoid
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) Int
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is ast
 ) => Term_fromI is (Proxy MonoFoldable) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy MonoFoldable ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "ofoldMap" -> ofoldMap_from
		 "ofoldr"   -> ofoldr_from ofoldr
		 "ofoldl'"  -> ofoldl_from ofoldl'
		 "olength"  -> o2ty_from olength
		 "onull"    -> o2ty_from onull
		 "oall"     -> oalloany_from oall
		 "oany"     -> oalloany_from oany
		 "otoList"  -> otoList_from
		 _ -> Left $ Error_Term_unsupported
		where
		ofoldMap_from =
		 -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
			from_ast2 ast $ \ast_f ast_o as ->
			term_from ast_f ctx $ \ty_f (TermLC f) ->
			term_from ast_o ctx $ \ty_o (TermLC o) ->
			check_type2 tyFun ast_f ty_f $ \Refl ty_f_a ty_m ->
			check_constraint (At (Just ast_f) (tyMonoFoldable :$ ty_o)) $ \Con ->
			check_constraint (At (Just ast_f) (tyMonoid :$ ty_m)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type (At Nothing ty_o_e) (At (Just ast_f) ty_f_a) $ \Refl ->
			k as ty_m $ TermLC $
			 \c -> ofoldMap (f c) (o c)
		ofoldr_from
		 (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
			from_ast3 ast $ \ast_e2b2b ast_b ast_o as ->
			term_from ast_e2b2b ctx $ \ty_e2b2b (TermLC e2b2b) ->
			term_from ast_b     ctx $ \ty_b     (TermLC b) ->
			term_from ast_o     ctx $ \ty_o     (TermLC o) ->
			check_type2 tyFun ast_e2b2b ty_e2b2b $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
			check_type2 tyFun ast_e2b2b ty_e2b2b_b2b $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
			check_type (At (Just ast_e2b2b) ty_e2b2b_b2b_b0) (At (Just ast_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
			check_type (At (Just ast_e2b2b) ty_e2b2b_b2b_b0) (At (Just ast_b) ty_b) $ \Refl ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type (At (Just ast_e2b2b) ty_e2b2b_e) (At (Just ast_o) ty_o_e) $ \Refl ->
			k as ty_b $ TermLC $
			 \c -> fold (e2b2b c) (b c) (o c)
		ofoldl_from
		 (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
			from_ast3 ast $ \ast_b2e2b ast_b ast_o as ->
			term_from ast_b2e2b ctx $ \ty_b2e2b (TermLC b2e2b) ->
			term_from ast_b     ctx $ \ty_b     (TermLC b) ->
			term_from ast_o     ctx $ \ty_o     (TermLC o) ->
			check_type2 tyFun ast_b2e2b ty_b2e2b $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
			check_type2 tyFun ast_b2e2b ty_b2e2b_a2b $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
			check_type (At (Just ast_b2e2b) ty_b2e2b_b) (At (Just ast_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
			check_type (At (Just ast_b2e2b) ty_b2e2b_b) (At (Just ast_b) ty_b) $ \Refl ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type (At (Just ast_b2e2b) ty_b2e2b_a2b_e) (At (Just ast_o) ty_o_e) $ \Refl ->
			k as ty_b $ TermLC $
			 \c -> fold (b2e2b c) (b c) (o c)
		o2ty_from
		 :: forall ty. Inj_Const (Consts_of_Ifaces is) ty
		 => (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term ty)
		 -> Either (Error_Term is ast) ret
		o2ty_from f =
		 -- length :: MonoFoldable o => o -> Int
		 -- null   :: MonoFoldable o => o -> Bool
			from_ast1 ast $ \ast_o as ->
			term_from ast_o ctx $ \ty_o (TermLC o) ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			k as (TyConst inj_const::Type (Consts_of_Ifaces is) ty) $ TermLC $
			 \c -> f (o c)
		oalloany_from
		 (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
			from_ast2 ast $ \ast_e2Bool ast_o as ->
			term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
			term_from ast_o ctx $ \ty_o (TermLC o) ->
			check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type (At (Just ast_e2Bool) ty_e2Bool_e) (At (Just ast_o) ty_o_e) $ \Refl ->
			check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			k as tyBool $ TermLC $
			 \c -> g (e2Bool c) (o c)
		otoList_from =
		 -- otoList :: MonoFoldable o => o -> [MT.Element o]
			from_ast1 ast $ \ast_o as ->
			term_from ast_o ctx $ \ty_o (TermLC o) ->
			check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			k as (tyList :$ ty_o_e) $ TermLC $
			 \c -> otoList (o c)

-- | The 'MonoFoldable' 'Type'
tyMonoFoldable :: Inj_Const cs MonoFoldable => Type cs MonoFoldable
tyMonoFoldable = TyConst inj_const

sym_MonoFoldable :: Proxy Sym_MonoFoldable
sym_MonoFoldable = Proxy

syMonoFoldable :: IsString a => [Syntax a] -> Syntax a
syMonoFoldable = Syntax "MonoFoldable"