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

import Control.Monad (liftM2)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (traverse)
import qualified Data.Traversable as Traversable

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Applicative (Sym_Applicative)

-- * Class 'Sym_Traversable'
class Sym_Applicative term => Sym_Traversable term where
	traverse :: (Traversable t, Applicative f)
	 => term (a -> f b) -> term (t a) -> term (f (t b))
	default traverse :: (Trans tr term, Traversable t, Applicative f)
	 => tr term (a -> f b) -> tr term (t a) -> tr term (f (t b))
	traverse = trans_map2 traverse

type instance Sym_of_Iface (Proxy Traversable) = Sym_Traversable
type instance TyConsts_of_Iface (Proxy Traversable) = Proxy Traversable ': TyConsts_imported_by (Proxy Traversable)
type instance TyConsts_imported_by (Proxy Traversable) = '[ Proxy Applicative ]

instance Sym_Traversable HostI where
	traverse = liftM2 Traversable.traverse
instance Sym_Traversable TextI where
	traverse = textI2 "traverse"
instance (Sym_Traversable r1, Sym_Traversable r2) => Sym_Traversable (DupI r1 r2) where
	traverse = dupI2 @Sym_Traversable traverse

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

instance Proj_TyConC cs (Proxy Traversable)
data instance TokenT meta (ts::[*]) (Proxy Traversable)
 = Token_Term_Traversable_traverse (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Traversable))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Traversable))

instance -- CompileI
 ( Inj_TyConst cs Traversable
 , Inj_TyConst cs (->)
 , Inj_TyConsts cs (TyConsts_imported_by (Proxy Traversable))
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Traversable) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Traversable_traverse tok_a2fb tok_ta ->
			-- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
			compileO tok_a2fb ctx $ \ty_a2fb (TermO a2fb) ->
			compileO tok_ta   ctx $ \ty_ta   (TermO ta) ->
			check_TyEq2 (ty @(->)) (At (Just tok_a2fb) ty_a2fb) $ \Refl ty_a2fb_a ty_a2fb_fb ->
			check_TyCon1 (ty @Applicative) (At (Just tok_a2fb) ty_a2fb_fb) $ \Refl TyCon ty_a2fb_fb_f ty_a2fb_fb_b ->
			check_TyCon1 (ty @Traversable) (At (Just tok_ta)   ty_ta)      $ \Refl TyCon ty_ta_t ty_ta_a ->
			check_TyEq
			 (At (Just tok_a2fb) ty_a2fb_a)
			 (At (Just tok_ta) ty_ta_a) $ \Refl ->
			k (ty_a2fb_fb_f :$ (ty_ta_t :$ ty_a2fb_fb_b)) $ TermO $
			 \c -> traverse (a2fb c) (ta c)
instance -- TokenizeT
 Inj_Token meta ts Traversable =>
 TokenizeT meta ts (Proxy Traversable) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "traverse" infixN5 Token_Term_Traversable_traverse
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Traversable) g