{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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)
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:: * -> *)
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)
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)
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
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
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
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