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

import Control.Applicative (Applicative)
import Control.Monad (Monad)
import Data.Eq (Eq)
import Data.Function (($))
import Data.Functor (Functor)
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Prelude (Enum)
import System.IO (IO, FilePath)
import qualified Data.MonoTraversable as MT
import qualified System.IO as IO

import Language.Symantic
import Language.Symantic.Lib.Char (tyString)
import Language.Symantic.Lib.MonoFunctor (Element)
import Language.Symantic.Lib.Unit (tyUnit)

-- * Class 'Sym_IO'
type instance Sym IO        = Sym_IO
type instance Sym IO.Handle = Sym_IO_Handle
type instance Sym IO.IOMode = Sym_IO_Mode
class Sym_IO (term:: * -> *)
class Sym_IO_Handle (term:: * -> *) where
	io_hClose   :: term IO.Handle -> term (IO ())
	io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
	
	default io_hClose   :: Sym_IO_Handle (UnT term) => Trans term => term IO.Handle -> term (IO ())
	default io_openFile :: Sym_IO_Handle (UnT term) => Trans term => term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
	
	io_hClose   = trans1 io_hClose
	io_openFile = trans2 io_openFile
class Sym_IO_Mode (term:: * -> *)

-- Interpreting
instance Sym_IO Eval
instance Sym_IO_Handle Eval where
	io_hClose   = eval1 IO.hClose
	io_openFile = eval2 IO.openFile
instance Sym_IO_Mode Eval

instance Sym_IO View
instance Sym_IO_Handle View where
	io_hClose   = view1 "IO.hClose"
	io_openFile = view2 "IO.openFile"
instance Sym_IO_Mode View

instance Sym_IO (Dup r1 r2)
instance (Sym_IO_Handle r1, Sym_IO_Handle r2) => Sym_IO_Handle (Dup r1 r2) where
	io_hClose   = dup1 @Sym_IO_Handle io_hClose
	io_openFile = dup2 @Sym_IO_Handle io_openFile
instance Sym_IO_Mode (Dup r1 r2)

-- Transforming
instance (Sym_IO term, Sym_Lambda term) => Sym_IO (BetaT term)
instance (Sym_IO_Handle term, Sym_Lambda term) => Sym_IO_Handle (BetaT term)
instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)

-- Typing
instance NameTyOf IO where
	nameTyOf _c = ["IO"] `Mod` "IO"
instance NameTyOf IO.Handle where
	nameTyOf _c = ["IO"] `Mod` "Handle"
instance NameTyOf IO.IOMode where
	nameTyOf _c = ["IO"] `Mod` "IOMode"
instance FixityOf IO
instance ClassInstancesFor IO where
	proveConstraintFor _ (TyConst _ _ q :$ z)
	 | Just HRefl <- proj_ConstKiTy @_ @IO z
	 = case () of
		 _ | Just Refl <- proj_Const @Applicative q -> Just Dict
		   | Just Refl <- proj_Const @Functor     q -> Just Dict
		   | Just Refl <- proj_Const @Monad       q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _ (TyConst _ _ q :$ z:@_a)
	 | Just HRefl <- proj_ConstKiTy @_ @IO z
	 = case () of
		 _ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance ClassInstancesFor IO.Handle where
	proveConstraintFor _ (TyConst _ _ q :$ z)
	 | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance ClassInstancesFor IO.IOMode where
	proveConstraintFor _ (TyConst _ _ q :$ c)
	 | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c
	 = case () of
		 _ | Just Refl <- proj_Const @Enum q -> Just Dict
		   | Just Refl <- proj_Const @Eq   q -> Just Dict
		   | Just Refl <- proj_Const @Ord  q -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor IO where
	expandFamFor _c _len f (z:@a `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @IO z
	 = Just a
	expandFamFor _c _len _fam _as = Nothing
instance TypeInstancesFor IO.Handle
instance TypeInstancesFor IO.IOMode

-- Compiling
instance ModuleFor src ss IO
instance (Source src, SymInj ss IO.Handle) => ModuleFor src ss IO.Handle where
	moduleFor = ["IO"] `moduleWhere`
	 [ "hClose"   := teIO_hClose
	 , "openFile" := teIO_openFile
	 ]
instance ModuleFor src ss IO.IOMode
instance Gram_Term_AtomsFor src ss g IO
instance Gram_Term_AtomsFor src ss g IO.Handle
instance Gram_Term_AtomsFor src ss g IO.IOMode

-- ** 'Type's
tyIO :: Source src => Type src vs a -> Type src vs (IO a)
tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a

tyIO_Handle :: Source src => LenInj vs => Type src vs IO.Handle
tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle

tyIO_Mode :: Source src => LenInj vs => Type src vs IO.IOMode
tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode

tyFilePath :: Source src => LenInj vs => Type src vs FilePath
tyFilePath = tyString

-- ** 'Term's
teIO_hClose :: TermDef IO.Handle '[] (() #> (IO.Handle -> IO ()))
teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose

teIO_openFile :: TermDef IO.Handle '[] (() #> (FilePath -> IO.IOMode -> IO (IO.Handle)))
teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile