{-# 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