{-# 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.Map.Strict (Map)
import Data.MonoTraversable (MonoFunctor)
import qualified Data.MonoTraversable as MT
import Data.Proxy
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import GHC.Exts (Constraint)
import qualified System.IO as IO

import Language.Symantic.Helper.Data.Type.List hiding (Map)
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 MonoFunctor
type instance TyConsts_imported_by MonoFunctor =
 [ Proxy (->)
 , Proxy (,)
 , Proxy []
 , Proxy Either
 , Proxy IO
 , Proxy Map
 , Proxy Maybe
 , Proxy Text
 ] ++ TyConsts_imported_by IO

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_TyFamC cs TyFam_MonoElement ()
instance -- Bool
 Proj_TyFamC cs TyFam_MonoElement Bool
instance -- Char
 Proj_TyFamC cs TyFam_MonoElement Char
instance -- Int
 Proj_TyFamC cs TyFam_MonoElement Int
instance -- Integer
 Proj_TyFamC cs TyFam_MonoElement Integer
instance -- Text
 ( Proj_TyConst cs Text
 , Inj_TyConst cs (MT.Element Text)
 ) => Proj_TyFamC cs TyFam_MonoElement Text where
	proj_TyFamC _c _fam (TyConst c `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Text)
	 = Just (TyConst inj_TyConst::Type cs (MT.Element Text))
	proj_TyFamC _c _fam _ty = Nothing
instance -- []
 ( Proj_TyConst cs []
 ) => Proj_TyFamC cs TyFam_MonoElement [] where
	proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @[])
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing
instance -- IO
 ( Proj_TyConst cs IO
 ) => Proj_TyFamC cs TyFam_MonoElement IO where
	proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @IO)
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing
instance -- IO.Handle
 Proj_TyFamC cs TyFam_MonoElement IO.Handle
instance -- IO.IOMode
 Proj_TyFamC cs TyFam_MonoElement IO.IOMode
instance -- Maybe
 ( Proj_TyConst cs Maybe
 ) => Proj_TyFamC cs TyFam_MonoElement Maybe where
	proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Maybe)
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing
instance -- (->)
 ( Proj_TyConst cs (->)
 ) => Proj_TyFamC cs TyFam_MonoElement (->) where
	proj_TyFamC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(->))
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing
instance -- (,)
 ( Proj_TyConst cs (,)
 ) => Proj_TyFamC cs TyFam_MonoElement (,) where
	proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @(,))
	 = Just ty_b
	proj_TyFamC _c _fam _ty = Nothing
instance -- Either
 ( Proj_TyConst cs Either
 ) => Proj_TyFamC cs TyFam_MonoElement Either where
	proj_TyFamC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Either)
	 = Just ty_r
	proj_TyFamC _c _fam _ty = Nothing
instance -- Map
 ( Proj_TyConst cs Map
 ) => Proj_TyFamC cs TyFam_MonoElement Map where
	proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Map)
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing

instance -- Proj_TyConC
 ( Proj_TyConst cs MonoFunctor
 , Proj_TyConsts cs (TyConsts_imported_by MonoFunctor)
 ) => Proj_TyConC cs (Proxy MonoFunctor) where
	proj_TyConC _ (TyConst q :$ typ)
	 | Just Refl <- eq_skind (kind_of_TyConst q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_TyConst q (Proxy @MonoFunctor)
	 = case typ of
		 TyConst c
		  | Just Refl <- proj_TyConst c (Proxy @Text) -> Just TyCon
		 TyConst c :$ _a
		  | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
		  -> case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @[])    -> Just TyCon
			   | Just Refl <- proj_TyConst c (Proxy @IO)    -> Just TyCon
			   | Just Refl <- proj_TyConst c (Proxy @Maybe) -> Just TyCon
			 _ -> Nothing
		 TyConst c :$ _a :$ _b
		  | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
		  -> case () of
			 _ | Just Refl <- proj_TyConst c (Proxy @(->))   -> Just TyCon
			   | Just Refl <- proj_TyConst c (Proxy @(,))    -> Just TyCon
			   | Just Refl <- proj_TyConst c (Proxy @Either) -> Just TyCon
			   | Just Refl <- proj_TyConst c (Proxy @Map)    -> Just TyCon
			 _ -> Nothing
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
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 (TyConsts_of_Ifaces is) MonoFunctor
 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 , Proj_TyCon  (TyConsts_of_Ifaces is)
 , Proj_TyFam  (TyConsts_of_Ifaces is) TyFam_MonoElement
 , Compile is
 ) => CompileI 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