{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'MonoFunctor'.
module Language.Symantic.Compiling.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.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans
import Language.Symantic.Lib.Data.Type.List hiding (Map)

-- * 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 Consts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': Consts_imported_by MonoFunctor
type instance Consts_imported_by MonoFunctor =
 [ Proxy (->)
 , Proxy (,)
 , Proxy []
 , Proxy Either
 , Proxy IO
 , Proxy Map
 , Proxy Maybe
 , Proxy String
 , Proxy Text
 ] ++ Consts_imported_by IO

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

instance Const_from Text cs => Const_from Text (Proxy MonoFunctor ': cs) where
	const_from "MonoFunctor" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
	show_const ConstZ{} = "MonoFunctor"
	show_const (ConstS c) = show_const c

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

instance -- Constraint
 Proj_FamC cs Fam_MonoElement (c::Constraint)
instance -- k -> Constraint
 Proj_FamC cs Fam_MonoElement (c::k -> Constraint)
instance -- ()
 Proj_FamC cs Fam_MonoElement ()
instance -- Bool
 Proj_FamC cs Fam_MonoElement Bool
instance -- Char
 Proj_FamC cs Fam_MonoElement Char
instance -- String
 ( Proj_Const cs String
 , Inj_Const cs (MT.Element String)
 ) => Proj_FamC cs Fam_MonoElement String where
	proj_famC _c _fam (TyConst c `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy String)
	 = Just (TyConst inj_const::Type cs (MT.Element String))
	proj_famC _c _fam _ty = Nothing
instance -- Text
 ( Proj_Const cs Text
 , Inj_Const cs (MT.Element Text)
 ) => Proj_FamC cs Fam_MonoElement Text where
	proj_famC _c _fam (TyConst c `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy Text)
	 = Just (TyConst inj_const::Type cs (MT.Element Text))
	proj_famC _c _fam _ty = Nothing
instance -- []
 ( Proj_Const cs []
 ) => Proj_FamC cs Fam_MonoElement [] where
	proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy [])
	 = Just ty_a
	proj_famC _c _fam _ty = Nothing
instance -- IO
 ( Proj_Const cs IO
 ) => Proj_FamC cs Fam_MonoElement IO where
	proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy IO)
	 = Just ty_a
	proj_famC _c _fam _ty = Nothing
instance -- IO.Handle
 Proj_FamC cs Fam_MonoElement IO.Handle
instance -- IO.IOMode
 Proj_FamC cs Fam_MonoElement IO.IOMode
instance -- Maybe
 ( Proj_Const cs Maybe
 ) => Proj_FamC cs Fam_MonoElement Maybe where
	proj_famC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Maybe)
	 = Just ty_a
	proj_famC _c _fam _ty = Nothing
instance -- (->)
 ( Proj_Const cs (->)
 ) => Proj_FamC cs Fam_MonoElement (->) where
	proj_famC _c _fam ((TyConst c :$ _ty_r :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (->))
	 = Just ty_a
	proj_famC _c _fam _ty = Nothing
instance -- (,)
 ( Proj_Const cs (,)
 ) => Proj_FamC cs Fam_MonoElement (,) where
	proj_famC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (,))
	 = Just ty_b
	proj_famC _c _fam _ty = Nothing
instance -- Either
 ( Proj_Const cs Either
 ) => Proj_FamC cs Fam_MonoElement Either where
	proj_famC _c _fam ((TyConst c :$ _ty_l :$ ty_r) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Either)
	 = Just ty_r
	proj_famC _c _fam _ty = Nothing
instance -- Map
 ( Proj_Const cs Map
 ) => Proj_FamC cs Fam_MonoElement Map where
	proj_famC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy Map)
	 = Just ty_a
	proj_famC _c _fam _ty = Nothing

instance -- Proj_ConC
 ( Proj_Const cs MonoFunctor
 , Proj_Consts cs (Consts_imported_by MonoFunctor)
 ) => Proj_ConC cs (Proxy MonoFunctor) where
	proj_conC _ (TyConst q :$ typ)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
	 = case typ 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 IO)    -> 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 (,))    -> Just Con
			   | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
			   | Just Refl <- proj_const c (Proxy::Proxy Map)    -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _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 -- Term_fromI
 ( Inj_Const (Consts_of_Ifaces is) MonoFunctor
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is
 ) => Term_fromI is (Proxy MonoFunctor) where
	term_fromI tok ctx k =
		case tok of
		 Token_Term_MonoFunctor_omap tok_f tok_o ->
			-- omap :: (Element o -> Element o) -> o -> o
			term_from tok_f ctx $ \ty_f (TermLC f) ->
			term_from tok_o ctx $ \ty_o (TermLC m) ->
			check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_f_b ->
			check_type
			 (At (Just tok_f) ty_f_a)
			 (At (Just tok_f) ty_f_b) $ \Refl ->
			check_con (At (Just tok_f) (ty @MonoFunctor :$ ty_o)) $ \Con ->
			check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type
			 (At Nothing ty_o_e)
			 (At (Just tok_f) ty_f_a) $ \Refl ->
			k ty_o $ TermLC $
			 \c -> omap (f c) (m c)