{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'IO'.
module Language.Symantic.Expr.IO where

import Control.Monad
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import qualified System.IO as IO

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Trans.Common

-- * Class 'Sym_IO_Lam'
-- | Symantic.
class Sym_IO repr where
	io_hClose   :: repr IO.Handle -> repr (IO ())
	io_openFile :: repr IO.FilePath -> repr IO.IOMode -> repr (IO IO.Handle)
	
	default io_hClose   :: Trans t repr => t repr IO.Handle -> t repr (IO ())
	default io_openFile :: Trans t repr => t repr IO.FilePath -> t repr IO.IOMode -> t repr (IO IO.Handle)
	io_hClose   = trans_map1 io_hClose
	io_openFile = trans_map2 io_openFile
instance Sym_IO Repr_Host where
	io_hClose   = liftM IO.hClose
	io_openFile = liftM2 IO.openFile
instance Sym_IO Repr_Text where
	io_hClose   = repr_text_app1 "io_hClose"
	io_openFile = repr_text_app2 "io_openFile"
instance (Sym_IO r1, Sym_IO r2) => Sym_IO (Repr_Dup r1 r2) where
	io_hClose (h1 `Repr_Dup` h2) =
		io_hClose h1 `Repr_Dup` io_hClose h2
	io_openFile (f1 `Repr_Dup` f2) (m1 `Repr_Dup` m2) =
		io_openFile f1 m1 `Repr_Dup` io_openFile f2 m2

-- * Type 'Expr_IO'
-- | Expression.
data Expr_IO (root:: *)
type instance Root_of_Expr      (Expr_IO root)      = root
type instance Type_of_Expr      (Expr_IO root)      = Type_IO
type instance Sym_of_Expr       (Expr_IO root) repr = (Sym_IO repr)
type instance Error_of_Expr ast (Expr_IO root)      = No_Error_Expr

-- | Parsing utility to check that the given type is a 'Type_IO'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_io
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type0_Lift   Type_IO (Type_of_Expr root)
 , Type0_Unlift Type_IO (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_IO ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_io ex ast ty k =
	case type0_unlift $ unType_Root ty of
	 Just ty_l -> k ty_l
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type0 (type_io $ type_var0 SZero
		 :: ty (IO Var0)))
		 (Exists_Type0 ty)

-- | Parse 'io_hClose'.
io_hclose_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_IO root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_Unit (Type_of_Expr root)
 , Type0_Lift   Type_IO_Handle (Type_of_Expr root)
 , Type0_Lift   Type_IO (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> ExprFrom ast (Expr_IO root) hs ret
io_hclose_from ast_h ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_h ctx $
	 \(ty_h::ty h_h) (Forall_Repr_with_Context h) ->
	check_type0_eq ex ast type_io_handle ty_h $ \Refl ->
	k (type_io type_unit) $ Forall_Repr_with_Context $
		\c -> io_hClose (h c)

-- | Parse 'io_openFile'.
io_openfile_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_IO root)
 , Type0_Eq ty
 , Expr_From ast root
 , Type0_Lift   Type_IO_FilePath (Type_of_Expr root)
 , Type0_Lift   Type_IO_Handle   (Type_of_Expr root)
 , Type0_Lift   Type_IO_Mode     (Type_of_Expr root)
 , Type0_Lift   Type_IO          (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> ExprFrom ast (Expr_IO root) hs ret
io_openfile_from ast_file ast_mode ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_file ctx $
	 \(ty_file::ty h_file) (Forall_Repr_with_Context file) ->
	expr_from (Proxy::Proxy root) ast_mode ctx $
	 \(ty_mode::ty h_mode) (Forall_Repr_with_Context mode) ->
	check_type0_eq ex ast type_io_filepath ty_file $ \Refl ->
	check_type0_eq ex ast type_io_mode ty_mode $ \Refl ->
	k (type_io type_io_handle) $ Forall_Repr_with_Context $
		\c -> io_openFile (file c) (mode c)