{-# 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.Ratio (Ratio)
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_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) `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 -- ()
 Proj_TyFamC cs TyFam_MonoElement ()
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 -- Bool
 Proj_TyFamC cs TyFam_MonoElement Bool
instance -- Char
 Proj_TyFamC cs TyFam_MonoElement Char
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 -- Int
 Proj_TyFamC cs TyFam_MonoElement Int
instance -- Integer
 Proj_TyFamC cs TyFam_MonoElement Integer
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 -- 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 -- 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 -- Ordering
 Proj_TyFamC cs TyFam_MonoElement Ordering
instance -- Ratio
 Proj_TyFamC cs TyFam_MonoElement Ratio
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_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 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