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

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