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

import Control.Monad (liftM2)
import Data.MonoTraversable (MonoFunctor)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import GHC.Exts (Constraint)
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

-- * Class 'Sym_MonoFunctor'
class Sym_MonoFunctor term where
	omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
	default omap :: (Trans t term, MonoFunctor o)
	 => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
	omap = trans_map2 omap

type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
type instance TyConsts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': TyConsts_imported_by (Proxy MonoFunctor)
type instance TyConsts_imported_by (Proxy MonoFunctor) = '[ Proxy (->) ]

instance Sym_MonoFunctor HostI where
	omap = liftM2 MT.omap
instance Sym_MonoFunctor TextI where
	omap = textI2 "omap"
instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
	omap = dupI2 @Sym_MonoFunctor omap

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

-- * Type 'TyFam_MonoElement'
data TyFam_MonoElement
 =   TyFam_MonoElement
 deriving (Eq, Show)
type instance TyFam TyFam_MonoElement '[h] = MT.Element (UnProxy h)

instance -- Constraint
 Proj_TyFamC cs TyFam_MonoElement (c::Constraint)
instance -- k -> Constraint
 Proj_TyFamC cs TyFam_MonoElement (c::k -> Constraint)

instance Proj_TyConC cs (Proxy MonoFunctor)

data instance TokenT meta (ts::[*]) (Proxy MonoFunctor)
 = Token_Term_MonoFunctor_omap (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFunctor))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFunctor))
instance -- CompileI
 ( Inj_TyConst cs MonoFunctor
 , Inj_TyConst cs (->)
 , Proj_TyCon  cs
 , Proj_TyFam  cs TyFam_MonoElement
 , Compile cs is
 ) => CompileI cs is (Proxy MonoFunctor) where
	compileI tok ctx k =
		case tok of
		 Token_Term_MonoFunctor_omap tok_f tok_o ->
			-- omap :: (Element o -> Element o) -> o -> o
			compileO tok_f ctx $ \ty_f (TermO f) ->
			compileO tok_o ctx $ \ty_o (TermO m) ->
			check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
			check_TyEq
			 (At (Just tok_f) ty_f_a)
			 (At (Just tok_f) ty_f_b) $ \Refl ->
			check_TyCon (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \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_o $ TermO $
			 \c -> omap (f c) (m c)
instance -- TokenizeT
 Inj_Token meta ts MonoFunctor =>
 TokenizeT meta ts (Proxy MonoFunctor) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize2 "omap" infixN5 Token_Term_MonoFunctor_omap
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy MonoFunctor) g