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

import Control.Monad (liftM, liftM2)
import Data.MonoTraversable (MonoFunctor)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified System.IO as IO

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class 'Sym_IO'
class Sym_IO term where
	io_hClose   :: term IO.Handle -> term (IO ())
	io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
	
	default io_hClose   :: Trans t term => t term IO.Handle -> t term (IO ())
	default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
	
	io_hClose   = trans_map1 io_hClose
	io_openFile = trans_map2 io_openFile
class Sym_IO_Handle (term:: * -> *)
class Sym_IO_IOMode (term:: * -> *)

type instance Sym_of_Iface      (Proxy IO)        = Sym_IO
type instance Sym_of_Iface      (Proxy IO.Handle) = Sym_IO_Handle
type instance Sym_of_Iface      (Proxy IO.IOMode) = Sym_IO_IOMode
type instance TyConsts_of_Iface (Proxy IO)        = Proxy IO ': TyConsts_imported_by (Proxy IO)
type instance TyConsts_of_Iface (Proxy IO.Handle) = Proxy IO.Handle ': TyConsts_imported_by (Proxy IO.Handle)
type instance TyConsts_of_Iface (Proxy IO.IOMode) = Proxy IO.IOMode ': TyConsts_imported_by (Proxy IO.IOMode)
type instance TyConsts_imported_by (Proxy IO) =
 [ Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 , Proxy MonoFunctor
 ]
type instance TyConsts_imported_by (Proxy IO.Handle) =
 '[ Proxy Eq
 ]
type instance TyConsts_imported_by (Proxy IO.IOMode) =
 [ Proxy Enum
 , Proxy Eq
 , Proxy Ord
 ]

instance Sym_IO HostI where
	io_hClose   = liftM IO.hClose
	io_openFile = liftM2 IO.openFile
instance Sym_IO_Handle HostI
instance Sym_IO_IOMode HostI
instance Sym_IO TextI where
	io_hClose   = textI1 "IO.hClose"
	io_openFile = textI2 "IO.openFile"
instance Sym_IO_Handle TextI
instance Sym_IO_IOMode TextI
instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
	io_hClose   = dupI1 @Sym_IO io_hClose
	io_openFile = dupI2 @Sym_IO io_openFile
instance Sym_IO_Handle (DupI r1 r2)
instance Sym_IO_IOMode (DupI r1 r2)

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs IO
 ) => Read_TyNameR TyName cs (Proxy IO ': rs) where
	read_TyNameR _cs (TyName "IO") k = k (ty @IO)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs IO.Handle
 ) => Read_TyNameR TyName cs (Proxy IO.Handle ': rs) where
	read_TyNameR _cs (TyName "IO.Handle") k = k (ty @IO.Handle)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs IO.IOMode
 ) => Read_TyNameR TyName cs (Proxy IO.IOMode ': rs) where
	read_TyNameR _cs (TyName "IO.Mode") k = k (ty @IO.IOMode)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k

instance Show_TyConst cs => Show_TyConst (Proxy IO ': cs) where
	show_TyConst TyConstZ{} = "IO"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy IO.Handle ': cs) where
	show_TyConst TyConstZ{} = "IO.Handle"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy IO.IOMode ': cs) where
	show_TyConst TyConstZ{} = "IO.IOMode"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyFamC TyFam_MonoElement 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 -- Proj_TyFamC TyFam_MonoElement IO.Handle
 Proj_TyFamC cs TyFam_MonoElement IO.Handle
instance -- Proj_TyFamC TyFam_MonoElement IO.IOMode
 Proj_TyFamC cs TyFam_MonoElement IO.IOMode

instance -- Proj_TyConC IO
 ( Proj_TyConst cs IO
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO))
 ) => Proj_TyConC cs (Proxy IO) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_SKind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @IO)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (TyConst q :$ (TyConst c :$ _a))
	 | Just Refl <- eq_SKind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @IO)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
instance -- Proj_TyConC IO.Handle
 ( Proj_TyConst cs IO.Handle
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.Handle))
 ) => Proj_TyConC cs (Proxy IO.Handle) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @IO.Handle)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
instance -- Proj_TyConC IO.IOMode
 ( Proj_TyConst cs IO.IOMode
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.IOMode))
 ) => Proj_TyConC cs (Proxy IO.IOMode) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @IO.IOMode)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)  -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy IO)
 = Token_Term_IO_hClose   (EToken meta ts)
 | Token_Term_IO_openFile (EToken meta ts)
data instance TokenT meta (ts::[*]) (Proxy IO.Handle)
data instance TokenT meta (ts::[*]) (Proxy IO.IOMode)
deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.Handle))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.Handle))
deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.IOMode))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.IOMode))

instance -- CompileI IO
 ( Inj_TyConst cs IO
 , Inj_TyConst cs IO.Handle
 , Inj_TyConst cs []
 , Inj_TyConst cs Char
 , Inj_TyConst cs IO.IOMode
 , Inj_TyConst cs (->)
 , Inj_TyConst cs ()
 , Compile cs is
 ) => CompileI cs is (Proxy IO) where
	compileI tok ctx k =
		case tok of
		 Token_Term_IO_hClose tok_h ->
			-- hClose :: Handle -> IO ()
			compile tok_h ctx $ \ty_h (Term h) ->
			check_TyEq
			 (At Nothing (ty @IO.Handle))
			 (At (Just tok_h) ty_h) $ \Refl ->
			k (ty @IO :$ ty @()) $ Term $
				io_hClose . h
		 Token_Term_IO_openFile tok_fp ->
			-- openFile :: FilePath -> IOMode -> IO Handle
			compile tok_fp ctx $ \ty_fp (Term fp) ->
			check_TyEq
			 (At Nothing tyFilePath)
			 (At (Just tok_fp) ty_fp) $ \Refl ->
			k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ Term $
			 \c -> lam $ io_openFile (fp c)
		where tyFilePath = ty @[] :$ ty @Char
instance CompileI cs is (Proxy IO.Handle) where
	compileI tok _ctx _k = case tok of _ -> undefined
instance CompileI cs is (Proxy IO.IOMode) where
	compileI tok _ctx _k = case tok of _ -> undefined
instance -- TokenizeT IO
 Inj_Token meta ts IO =>
 TokenizeT meta ts (Proxy IO) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
		 [ tokenize1 "hClose"   infixN5 Token_Term_IO_hClose
		 , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
		 ]
	 }
instance TokenizeT meta ts (Proxy IO.Handle)
instance TokenizeT meta ts (Proxy IO.IOMode)
instance Gram_Term_AtomsT meta ts (Proxy IO) g
instance Gram_Term_AtomsT meta ts (Proxy IO.Handle) g
instance Gram_Term_AtomsT meta ts (Proxy IO.IOMode) g