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)
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 _ (TyApp _ (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 _ (TyApp _ q (TyApp _ z _a))
| Just HRefl <- proj_ConstKiTy @_ @IO z
= case () of
_ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance ClassInstancesFor IO.Handle where
proveConstraintFor _ (TyApp _ q z)
| Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
= case () of
_ | Just Refl <- proj_ConstTy @Eq q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance ClassInstancesFor IO.IOMode where
proveConstraintFor _ (TyApp _ (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 (TyApp _ 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