{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Type.IO where

import qualified Data.MonoTraversable as MT
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified System.IO as IO

import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
import Language.Symantic.Type.Type1
import Language.Symantic.Type.Constraint
import Language.Symantic.Type.Family

-- * Type 'Type_IO'
-- | The list type.
type Type_IO          = Type1 (Proxy IO)
type Type_IO_Handle   = Type0 (Proxy IO.Handle)
type Type_IO_FilePath = Type0 (Proxy IO.FilePath)
type Type_IO_Mode     = Type0 (Proxy IO.IOMode)

pattern Type_IO :: root a -> Type_IO root (IO a)
pattern Type_IO a = Type1 Proxy a

instance Type0_Constraint Eq (Type_IO root)
instance Type0_Constraint Ord (Type_IO root)
instance Type0_Constraint Monoid (Type_IO root)
instance Type0_Constraint Num (Type_IO root)
instance Type0_Constraint Integral (Type_IO root)
instance Type0_Family Type_Family_MonoElement (Type_IO root) where
	type0_family _at (Type1 _px a) = Just a
instance Type0_Constraint MT.MonoFunctor (Type_IO root) where
	type0_constraint _c Type1{} = Just Dict
instance Type1_Constraint Functor (Type_IO root) where
	type1_constraint _c Type1{} = Just Dict
instance Type1_Constraint Applicative (Type_IO root) where
	type1_constraint _c Type1{} = Just Dict
instance Type1_Constraint Monad (Type_IO root) where
	type1_constraint _c Type1{} = Just Dict
instance -- Type0_Eq
 Type0_Eq root =>
 Type0_Eq (Type_IO root) where
	type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
	 | Just Refl <- a1 `type0_eq` a2
	 = Just Refl
	type0_eq _ _ = Nothing
instance -- Type1_Eq
 Type1_Eq (Type_IO root) where
	type1_eq Type1{} Type1{}
	 = Just Refl
instance -- String_from_Type
 String_from_Type root =>
 String_from_Type (Type_IO root) where
	string_from_type (Type1 _f a) =
		"[" ++ string_from_type a ++ "]"

-- | Inject 'Type_IO' within a root type.
type_io :: Type_Root_Lift Type_IO root => root h_a -> root (IO h_a)
type_io = type1

-- | Inject 'Type_IO_Handle' within a root type.
type_io_handle
 :: Type_Root_Lift Type_IO_Handle root
 => root IO.Handle
type_io_handle = type_root_lift $ Type0 (Proxy::Proxy IO.Handle)

-- | Inject 'Type_IO_FilePath' within a root type.
type_io_filepath
 :: Type_Root_Lift Type_IO_FilePath root
 => root IO.FilePath
type_io_filepath = type_root_lift $ Type0 (Proxy::Proxy IO.FilePath)

-- | Inject 'Type_IO_Mode' within a root type.
type_io_mode
 :: Type_Root_Lift Type_IO_Mode root
 => root IO.IOMode
type_io_mode = type_root_lift $ Type0 (Proxy::Proxy IO.IOMode)