{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for 'IO'.
module Language.Symantic.Compiling.IO where

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

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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

type instance Sym_of_Iface (Proxy IO) = Sym_IO
type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO
type instance Consts_imported_by IO =
 [ Proxy IO.Handle
 , Proxy IO.IOMode
 , Proxy IO.FilePath
 , Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 ]
type instance Consts_imported_by IO.Handle =
 '[ Proxy Eq
 ]
type instance Consts_imported_by 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 TextI where
	io_hClose   = textI_app1 "IO.hClose"
	io_openFile = textI_app2 "IO.openFile"
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 Const_from Text cs => Const_from Text (Proxy IO ': cs) where
	const_from "IO" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy IO.Handle ': cs) where
	const_from "IO.Handle" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Const_from Text cs => Const_from Text (Proxy IO.IOMode ': cs) where
	const_from "IO.IOMode" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS

instance Show_Const cs => Show_Const (Proxy IO ': cs) where
	show_const ConstZ{} = "IO"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where
	show_const ConstZ{} = "IO.Handle"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where
	show_const ConstZ{} = "IO.IOMode"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC IO
 ( Proj_Const cs IO
 , Proj_Consts cs (Consts_imported_by IO)
 ) => Proj_ConC cs (Proxy IO) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy IO)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Proj_ConC IO.Handle
 ( Proj_Const cs IO.Handle
 , Proj_Consts cs (Consts_imported_by IO.Handle)
 ) => Proj_ConC cs (Proxy IO.Handle) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy IO.Handle)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Proj_ConC IO.IOMode
 ( Proj_Const cs IO.IOMode
 , Proj_Consts cs (Consts_imported_by IO.IOMode)
 ) => Proj_ConC cs (Proxy IO.IOMode) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy::Proxy IO.IOMode)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Eq)   -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)  -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) IO
 , Inj_Const (Consts_of_Ifaces is) IO.Handle
 , Inj_Const (Consts_of_Ifaces is) IO.FilePath
 , Inj_Const (Consts_of_Ifaces is) IO.IOMode
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) ()
 , Term_from is ast
 ) => Term_fromI is (Proxy IO) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "IO.hClose"   -> io_hClose_from
		 "IO.openFile" -> io_openFile_from
		 _ -> Left $ Error_Term_unsupported
		where
		io_hClose_from =
		 -- hClose :: Handle -> IO ()
			from_ast1 ast $ \ast_h as ->
			term_from ast_h ctx $ \ty_h (TermLC h) ->
			check_type (At Nothing tyIO_Handle) (At (Just ast_h) ty_h) $ \Refl ->
			k as (tyIO :$ tyUnit) $ TermLC $
			io_hClose . h
		io_openFile_from =
		 -- openFile :: FilePath -> IOMode -> IO Handle
			from_ast1 ast $ \ast_fp as ->
			term_from ast_fp ctx $ \ty_fp (TermLC fp) ->
			check_type (At Nothing tyIO_FilePath) (At (Just ast_fp) ty_fp) $ \Refl ->
			k as (tyIO_IOMode ~> tyIO :$ tyIO_Handle) $ TermLC $
			 \c -> lam $ io_openFile (fp c)

-- | The 'IO' 'Type'
tyIO :: Inj_Const cs IO => Type cs IO
tyIO = TyConst inj_const

-- | The 'IO.Handle' 'Type'
tyIO_Handle :: Inj_Const cs IO.Handle => Type cs IO.Handle
tyIO_Handle = TyConst inj_const

-- | The 'IO.IOMode' 'Type'
tyIO_IOMode :: Inj_Const cs IO.IOMode => Type cs IO.IOMode
tyIO_IOMode = TyConst inj_const

-- | The 'IO.FilePath' 'Type'
tyIO_FilePath :: Inj_Const cs IO.FilePath => Type cs IO.FilePath
tyIO_FilePath = TyConst inj_const

sym_IO :: Proxy Sym_IO
sym_IO = Proxy

syIO :: IsString a => [Syntax a] -> Syntax a
syIO = Syntax "IO"