{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# 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.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import GHC.Exts (Constraint)
import qualified System.IO as IO

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 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 :$ ty)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
	 = case ty 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
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , 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 ast
 ) => Term_fromI is (Proxy MonoFunctor) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "omap" -> omap_from
		 _ -> Left $ Error_Term_unsupported
		where
		omap_from =
		 -- omap :: (Element o -> Element o) -> o -> o
			from_ast2 ast $ \ast_f ast_o as ->
			term_from ast_f ctx $ \ty_f (TermLC f) ->
			term_from ast_o ctx $ \ty_o (TermLC m) ->
			check_type2 tyFun ast_f ty_f $ \Refl ty_f_a ty_f_b ->
			check_type (At (Just ast_f) ty_f_a) (At (Just ast_f) ty_f_b) $ \Refl ->
			check_constraint (At (Just ast_f) (tyMonoFunctor :$ ty_o)) $ \Con ->
			check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			check_type (At Nothing ty_o_e) (At (Just ast_f) ty_f_a) $ \Refl ->
			k as ty_o $ TermLC $
			 \c -> omap (f c) (m c)

-- | The 'MonoFunctor' 'Type'
tyMonoFunctor :: Inj_Const cs MonoFunctor => Type cs MonoFunctor
tyMonoFunctor = TyConst inj_const

sym_MonoFunctor :: Proxy Sym_MonoFunctor
sym_MonoFunctor = Proxy

syMonoFunctor :: IsString a => [Syntax a] -> Syntax a
syMonoFunctor = Syntax "MonoFunctor"